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

author	Morgan Deters <mdeters@cs.nyu.edu>
	Mon, 24 Jun 2013 23:35:58 +0000 (19:35 -0400)
committer	Morgan Deters <mdeters@cs.nyu.edu>
	Tue, 25 Jun 2013 00:07:39 +0000 (20:07 -0400)
commit	0a3422299da7e882bae22c5fa3e5ec3c80b42046
tree	d00f31a33f03f11608ee046b851f4c63e194fe87	tree
parent	30d21b25af6ee619e5f53d1ca8821b710fad4cb7	commit \| diff

Support for abs, to_int, is_int, divisible in SMT-LIB; also --rewrite-divk allows linearization of div,mod,/ by a constant.

20 files changed:

NEWS		diff \| blob \| history
RELEASE-NOTES		diff \| blob \| history
src/parser/smt2/Smt2.g		diff \| blob \| history
src/parser/smt2/smt2.cpp		diff \| blob \| history
src/printer/smt2/smt2_printer.cpp		diff \| blob \| history
src/smt/boolean_terms.cpp		diff \| blob \| history
src/smt/smt_engine.cpp		diff \| blob \| history
src/theory/arith/arith_rewriter.cpp		diff \| blob \| history
src/theory/arith/kinds		diff \| blob \| history
src/theory/arith/normal_form.h		diff \| blob \| history
src/theory/arith/options		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/arith/theory_arith_type_rules.h		diff \| blob \| history
src/util/Makefile.am		diff \| blob \| history
test/regress/regress0/arith/Makefile.am		diff \| blob \| history
test/regress/regress0/arith/div.09.smt2		diff \| blob \| history
test/regress/regress0/arith/mult.02.smt2		diff \| blob \| history