summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/theory_quantifiers.cpp
diff options
context:
space:
mode:
authorajreynol <andrew.j.reynolds@gmail.com>2017-03-29 13:49:51 -0500
committerajreynol <andrew.j.reynolds@gmail.com>2017-03-29 13:50:08 -0500
commitfa5df1aad69f8ad62686b9418070a1baf74b4a77 (patch)
treead780365050498223b2a3fceb703556713cb49d0 /src/theory/quantifiers/theory_quantifiers.cpp
parent599329b76da2e95f18479a19c1bbbc3e3228b100 (diff)
Add quantifiers options related to model and master equality engine.
Diffstat (limited to 'src/theory/quantifiers/theory_quantifiers.cpp')
-rw-r--r--src/theory/quantifiers/theory_quantifiers.cpp5
1 files changed, 2 insertions, 3 deletions
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index 94a11a09e..4d3e584b4 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -35,8 +35,7 @@ using namespace CVC4::theory;
using namespace CVC4::theory::quantifiers;
TheoryQuantifiers::TheoryQuantifiers(Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) :
- Theory(THEORY_QUANTIFIERS, c, u, out, valuation, logicInfo),
- d_masterEqualityEngine(0)
+ Theory(THEORY_QUANTIFIERS, c, u, out, valuation, logicInfo)
{
d_numInstantiations = 0;
d_baseDecLevel = -1;
@@ -55,7 +54,7 @@ TheoryQuantifiers::~TheoryQuantifiers() {
}
void TheoryQuantifiers::setMasterEqualityEngine(eq::EqualityEngine* eq) {
- d_masterEqualityEngine = eq;
+
}
void TheoryQuantifiers::addSharedTerm(TNode t) {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback