diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-06-11 16:28:23 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-06-11 16:28:23 +0000 |
commit | 3378e253fcdb34c753407bb16d08929da06b3aaa (patch) | |
tree | db7c7118dd0d1594175b56866f845b42426ae0a7 /src/theory/uf/theory_uf.cpp | |
parent | 42794501e81c44dce5c2f7687af288af030ef63e (diff) |
Merge from quantifiers2-trunkmerge branch.
Adds TheoryQuantifiers and TheoryRewriteRules, QuantifiersEngine, and other infrastructure.
Adds theory instantiators to many theories.
Adds the UF strong solver.
Diffstat (limited to 'src/theory/uf/theory_uf.cpp')
-rw-r--r-- | src/theory/uf/theory_uf.cpp | 88 |
1 files changed, 85 insertions, 3 deletions
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 7583f8ee7..dc7bb7c92 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -18,6 +18,8 @@ **/ #include "theory/uf/theory_uf.h" +#include "theory/uf/theory_uf_instantiator.h" +#include "theory/uf/theory_uf_strong_solver.h" using namespace std; using namespace CVC4; @@ -25,8 +27,8 @@ using namespace CVC4::theory; using namespace CVC4::theory::uf; /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/ -TheoryUF::TheoryUF(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) : - Theory(THEORY_UF, c, u, out, valuation, logicInfo), +TheoryUF::TheoryUF(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe) : + Theory(THEORY_UF, c, u, out, valuation, logicInfo, qe), d_notify(*this), d_equalityEngine(d_notify, c, "theory::uf::TheoryUF"), d_conflict(c, false), @@ -36,6 +38,12 @@ TheoryUF::TheoryUF(context::Context* c, context::UserContext* u, OutputChannel& { // The kinds we are treating as function application in congruence d_equalityEngine.addFunctionKind(kind::APPLY_UF); + + if (Options::current()->finiteModelFind) { + d_thss = new StrongSolverTheoryUf(c, u, out, this); + } else { + d_thss = NULL; + } }/* TheoryUF::TheoryUF() */ static Node mkAnd(const std::vector<TNode>& conjunctions) { @@ -62,29 +70,46 @@ static Node mkAnd(const std::vector<TNode>& conjunctions) { void TheoryUF::check(Effort level) { - while (!done() && !d_conflict) + while (!done() && !d_conflict) { // Get all the assertions Assertion assertion = get(); TNode fact = assertion.assertion; Debug("uf") << "TheoryUF::check(): processing " << fact << std::endl; + if (d_thss != NULL) { + bool isDecision = d_valuation.isSatLiteral(fact) && d_valuation.isDecision(fact); + d_thss->assertNode(fact, isDecision); + } // Do the work bool polarity = fact.getKind() != kind::NOT; TNode atom = polarity ? fact : fact[0]; if (atom.getKind() == kind::EQUAL) { d_equalityEngine.assertEquality(atom, polarity, fact); + } else if (atom.getKind() == kind::CARDINALITY_CONSTRAINT) { + // do nothing } else { d_equalityEngine.assertPredicate(atom, polarity, fact); } } + + if (d_thss != NULL) { + if (! d_conflict) { + d_thss->check(level); + } + } + }/* TheoryUF::check() */ void TheoryUF::preRegisterTerm(TNode node) { Debug("uf") << "TheoryUF::preRegisterTerm(" << node << ")" << std::endl; + if (d_thss != NULL) { + d_thss->preRegisterTerm(node); + } + switch (node.getKind()) { case kind::EQUAL: // Add the trigger for equality @@ -124,6 +149,12 @@ bool TheoryUF::propagate(TNode literal) { return ok; }/* TheoryUF::propagate(TNode) */ +void TheoryUF::propagate(Effort effort) { + if (d_thss != NULL) { + return d_thss->propagate(effort); + } +} + void TheoryUF::explain(TNode literal, std::vector<TNode>& assumptions) { // Do the work bool polarity = literal.getKind() != kind::NOT; @@ -395,3 +426,54 @@ void TheoryUF::conflict(TNode a, TNode b) { d_out->conflict(d_conflictNode); d_conflict = true; } + +void TheoryUF::eqNotifyNewClass(TNode t) { + if (d_thss != NULL) { + d_thss->newEqClass(t); + } + // this can be called very early, during initialization + if (!getLogicInfo().isLocked() || getLogicInfo().isQuantified()) { + ((InstantiatorTheoryUf*) getInstantiator())->newEqClass(t); + } +} + +void TheoryUF::eqNotifyPreMerge(TNode t1, TNode t2) { + if (getLogicInfo().isQuantified()) { + ((InstantiatorTheoryUf*) getInstantiator())->merge(t1, t2); + } +} + +void TheoryUF::eqNotifyPostMerge(TNode t1, TNode t2) { + if (d_thss != NULL) { + d_thss->merge(t1, t2); + } +} + +void TheoryUF::eqNotifyDisequal(TNode t1, TNode t2, TNode reason) { + if (d_thss != NULL) { + d_thss->assertDisequal(t1, t2, reason); + } + if (getLogicInfo().isQuantified()) { + ((InstantiatorTheoryUf*) getInstantiator())->assertDisequal(t1, t2, reason); + } +} + +Node TheoryUF::ppRewrite(TNode node) { + + if (node.getKind() != kind::APPLY_UF) { + return node; + } + + // perform the callbacks requested by TheoryUF::registerPpRewrite() + RegisterPpRewrites::iterator c = d_registeredPpRewrites.find(node.getOperator()); + if (c == d_registeredPpRewrites.end()) { + return node; + } else { + Node res = c->second->ppRewrite(node); + if (res != node) { + return ppRewrite(res); + } else { + return res; + } + } +} |