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

Age	Commit message (Collapse)	Author
2014-11-17	New, uniform checkTime statistic for all theories (as discussed in meeting).	Morgan Deters

2014-07-01	Update copyrights.	Morgan Deters

2014-01-22	Delay QuantifiersEngine and UF strong solver initialization until after ↵	Morgan Deters
	final options/logic are set.
2013-11-10	Flatten libcvc4 build structure; remove some #include interdependences	Morgan Deters

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

2013-04-01	update copyrights	Morgan Deters

2013-03-14	fix to build system: #include the proper file when they are in both builds ↵	Morgan Deters
	and src
2012-10-11	Standardizing copyright notice. Touches ALL sources, guys, sorry.. it's	Morgan Deters
	just the header comments at the top, though. Don't update to this rev if you don't have time for a complete rebuild, and exclude this rev if you want to see what's new across a range of commits. (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-07-12	merged fmf-devel branch, includes support for SMT2 command get-value and ↵	Andrew Reynolds
	(extended) SMT command get-model. added collectModelInfo and removed getValue from theory interface. merge also includes major updates to finite model finding module (from CASC), added fmf options, some updates to strong solver and quantifiers engine interface. The test recursion_breaker_black currently fails for me on production builds, Morgan is planning to look into this.
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.
2011-09-29	Some base infrastructure for user push/pop; a few bugfixes to user push/pop ↵	Morgan Deters
	and model gen also. I also expect this commit to fix bug #273. No performance change is expected on regressions with this commit, see http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=2871&reference_id=2863
2011-09-16	include example theory (former "UF-Tim") that's included in the dist but not ↵	Morgan Deters
	built for the library