From 28b20948a3b236bf32ca399e2cd85b09c1e57e67 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Thu, 26 May 2016 14:51:01 -0500 Subject: 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. --- src/theory/uf/theory_uf.h | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'src/theory/uf/theory_uf.h') 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 */ -- cgit v1.2.3