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

Age	Commit message (Collapse)	Author
2013-12-05	Update copyrights, add missing file-level documentation; fix perms.	Morgan Deters

2013-11-27	General pre-release cleanup commit	Morgan Deters
	* Rename {model,util_model}.{h,cpp} files to match class names * Fix alreadyVisited() issue in TheoryEngine * Remove spurious Message that causes compliance issues * Update copyrights, fix public/private markings in headers * minor comment fixes * remove EXTRACT_OP as a special-case in typechecker * note about rewriters in theoryskel readme * Clean up some compiler warnings * Code typos and spacing
2012-10-04	Implemented array type enumerator, more fixes for models	Clark Barrett

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-07-27	Minor cleanup after today's commits:	Morgan Deters
	* change some uses of "std::cout" to "Message()" * change some files to use Unix newlines instead of DOS newlines * fix compiler warning
2012-07-12	merged fmf-devel branch, includes support for SMT2 command get-value and ↵	Andrew Reynolds
	(extended) SMT command get-model. added collectModelInfo and removed getValue from theory interface. merge also includes major updates to finite model finding module (from CASC), added fmf options, some updates to strong solver and quantifiers engine interface. The test recursion_breaker_black currently fails for me on production builds, Morgan is planning to look into this.