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/prop/prop_engine.cpp | |
| parent | 4ec2c8eb8b8a50dc743119100767e101f19305f6 (diff) | |
Unsat core infrastruture and API (SMT-LIB compliance to come).
Diffstat (limited to 'src/prop/prop_engine.cpp')
| -rw-r--r-- | src/prop/prop_engine.cpp | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 82c0bae1a..a02e40e32 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -25,6 +25,7 @@ #include "decision/options.h" #include "theory/theory_engine.h" #include "theory/theory_registrar.h" +#include "proof/proof_manager.h" #include "util/cvc4_assert.h" #include "options/options.h" #include "smt/options.h" @@ -109,15 +110,15 @@ void PropEngine::assertFormula(TNode node) { Assert(!d_inCheckSat, "Sat solver in solve()!"); Debug("prop") << "assertFormula(" << node << ")" << endl; // Assert as non-removable - d_cnfStream->convertAndAssert(node, false, false); + d_cnfStream->convertAndAssert(node, false, false, RULE_GIVEN); } -void PropEngine::assertLemma(TNode node, bool negated, bool removable) { +void PropEngine::assertLemma(TNode node, bool negated, bool removable, ProofRule rule, TNode from) { //Assert(d_inCheckSat, "Sat solver should be in solve()!"); Debug("prop::lemmas") << "assertLemma(" << node << ")" << endl; - // Assert as removable - d_cnfStream->convertAndAssert(node, removable, negated); + // Assert as (possibly) removable + d_cnfStream->convertAndAssert(node, removable, negated, rule, from); } void PropEngine::requirePhase(TNode n, bool phase) { |