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

Age	Commit message (Collapse)	Author
2012-12-01	remove instantiator framework	Morgan Deters
	(this commit was certified error- and warning-free by the test-and-commit script.)
2012-08-03	fix uses of getMetaKind() from outside the expr package. (they now use ↵	Morgan Deters
	isConst() and isVar() as appropriate) also some base infrastructure for the new ::isConst().
2012-07-14	Type enumerator infrastructure and uninterpreted constant support. No ↵	Morgan Deters
	support yet for enumerating arrays, or for enumerating non-trivial datatypes.
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.