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

Age	Commit message (Collapse)	Author
2011-03-03	resurrecting triple.h from r1023 (after which it was removed)	Morgan Deters

2010-10-22	removing unused functionality from util; related to bug #222	Morgan Deters

2010-10-08	* (define-fun...) now has proper type checking in non-debug builds	Morgan Deters
	(resolves bug #212) * also closed some other type checking loopholes in SmtEngine * small fixes to define-sort (resolves bug #214) * infrastructural support for printing expressions in languages other than the internal representation language using an IO manipulator, e.g.: cout << Expr::setlanguage(language::output::LANG_SMTLIB_V2) << expr; main() sets the output language for all streams to correspond to the input language * support delaying type checking in debug builds, so that one can debug the type checker itself (before it was difficult, because debug builds did all the type checking on Node creation!): new command-line flag --no-early-type-checking (only makes sense for debug builds) * disallowed copy-construction of ExprManager and NodeManager, and made other constructors explicit; previously it was easy to unintentionally create duplicate managers, with really weird results (i.e., disappearing attributes!)
2010-06-30	* theory "tree" rewriting implemented and works	Morgan Deters
	* added TheoryArith::preRewrite() to test and demonstrate the use of pre-rewriting. * array types and type checking now supported * array type checking now supported * theoryOf() dispatching properly to arrays now * theories now required to implement a (simple) identify() function that returns a string identifying them for debugging/user output purposes * added "builtin" theory to hold all built-in kinds and their type rules and rewriting (currently only exploding distinct) * fixed production build failure (regarding NodeSetDepth) * removed an errant "using namespace std" in util/bitvector.h (and made associated trivial fixes elsewhere) * fixes to make unexpected exceptions more verbose in debug builds * fixes to make multiple, cascading assertion fails simpler * minor other fixes to comments etc.