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	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.)
2012-11-28	treat all get commands like getValue (send only to lastWinner)	Kshitij Bansal

2012-11-28	Bug fix:	Morgan Deters
	* Fix creation of bound variables in CVC native language parser * This corrects a problem with misleading model output (this commit was certified error- and warning-free by the test-and-commit script.)
2012-11-28	fix: correct misleading comment in dump output	Morgan Deters

2012-11-27	Functions and predicates over Boolean now work with --check-models and ↵	Morgan Deters
	output correct models for such functions (though they are somewhat ugly at present). There's still a problem with model extraction, but it's not Boolean terms' fault. Sometimes checkModel() can report that the model is just fine, but if a user extracts values with getValue(), they find problems with the model (i.e., it doesn't satisfy some assertions). This appears to be due to an asymmetry between how checkModel() works and how Model::getValue() works. I'll open a bugzilla report to discuss this after thinking some more on it. (this commit was certified error- and warning-free by the test-and-commit script.)
2012-11-27	fix in CommandSequence invoke : maintain success/failure. Fixes bug 465.	Kshitij Bansal
	(this commit was certified error- and warning-free by the test-and-commit script.)
2012-11-27	more mac fixes	Morgan Deters

2012-11-27	fix for some Mac builds	Morgan Deters

2012-11-27	Simplify --help=decision with only currently supported options	Kshitij Bansal
	Add notice/warning when using incremental-mode + decision (it was already disabled) Some other minor cleanup (this commit was certified error- and warning-free by the test-and-commit script.)
2012-11-27	do not turn on BV for QF_SAT	Morgan Deters
	(this commit was certified error- and warning-free by the test-and-commit script.)
2012-11-27	First chunk of boolean-terms support.	Morgan Deters
	Passes simple tests and doesn't break existing functionality. Still need some work merged in for models. This version enables BV except for pure arithmetic (since we might otherwise need Boolean term support, which uses BV). Tonight's nightly regression run should tell us if/how that hurts performance. (this commit was certified error- and warning-free by the test-and-commit script.)