diff options
author | Guy <katz911@gmail.com> | 2016-07-24 20:56:08 -0700 |
---|---|---|
committer | Guy <katz911@gmail.com> | 2016-07-24 20:56:08 -0700 |
commit | 1d07595a25267066a77ffce8216a759be5fbbdde (patch) | |
tree | a2ea392bbbe61b2f17fd303b0d77beb228f957b9 /src/prop/prop_engine.cpp | |
parent | f827fb06c949d421fb32f6629c2c353ca7bd026e (diff) |
Proper handling for lemmas that are conjuncts:
Record a separate recipe for each conjunct, but have as the "original lemma" in this recipe the complete conjunction, so that we can report this to the theory solver later, if asked.
Refactoring: instead of propagating the proof recipes from the theory engine to the prop engine and cnf stream to be registered there, just register them at the theory engine - as the prop engine and cnf stream don't change them.
Diffstat (limited to 'src/prop/prop_engine.cpp')
-rw-r--r-- | src/prop/prop_engine.cpp | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index eb607e901..6cdf17f30 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -132,13 +132,12 @@ void PropEngine::assertFormula(TNode node) { void PropEngine::assertLemma(TNode node, bool negated, bool removable, ProofRule rule, - LemmaProofRecipe* proofRecipe, TNode from) { //Assert(d_inCheckSat, "Sat solver should be in solve()!"); Debug("prop::lemmas") << "assertLemma(" << node << ")" << endl; // Assert as (possibly) removable - d_cnfStream->convertAndAssert(node, removable, negated, rule, from, proofRecipe); + d_cnfStream->convertAndAssert(node, removable, negated, rule, from); } void PropEngine::requirePhase(TNode n, bool phase) { |