diff options
Diffstat (limited to 'src/theory/quantifiers/theory_quantifiers.h')
-rw-r--r-- | src/theory/quantifiers/theory_quantifiers.h | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h index 7b050bb1c..12b735497 100644 --- a/src/theory/quantifiers/theory_quantifiers.h +++ b/src/theory/quantifiers/theory_quantifiers.h @@ -31,6 +31,7 @@ namespace CVC4 { class TheoryEngine; namespace theory { + namespace quantifiers { class ModelEngine; @@ -49,10 +50,14 @@ private: KEEP_STATISTIC(TimerStat, d_theoryTime, "theory::quantifiers::theoryTime"); + eq::EqualityEngine* d_masterEqualityEngine; + public: TheoryQuantifiers(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe); ~TheoryQuantifiers(); + void setMasterEqualityEngine(eq::EqualityEngine* eq); + void addSharedTerm(TNode t); void notifyEq(TNode lhs, TNode rhs); void preRegisterTerm(TNode n); |