diff options
Diffstat (limited to 'src/theory/theory_engine.h')
-rw-r--r-- | src/theory/theory_engine.h | 64 |
1 files changed, 34 insertions, 30 deletions
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index be3068a45..80890303b 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -96,7 +96,7 @@ class TheoryEngine { * runs (no sharing), can reduce the cost of walking the DAG on * registration, etc. */ - theory::Theory::Set d_activeTheories; + context::CDO<theory::Theory::Set> d_activeTheories; /** * The database of shared terms. @@ -191,7 +191,7 @@ class TheoryEngine { void conflict(TNode conflictNode) throw(AssertionException) { Trace("theory") << "EngineOutputChannel<" << d_theory << ">::conflict(" << conflictNode << ")" << std::endl; ++ d_statistics.conflicts; - d_engine->conflict(conflictNode); + d_engine->conflict(conflictNode, d_theory); } void propagate(TNode literal) throw(AssertionException) { @@ -226,21 +226,26 @@ class TheoryEngine { */ context::CDO<bool> d_inConflict; - void conflict(TNode conflict) { - - Assert(properConflict(conflict), "not a proper conflict: %s", conflict.toString().c_str()); + /** + * Does the context contain terms shared among multiple theories. + */ + context::CDO<bool> d_sharedTermsExist; - // Mark that we are in conflict - d_inConflict = true; + /** + * Explain the equality literals and push all the explaining literals into the builder. All + * the non-equality literals are pushed to the builder. + */ + void explainEqualities(theory::TheoryId theoryId, TNode literals, NodeBuilder<>& builder); - if(Dump.isOn("t-conflicts")) { - Dump("t-conflicts") << CommentCommand("theory conflict: expect unsat") << std::endl - << CheckSatCommand(conflict.toExpr()) << std::endl; - } + /** + * Same as above, but just for single equalities. + */ + void explainEquality(theory::TheoryId theoryId, TNode eqLiteral, NodeBuilder<>& builder); - // Construct the lemma (note that no CNF caching should happen as all the literals already exists) - lemma(conflict, true, false); - } + /** + * Called by the theories to notify of a conflict. + */ + void conflict(TNode conflict, theory::TheoryId theoryId); /** * Debugging flag to ensure that shutdown() is called before the @@ -282,15 +287,20 @@ class TheoryEngine { NodeTheoryPair toExplain; SharedEquality(TNode assertion, TNode original, theory::TheoryId sendingTheory, theory::TheoryId receivingTheory) - : toAssert(assertion, sendingTheory), - toExplain(original, receivingTheory) + : toAssert(assertion, receivingTheory), + toExplain(original, sendingTheory) { } }; /** + * Map from equalities asserted to a theory, to the theory that can explain them. + */ + typedef context::CDMap<NodeTheoryPair, NodeTheoryPair, NodeTheoryPairHashFunction> SharedAssertionsMap; + + /** * A map from asserted facts to where they came from (for explanations). */ - context::CDMap<NodeTheoryPair, NodeTheoryPair, NodeTheoryPairHashFunction> d_sharedAssertions; + SharedAssertionsMap d_sharedAssertions; /** * Assert a shared equalities propagated by theories. @@ -480,23 +490,11 @@ public: } } - Node getExplanation(TNode node, theory::Theory* theory); - bool properConflict(TNode conflict) const; bool properPropagation(TNode lit) const; bool properExplanation(TNode node, TNode expl) const; - inline Node getExplanation(TNode node) { - TNode atom = node.getKind() == kind::NOT ? node[0] : node; - Node explanation = theoryOf(atom)->explain(node); - Assert(!explanation.isNull()); - if(Dump.isOn("t-explanations")) { - Dump("t-explanations") << CommentCommand(std::string("theory explanation from ") + theoryOf(atom)->identify() + ": expect valid") << std::endl - << QueryCommand(explanation.impNode(node).toExpr()) << std::endl; - } - Assert(properExplanation(node, explanation)); - return explanation; - } + Node getExplanation(TNode node); Node getValue(TNode node); @@ -522,6 +520,12 @@ public: return d_theoryTable[theoryId]; } + /** + * Returns the equality status of the two terms, from the theory that owns the domain type. + * The types of a and b must be the same. + */ + theory::EqualityStatus getEqualityStatus(TNode a, TNode b); + private: /** Default visitor for pre-registration */ |