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

author	ajreynol <andrew.j.reynolds@gmail.com>
	Mon, 26 Jan 2015 12:11:01 +0000 (13:11 +0100)
committer	ajreynol <andrew.j.reynolds@gmail.com>
	Mon, 26 Jan 2015 12:11:01 +0000 (13:11 +0100)
commit	edd8886e56c8bb84f3fd85fc6f697d870bc0a3b7
tree	1fe3e8699f3c4831a302a369b377396ae5a347a4	tree
parent	f3045ccce9d30114f6e90cfa72de176da344cb1f	commit \| diff

Output solutions for synthesis conjectures with --dump-synth. Minor refactor of previous commit.

18 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/parser/smt2/Smt2.g		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/datatypes/datatypes_sygus.cpp		diff \| blob \| history
src/theory/datatypes/datatypes_sygus.h		diff \| blob \| history
src/theory/quantifiers/ce_guided_instantiation.cpp		diff \| blob \| history
src/theory/quantifiers/ce_guided_instantiation.h		diff \| blob \| history
src/theory/quantifiers_engine.cpp		diff \| blob \| history
src/theory/quantifiers_engine.h		diff \| blob \| history
src/theory/theory_engine.cpp		diff \| blob \| history
src/theory/theory_engine.h		diff \| blob \| history
src/util/datatype.cpp		diff \| blob \| history
src/util/datatype.h		diff \| blob \| history