projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 1e59e3f) | patch
fixed CNF conversion, and more modular; CNF conversion command line option; various...
authorMorgan Deters <mdeters@gmail.com>
Fri, 29 Jan 2010 00:05:16 +0000 (00:05 +0000)
committerMorgan Deters <mdeters@gmail.com>
Fri, 29 Jan 2010 00:05:16 +0000 (00:05 +0000)
commit2a9e6970b971eb0a9ac4c216fe5f5f1542e195e0
tree23631643798b923b7e9883286296269c8f5e772dtree
parent1e59e3f37ecb7b84371691358f3eb3804a845c04commit | diff
fixed CNF conversion, and more modular; CNF conversion command line option; various cleanups; renamed numChildren() to getNumChildren() and added it to NodeBuilder interface; fancier, non-exponential CNF conversion with variable introduction is still buggy (?)
20 files changed:
src/expr/expr.cpp diff | blob | history
src/expr/expr.h diff | blob | history
src/expr/kind.h diff | blob | history
src/expr/node.h diff | blob | history
src/expr/node_builder.h diff | blob | history
src/expr/node_manager.cpp diff | blob | history
src/expr/node_value.h diff | blob | history
src/main/getopt.cpp diff | blob | history
src/prop/prop_engine.cpp diff | blob | history
src/smt/Makefile.am diff | blob | history
src/smt/Makefile.in [new file with mode: 0644] blob
src/smt/cnf_conversion.h [new file with mode: 0644] blob
src/smt/cnf_converter.cpp [new file with mode: 0644] blob
src/smt/cnf_converter.h [new file with mode: 0644] blob
src/smt/smt_engine.cpp diff | blob | history
src/smt/smt_engine.h diff | blob | history
src/theory/theory.h diff | blob | history
src/util/options.h diff | blob | history
test/regress/simple.cvc diff | blob | history
test/unit/expr/node_black.h diff | blob | history