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

Age	Commit message (Collapse)	Author
2013-09-18	Support a personal build configuration and make rules.	Morgan Deters

2013-01-28	some fixes for win32, including ability to "make check" win32 builds via wine	Morgan Deters

2012-11-30	fix the syntax of assert-rewrite/-propagation/-reduction by putting the ↵	François Bobot
	pattern first just after the bindings Do it before the release in order to not break user files later
2012-11-23	Example of rewrite rules use that comes from an harness test	François Bobot

2012-10-09	fix beta reduction in both preRewrite() and postRewrite(), related to bug ↵	Morgan Deters
	417. oops. also fix spelling on "rewritting" test
2012-08-28	fix regression tests for automake 1.11 and automake 1.12---both versions ↵	Morgan Deters
	should work now
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-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.