diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-08-22 16:59:28 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-08-22 17:58:14 -0400 |
| commit | 2dbe1f150d30f0fb0c8522f891104270ce09db4c (patch) | |
| tree | 1305f3de890f4353c3b5695a93ab7e2419760617 /src/theory/theory_engine.cpp | |
| parent | 4ec2c8eb8b8a50dc743119100767e101f19305f6 (diff) | |
Unsat core infrastruture and API (SMT-LIB compliance to come).
Diffstat (limited to 'src/theory/theory_engine.cpp')
| -rw-r--r-- | src/theory/theory_engine.cpp | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 1b0270b94..53a529325 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -34,6 +34,8 @@ #include "smt/logic_exception.h" +#include "proof/proof_manager.h" + #include "util/node_visitor.h" #include "util/ite_removal.h" @@ -168,7 +170,7 @@ TheoryEngine::TheoryEngine(context::Context* context, d_true = NodeManager::currentNM()->mkConst<bool>(true); d_false = NodeManager::currentNM()->mkConst<bool>(false); - PROOF (ProofManager::currentPM()->initTheoryProof(); ); + PROOF (ProofManager::initTheoryProof(); ); d_iteUtilities = new ITEUtilities(d_iteRemover.getContainsVisitor()); @@ -1385,10 +1387,10 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node, bool negated, bool removable } // assert to prop engine - d_propEngine->assertLemma(additionalLemmas[0], negated, removable); + d_propEngine->assertLemma(additionalLemmas[0], negated, removable, RULE_INVALID, node); for (unsigned i = 1; i < additionalLemmas.size(); ++ i) { additionalLemmas[i] = theory::Rewriter::rewrite(additionalLemmas[i]); - d_propEngine->assertLemma(additionalLemmas[i], false, removable); + d_propEngine->assertLemma(additionalLemmas[i], false, removable, RULE_INVALID, node); } // WARNING: Below this point don't assume additionalLemmas[0] to be not negated. |