projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: cfb3b78) | patch
In order for splitting on demand to be able to retract clauses every translation...
authorDejan Jovanović <dejan.jovanovic@gmail.com>
Tue, 1 Jun 2010 01:26:24 +0000 (01:26 +0000)
committerDejan Jovanović <dejan.jovanovic@gmail.com>
Tue, 1 Jun 2010 01:26:24 +0000 (01:26 +0000)
commiteee91ecc512e94358a02d2aa155764e4cda2e5fa
tree7611e3305463978cb9a957a75d218083fe6fb677tree
parentcfb3b789e26fdab73e733825950b24492c6c5e4ccommit | 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.
src/prop/cnf_stream.cpp diff | blob | history
src/prop/cnf_stream.h diff | blob | history
src/prop/prop_engine.cpp diff | blob | history
test/unit/prop/cnf_stream_black.h diff | blob | history