diff options
Diffstat (limited to 'src/theory/fp')
-rw-r--r-- | src/theory/fp/theory_fp.cpp | 35 | ||||
-rw-r--r-- | src/theory/fp/theory_fp.h | 6 |
2 files changed, 15 insertions, 26 deletions
diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp index d17e2999e..3099d9aab 100644 --- a/src/theory/fp/theory_fp.cpp +++ b/src/theory/fp/theory_fp.cpp @@ -114,7 +114,6 @@ TheoryFp::TheoryFp(context::Context* c, d_registeredTerms(u), d_conv(new FpConverter(u)), d_expansionRequested(false), - d_conflictNode(c, Node::null()), d_minMap(u), d_maxMap(u), d_toUBVMap(u), @@ -123,10 +122,12 @@ TheoryFp::TheoryFp(context::Context* c, d_realToFloatMap(u), d_floatToRealMap(u), d_abstractionMap(u), - d_state(c, u, valuation) + d_state(c, u, valuation), + d_im(*this, d_state, pnm, "theory::fp", false) { - // indicate we are using the default theory state object + // indicate we are using the default theory state and inference manager d_theoryState = &d_state; + d_inferManager = &d_im; } /* TheoryFp::TheoryFp() */ TheoryRewriter* TheoryFp::getTheoryRewriter() { return &d_rewriter; } @@ -917,39 +918,25 @@ void TheoryFp::preRegisterTerm(TNode node) return; } -void TheoryFp::handleLemma(Node node) { +void TheoryFp::handleLemma(Node node, InferenceId id) +{ Trace("fp") << "TheoryFp::handleLemma(): asserting " << node << std::endl; // will be preprocessed when sent, which is important because it contains // embedded ITEs - d_out->lemma(node); + d_im.lemma(node, id); } bool TheoryFp::propagateLit(TNode node) { Trace("fp") << "TheoryFp::propagateLit(): propagate " << node << std::endl; - - bool stat = d_out->propagate(node); - - if (!stat) - { - d_state.notifyInConflict(); - } - return stat; + return d_im.propagateLit(node); } void TheoryFp::conflictEqConstantMerge(TNode t1, TNode t2) { - std::vector<TNode> assumptions; - d_equalityEngine->explainEquality(t1, t2, true, assumptions); - - Node conflict = helper::buildConjunct(assumptions); - Trace("fp") << "TheoryFp::conflictEqConstantMerge(): conflict detected " - << conflict << std::endl; - - d_conflictNode = conflict; - d_state.notifyInConflict(); - d_out->conflict(conflict); - return; + Trace("fp") << "TheoryFp::conflictEqConstantMerge(): conflict detected" + << std::endl; + d_im.conflictEqConstantMerge(t1, t2); } diff --git a/src/theory/fp/theory_fp.h b/src/theory/fp/theory_fp.h index 1660d5799..b15b5c2dd 100644 --- a/src/theory/fp/theory_fp.h +++ b/src/theory/fp/theory_fp.h @@ -27,6 +27,7 @@ #include "context/cdo.h" #include "theory/fp/theory_fp_rewriter.h" #include "theory/theory.h" +#include "theory/theory_inference_manager.h" #include "theory/theory_state.h" #include "theory/uf/equality_engine.h" @@ -142,7 +143,7 @@ class TheoryFp : public Theory void convertAndEquateTerm(TNode node); /** Interaction with the rest of the solver **/ - void handleLemma(Node node); + void handleLemma(Node node, InferenceId id = InferenceId::UNKNOWN); /** * Called when literal node is inferred by the equality engine. This * propagates node on the output channel. @@ -168,7 +169,6 @@ class TheoryFp : public Theory Node abstractFloatToReal(Node); private: - context::CDO<Node> d_conflictNode; ComparisonUFMap d_minMap; ComparisonUFMap d_maxMap; @@ -183,6 +183,8 @@ class TheoryFp : public Theory TheoryFpRewriter d_rewriter; /** A (default) theory state object */ TheoryState d_state; + /** A (default) inference manager */ + TheoryInferenceManager d_im; }; /* class TheoryFp */ } // namespace fp |