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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Thu, 10 Apr 2014 15:31:47 +0000 (10:31 -0500)
committer	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Thu, 10 Apr 2014 15:33:24 +0000 (10:33 -0500)
commit	c431410d0bd4a688d5d446f906d80634424dcd53
tree	8b13a5598a0ed201744e0a44669f8ade1eac2af3	tree
parent	fccff6adcc0a69273a54110596214f7927a96033	commit \| diff

Add support for cardinality constraints logic UFC. Add regressions in fmf/. Fix datatypes E-matching bug. Change defaults : mbqi=fmc, decision heuristic stoponly=false for quantified logics, decision=justification for ALL_SUPPORTED, full-saturate-quant=false. Minor fix for fmc models. Add infrastructure to datatypes to prepare for next commit.

27 files changed:

src/parser/smt1/smt1.h		diff \| blob \| history
src/smt/smt_engine.cpp		diff \| blob \| history
src/theory/datatypes/theory_datatypes.cpp		diff \| blob \| history
src/theory/logic_info.cpp		diff \| blob \| history
src/theory/logic_info.h		diff \| blob \| history
src/theory/quantifiers/first_order_model.cpp		diff \| blob \| history
src/theory/quantifiers/modes.cpp		diff \| blob \| history
src/theory/quantifiers/modes.h		diff \| blob \| history
src/theory/quantifiers/options		diff \| blob \| history
src/theory/quantifiers/options_handlers.h		diff \| blob \| history
src/theory/quantifiers/term_database.cpp		diff \| blob \| history
src/theory/uf/theory_uf.cpp		diff \| blob \| history
src/util/datatype.cpp		diff \| blob \| history
src/util/datatype.h		diff \| blob \| history
test/regress/regress0/bug512.smt2		diff \| blob \| history
test/regress/regress0/fmf/Arrow_Order-smtlib.778341.smt		diff \| blob \| history
test/regress/regress0/fmf/Makefile.am		diff \| blob \| history
test/regress/regress0/fmf/QEpres-uf.855035.smt		diff \| blob \| history
test/regress/regress0/fmf/fc-pigeonhole19.smt2	[new file with mode: 0755]	blob
test/regress/regress0/fmf/fc-simple.smt2	[new file with mode: 0755]	blob
test/regress/regress0/fmf/fc-unsat-pent.smt2	[new file with mode: 0755]	blob
test/regress/regress0/fmf/fc-unsat-tot-2.smt2	[new file with mode: 0755]	blob
test/regress/regress0/quantifiers/bug269.smt2		diff \| blob \| history
test/regress/regress0/quantifiers/burns13.smt2		diff \| blob \| history
test/regress/regress0/rewriterules/Makefile.am		diff \| blob \| history
test/regress/regress0/rewriterules/read5.smt2	[new file with mode: 0755]	blob
test/regress/regress0/tptp/Makefile.am		diff \| blob \| history

RSS Atom