diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-05-25 05:30:40 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-05-25 05:30:40 +0000 |
commit | e87c14798b99ccb586751d291b0eeb3208265bd8 (patch) | |
tree | 8ffab42bc3b5b27d4a0f209adfd274f8741f26cd /src/prop/cnf_stream.h | |
parent | 4ba56dc24c972afae6137e4dd6a05f3957e48bf5 (diff) |
Some initial changes to allow for lemmas on demand.
To be done:
* Add erasable map Clause* to bool to minisat (backtracks with the solver)
* Add map from Clause* to Node (clauses that came from a node)
* Add reference counting Literal -> Node to CNFManager
* If Literal -> Node refcount goes to zero, the clauses of Node can be erased (if eresable)
* If clause is erased for each L in clause L -> Node refcount goes down
Diffstat (limited to 'src/prop/cnf_stream.h')
-rw-r--r-- | src/prop/cnf_stream.h | 22 |
1 files changed, 16 insertions, 6 deletions
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index 7546a8880..1ea600322 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -39,7 +39,9 @@ class PropEngine; * @author Tim King <taking@cs.nyu.edu> */ class CnfStream { + public: + /** Cache of what nodes have been registered to a literal. */ typedef __gnu_cxx::hash_map<SatLiteral, Node, SatSolver::SatLiteralHashFunction> NodeCache; @@ -57,23 +59,30 @@ private: protected: /** + * Are we asserting a lemma (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; + + /** * Asserts the given clause to the sat solver. * @param clause the clasue to assert */ - void assertClause(SatClause& clause); + void assertClause(TNode node, SatClause& clause); /** * Asserts the unit clause to the sat solver. * @param a the unit literal of the clause */ - void assertClause(SatLiteral a); + void assertClause(TNode node, SatLiteral a); /** * Asserts the binary clause to the sat solver. * @param a the first literal in the clause * @param b the second literal in the clause */ - void assertClause(SatLiteral a, SatLiteral b); + void assertClause(TNode node, SatLiteral a, SatLiteral b); /** * Asserts the ternary clause to the sat solver. @@ -81,7 +90,7 @@ protected: * @param b the second literal in the clause * @param c the thirs literal in the clause */ - void assertClause(SatLiteral a, SatLiteral b, SatLiteral c); + void assertClause(TNode node, SatLiteral a, SatLiteral b, SatLiteral c); /** * Returns true if the node has been cashed in the translation cache. @@ -137,7 +146,7 @@ public: * @param node node to convert and assert * @param whether the sat solver can choose to remove this clause */ - virtual void convertAndAssert(TNode node) = 0; + virtual void convertAndAssert(TNode node, bool lemma = false) = 0; /** * Get the node that is represented by the given SatLiteral. @@ -175,8 +184,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 */ - void convertAndAssert(TNode node); + void convertAndAssert(TNode node, bool lemma); /** * Constructs the stream to use the given sat solver. |