diff options
Diffstat (limited to 'src/prop/cnf_stream.h')
| -rw-r--r-- | src/prop/cnf_stream.h | 58 |
1 files changed, 27 insertions, 31 deletions
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index cfab216fe..a07944a58 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -84,8 +84,11 @@ protected: /** The "registrar" for pre-registration of terms */ Registrar* d_registrar; - /** A table of assertions, used for regenerating proofs. */ - context::CDList<Node> d_assertionTable; + /** The name of this CNF stream*/ + std::string d_name; + + /** Pointer to the proof corresponding to this CnfStream */ + CnfProof* d_cnfProof; /** Container for misc. globals. */ SmtGlobals* d_globals; @@ -117,14 +120,6 @@ protected: } /** - * A reference into the assertion table, used to map clauses back to - * their "original" input assertion/lemma. This variable is manipulated - * by the top-level convertAndAssert(). This is needed in proofs-enabled - * runs, to justify where the SAT solver's clauses came from. - */ - uint64_t d_proofId; - - /** * Are we asserting a removable clause (true) or a permanent clause (false). * This is set at the beginning of convertAndAssert so that it doesn't * need to be passed on over the stack. Only pure clauses can be asserted @@ -137,14 +132,14 @@ protected: * @param node the node giving rise to this clause * @param clause the clause to assert */ - void assertClause(TNode node, SatClause& clause, ProofRule proof_id); + void assertClause(TNode node, SatClause& clause); /** * Asserts the unit clause to the sat solver. * @param node the node giving rise to this clause * @param a the unit literal of the clause */ - void assertClause(TNode node, SatLiteral a, ProofRule proof_id); + void assertClause(TNode node, SatLiteral a); /** * Asserts the binary clause to the sat solver. @@ -152,7 +147,7 @@ protected: * @param a the first literal in the clause * @param b the second literal in the clause */ - void assertClause(TNode node, SatLiteral a, SatLiteral b, ProofRule proof_id); + void assertClause(TNode node, SatLiteral a, SatLiteral b); /** * Asserts the ternary clause to the sat solver. @@ -161,7 +156,7 @@ protected: * @param b the second literal in the clause * @param c the thirs literal in the clause */ - void assertClause(TNode node, SatLiteral a, SatLiteral b, SatLiteral c, ProofRule proof_id); + void assertClause(TNode node, SatLiteral a, SatLiteral b, SatLiteral c); /** * Acquires a new variable from the SAT solver to represent the node @@ -193,9 +188,15 @@ public: * @param registrar the entity that takes care of preregistration of Nodes * @param context the context that the CNF should respect * @param fullLitToNodeMap maintain a full SAT-literal-to-Node mapping, + * @param name string identifier to distinguish between different instances * even for non-theory literals */ - CnfStream(SatSolver* satSolver, Registrar* registrar, context::Context* context, SmtGlobals* globals, bool fullLitToNodeMap = false); + CnfStream(SatSolver* satSolver, + Registrar* registrar, + context::Context* context, + SmtGlobals* globals, + bool fullLitToNodeMap = false, + std::string name=""); /** * Destructs a CnfStream. This implementation does nothing, but we @@ -244,13 +245,6 @@ public: SatLiteral getLiteral(TNode node); /** - * Get the assertion with a given ID. (Used for reconstructing proofs.) - */ - TNode getAssertion(uint64_t id) { - return d_assertionTable[id]; - } - - /** * Returns the Boolean variables from the input problem. */ void getBooleanVariables(std::vector<TNode>& outputVariables) const; @@ -263,6 +257,7 @@ public: return d_literalToNodeMap; } + void setProof(CnfProof* proof); };/* class CnfStream */ @@ -286,7 +281,8 @@ public: * @param removable is this something that can be erased * @param negated true if negated */ - void convertAndAssert(TNode node, bool removable, bool negated, ProofRule proof_id, TNode from = TNode::null()); + void convertAndAssert(TNode node, bool removable, + bool negated, ProofRule rule, TNode from = TNode::null()); /** * Constructs the stream to use the given sat solver. @@ -295,14 +291,14 @@ public: * @param fullLitToNodeMap maintain a full SAT-literal-to-Node mapping, * even for non-theory literals */ - TseitinCnfStream(SatSolver* satSolver, Registrar* registrar, context::Context* context, SmtGlobals* globals, bool fullLitToNodeMap = false); + TseitinCnfStream(SatSolver* satSolver, Registrar* registrar, context::Context* context, SmtGlobals* globals, bool fullLitToNodeMap = false, std::string name = ""); private: /** * Same as above, except that removable is remembered. */ - void convertAndAssert(TNode node, bool negated, ProofRule proof_id); + void convertAndAssert(TNode node, bool negated); // Each of these formulas handles takes care of a Node of each Kind. // @@ -322,12 +318,12 @@ private: SatLiteral handleAnd(TNode node); SatLiteral handleOr(TNode node); - void convertAndAssertAnd(TNode node, bool negated, ProofRule proof_id); - void convertAndAssertOr(TNode node, bool negated, ProofRule proof_id); - void convertAndAssertXor(TNode node, bool negated, ProofRule proof_id); - void convertAndAssertIff(TNode node, bool negated, ProofRule proof_id); - void convertAndAssertImplies(TNode node, bool negated, ProofRule proof_id); - void convertAndAssertIte(TNode node, bool negated, ProofRule proof_id); + void convertAndAssertAnd(TNode node, bool negated); + void convertAndAssertOr(TNode node, bool negated); + void convertAndAssertXor(TNode node, bool negated); + void convertAndAssertIff(TNode node, bool negated); + void convertAndAssertImplies(TNode node, bool negated); + void convertAndAssertIte(TNode node, bool negated); /** * Transforms the node into CNF recursively. |