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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Sun, 11 May 2014 19:36:50 +0000 (14:36 -0500)
committer	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Sun, 11 May 2014 19:36:50 +0000 (14:36 -0500)
commit	0b2f9943d55152e0958369083649dd71340864c9
tree	cd040f1dd12816c6af37548597bd674cafb45271	tree
parent	8ebd49cb903ba19f9330820d02af08e226c9b791	commit \| diff

More preparation for CASC proofs. Minor fix for sort inference (rewrite new assertions). Bug fix for ambqi : simplify correctly for multi-sorted case. Bug fix for fmc : only do exh-simplification for uninterpreted sorts, ensure reps are enumerated for quantification over Real.

30 files changed:

contrib/run-script-cascj7-fnt		diff \| blob \| history
contrib/run-script-cascj7-fof		diff \| blob \| history
contrib/run-script-cascj7-tff		diff \| blob \| history
src/Makefile.am		diff \| blob \| history
src/expr/command.cpp		diff \| blob \| history
src/expr/command.h		diff \| blob \| history
src/main/command_executor.cpp		diff \| blob \| history
src/printer/model_format_mode.cpp	[deleted file]	blob \| history
src/printer/model_format_mode.h	[deleted file]	blob \| history
src/printer/modes.cpp	[new file with mode: 0644]	blob
src/printer/modes.h	[new file with mode: 0644]	blob
src/printer/options		diff \| blob \| history
src/printer/options_handlers.h		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/full_model_check.cpp		diff \| blob \| history
src/theory/quantifiers/inst_match.cpp		diff \| blob \| history
src/theory/quantifiers/inst_match.h		diff \| blob \| history
src/theory/quantifiers/instantiation_engine.cpp		diff \| blob \| history
src/theory/quantifiers_engine.cpp		diff \| blob \| history
src/theory/quantifiers_engine.h		diff \| blob \| history
src/theory/rep_set.cpp		diff \| blob \| history
src/theory/rep_set.h		diff \| blob \| history
src/theory/theory_engine.cpp		diff \| blob \| history
src/theory/theory_engine.h		diff \| blob \| history
src/theory/theory_model.cpp		diff \| blob \| history
src/util/sort_inference.cpp		diff \| blob \| history

RSS Atom