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/cnf_stream.h | |
| 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/cnf_stream.h')
| -rw-r--r-- | src/prop/cnf_stream.h | 8 |
1 files changed, 2 insertions, 6 deletions
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index 6cc10d878..661108dd0 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -37,8 +37,6 @@ namespace CVC4 { -class LemmaProofRecipe; - namespace prop { class PropEngine; @@ -210,9 +208,8 @@ public: * @param node node to convert and assert * @param removable whether the sat solver can choose to remove the clauses * @param negated whether we are asserting the node negated - * @param proofRecipe contains the proof recipe for proving this node */ - virtual void convertAndAssert(TNode node, bool removable, bool negated, ProofRule proof_id, TNode from = TNode::null(), LemmaProofRecipe* proofRecipe = NULL) = 0; + virtual void convertAndAssert(TNode node, bool removable, bool negated, ProofRule proof_id, TNode from = TNode::null()) = 0; /** * Get the node that is represented by the given SatLiteral. @@ -282,8 +279,7 @@ public: * @param negated true if negated */ void convertAndAssert(TNode node, bool removable, - bool negated, ProofRule rule, TNode from = TNode::null(), - LemmaProofRecipe* proofRecipe = NULL); + bool negated, ProofRule rule, TNode from = TNode::null()); /** * Constructs the stream to use the given sat solver. |