diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-03-10 15:15:26 +0100 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-03-10 15:15:26 +0100 |
commit | 10df4ba0752eb23c76b9aa847e3ad116673a47b6 (patch) | |
tree | f41eec3963b7a9d96c0ea85179227d88ae57f0f6 /src/prop/cnf_stream.h | |
parent | 8d140a28c76095e148acd64e47b5ca0a92ca09be (diff) |
CNF proofs. Infrastructure for preprocessing proofs. Updates to smt.plf signature. Add regressions.
Diffstat (limited to 'src/prop/cnf_stream.h')
-rw-r--r-- | src/prop/cnf_stream.h | 24 |
1 files changed, 12 insertions, 12 deletions
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index b22290ae4..d5d01d126 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -3,7 +3,7 @@ ** \verbatim ** Original author: Tim King ** Major contributors: Morgan Deters, Dejan Jovanovic - ** Minor contributors (to current version): Clark Barrett, Liana Hadarean, Christopher L. Conway + ** Minor contributors (to current version): Clark Barrett, Liana Hadarean, Christopher L. Conway, Andrew Reynolds ** This file is part of the CVC4 project. ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing @@ -133,14 +133,14 @@ protected: * @param node the node giving rise to this clause * @param clause the clause to assert */ - void assertClause(TNode node, SatClause& clause); + void assertClause(TNode node, SatClause& clause, ProofRule proof_id); /** * 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); + void assertClause(TNode node, SatLiteral a, ProofRule proof_id); /** * Asserts the binary clause to the sat solver. @@ -148,7 +148,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); + void assertClause(TNode node, SatLiteral a, SatLiteral b, ProofRule proof_id); /** * Asserts the ternary clause to the sat solver. @@ -157,7 +157,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); + void assertClause(TNode node, SatLiteral a, SatLiteral b, SatLiteral c, ProofRule proof_id); /** * Acquires a new variable from the SAT solver to represent the node @@ -298,7 +298,7 @@ private: /** * Same as above, except that removable is remembered. */ - void convertAndAssert(TNode node, bool negated); + void convertAndAssert(TNode node, bool negated, ProofRule proof_id); // Each of these formulas handles takes care of a Node of each Kind. // @@ -318,12 +318,12 @@ private: SatLiteral handleAnd(TNode node); SatLiteral handleOr(TNode node); - 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); + 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); /** * Transforms the node into CNF recursively. |