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

Age	Commit message (Collapse)	Author
2012-07-07	Various fixes to documentation---typos, some incomplete documentation fixed, ↵	Morgan Deters
	\file tags corrected, copyright added to files that had it missing, etc. I ensured that I didn't change any code with this commit, and even tested on the cluster to be doubly sure: http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=4655&reference_id=4646&p=0
2012-06-09	Dagification of output expressions.	Morgan Deters
	By default, common subexpressions are dagified if they appear > 1 time and are not constants or variables. This can be changed with --default-expr-dag=N --- N is a threshold such that if the subexpression occurs > N times, it is dagified; a setting of 0 turns off dagification entirely. If you notice strange dumping behavior (taking too long to print anything, e.g.), revert to the old behavior with --default-expr-dag=0 and let me know of the problem.
2012-06-08	minor fixes, for Mac OS	Morgan Deters

2012-06-08	threadlocal	Kshitij Bansal

2012-05-08	Merging in bvprop branch, with proper bit-vector propagation.	Liana Hadarean
	This should also fix bug 325.
2011-10-17	Sharing work	Dejan Jovanović

2011-09-15	additional stuff for sharing,	Dejan Jovanović

2011-08-27	Removing Theory::registerTerm() as discussed in the meeting. Now ↵	Dejan Jovanović
	pre-register is called on all the theory terms and the foreign-terms also. This means, if x: REAL and f:REAL, that in f(x) >= 0, arithmetic gets pre-register call with x, f(x) and f(x) >= 0, while UF gets pre-register call with x, f(x).
2011-08-24	Simplification of the preregister and register throught a NodeVisitor class. ↵	Dejan Jovanović
	The theoryOf is not all in one place, theory::theoryOf. The uninterpreted sorts belong to the builtin theory and are dispatched to the apropriate theory (QF_UF, QF_AX) through theoryOf based on the setting in the Theory class.