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

Age	Commit message (Collapse)	Author
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
2014-02-10	Fix build (some nonexistent files listed in Makefile)	Morgan Deters

2014-02-09	More complete guess instantiation strategy, cvc4 now typically times out ↵	Andrew Reynolds
	instead of answering unknown for benchmarks with quantifiers. Modified regressions accordingly. Minor fix for QCF regarding variable ordering. Improved relevant domain computation. Minor optimization for --mbqi=fmc
2014-01-26	More optimization of QCF. Fixed InstMatchTrie for caching instantiations. ↵	Andrew Reynolds
	Use non-context dependent cache for instantiations when not incremental. Instantiate from relevant domain when no other instantiations apply. Minor cleanup of relevance for triggers.
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-11-11	Change exit status to be more consistent with other command-line tools: 0 ↵	Morgan Deters
	success, nonzero error
2013-09-18	Support a personal build configuration and make rules.	Morgan Deters

2013-09-13	Move some regress benchmarks around that took too long, other test cleanup.	Morgan Deters

2013-02-04	Model no longer adds subterms of quantifiers to equality engine, this fixed ↵	Andrew Reynolds
	bug 492 and resolves previous issue for bug 486.\n Multiple improvements for E-matching: do not choose multi-triggers if single triggers exist, only create multi-triggers that contain all variables, consider multiple terms per equivalence class but only add one instantiation per round per (trigger,term) pair.\nImprovements for strong solver: make use of sort inference information when choosing splits, check for cliques eagerly when disequalities are asserted.
2013-01-28	some fixes for win32, including ability to "make check" win32 builds via wine	Morgan Deters

2012-09-18	SMT-LIBv2 compliance regarding outputting "unknown".	Morgan Deters
	Thanks to Peter Collingbourne for the report, and the patch! (this commit was certified error- and warning-free by the test-and-commit script.)
2012-08-31	merge from fmf-devel branch. more updates to models: now with ↵	Andrew Reynolds
	collectModelInfo with fullModel argument, most theory-specific implementation out of the model class, model printer relegated to printer classes. Also updates to finite mode finding, modifications to datatypes making them compatible with theory combination, support for theory-specific handling of user attributes, refactoring of uf models
2012-08-28	fix regression tests for automake 1.11 and automake 1.12---both versions ↵	Morgan Deters
	should work now
2012-08-27	* Reversing commit r4258 (which disabled failing regressions). Fixed the ↵	Morgan Deters
	problem so they're no longer failing (in the quantifiers rewriter). Resolves bug #381. * Added LAMBDA kind and type rule, and Node::isClosure(). (this commit was certified error- and warning-free by the test-and-commit script.)
2012-08-26	disabling failing regressions	Kshitij Bansal

2012-07-27	Minor cleanup after today's commits:	Morgan Deters
	* change some uses of "std::cout" to "Message()" * change some files to use Unix newlines instead of DOS newlines * fix compiler warning
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-17	fixing makefile error that brakes build	Dejan Jovanović

2012-06-17	Fix array bug causing incorrect answers	Clark Barrett

2012-06-11	distribute an .expect file. fixes a "make check" failure not for svn ↵	Morgan Deters
	working dirs but for distributed tarballs.
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.