git.libre-soc.org Git - cvc5.git/commit

author	Morgan Deters <mdeters@gmail.com>
	Sun, 10 Oct 2010 22:15:38 +0000 (22:15 +0000)
committer	Morgan Deters <mdeters@gmail.com>
	Sun, 10 Oct 2010 22:15:38 +0000 (22:15 +0000)
commit	d6b37239a2e525e7878d3bb0b4372a8dabc340a9
tree	3db6b54c8b5873db1e6c91b1577d431d74632c66	tree
parent	7a059452ebf5729723f610da9258a47007e38253	commit \| diff

additional model gen and SMT-LIBv2 compliance work: (get-assignment) now supported; work on Result type (biggest noticeable change is that CVC4 now outputs lowercase "sat" and "unsat"), Options class moved to src/smt, to allow for future work on runtime configuration via (set-option) command

98 files changed:

configure.ac		diff \| blob \| history
src/context/cdset.h		diff \| blob \| history
src/context/cdset_forward.h	[new file with mode: 0644]	blob
src/expr/command.cpp		diff \| blob \| history
src/expr/command.h		diff \| blob \| history
src/main/getopt.cpp		diff \| blob \| history
src/main/main.cpp		diff \| blob \| history
src/main/util.cpp		diff \| blob \| history
src/parser/smt2/Smt2.g		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/Makefile.am		diff \| blob \| history
src/smt/options.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/shared_data.h		diff \| blob \| history
src/theory/shared_term_manager.h		diff \| blob \| history
src/theory/theory_engine.cpp		diff \| blob \| history
src/theory/theory_engine.h		diff \| blob \| history
src/util/Assert.h		diff \| blob \| history
src/util/Makefile.am		diff \| blob \| history
src/util/options.h	[deleted file]	blob \| history
src/util/result.cpp	[new file with mode: 0644]	blob
src/util/result.h		diff \| blob \| history
src/util/sexpr.h		diff \| blob \| history
test/regress/regress0/arith/arith.01.cvc		diff \| blob \| history
test/regress/regress0/arith/arith.02.cvc		diff \| blob \| history
test/regress/regress0/arith/arith.03.cvc		diff \| blob \| history
test/regress/regress0/boolean-prec.cvc		diff \| blob \| history
test/regress/regress0/boolean.cvc		diff \| blob \| history
test/regress/regress0/bug32.cvc		diff \| blob \| history
test/regress/regress0/cvc3-bug15.cvc		diff \| blob \| history
test/regress/regress0/hole6.cvc		diff \| blob \| history
test/regress/regress0/ite.cvc		diff \| blob \| history
test/regress/regress0/logops.01.cvc		diff \| blob \| history
test/regress/regress0/logops.02.cvc		diff \| blob \| history
test/regress/regress0/logops.03.cvc		diff \| blob \| history
test/regress/regress0/logops.04.cvc		diff \| blob \| history
test/regress/regress0/logops.05.cvc		diff \| blob \| history
test/regress/regress0/precedence/and-not.cvc		diff \| blob \| history
test/regress/regress0/precedence/and-xor.cvc		diff \| blob \| history
test/regress/regress0/precedence/bool-cmp.cvc		diff \| blob \| history
test/regress/regress0/precedence/cmp-plus.cvc		diff \| blob \| history
test/regress/regress0/precedence/eq-fun.cvc		diff \| blob \| history
test/regress/regress0/precedence/iff-assoc.cvc		diff \| blob \| history
test/regress/regress0/precedence/iff-implies.cvc		diff \| blob \| history
test/regress/regress0/precedence/implies-assoc.cvc		diff \| blob \| history
test/regress/regress0/precedence/implies-iff.cvc		diff \| blob \| history
test/regress/regress0/precedence/implies-or.cvc		diff \| blob \| history
test/regress/regress0/precedence/not-and.cvc		diff \| blob \| history
test/regress/regress0/precedence/not-eq.cvc		diff \| blob \| history
test/regress/regress0/precedence/or-implies.cvc		diff \| blob \| history
test/regress/regress0/precedence/or-xor.cvc		diff \| blob \| history
test/regress/regress0/precedence/plus-mult.cvc		diff \| blob \| history
test/regress/regress0/precedence/xor-and.cvc		diff \| blob \| history
test/regress/regress0/precedence/xor-assoc.cvc		diff \| blob \| history
test/regress/regress0/precedence/xor-or.cvc		diff \| blob \| history
test/regress/regress0/queries0.cvc		diff \| blob \| history
test/regress/regress0/simple.cvc		diff \| blob \| history
test/regress/regress0/smallcnf.cvc		diff \| blob \| history
test/regress/regress0/test11.cvc		diff \| blob \| history
test/regress/regress0/test12.cvc		diff \| blob \| history
test/regress/regress0/test9.cvc		diff \| blob \| history
test/regress/regress0/uf/simple.01.cvc		diff \| blob \| history
test/regress/regress0/uf/simple.02.cvc		diff \| blob \| history
test/regress/regress0/uf/simple.03.cvc		diff \| blob \| history
test/regress/regress0/uf/simple.04.cvc		diff \| blob \| history
test/regress/regress0/uf20-03.cvc		diff \| blob \| history
test/regress/regress0/wiki.01.cvc		diff \| blob \| history
test/regress/regress0/wiki.02.cvc		diff \| blob \| history
test/regress/regress0/wiki.03.cvc		diff \| blob \| history
test/regress/regress0/wiki.04.cvc		diff \| blob \| history
test/regress/regress0/wiki.05.cvc		diff \| blob \| history
test/regress/regress0/wiki.06.cvc		diff \| blob \| history
test/regress/regress0/wiki.07.cvc		diff \| blob \| history
test/regress/regress0/wiki.08.cvc		diff \| blob \| history
test/regress/regress0/wiki.09.cvc		diff \| blob \| history
test/regress/regress0/wiki.10.cvc		diff \| blob \| history
test/regress/regress0/wiki.11.cvc		diff \| blob \| history
test/regress/regress0/wiki.12.cvc		diff \| blob \| history
test/regress/regress0/wiki.13.cvc		diff \| blob \| history
test/regress/regress0/wiki.14.cvc		diff \| blob \| history
test/regress/regress0/wiki.15.cvc		diff \| blob \| history
test/regress/regress0/wiki.16.cvc		diff \| blob \| history
test/regress/regress0/wiki.17.cvc		diff \| blob \| history
test/regress/regress0/wiki.18.cvc		diff \| blob \| history
test/regress/regress0/wiki.19.cvc		diff \| blob \| history
test/regress/regress0/wiki.20.cvc		diff \| blob \| history
test/regress/regress0/wiki.21.cvc		diff \| blob \| history
test/regress/regress1/hole7.cvc		diff \| blob \| history
test/regress/regress1/hole8.cvc		diff \| blob \| history
test/regress/regress2/hole9.cvc		diff \| blob \| history
test/regress/regress3/hole10.cvc		diff \| blob \| history
test/regress/run_regression		diff \| blob \| history
test/unit/prop/cnf_stream_black.h		diff \| blob \| history
test/unit/theory/shared_term_manager_black.h		diff \| blob \| history
test/unit/theory/theory_engine_white.h		diff \| blob \| history

RSS Atom