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

author	Morgan Deters <mdeters@gmail.com>
	Mon, 11 Jul 2011 03:33:14 +0000 (03:33 +0000)
committer	Morgan Deters <mdeters@gmail.com>
	Mon, 11 Jul 2011 03:33:14 +0000 (03:33 +0000)
commit	25e9c72dd689d3b621b901220794c652a3ba589a
tree	58b14dd3818f3e7a8ca3311a0457716e7753a95e	tree
parent	587520ce888b88294fb9e4ca476e2425d8bf026e	commit \| diff

merge from symmetry branch

27 files changed:

src/expr/command.cpp		diff \| blob \| history
src/expr/command.h		diff \| blob \| history
src/printer/ast/ast_printer.cpp		diff \| blob \| history
src/printer/ast/ast_printer.h		diff \| blob \| history
src/printer/cvc/cvc_printer.cpp		diff \| blob \| history
src/printer/cvc/cvc_printer.h		diff \| blob \| history
src/printer/printer.h		diff \| blob \| history
src/printer/smt/smt_printer.cpp		diff \| blob \| history
src/printer/smt/smt_printer.h		diff \| blob \| history
src/printer/smt2/smt2_printer.cpp		diff \| blob \| history
src/printer/smt2/smt2_printer.h		diff \| blob \| history
src/prop/minisat/core/Solver.cc		diff \| blob \| history
src/prop/prop_engine.cpp		diff \| blob \| history
src/smt/smt_engine.cpp		diff \| blob \| history
src/theory/theory_engine.cpp		diff \| blob \| history
src/theory/uf/Makefile.am		diff \| blob \| history
src/theory/uf/morgan/theory_uf_morgan.cpp		diff \| blob \| history
src/theory/uf/morgan/theory_uf_morgan.h		diff \| blob \| history
src/theory/uf/symmetry_breaker.cpp	[new file with mode: 0644]	blob
src/theory/uf/symmetry_breaker.h	[new file with mode: 0644]	blob
src/theory/uf/theory_uf.cpp		diff \| blob \| history
src/theory/uf/theory_uf.h		diff \| blob \| history
src/util/options.cpp		diff \| blob \| history
src/util/options.h		diff \| blob \| history
test/regress/regress0/uf/Makefile.am		diff \| blob \| history
test/regress/regress0/uf/gensys_brn001.smt2	[new file with mode: 0644]	blob
test/regress/regress0/uf/mkpidgeon	[new file with mode: 0755]	blob