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

Age	Commit message (Collapse)	Author
2013-01-10	minor bug fixes	Liana Hadarean

2013-01-10	slicer bug fixing	Liana Hadarean

2012-12-13	more slicer bug fixes	lianah

2012-12-11	fixed some slicer bugs; set up bv theory to run bit-blaster to check for ↵	Liana Hadarean
	correctness
2012-12-10	ported my bv-core branch from svn to git	Liana Hadarean

2012-12-06	Fix to portfolio builds	Morgan Deters

2012-12-06	Fix performance issue in a DFS search (bug 474)	Kshitij Bansal

2012-12-06	* tuple and record support in compatibility library	Morgan Deters
	(this commit was certified error- and warning-free by the test-and-commit script.)
2012-12-06	* some build fixes; thanks; thanks to Kunal Ganeshpure for noting these issues	Morgan Deters
	* build bugfix for win32 * also fix a bug re: tuples and records in the datatypes rewriter These fixes are for both trunk and 1.0.x branches.
2012-12-05	Improved garbage collection for TheoryArith. The merges all of the code ↵	Tim King
	over from branches/arithmetic/converge except for the new code for simplex.
2012-12-05	Cleanup of arithmetic, and some new utility functions for the coming ↵	Tim King
	fcsimplex code.
2012-12-05	This commit merges in CDTrailHashMap and CDInsertHashMap. CDHashSet now uses ↵	Tim King
	CDInsertHashMap. CDHashSet<TNode> have been changed to CDHashSet<Node>. Switching CnfStream to use CDInsertSet. Switches a few CDHashMaps in arithmetic to use CDTrailHashMap. Documentation changes to CDHashMap.
2012-12-04	* Add support for --decision=justification + incremental (bug 437)	Kshitij Bansal
	- Fix a destruction order issue this triggered in DE (this commit was certified error- and warning-free by the test-and-commit script.)
2012-12-03	Fix for fuzzer-found model bug	Clark Barrett

2012-12-01	fix to TNode assertion (which is too strict, given lax ordering requirements ↵	Morgan Deters
	on static data initialization)---this should fix debug-staticbinary Mac builds, maybe others
2012-12-01	Throw a logic exception if user makes an assertion using a STORE_ALL	Clark Barrett

2012-12-01	remove instantiator framework	Morgan Deters
	(this commit was certified error- and warning-free by the test-and-commit script.)
2012-12-01	Fix the way abstract values are typed; fixes some compliance issues.	Morgan Deters
	Also support array-store-all for Boolean terms (related to abstract values, since that's the only way for the user to include an array-store-all in an assertion). (this commit was certified error- and warning-free by the test-and-commit script.)
2012-12-01	fix memory corruption issue in debug builds that led to unhelpful output	Morgan Deters

2012-12-01	remove an obsolete (and incorrect) assertion in boolean-terms; also add ↵	Morgan Deters
	failing regression for bug 472
2012-12-01	drastic simplification of quantifiers code regarding equality queries, ↵	Andrew Reynolds
	instantiation strategies moved from instantiators to central instantiation engine, removed instantiator objects, simplified rewrite rules candidate generator to use central equality engine, efficient e-matching now uses central equality engine
2012-12-01	Fix for a CLN related bug on 32 bit systems. Integer((1<<29)+1) and ↵	Tim King
	Integer((long int)((1<<29)+1)) gave different values. This was confirmed on vm-int1.cims.nyu.edu. See http://www.ginac.de/CLN/cln_3.html#SEC15 for more details. rational_white and integer_white have tests covering this.
2012-12-01	Some fixes for boolean arrays	Morgan Deters
	also a regression for bug 411 (this commit was certified error- and warning-free by the test-and-commit script.)
2012-12-01	fix #line annotation warning	Morgan Deters

2012-12-01	another part of last commit	Morgan Deters

2012-12-01	definition-expansion fixed for get-model, resolves bug 411	Morgan Deters

2012-12-01	Adding SmtEngine::setLogic(const char* logic) so that ↵	Tim King
	smt.setLogic("QF_LRA"); works.
2012-11-30	Changing the documentation of ARR_TABLE_FUN to say (internal symbol).	Tim King

2012-11-30	Fix assertion in smt_engine's getValue	Clark Barrett
	Minor changes to RELASE-NOTES
2012-11-30	Updating the combination.cpp example.	Tim King

2012-11-30	renaming --smtlib to --smtlib-strict; removing --smtlib2 option	Morgan Deters

2012-11-30	internal variables (skolems) aren't printed as part of the model	Morgan Deters
	(this commit was certified error- and warning-free by the test-and-commit script.)
2012-11-30	change detection/handling of output language more reasonably; fixes a ↵	Morgan Deters
	nagging bug Tim found in API examples (this commit was certified error- and warning-free by the test-and-commit script.)
2012-11-30	quantifiers now uses master equality engine, preparation work to cleanup code	Andrew Reynolds

2012-11-30	parametric datatypes fix related to non-ascribed type constructors ↵	Andrew Reynolds
	introduced by decision procedure
2012-11-30	Changes to SExpr to accept autoconversion from bool and const char*. Adding ↵	Tim King
	an example for combination.
2012-11-30	Adding smtname level options for tlimit, rlimit, etc. Fix to the internal ↵	Tim King
	documentation in base_options.
2012-11-30	Partial fix for bug 435; still needs some effort.	Morgan Deters
	(this commit was certified error- and warning-free by the test-and-commit script.)
2012-11-30	fix the syntax of assert-rewrite/-propagation/-reduction by putting the ↵	François Bobot
	pattern first just after the bindings Do it before the release in order to not break user files later
2012-11-29	reliable benchmark corresponding to bug468	Kshitij Bansal

2012-11-29	require type ascriptions for parametric datatype constructors (making them ↵	Andrew Reynolds
	canonical), this fixes the followup issue of bug 438
2012-11-29	fixes bug 438, incorporate subtypes into type unification when typechecking ↵	Andrew Reynolds
	parameterized datatypes
2012-11-29	fix for andy: boolean terms stuff really shouldn't look at datatypes at all ↵	Morgan Deters
	in this release
2012-11-29	minor documentation fix	Morgan Deters

2012-11-29	Fix for nasty corner case found by fuzzer...	Clark Barrett

2012-11-29	Hack to support global variables for CVC language extended to export mechanism.	Kshitij Bansal
	- Adds GlobalVarAttr node attribute (this commit was certified error- and warning-free by the test-and-commit script.)
2012-11-29	Fixing function models with Boolean terms. Also, LAMBDA's should not be const.	Clark Barrett

2012-11-28	fix a potential race (have failed to reproduce)	Kshitij Bansal

2012-11-28	Fix for getValue. Now it can handle lambda applications	Clark Barrett

2012-11-28	Attempted "quick-fix" for QF_UF performance regression since Boolean terms ↵	Morgan Deters
	added. Sharing is turned on only when Boolean terms are detected during preprocessing. QF_UF problems (and others) that don't use any Boolean terms won't have BV turned on. (this commit was certified error- and warning-free by the test-and-commit script.)