diff options
Diffstat (limited to 'src/theory/theory_engine.cpp')
-rw-r--r-- | src/theory/theory_engine.cpp | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 1bb830aa8..46a9f5855 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -936,3 +936,20 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) { lemma(conflict, true, false); } } + + +//Conflict from shared terms database +void TheoryEngine::sharedConflict(TNode conflict) { + // Mark that we are in conflict + d_inConflict = true; + + if(Dump.isOn("t-conflicts")) { + Dump("t-conflicts") << CommentCommand("theory conflict: expect unsat") + << CheckSatCommand(conflict.toExpr()); + } + + Node fullConflict = explain(ExplainTask(d_sharedTerms.explain(conflict), SHARED_DATABASE_EXPLANATION)); + Assert(properConflict(fullConflict)); + Debug("theory") << "TheoryEngine::sharedConflict(" << conflict << "): " << fullConflict << std::endl; + lemma(fullConflict, true, false); +} |