diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2014-11-25 16:15:10 +0100 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2014-11-25 16:15:10 +0100 |
commit | 29bdfca306a7cd35801c7d9cb3023d78a8b82a1f (patch) | |
tree | 1c50ca8eb48010b3f327d3d9ada06161e27d9834 /src/theory/quantifiers/theory_quantifiers.h | |
parent | 38e077ab219082ee044c2e17ed809e3519c80842 (diff) |
Fix bug in --term-db-mode=relevant with variable triggers. Support inst-closure predicate and mode --term-db-inst-closure. Minor changes to theory_quantifiers.
Diffstat (limited to 'src/theory/quantifiers/theory_quantifiers.h')
-rw-r--r-- | src/theory/quantifiers/theory_quantifiers.h | 7 |
1 files changed, 2 insertions, 5 deletions
diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h index aace13b24..6d3fa4d46 100644 --- a/src/theory/quantifiers/theory_quantifiers.h +++ b/src/theory/quantifiers/theory_quantifiers.h @@ -44,17 +44,15 @@ private: /** number of instantiations */ int d_numInstantiations; int d_baseDecLevel; - /** number of restarts */ - int d_numRestarts; eq::EqualityEngine* d_masterEqualityEngine; - +private: + void computeCareGraph(); public: TheoryQuantifiers(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo); ~TheoryQuantifiers(); void setMasterEqualityEngine(eq::EqualityEngine* eq); - void addSharedTerm(TNode t); void notifyEq(TNode lhs, TNode rhs); void preRegisterTerm(TNode n); @@ -73,7 +71,6 @@ public: private: void assertUniversal( Node n ); void assertExistential( Node n ); - bool restart(); };/* class TheoryQuantifiers */ }/* CVC4::theory::quantifiers namespace */ |