| Maude object | Method | Mod object | Description |
|---|---|---|---|
Symbol |
fillInSortInfo(Term* subject) |
Term::fill_in_sort_info(&mut self) |
Virtual in base class SortTable, but has default impl in Symbol |
Symbol |
computeBaseSort(DagNode* subject) |
DagNode::compute_base_sort(&mut self) |
Pure virtual, defined in each theory |
Put the following back into Symbol |
|||
Symbol |
fastComputeTrueSort(DagNode* subject, RewritingContext& context); |
DagNode::fast_compute_true_sort(&mut self, context: &mut RewritingContext) |
|
DagNode |
reduce(RewritingContext &context) |
RewritingContext::reduce(&mut self) |
|
Symbol |
fastComputeTrueSort(DagNode* subject, RewritingContext& context) |
RewritingContext::fast_compute_true_sort(&mut self) |
|
Symbol |
slowComputeTrueSort(DagNode* subject, RewritingContext& context) |
RewritingContext::slow_compute_true_sort(&mut self) |
Calls constrain_to_smaller_sort(root.clone(), self) on symbol.sort_constraint_table() |
Symbol |
makeCanonical(DagNode *original, HashConsSet *hcs) |
DagNode::make_canonical() |
|
Symbol |
makeCanonicalCopy(DagNode *original, HashConsSet *hcs) |
DagNode::make_canonical_copy() |