diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-05-26 14:51:01 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-05-26 14:51:11 -0500 |
| commit | 28b20948a3b236bf32ca399e2cd85b09c1e57e67 (patch) | |
| tree | 54319cbb8b27a94240ef5cfcd53bc0d7fb0c9fe4 /src/theory/uf/theory_uf.h | |
| parent | 7f079d6d88fc6e7e5c73eb4bfa9cb42e6930c224 (diff) | |
Use term indexing in TheoryUF::computeCareGraph. Do not reject model value instantiations in cbqi+BV. Use dag in alpha equivalence check. Fix simple memory leak in fmf.
Diffstat (limited to 'src/theory/uf/theory_uf.h')
| -rw-r--r-- | src/theory/uf/theory_uf.h | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index ff7d7419a..3a83decec 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -209,8 +209,8 @@ public: StrongSolverTheoryUF* getStrongSolver() { return d_thss; } -//private: - //void addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::TermArgTrie * t2, unsigned arity, unsigned depth ); +private: + void addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::TermArgTrie * t2, unsigned arity, unsigned depth ); };/* class TheoryUF */ }/* CVC4::theory::uf namespace */ |