diff options
| author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-06-01 01:26:24 +0000 |
|---|---|---|
| committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-06-01 01:26:24 +0000 |
| commit | eee91ecc512e94358a02d2aa155764e4cda2e5fa (patch) | |
| tree | 7611e3305463978cb9a957a75d218083fe6fb677 /src/prop/cnf_stream.h | |
| parent | cfb3b789e26fdab73e733825950b24492c6c5e4c (diff) | |
In order for splitting on demand to be able to retract clauses every translation must indeed be a clause (if possible). I've changed the top level CNF conversion to generate clauses, instead of introducing unit clauses for each assertion.
Diffstat (limited to 'src/prop/cnf_stream.h')
| -rw-r--r-- | src/prop/cnf_stream.h | 17 |
1 files changed, 13 insertions, 4 deletions
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index a574adf23..ce6c7eb1e 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -144,9 +144,10 @@ public: /** * Converts and asserts a formula. * @param node node to convert and assert - * @param whether the sat solver can choose to remove this clause + * @param whether the sat solver can choose to remove the clauses + * @param negated wheather we are asserting the node negated */ - virtual void convertAndAssert(TNode node, bool lemma = false) = 0; + virtual void convertAndAssert(TNode node, bool lemma, bool negated = false) = 0; /** * Get the node that is represented by the given SatLiteral. @@ -185,8 +186,9 @@ public: * Convert a given formula to CNF and assert it to the SAT solver. * @param node the formula to assert * @param lemma is this a lemma that is erasable + * @param negated true if negated */ - void convertAndAssert(TNode node, bool lemma); + void convertAndAssert(TNode node, bool lemma, bool negated = false); /** * Constructs the stream to use the given sat solver. @@ -215,13 +217,20 @@ private: SatLiteral handleAnd(TNode node); SatLiteral handleOr(TNode node); + void convertAndAssertAnd(TNode node, bool lemma, bool negated); + void convertAndAssertOr(TNode node, bool lemma, bool negated); + void convertAndAssertXor(TNode node, bool lemma, bool negated); + void convertAndAssertIff(TNode node, bool lemma, bool negated); + void convertAndAssertImplies(TNode node, bool lemma, bool negated); + void convertAndAssertIte(TNode node, bool lemma, bool negated); /** * Transforms the node into CNF recursively. * @param node the formula to transform + * @param negated wheather the literal is negated * @return the literal representing the root of the formula */ - SatLiteral toCNF(TNode node); + SatLiteral toCNF(TNode node, bool negated = false); }; /* class TseitinCnfStream */ |