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 /test/unit | |
| 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 'test/unit')
0 files changed, 0 insertions, 0 deletions