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

Age	Commit message (Collapse)	Author
2013-04-16	generalize to handle and	Kshitij Bansal

2013-04-16	flatten or nodes	Kshitij Bansal

2013-04-05	Fix unit test (compile error) for new SatSolver interface	Morgan Deters

2013-04-03	Some final minor changes before cutting 1.1.	Morgan Deters
	* update documentation * update the cut-release script * spelling/wording updates * add a (previously-failing) fuzzer regression
2013-04-02	Regenerated copyrights: canonicalized names, no emails	Morgan Deters

2013-04-01	update copyrights	Morgan Deters

2013-04-01	Fixes for two bugs:	Morgan Deters
	* one that Tim found in model generation for records containing Booleans * another that the fuzzer found in quantifiers + check-models Test cases enabled/added for both.
2013-04-01	Adding tests for the previous commit.	Tim King

2013-04-01	Merging some cleanup work:	Morgan Deters
	* Comment cleanup * Spelling fixes * Fix warnings * Documentation updates * References in docs to cryptominisat removed * Unneeded scope resolutions removed * Old, unused regression removed
2013-04-01	Fix for iff terms over equalities between the same term and differing constants.	Tim King

2013-04-01	Fix bug 491 and related issues with checkModel() and quantifiers. Enabling ↵	Morgan Deters
	previously-failing testcase.
2013-04-01	fixed TheoryBool rewriter bug	lianah

2013-03-26	added model generation for bv subtheories and bv-inequality solver option	lianah

2013-03-23	non-incremental inequality solver seems to be bug-free (i.e. passes fuzzing)	lianah

2013-03-22	Support for Boolean term conversion in datatypes.	Morgan Deters

2013-03-21	Merge branch 'master' into bv-core	lianah

2013-03-21	Some model and printing fixes for defined functions in input.	Morgan Deters

2013-03-21	added regression test for constant eval	lianah

2013-03-21	Merge branch 'master' into bv-core	lianah

2013-03-20	added more tests	lianah

2013-03-20	generalized bv inequality reasoning to handle both strict and non-strict ↵	lianah
	inequalities
2013-03-20	Fix to bug 497: make justification heuristic's ITE cache context-dependent.	Morgan Deters

2013-03-20	Interactive mode support for multiline input	Morgan Deters

2013-03-20	Properly \|quote\| symbols in SMT-LIBv2 output.	Morgan Deters

2013-03-20	one more ineq regression	Liana Hadarean

2013-03-19	fixed reversed concat in core theory	Liana Hadarean

2013-03-19	merged master with dejan's constant evaluating equality engine	Liana Hadarean

2013-03-19	inequality reasoning works on small examples added to regressions (not ↵	Liana Hadarean
	incremental); currently disabled though
2013-03-19	Fixes for miplib-trick application (and a new testcase)	Morgan Deters

2013-03-16	started work on the inequality bv subtheory	lianah

2013-03-14	Merge branch '1.0.x'	Morgan Deters

2013-03-14	fix to build system: #include the proper file when they are in both builds ↵	Morgan Deters
	and src
2013-02-26	Merge branch '1.0.x'	lianah

2013-02-26	fix for bv crash in incremental mode; this is a temporary fix for bug 493	lianah

2013-02-16	Some cleanup and copyright updating	Morgan Deters
	* update some copyrights for 2013 * cleaned up some comments/ifdefs, indentation * some spelling corrections * add some missing makefiles
2013-02-07	Merge branch '1.0.x'	Morgan Deters
	Conflicts: src/theory/quantifiers/theory_quantifiers.cpp
2013-02-07	Significant work on bug #491 (not yet closed).	Morgan Deters

2013-02-07	More complete fix for bug 484 (includes fixes for records and tuples).	Morgan Deters

2013-02-05	Fix to miplib trick to make it less "cautious" and apply in more cases	Morgan Deters

2013-02-04	Merge branch '1.0.x'	Morgan Deters

2013-02-04	Fix NodeBuilder bug which could attempt to allocate beyond hard limit	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-02-03	Some cleanup of miplib regressions and options	Morgan Deters

2013-02-03	Merge from mdeters/miplib branch (commit ↵	Morgan Deters
	'ce7c485182902ae43871057185095f71f74a8a58')
2013-02-03	new miplib pass, works for 1 or 2 vars	Morgan Deters

2013-02-01	Merge branch '1.0.x'	Morgan Deters

2013-02-01	Fix a tuple attribute bug that was causing model-generation problems for tuples	Morgan Deters

2013-01-29	currently disabling bug486 regression. we need to discuss ↵	Andrew Reynolds
	getValue/collectModelInfo for quantifiers more.
2013-01-28	Fix the regression test for bug 486, and enable it	Morgan Deters
	(cherry-picked from master 23b4fd82d1ed326cd57e9bc57ef9fab98b0b1c87)
2013-01-28	Fix the regression test for bug 486, and enable it	Morgan Deters