projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 0feb78d) | patch
Changes to the CNF conversion and the SAT solver. All regression pass now, and we...
authorDejan Jovanović <dejan.jovanovic@gmail.com>
Tue, 9 Feb 2010 23:07:33 +0000 (23:07 +0000)
committerDejan Jovanović <dejan.jovanovic@gmail.com>
Tue, 9 Feb 2010 23:07:33 +0000 (23:07 +0000)
commit044329296028ad944b703929fad4d85aa6183472
treeb2a6d56fc5eb4d1bbc4d8d75a1b2814f5b4382betree
parent0feb78d917ce5847ede01a5895611e54195bafcdcommit | diff
Changes to the CNF conversion and the SAT solver. All regression pass now, and we're ready for nightly testing. We should not add regression tests that test future behaviour, as the builds will nag for all failing regressions. Thus, I've separated the multi-query regressions into multiple regressions until the cnf/context/sat is able to handle it. Also, fixed a typo in the CVC parser.
40 files changed:
src/parser/cvc/cvc_parser.g diff | blob | history
src/prop/cnf_stream.cpp diff | blob | history
src/prop/cnf_stream.h diff | blob | history
src/prop/minisat/CVC4-README [new file with mode: 0644] blob
src/prop/minisat/core/Solver.h diff | blob | history
src/prop/prop_engine.cpp diff | blob | history
src/prop/prop_engine.h diff | blob | history
src/prop/sat.h diff | blob | history
src/smt/smt_engine.cpp diff | blob | history
src/smt/smt_engine.h diff | blob | history
test/regress/regress0/Makefile.am diff | blob | history
test/regress/regress0/logops.01.cvc [new file with mode: 0644] blob
test/regress/regress0/logops.02.cvc [new file with mode: 0644] blob
test/regress/regress0/logops.03.cvc [new file with mode: 0644] blob
test/regress/regress0/logops.04.cvc [new file with mode: 0644] blob
test/regress/regress0/logops.05.cvc [new file with mode: 0644] blob
test/regress/regress0/logops.cvc [deleted file] blob | history
test/regress/regress0/wiki.01.cvc [new file with mode: 0644] blob
test/regress/regress0/wiki.02.cvc [new file with mode: 0644] blob
test/regress/regress0/wiki.03.cvc [new file with mode: 0644] blob
test/regress/regress0/wiki.04.cvc [new file with mode: 0644] blob
test/regress/regress0/wiki.05.cvc [new file with mode: 0644] blob
test/regress/regress0/wiki.06.cvc [new file with mode: 0644] blob
test/regress/regress0/wiki.07.cvc [new file with mode: 0644] blob
test/regress/regress0/wiki.08.cvc [new file with mode: 0644] blob
test/regress/regress0/wiki.09.cvc [new file with mode: 0644] blob
test/regress/regress0/wiki.10.cvc [new file with mode: 0644] blob
test/regress/regress0/wiki.11.cvc [new file with mode: 0644] blob
test/regress/regress0/wiki.12.cvc [new file with mode: 0644] blob
test/regress/regress0/wiki.13.cvc [new file with mode: 0644] blob
test/regress/regress0/wiki.14.cvc [new file with mode: 0644] blob
test/regress/regress0/wiki.15.cvc [new file with mode: 0644] blob
test/regress/regress0/wiki.16.cvc [new file with mode: 0644] blob
test/regress/regress0/wiki.17.cvc [new file with mode: 0644] blob
test/regress/regress0/wiki.18.cvc [new file with mode: 0644] blob
test/regress/regress0/wiki.19.cvc [new file with mode: 0644] blob
test/regress/regress0/wiki.20.cvc [new file with mode: 0644] blob
test/regress/regress0/wiki.21.cvc [new file with mode: 0644] blob
test/regress/regress0/wiki.cvc [deleted file] blob | history
test/regress/run_regression diff | blob | history