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

Age	Commit message (Collapse)	Author
2011-05-23	fixes for "make dist" and "make doc", minor cleanups	Morgan Deters

2011-05-05	Merge from nonclausal-simplification-v2 branch:	Morgan Deters
	* Preprocessing-time, non-clausal, Boolean simplification round to support "quasi-non-linear rewrites" as discussed at last few meetings. * --simplification=none is the default for now, but we'll probably change that to --simplification=incremental. --simplification=batch is also a possibility. See --simplification=help for details. * RecursionBreaker<T> now uses a hash set for the seen trail. * Fixes to TLS stuff to support that. * Fixes to theory and SmtEngine documentation. * Fixes to stream indentation. * Other miscellaneous stuff.
2011-04-25	Monday tasks:	Morgan Deters
	* new "well-foundedness" type property (like cardinality) specified in Theory kinds files; specifies well-foundedness and a ground term * well-foundedness / finite checks in Datatypes now superseded by type system isFinite(), isWellFounded(), mkGroundTerm(). * new "RecursionBreaker" template class, a convenient class that keeps a "seen" trail without you having to pass it around (which is difficult in cases of mutual recursion) of the idea of passing around a "seen" trail