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

Age	Commit message (Collapse)	Author
2017-03-02	Minor cleanup and reorganization related to last commit.	ajreynol

2017-03-02	Eliminate Boolean term conversion. Generalizes removeITE pass to remove ↵	ajreynol
	Boolean terms, treats distinguished BOOLEAN_TERM_VARIABLE kind as theory literal. Fixes bugs 597, 604, 651, 652, 691, 694. Add regressions.
2016-10-31	Minor refactoring in preparation for datatypes node cycle breaking.	ajreynol

2016-04-20	update from the master	PaulMeng

2016-02-15	Eliminate most of the internal representation infrastructure for tuples and ↵	ajreynol
	records, replace with datatypes throughout, update cvc printer for tuples/records. Minor changes to API for records and tuples.
2016-02-10	Fix model postprocessor for tuples, add regression.	ajreynol

2015-12-15	Breaking the include cycle between Record and Expr.	Tim King

2015-09-04	Fix bugs 605 and 667.	ajreynol

2014-11-07	Fix missing case in Boolean terms rewriting. (Resolves bug #596.)	Morgan Deters

2014-11-07	Corrected fix for missing case in model postprocessor (resolves bug #595).	Morgan Deters

2014-11-07	Revert "Fix missing case in model postprocessor (resolves bug #595)."	Morgan Deters
	This reverts commit 61042cf551b19d06673be2b069bacc7cb1cd775a.
2014-11-07	Fix missing case in model postprocessor (resolves bug #595).	Morgan Deters

2014-10-06	Fix a bug in tuple-record handling. Thanks to Saumya Debray for the report.	Morgan Deters

2014-07-01	Update copyrights.	Morgan Deters

2013-12-05	Update copyrights, add missing file-level documentation; fix perms.	Morgan Deters

2013-12-05	Fix Boolean terms w.r.t. parametric datatypes (e.g., (Pair Bool Bool) now ↵	Morgan Deters
	works).
2013-11-10	Flatten libcvc4 build structure; remove some #include interdependences	Morgan Deters

2013-10-09	More improvements to datatypes, eager selector collapsing, improved collect ↵	Andrew Reynolds
	model info. Also fix bug in model post-processor.
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-03-22	Support for Boolean term conversion in datatypes.	Morgan Deters

2012-12-01	Some fixes for boolean arrays	Morgan Deters
	also a regression for bug 411 (this commit was certified error- and warning-free by the test-and-commit script.)
2012-11-27	Functions and predicates over Boolean now work with --check-models and ↵	Morgan Deters
	output correct models for such functions (though they are somewhat ugly at present). There's still a problem with model extraction, but it's not Boolean terms' fault. Sometimes checkModel() can report that the model is just fine, but if a user extracts values with getValue(), they find problems with the model (i.e., it doesn't satisfy some assertions). This appears to be due to an asymmetry between how checkModel() works and how Model::getValue() works. I'll open a bugzilla report to discuss this after thinking some more on it. (this commit was certified error- and warning-free by the test-and-commit script.)
2012-11-27	Tuples and records merge. Resolves bug 270.	Morgan Deters
	Also some fixes to parametric datatypes I found, and fixes for a handful of bugs, including some observed with --check-models --incremental on together. (this commit was certified error- and warning-free by the test-and-commit script.)