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

author	Dejan Jovanović <dejan.jovanovic@gmail.com>
	Tue, 5 Jul 2011 16:21:50 +0000 (16:21 +0000)
committer	Dejan Jovanović <dejan.jovanovic@gmail.com>
	Tue, 5 Jul 2011 16:21:50 +0000 (16:21 +0000)
commit	7342d1ca87397f3d5beb2c04b819243303e69a7c
tree	9e166f1884275be7d4b33b13b8bcfe9418e61033	tree
parent	af25c3f8498198dd6dd114c3b4ef39af54611e1e	commit \| diff

updated preprocessing and rewriting input equalities into inequalities for LRA

49 files changed:

src/expr/command.cpp		diff \| blob \| history
src/expr/node.h		diff \| blob \| history
src/expr/node_manager.cpp		diff \| blob \| history
src/prop/cnf_stream.cpp		diff \| blob \| history
src/prop/prop_engine.cpp		diff \| blob \| history
src/smt/smt_engine.cpp		diff \| blob \| history
src/smt/smt_engine.h		diff \| blob \| history
src/theory/Makefile.am		diff \| blob \| history
src/theory/arith/arith_rewriter.cpp		diff \| blob \| history
src/theory/arith/arith_static_learner.cpp		diff \| blob \| history
src/theory/arith/arith_static_learner.h		diff \| blob \| history
src/theory/arith/theory_arith.cpp		diff \| blob \| history
src/theory/arith/theory_arith.h		diff \| blob \| history
src/theory/booleans/circuit_propagator.cpp		diff \| blob \| history
src/theory/booleans/circuit_propagator.h		diff \| blob \| history
src/theory/booleans/theory_bool.cpp		diff \| blob \| history
src/theory/booleans/theory_bool.h		diff \| blob \| history
src/theory/booleans/theory_bool_rewriter.cpp		diff \| blob \| history
src/theory/builtin/theory_builtin.cpp		diff \| blob \| history
src/theory/builtin/theory_builtin.h		diff \| blob \| history
src/theory/bv/theory_bv.h		diff \| blob \| history
src/theory/substitutions.cpp	[new file with mode: 0644]	blob
src/theory/substitutions.h		diff \| blob \| history
src/theory/theory.h		diff \| blob \| history
src/theory/theory_engine.cpp		diff \| blob \| history
src/theory/theory_engine.h		diff \| blob \| history
src/theory/valuation.cpp		diff \| blob \| history
src/theory/valuation.h		diff \| blob \| history
src/util/Makefile.am		diff \| blob \| history
src/util/ite_removal.cpp	[new file with mode: 0644]	blob
src/util/ite_removal.h	[new file with mode: 0644]	blob
src/util/options.cpp		diff \| blob \| history
src/util/options.h		diff \| blob \| history
test/regress/regress0/Makefile.am		diff \| blob \| history
test/regress/regress0/preprocess/Makefile	[new file with mode: 0644]	blob
test/regress/regress0/preprocess/Makefile.am	[new file with mode: 0644]	blob
test/regress/regress0/preprocess/preprocess_00.cvc	[new file with mode: 0644]	blob
test/regress/regress0/preprocess/preprocess_01.cvc	[new file with mode: 0644]	blob
test/regress/regress0/preprocess/preprocess_02.cvc	[new file with mode: 0644]	blob
test/regress/regress0/preprocess/preprocess_03.cvc	[new file with mode: 0644]	blob
test/regress/regress0/preprocess/preprocess_04.cvc	[new file with mode: 0644]	blob
test/regress/regress0/preprocess/preprocess_05.cvc	[new file with mode: 0644]	blob
test/regress/regress0/preprocess/preprocess_06.cvc	[new file with mode: 0644]	blob
test/regress/regress0/preprocess/preprocess_07.cvc	[new file with mode: 0644]	blob
test/regress/regress0/preprocess/preprocess_08.cvc	[new file with mode: 0644]	blob
test/regress/regress0/preprocess/preprocess_09.cvc	[new file with mode: 0644]	blob
test/regress/regress0/preprocess/preprocess_10.cvc	[new file with mode: 0644]	blob
test/regress/regress0/preprocess/preprocess_11.cvc	[new file with mode: 0644]	blob
test/regress/regress0/push-pop/Makefile.am		diff \| blob \| history

RSS Atom