summaryrefslogtreecommitdiff
path: root/src/expr/term_canonize.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/expr/term_canonize.h')
-rw-r--r--src/expr/term_canonize.h8
1 files changed, 8 insertions, 0 deletions
diff --git a/src/expr/term_canonize.h b/src/expr/term_canonize.h
index e1524cbf6..74eefdd2d 100644
--- a/src/expr/term_canonize.h
+++ b/src/expr/term_canonize.h
@@ -87,6 +87,14 @@ class TermCanonize
Node getCanonicalTerm(TNode n,
bool apply_torder = false,
bool doHoVar = true);
+ /**
+ * Same as above but tracks visited map, mapping subterms of n to their
+ * canonical forms.
+ */
+ Node getCanonicalTerm(TNode n,
+ std::map<TNode, Node>& visited,
+ bool apply_torder = false,
+ bool doHoVar = true);
private:
/** The (optional) type class callback */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback