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

Age	Commit message (Collapse)	Author
2013-05-20	Fix error reporting on use of (nonlinear) div,mod,/ symbols	Morgan Deters

2013-05-20	Don't allow get-model & co after a user push/pop	Morgan Deters
	This makes us more strictly adhere to the spec, but it's useful anyway: previously we would support a get-model until the problem was explicitly changed with e.g. a new assertion. That meant you could check-sat, then pop, then get-model, but you'd only get the part of the model still in scope. This is strange, and would likely lead to problems, so it's now disabled. Thanks to David Cok for inquiring about this.
2013-05-20	Fix for equality-chaining of Booleans in SMT-LIBv2.	Morgan Deters
	Thanks to David Cok for reporting this.
2013-05-20	Better error on invalid logic strings.	Morgan Deters
	Thanks to David Cok for reporting this issue. Conflicts: library_versions
2013-05-20	Fix to empty response to (get-assignment).	Morgan Deters
	Thanks to David Cok for reporting this issue.
2013-05-08	final updates for smt-eval script	Morgan Deters

2013-05-06	Disables justification stop only for LRA if the problem contains no ites. ↵	Tim King
	This is a bandaid for constraints-tempo-width family of benchmarks.
2013-05-02	Merge branch 'master' of https://github.com/CVC4/CVC4	lianah

2013-05-01	Fix to dumping re: boolean terms, datatypes	Morgan Deters

2013-05-01	Fix to boolean-terms; resolves bug #507	Morgan Deters

2013-05-01	added back BitwiseEq rule	lianah

2013-04-30	innd examples are solved fast, but destruction assertion fail	lianah

2013-04-30	uncompiling new bv to bool lifting	lianah

2013-04-30	finished implementing bv to bool lifting and added --bv-to-bool option	lianah

2013-04-23	Theory "alternates" support	Morgan Deters
	* This is a feature that Dejan and I want for the upcoming tutorial. It allows rapid prototyping of new decision procedure implementations (which we may choose to demonstrate), and a new --use-theory command-line option to select from different available implementations. It has no affect on the current set of theories, as no "alternates" are defined. * Also update the new-theory script, which was broken and incomplete.
2013-04-18	making sure sat context is zero when user context is popped to 0 in ↵	lianah
	SmtEngine destructor
2013-04-18	fixing destruction order in SmtEngine	lianah

2013-04-03	* changing the bitblast-eager to bitblast on pre-register	Dejan Jovanović
	* the newVar interface of the sat solver now changed to include (isTheoryLiteral, preRegister, canEliminate) * when bitblast-eager all bv atoms are (theory=false, prereg = true, canelim = true) * bitblast-eager implies decision=internal
2013-04-02	Regenerated copyrights: canonicalized names, no emails	Morgan Deters

2013-04-01	update copyrights	Morgan Deters

2013-04-01	Fix regression error by turning off model-based solver when models are on	Clark Barrett
	(ironic, yes, but model-based solver doesn't yet produce models)
2013-04-01	Turning on model based array solver for QF_AX	Clark Barrett

2013-04-01	Made eager lemmas an option, enabled for QF_AX	Clark Barrett

2013-04-01	Disabling eager array index splitting for QF_AX	Clark Barrett

2013-04-01	Fixes for two bugs:	Morgan Deters
	* one that Tim found in model generation for records containing Booleans * another that the fuzzer found in quantifiers + check-models Test cases enabled/added for both.
2013-04-01	Merging some cleanup work:	Morgan Deters
	* Comment cleanup * Spelling fixes * Fix warnings * Documentation updates * References in docs to cryptominisat removed * Unneeded scope resolutions removed * Old, unused regression removed
2013-04-01	Fix bug 491 and related issues with checkModel() and quantifiers. Enabling ↵	Morgan Deters
	previously-failing testcase.
2013-03-30	Disabling eager array index splitting for QF_AUFLIA	Clark Barrett
	Minor changes to model-based array solver
2013-03-29	make Boolean term conversion partially non-recursive (resolves bug 501)	Morgan Deters

2013-03-26	Fixes for warnings from clang++, from -std=gnu++0x, from swig, and from javac	Morgan Deters

2013-03-22	Support for Boolean term conversion in datatypes.	Morgan Deters

2013-03-21	Some model and printing fixes for defined functions in input.	Morgan Deters

2013-03-21	Fix for SmtEngine::expandDefinitions()---improper TypeCheckingException	Morgan Deters

2013-03-20	Some statistics for narrowing down incrementality issues (push/pop vs solve ↵	Morgan Deters
	timing)
2013-03-19	Fixes for miplib-trick application (and a new testcase)	Morgan Deters

2013-03-15	Boolean terms rewriting for quantified variables of type Bool, when ↵	Morgan Deters
	quantifier body uses them in term context
2013-03-14	Merge branch '1.0.x'	Morgan Deters

2013-03-14	fix to build system: #include the proper file when they are in both builds ↵	Morgan Deters
	and src
2013-03-11	ite removal option for quantifiers --ite-remove-quant, e-matching for ↵	Andrew Reynolds
	boolean terms, improvement for pre skolemization
2013-03-05	Merge branch '1.0.x'	Morgan Deters
	Conflicts: src/smt/smt_engine.cpp
2013-03-05	Bugfix for SmtEngine: proper unsubscribing for NodeManager events	Morgan Deters

2013-03-01	Merge branch '1.0.x'	Morgan Deters

2013-02-26	Fix for quantifiers containing Boolean terms.	Morgan Deters

2013-02-24	added option --model-u-dt-enum for outputting uninterpreted sorts as ↵	Andrew Reynolds
	datatype enumerations + minor update to array rewriter to improve output for this option, minor refactoring of representative selection for quantifier instantiation, initial draft of disequality propagation option --uf-ss-deq-prop, other refactoring of uf strong solver, fixed bug 496, improvement for fmf enumeration of finite built-in sorts
2013-02-20	Some exception specification fixes in SmtEngine/Command infrastructure	Morgan Deters

2013-02-16	Some cleanup and copyright updating	Morgan Deters
	* update some copyrights for 2013 * cleaned up some comments/ifdefs, indentation * some spelling corrections * add some missing makefiles
2013-02-12	Fix a preprocessing performance issue.	Morgan Deters

2013-02-07	Merge branch '1.0.x'	Morgan Deters
	Conflicts: src/theory/quantifiers/theory_quantifiers.cpp
2013-02-07	Significant work on bug #491 (not yet closed).	Morgan Deters

2013-02-05	Fix to miplib trick to make it less "cautious" and apply in more cases	Morgan Deters