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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Fri, 9 May 2014 11:51:43 +0000 (06:51 -0500)
committer	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Fri, 9 May 2014 11:51:43 +0000 (06:51 -0500)
commit	cc01e2119801bbd4fd99548b79c297fa57a1977d
tree	cf9c64efbc286089a898d93abb3150e79138e5a7	tree
parent	88907b94e858b701e83bbee67f542ad0ee5ae626	commit \| diff

Add variable ordering to ambqi. Bug fix to macros. More preparation for CASC proofs.

13 files changed:

src/expr/command.cpp		diff \| blob \| history
src/expr/command.h		diff \| blob \| history
src/main/command_executor.cpp		diff \| blob \| history
src/main/command_executor_portfolio.cpp		diff \| blob \| history
src/smt/options		diff \| blob \| history
src/smt/smt_engine.cpp		diff \| blob \| history
src/smt/smt_engine.h		diff \| blob \| history
src/theory/quantifiers/ambqi_builder.cpp		diff \| blob \| history
src/theory/quantifiers/ambqi_builder.h		diff \| blob \| history
src/theory/quantifiers/first_order_model.cpp		diff \| blob \| history
src/theory/quantifiers/first_order_model.h		diff \| blob \| history
src/theory/quantifiers/macros.cpp		diff \| blob \| history
src/theory/quantifiers/macros.h		diff \| blob \| history