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

Age	Commit message (Collapse)	Author
2013-04-01	update copyrights	Morgan Deters

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-09-19	General subscriber infrastructure for NodeManager, as discussed in the	Morgan Deters
	meeting last week. The SmtEngine now subscribes to NodeManager events, does appropriate dumping of variable declarations, and notifies the Model class. The way to create a skolem is now: nodeManager->mkSkolem("myvar_$$", TypeNode, "is a variable created by the theory of Foo") The first argument is the name of the skolem, and the (optional) "$$" is a placeholder for the node id (to get a unique name). Without a "$$", a "_$$" is automatically appended to the given name. The second argument is the type. The (optional, but recommended) third argument is a comment, used by the dump infrastructure to indicate what the variable is for / who owns it. An optional fourth argument (not shown) allows you to specify flags that control the behavior (e.g., don't do notification, and/or don't make a unique name). Look at the documentation for details on these. In particular, the above means you can't just do a mkSkolem(boolType) for example---you have to specify a name and (hopefully also, but it's optional) a comment. This leads to easier debugging than the anonymous skolems before, since we'll be able to track where the skolems came from. Much of the Model and Dump stuff, as well as some Command stuff, is cleaned up by this commit. Some remains to be cleaned up. (this commit was certified error- and warning-free by the test-and-commit script.)
2012-08-24	* disallow internal uses of mkVar() (you have to mkSkolem())	Morgan Deters
	* add support for mkBoundVar() (BOUND_VAR_LISTs in quantifiers must be bound vars)
2012-06-18	small bug fix and performance fix in ite simplifier	Clark Barrett

2012-06-12	Fixed bug causing QF_LIA/solver_cvc4/incorrect1.smt and ↵	Clark Barrett
	QF_LIA/solver_cvc4/incorrect3.smt
2012-06-07	Fixed performance issue with ite_simplifier on some QF_AUFBV benchmarks	Clark Barrett

2012-05-28	Added some BV rewrites, fixed bugs in array theory, made ite simp work with BV	Clark Barrett

2012-05-11	Added some ITE rewrites,	Clark Barrett
	Added ITE simplifier - on by default only for QF_LIA benchmarks Fixed one bug in arrays Added negate() to node.h - it returns kind == NOT ? kind[0] : kind.notNode()