diff options
Diffstat (limited to 'src/theory/quantifiers/term_canonize.h')
-rw-r--r-- | src/theory/quantifiers/term_canonize.h | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/src/theory/quantifiers/term_canonize.h b/src/theory/quantifiers/term_canonize.h index 8f7b8722e..207e6150c 100644 --- a/src/theory/quantifiers/term_canonize.h +++ b/src/theory/quantifiers/term_canonize.h @@ -55,12 +55,17 @@ class TermCanonize * * This returns a canonical (alpha-equivalent) version of n, where * bound variables in n may be replaced by other ones, and arguments of - * commutative operators of n may be sorted (if apply_torder is true). + * commutative operators of n may be sorted (if apply_torder is true). If + * doHoVar is true, we also canonicalize bound variables that occur in + * operators. + * * In detail, we replace bound variables in n so the the leftmost occurrence * of a bound variable for type T is the first canonical free variable for T, * the second leftmost is the second, and so on, for each type T. */ - Node getCanonicalTerm(TNode n, bool apply_torder = false); + Node getCanonicalTerm(TNode n, + bool apply_torder = false, + bool doHoVar = true); private: /** the number of ids we have allocated for operators */ @@ -81,6 +86,7 @@ class TermCanonize */ Node getCanonicalTerm(TNode n, bool apply_torder, + bool doHoVar, std::map<TypeNode, unsigned>& var_count, std::map<TNode, Node>& visited); }; |