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

Age	Commit message (Collapse)	Author
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	distribute the find_public_interface.sh script	Morgan Deters

2012-12-03	version numbering	Morgan Deters

2012-12-03	Fix for fuzzer-found model bug	Clark Barrett

2012-12-01	Cutting release 1.0.1.0	Morgan Deters

2012-12-01	fix cut-release sanity checks	Morgan Deters

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	fix java system test dependences	Morgan Deters

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	updated examples	Morgan Deters

2012-12-01	added a new example for the combination of bit-vectors and arrays (includes ↵	Liana Hadarean
	model generation) and set the logic for the bitvector example
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	Polishing API examples.	Tim King

2012-12-01	Adding SmtEngine::setLogic(const char* logic) so that ↵	Tim King
	smt.setLogic("QF_LRA"); works.
2012-11-30	Fixes for stricter compilers Andy brought to my attention.	Tim King

2012-11-30	Changing the documentation of ARR_TABLE_FUN to say (internal symbol).	Tim King

2012-11-30	all API examples now have java versions too; bitvectors gets built; also ↵	Morgan Deters
	updated old-style copyrights in the examples
2012-11-30	incorporating some comments from Clark	Morgan Deters

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	Committing tests to potentially discover an obscure CLN library issue on 32 ↵	Tim King
	bit platforms. The issue is discussed here: http://www.ginac.de/CLN/cln_3.html#SEC15.
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	added a simple API example example showing how to use the bit-vector theory.	Liana Hadarean

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	Add some regressions for bug 438.	Morgan Deters
	(this commit was certified error- and warning-free by the test-and-commit script.)
2012-11-30	fix rewrite-rules syntax in regression	Morgan Deters

2012-11-30	minor fix to release script	Morgan Deters

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	Fix for hidden symbols in library on Mac. It's a strange issue to do with	Morgan Deters
	explicit template instantiation rules, -fvisibility=hidden, and the way that Apple distributes libstdc++. (this commit was certified error- and warning-free by the test-and-commit script.)
2012-11-29	fixes bug 438, incorporate subtypes into type unification when typechecking ↵	Andrew Reynolds
	parameterized datatypes