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

author	Tim King <taking@google.com>
	Mon, 3 Apr 2017 02:29:36 +0000 (19:29 -0700)
committer	Tim King <taking@google.com>
	Mon, 3 Apr 2017 02:29:36 +0000 (19:29 -0700)
commit	f278f060c177593a1835422e688fe2a022c40e2f
tree	cc2eaa62bfc4c581643cbd237d93247b8c40134f	tree
parent	e9f3b6a54e4bf35f915c46d822ed9ee051cc7df3	commit \| diff

Adding a model based axiom instantiation scheme for multiplication. Merge commit for nlAlgMaster.

35 files changed:

src/Makefile.am		diff \| blob \| history
src/options/arith_options		diff \| blob \| history
src/options/smt_options		diff \| blob \| history
src/printer/cvc/cvc_printer.cpp		diff \| blob \| history
src/printer/smt2/smt2_printer.cpp		diff \| blob \| history
src/smt/smt_engine.cpp		diff \| blob \| history
src/theory/arith/arith_rewriter.cpp		diff \| blob \| history
src/theory/arith/arith_utilities.h		diff \| blob \| history
src/theory/arith/congruence_manager.cpp		diff \| blob \| history
src/theory/arith/congruence_manager.h		diff \| blob \| history
src/theory/arith/kinds		diff \| blob \| history
src/theory/arith/nonlinear_extension.cpp	[new file with mode: 0644]	blob
src/theory/arith/nonlinear_extension.h	[new file with mode: 0644]	blob
src/theory/arith/normal_form.cpp		diff \| blob \| history
src/theory/arith/normal_form.h		diff \| blob \| history
src/theory/arith/theory_arith.cpp		diff \| blob \| history
src/theory/arith/theory_arith.h		diff \| blob \| history
src/theory/arith/theory_arith_private.cpp		diff \| blob \| history
src/theory/arith/theory_arith_private.h		diff \| blob \| history
src/theory/booleans/theory_bool.cpp		diff \| blob \| history
src/theory/quantifiers/quant_util.cpp		diff \| blob \| history
src/theory/quantifiers/quant_util.h		diff \| blob \| history
src/theory/theory.cpp		diff \| blob \| history
src/theory/theory.h		diff \| blob \| history
src/theory/theory_engine.cpp		diff \| blob \| history
test/regress/regress0/arith/bug716.0.smt2		diff \| blob \| history
test/regress/regress0/arith/div.09.smt2		diff \| blob \| history
test/regress/regress0/expect/scrub.01.smt.expect		diff \| blob \| history
test/regress/regress0/expect/scrub.02.smt		diff \| blob \| history
test/regress/regress0/expect/scrub.03.smt2.expect		diff \| blob \| history
test/regress/regress0/expect/scrub.04.smt2		diff \| blob \| history
test/regress/regress0/expect/scrub.06.cvc		diff \| blob \| history
test/regress/regress0/expect/scrub.07.sy.expect		diff \| blob \| history
test/regress/regress0/expect/scrub.08.sy		diff \| blob \| history
test/regress/regress0/expect/scrub.09.p		diff \| blob \| history

RSS Atom