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

projects / cvc5.git / commit

summary | shortlog | log | commit | commitdiff | tree
(parent: 7bd874b) | patch

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Thu, 16 Nov 2017 20:09:30 +0000 (14:09 -0600)
committer	GitHub <noreply@github.com>
	Thu, 16 Nov 2017 20:09:30 +0000 (14:09 -0600)
commit	6c6f4e23aea405a812b1c6a3dd4d80696eb34741
tree	acdb79a293d6f1e9034913dc51f45ad75d892be1	tree
parent	7bd874b098f210b53f5b608bc159d1d90c8794b8	commit \| diff

(Refactor) Arithmetic monomial sum (#1381)

* Add arithmetic monomial sum utility.

* Clang format

* Fix

* Address review.

* Fix missed comment.

* Format

* Fix

14 files changed:

src/Makefile.am		diff \| blob \| history
src/smt/smt_engine.cpp		diff \| blob \| history
src/theory/arith/arith_msum.cpp	[new file with mode: 0644]	blob
src/theory/arith/arith_msum.h	[new file with mode: 0644]	blob
src/theory/quantifiers/bounded_integers.cpp		diff \| blob \| history
src/theory/quantifiers/ce_guided_single_inv.cpp		diff \| blob \| history
src/theory/quantifiers/ce_guided_single_inv_sol.cpp		diff \| blob \| history
src/theory/quantifiers/equality_infer.cpp		diff \| blob \| history
src/theory/quantifiers/extended_rewrite.cpp		diff \| blob \| history
src/theory/quantifiers/quantifiers_rewriter.cpp		diff \| blob \| history
src/theory/quantifiers/relevant_domain.cpp		diff \| blob \| history
src/theory/quantifiers/relevant_domain.h		diff \| blob \| history
src/theory/quantifiers/term_database_sygus.cpp		diff \| blob \| history
src/theory/quantifiers/term_util.cpp		diff \| blob \| history