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-04-20	update from the master	PaulMeng

2015-10-16	Throw error for recursively defined types involving Boolean.	ajreynol

2014-07-01	Update copyrights.	Morgan Deters

2014-04-10	Boolean terms conversion fix for datatypes, fixes a problem Andy discovered ↵	Morgan Deters
	on his branch.
2014-04-03	Some incremental bugs for Boolean terms, fixed. Thanks to Pantazis ↵	Morgan Deters
	Deligiannis and Jeroen Ketema for discovering this issue.
2013-12-16	Fix for bug 544.	Morgan Deters

2013-05-01	Fix to boolean-terms; resolves bug #507	Morgan Deters

2013-04-02	Regenerated copyrights: canonicalized names, no emails	Morgan Deters

2013-04-01	update copyrights	Morgan Deters

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

2013-03-15	Boolean terms rewriting for quantified variables of type Bool, when ↵	Morgan Deters
	quantifier body uses them in term context
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	First chunk of boolean-terms support.	Morgan Deters
	Passes simple tests and doesn't break existing functionality. Still need some work merged in for models. This version enables BV except for pure arithmetic (since we might otherwise need Boolean term support, which uses BV). Tonight's nightly regression run should tell us if/how that hurts performance. (this commit was certified error- and warning-free by the test-and-commit script.)