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

author	Tim King <taking@cs.nyu.edu>
	Wed, 30 Apr 2014 21:28:00 +0000 (17:28 -0400)
committer	Morgan Deters <mdeters@cs.nyu.edu>
	Wed, 30 Apr 2014 23:07:28 +0000 (19:07 -0400)
commit	c5e4a56d4895ce29cd37bac027bb3d486d687f9d
tree	6712748188bcfa6dc4e6074e091ee9106729f058	tree
parent	221e509c0eb230aa549fe0107ba88514b6944ca2	commit \| diff

T-entailment work, and QCF (quant conflict find) work that uses it.

This commit includes work from the past month on the T-entailment check
infrastructure (due to Tim), an entailment check for arithmetic
(also Tim), and QCF work that uses T-entailment (due to Andrew Reynolds).

Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>

30 files changed:

src/Makefile.am		diff \| blob \| history
src/smt/smt_engine.cpp		diff \| blob \| history
src/theory/arith/arith_utilities.h		diff \| blob \| history
src/theory/arith/delta_rational.h		diff \| blob \| history
src/theory/arith/infer_bounds.cpp	[new file with mode: 0644]	blob
src/theory/arith/infer_bounds.h	[new file with mode: 0644]	blob
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/quantifiers/instantiation_engine.cpp		diff \| blob \| history
src/theory/quantifiers/instantiation_engine.h		diff \| blob \| history
src/theory/quantifiers/options		diff \| blob \| history
src/theory/quantifiers/quant_conflict_find.cpp		diff \| blob \| history
src/theory/quantifiers/quant_conflict_find.h		diff \| blob \| history
src/theory/quantifiers/term_database.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
src/theory/theory_engine.h		diff \| blob \| history
src/util/integer_cln_imp.cpp		diff \| blob \| history
src/util/integer_cln_imp.h		diff \| blob \| history
src/util/integer_gmp_imp.cpp		diff \| blob \| history
src/util/integer_gmp_imp.h		diff \| blob \| history
src/util/maybe.h		diff \| blob \| history
test/regress/regress0/quantifiers/Makefile.am		diff \| blob \| history
test/regress/regress0/quantifiers/array-unsat-simp3.smt2		diff \| blob \| history
test/regress/regress0/quantifiers/array-unsat-simp3.smt2.expect		diff \| blob \| history
test/regress/regress0/quantifiers/qcft-javafe.filespace.TreeWalker.006.smt2	[new file with mode: 0644]	blob
test/regress/regress0/quantifiers/qcft-smtlib3dbc51.smt2	[new file with mode: 0644]	blob

RSS Atom