cvc5.git - CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems.

Age	Commit message (Collapse)	Author
2015-04-21	Fix file permissions	Clark Barrett

2014-04-10	Add support for cardinality constraints logic UFC. Add regressions in fmf/. ↵	Andrew Reynolds
	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.
2014-03-12	Some standardization of regression Makefiles that got out of sync. Fixes ↵	Morgan Deters
	cases of nonterminating rewrite-rules regressions.
2014-03-11	Initial refactor of rewrite rules, make theory_rewriterules empty theory. ↵	Andrew Reynolds
	Push kinds to quantifiers/kinds, rewrite rewrite rules in rewriter. Fix rewrite rule attribute, refactor QCF, instantiation engine does not register rewrite rules, minor clean up. QCF is now functional backend to rewrite rules. Support boolean variables in QCF. Change check-model to ignore rewrite rules. Incorporate some fixes from master. Move rewrite of rewrite rules from rewriter to preprocessor, attribute becomes pattern. Minor fixes to QCF/rewrite engine, removes RE on last call approach. Add option for one inst per round in RE. Merging rewrite rules into master, check-model current fails on 3 FMF regressions. Fix check-model issue, a line of code was omitted during merge.
2014-03-07	Remove --ite-remove-quant; support pulling ground ITEs out of quantifier ↵	Morgan Deters
	bodies; fix bug 551, improper ITE removal under quantifiers.
2014-03-05	Revert "fix naming conflicts in benchmarks"	Kshitij Bansal
	This reverts commit 4cac1b63f76a0a973a015ea6f8e21ad31d84d971.
2014-02-21	add new theory (sets)	Kshitij Bansal
	Specification (smt2) -- as per this commit, subject to change - Parameterized sort Set, e.g. (Set Int) - Empty set constant (typed), use with "as" to specify the type, e.g. (as emptyset (Set Int)) - Create a singleton set (setenum X (Set X)) : creates singleton set - Functions/operators (union (Set X) (Set X) (Set X)) (intersection (Set X) (Set X) (Set X)) (setminus (Set X) (Set X) (Set X)) - Predicates (in X (Set X) Bool) : membership (subseteq (Set X) (Set X) Bool) : set containment
2013-12-23	Proof-checking code; fixups of segfaults and missing functionality in proof ↵	Morgan Deters
	generation; fix bug 285. * segfaults/assert-fails in proof-generation fixed, including bug 285 * added --check-proofs to automatically check proofs, like --check-models (but only for UF/SAT at present) * proof generation now works in portfolio (but not --check-proofs, since LFSC code uses globals) * proofs are not yet supported in incremental mode * added --dump-proofs to dump out proofs, like --dump-models * run_regression script now runs with --check-proofs where appropriate * options scripts now support :link-smt for SMT options, like :link for command-line
2013-09-18	Support a personal build configuration and make rules.	Morgan Deters

2013-01-28	some fixes for win32, including ability to "make check" win32 builds via wine	Morgan Deters

2012-11-30	fix the syntax of assert-rewrite/-propagation/-reduction by putting the ↵	François Bobot
	pattern first just after the bindings Do it before the release in order to not break user files later
2012-11-23	Example of rewrite rules use that comes from an harness test	François Bobot

2012-10-09	fix beta reduction in both preRewrite() and postRewrite(), related to bug ↵	Morgan Deters
	417. oops. also fix spelling on "rewritting" test
2012-08-28	fix regression tests for automake 1.11 and automake 1.12---both versions ↵	Morgan Deters
	should work now
2012-07-27	Merge quantifiers2-trunk:	François Bobot
	- new syntax for rewrite rules - better rewrite rules theory - remove the rewriting with rewrite rules during ppRewrite temporarily - theory can define their own candidate generator - define a general candidate generator (inefficient ask to every theory) - split inst_match between the pattern matching used for quantifiers (inst_match.) and the one used for rewrite rules (rr_inst_match.): - the pattern matching is less exhaustive for quantifiers, - the one for rewrite rules can use efficient-e-matching.
2012-06-11	Merge from quantifiers2-trunkmerge branch.	Morgan Deters
	Adds TheoryQuantifiers and TheoryRewriteRules, QuantifiersEngine, and other infrastructure. Adds theory instantiators to many theories. Adds the UF strong solver.