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

author	Aina Niemetz <aina.niemetz@gmail.com>
	Mon, 5 Mar 2018 22:05:26 +0000 (14:05 -0800)
committer	GitHub <noreply@github.com>
	Mon, 5 Mar 2018 22:05:26 +0000 (14:05 -0800)
commit	d51c8347a3c6bf7857c474bd3493377f9fed58e5
tree	56da229cd8fcbe6988937514820c13c3894f2558	tree
parent	d1aa4ae101987093a06208650e2ea4878f7437ca	commit \| diff

Add support for check-sat-assuming. (#1637)

This adds support for check-sat-assuming. It further adds support for SmtEngine::query() over a
vector of Expressions, e.g., smtEngine->query({a, b}); checks the validity (of the current input
formula) under assumption (not (or a b)).

13 files changed:

RSS Atom

examples/api/bitvectors.cpp		diff \| blob \| history
src/expr/expr_template.cpp		diff \| blob \| history
src/expr/expr_template.h		diff \| blob \| history
src/parser/smt2/Smt2.g		diff \| blob \| history
src/printer/ast/ast_printer.cpp		diff \| blob \| history
src/printer/cvc/cvc_printer.cpp		diff \| blob \| history
src/printer/smt2/smt2_printer.cpp		diff \| blob \| history
src/smt/command.cpp		diff \| blob \| history
src/smt/command.h		diff \| blob \| history
src/smt/smt_engine.cpp		diff \| blob \| history
src/smt/smt_engine.h		diff \| blob \| history
test/regress/regress0/push-pop/Makefile.am		diff \| blob \| history
test/regress/regress0/push-pop/bug821-check_sat_assuming.smt2	[new file with mode: 0644]	blob