diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-08-01 15:08:06 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-08-04 13:25:23 -0400 |
| commit | 7adf1f2ba37912da65d86d811dd1fd9d572fc747 (patch) | |
| tree | 06c3572104faecd824a0ec0889254ef42c4627fd /src/theory/uf/symmetry_breaker.h | |
| parent | 429e6250b70ebd6e1f2bb31ddfebfb61bf10a3e5 (diff) | |
Some fixes to symmetry breaker (resolves bug 576).
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 === |