diff options
Diffstat (limited to 'src/theory/uf/symmetry_breaker.h')
-rw-r--r-- | src/theory/uf/symmetry_breaker.h | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/theory/uf/symmetry_breaker.h b/src/theory/uf/symmetry_breaker.h index 8cc2ef6a7..d07ef64e0 100644 --- a/src/theory/uf/symmetry_breaker.h +++ b/src/theory/uf/symmetry_breaker.h @@ -114,6 +114,7 @@ private: Template d_template; std::hash_map<Node, Node, NodeHashFunction> d_normalizationCache; TermEqs d_termEqs; + TermEqs d_termEqsOnly; void clear(); void rerunAssertionsIfNecessary(); @@ -123,7 +124,7 @@ private: void selectTerms(const Permutation& p); Terms::iterator selectMostPromisingTerm(Terms& terms); void insertUsedIn(Term term, const Permutation& p, std::set<Node>& cts); - Node normInternal(TNode phi); + Node normInternal(TNode phi, size_t level); Node norm(TNode n); // === STATISTICS === |