diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-05-20 13:59:13 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-05-20 13:59:20 -0500 |
| commit | d5d05e4723581c86808a866af1a9f20343ed36dc (patch) | |
| tree | b8b6985db8c361f4ad8a0a004ebb4596fca32824 /src/theory/uf/theory_uf.h | |
| parent | 8b57c18d24caced0744d8624b3e0208aeba923ef (diff) | |
Improvements to theory combination + strings: do not return trivial care graph, split on length terms for disequal strings. Term indexing for TheoryDatatypes::computeCareGraph. Minor fix in quantifiers rewriter for entailed conditions, strings cardinality.
Diffstat (limited to 'src/theory/uf/theory_uf.h')
| -rw-r--r-- | src/theory/uf/theory_uf.h | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index 42a804c09..ff7d7419a 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -32,6 +32,11 @@ namespace CVC4 { namespace theory { + +namespace quantifiers{ + class TermArgTrie; +} + namespace uf { class UfTermDb; @@ -204,6 +209,8 @@ public: StrongSolverTheoryUF* getStrongSolver() { return d_thss; } +//private: + //void addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::TermArgTrie * t2, unsigned arity, unsigned depth ); };/* class TheoryUF */ }/* CVC4::theory::uf namespace */ |