diff options
Diffstat (limited to 'src/prop/cnf_stream.h')
-rw-r--r-- | src/prop/cnf_stream.h | 21 |
1 files changed, 11 insertions, 10 deletions
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index 6cc10d878..cf9d519a7 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -36,9 +36,6 @@ #include "smt_util/lemma_channels.h" namespace CVC4 { - -class LemmaProofRecipe; - namespace prop { class PropEngine; @@ -177,7 +174,7 @@ protected: * structure in this expression. Assumed to not be in the * translation cache. */ - SatLiteral convertAtom(TNode node, bool noPreprocessing = false); + SatLiteral convertAtom(TNode node); public: @@ -210,10 +207,14 @@ 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 + * @param ownerTheory indicates the theory that should invoked to prove the formula. */ - 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(), + theory::TheoryId ownerTheory = theory::THEORY_LAST) = 0; /** * Get the node that is represented by the given SatLiteral. * @param literal the literal from the sat solver @@ -234,7 +235,7 @@ public: * this is like a "convert-but-don't-assert" version of * convertAndAssert(). */ - virtual void ensureLiteral(TNode n, bool noPreregistration = false) = 0; + virtual void ensureLiteral(TNode n) = 0; /** * Returns the literal that represents the given node in the SAT CNF @@ -283,7 +284,7 @@ public: */ void convertAndAssert(TNode node, bool removable, bool negated, ProofRule rule, TNode from = TNode::null(), - LemmaProofRecipe* proofRecipe = NULL); + theory::TheoryId ownerTheory = theory::THEORY_LAST); /** * Constructs the stream to use the given sat solver. @@ -336,7 +337,7 @@ private: */ SatLiteral toCNF(TNode node, bool negated = false); - void ensureLiteral(TNode n, bool noPreregistration = false); + void ensureLiteral(TNode n); };/* class TseitinCnfStream */ |