diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-08-17 15:20:19 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-08-17 15:20:19 +0000 |
commit | 32e1d3558f17d12f2631175776209a5f8cabbdd9 (patch) | |
tree | ebc20658d5375b17f13b5c83d3dc7ee078029f96 /src/prop/cnf_stream.h | |
parent | 41dc1b3685b9258660dab571f8f8b56deb0fb095 (diff) |
new implementation of lemmas on demand
comparison <http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=2673&&p=5&reference_id=2637>
Diffstat (limited to 'src/prop/cnf_stream.h')
-rw-r--r-- | src/prop/cnf_stream.h | 32 |
1 files changed, 17 insertions, 15 deletions
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index e53b46d9b..fd0ab6291 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -77,9 +77,6 @@ protected: /** Top level nodes that we translated */ std::vector<TNode> d_translationTrail; - /** Nodes belonging to asserted lemmas */ - std::vector<Node> d_lemmas; - /** Remove nots from the node */ TNode stripNot(TNode node) { while (node.getKind() == kind::NOT) { @@ -102,11 +99,11 @@ protected: void undoTranslate(TNode node, int level); /** - * Are we asserting a lemma (true) or a permanent clause (false). + * Are we asserting a removable clause (true) or a permanent clause (false). * This is set at the begining of convertAndAssert so that it doesn't * need to be passed on over the stack. */ - bool d_assertingLemma; + bool d_removable; /** * Asserts the given clause to the sat solver. @@ -187,10 +184,10 @@ public: /** * Converts and asserts a formula. * @param node node to convert and assert - * @param lemma whether the sat solver can choose to remove the clauses + * @param removable 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, bool negated = false) = 0; + virtual void convertAndAssert(TNode node, bool removable, bool negated) = 0; /** * Get the node that is represented by the given SatLiteral. @@ -248,10 +245,10 @@ 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 removable is this something that can be erased * @param negated true if negated */ - void convertAndAssert(TNode node, bool lemma, bool negated = false); + void convertAndAssert(TNode node, bool removable, bool negated); /** * Constructs the stream to use the given sat solver. @@ -262,6 +259,11 @@ public: private: + /** + * Same as above, except that removable is rememebered. + */ + void convertAndAssert(TNode node, bool negated); + // Each of these formulas handles takes care of a Node of each Kind. // // Each handleX(Node &n) is responsible for: @@ -280,12 +282,12 @@ 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); + 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. |