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

Age	Commit message (Collapse)	Author
2012-11-13	fixed failed bv regressions by refactoring out some rewrite rules from ↵	Liana Hadarean
	smt_engine.cpp
2012-11-13	added support for division by zero for bit-vector division operators	Liana Hadarean

2012-11-13	Relaxing too-strict assertion	Clark Barrett

2012-11-13	Fixed an array rewriting bug found by fuzzer	Clark Barrett

2012-11-13	Testcases for fixed bugs	Clark Barrett

2012-11-13	Fixed bug in array constant normalization found by fuzzer.	Clark Barrett

2012-11-12	Improved error reporting for improperly using non-linear division in linear ↵	Tim King
	arithmetic.
2012-11-12	Delta is now generated in arithmetic to keep consistent the total order of ↵	Tim King
	DeltaRational values for lowerbounds, upperbounds, assignments and disequalities. Throws LogicException when a non-linear term is asserted and the the LogicInfo isLinear() disagrees.
2012-11-12	changed BitVector::unsignedRem to match the behavior of the bit-blasted ↵	Liana Hadarean
	circuit for division by 0; temporary fix for bug440
2012-11-12	Fix for bug 444, dealing with the placing of set-logic in dumping modes.	Morgan Deters
	CVC4 now produces equivalent output when dumping the SMT1 and SMT2 attachments to that bug report. This also fixes a memory leak in the new-variable-notification mechanism. (this commit was certified error- and warning-free by the test-and-commit script.)
2012-11-12	* Fix language bindings: various issues	Morgan Deters
	remove a number of warnings in bindings generation give appropriate names for operator-overloading ** make sure Java language bindings are built with -fno-strict-aliasing, to ensure the optimizer doesn't produce bad code * Also remove BitVector::equals(), which wasn't used and was inconsistently implemented (operator==() is still there). (this commit was certified error- and warning-free by the test-and-commit script.)
2012-11-12	minor bug fixes for quantifiers, added sort inference module (not ready to ↵	Andrew Reynolds
	be used yet), added new totality lemma option for uf strong solver
2012-11-11	Fixes for the arithmetic normal form and rewriter to handle arbitrary ↵	Tim King
	constants for total functions.
2012-11-10	Beautifying integer_cln_imp.h	Tim King

2012-11-10	Fix to quantifier rewritting not being idempotent. See bug 441.	Tim King

2012-11-10	Removing rewriter call in SmtEngine::addFormula().	Tim King

2012-11-10	Fixed missing \ in uflra/Makefile.ma	Clark Barrett
	Fixed another model bug and added previously failing fuzz testcase
2012-11-10	Fix for bug 439. Delta computation now includes disequality information.	Tim King

2012-11-10	Change run-regression script to additionally run a second test with ↵	Morgan Deters
	--check-models if the benchmark is sat/invalid (or is incremental, with at least one sat/invalid result). This increases significantly the time to do a "make regress", as more tests are running. We need to run both with and without --check-models, since that option disables certain preprocessing. To turn off these extra tests during a make regress, you can set CVC4_REGRESSION_ARGS=--no-check-models. To turn off the extra test for a particular regression benchmark, you can put this in the benchmark: ; COMMAND-LINE: --no-check-models That might be necessary in e.g. nonlinear arithmetic benchmarks. (this commit was certified error- and warning-free by the test-and-commit script.)
2012-11-10	Updates to Clark's commit r4540:	Morgan Deters
	* ALL_SUPPORTED/QF_ALL_SUPPORTED don't include nonlinear * Change "Notice" to "Warning" when produce-models turned off due to non-linear (this commit was certified error- and warning-free by the test-and-commit script.)
2012-11-10	fix typo in language bindings	Morgan Deters

2012-11-10	Finally tracked down problems in regressions and fuzz results (this also	Clark Barrett
	explains why my build was giving different answers from Dejan's build). Problem was that if you run: cvc4 --check-models foo.smt it would fail, but if you run cvc4 --check-models --produce-models foo.smt it would succeed. Even though produce-models is supposed to be automatically set when you set check-models, it seems this was happening too late. Fixed by removing any distinction between produce-models and check-models in the heuristic setting code. Kind of ugly though. Also, disable models if nonlinear arithmetic is on.
2012-11-09	TheoryEngineModelBuilder::buildModel() is only called once with ↵	Morgan Deters
	fullModel=true, within a SAT context. This fixes some outstanding model bugs. Committing also a Clark-provided assertion the Model code to ensure the call is only done once per context. (this commit was certified error- and warning-free by the test-and-commit script.)
2012-11-09	export null nodes (fixes a bug in portfolio model stuff)	Kshitij Bansal

2012-11-09	Test that breaks arithmetic model building due to disequality terms.	Tim King

2012-11-09	Arithmetic problem that fails --check-models due incompleteness with ↵	Tim King
	multiplication.
2012-11-09	Bug-fix for a crash involving improperly-thrown exceptions; also, add ↵	Morgan Deters
	LogicException for errors where the user uses a feature not permitted in the current logic (e.g., a quantifier in a QF logic)
2012-11-09	In non-linear logics, rewrite DIVISION, INTS_DIVISION, and INTS_MODULUS into ↵	Morgan Deters
	ITEs of the form: IF (denom = 0) THEN divByZero(num) ELSE (DIVISION_TOTAL num denom) ENDIF where divByZero is an uninterpreted function symbol (there's one for each of the partial operators). In linear logics, don't do any of this. Bitvector partial functions to come, if this is successful for Tim. (this commit was certified error- and warning-free by the test-and-commit script.)
2012-11-09	another DISTCLEANFILES entry, for proper "make distclean" behavior (fixes ↵	Morgan Deters
	"distclean" target error last night)
2012-11-09	Fix for another model assertion failure	Clark Barrett

2012-11-08	Turns on TheoryUF when non-linear arithmetic is turned on. Adds test cases ↵	Tim King
	for division by 0.
2012-11-08	fix "make distcheck"	Morgan Deters

2012-11-08	Review of trunk r4525 (TypeNode::getBaseType()):	Morgan Deters
	* fixed TypeNode::getBaseType() for predicate subtypes * added Type::getBaseType() for public interface * added unit testing To avoid confusion, also: * renamed PredicateType::getBaseType() to "getParentType()" * renamed TypeNode::getSubtypeBaseType() to "getSubtypeParentType()" (this commit was certified error- and warning-free by the test-and-commit script.)
2012-11-08	Improved support for division by zero. This adds the *_TOTAL kinds and ↵	Tim King
	uninterpreted functions for division by 0.
2012-11-08	exception fix	Morgan Deters

2012-11-08	Fixed two small bugs in model generation	Clark Barrett

2012-11-08	Added getBaseType - Morgan please check	Clark Barrett

2012-11-08	added support for parametric datatypes in smt2 parser, includes support for ↵	Andrew Reynolds
	'as' qualifier
2012-11-07	* Type ascription bug fixed (resolves bug 432), but there are others I ↵	Morgan Deters
	discovered (still outstanding). :-( * Fix a documentation-building problem when building from tarballs (fixes distcheck build failure last night) * Provide expected output for arith regression 'mod.01.smt2' * Also, fix a compiler warning in inst_gen.cpp (this commit was certified error- and warning-free by the test-and-commit script.)
2012-11-07	Fix to a bug in integer mod lemmas.	Tim King

2012-11-06	fix issue in compatibility layer that could segfault	Morgan Deters

2012-11-05	Fix to the context dependent static learning code.	Tim King

2012-11-05	fixes for replacement function library	Morgan Deters

2012-11-05	fixes for mac os	Morgan Deters

2012-11-05	fix for tarball building (fixes debian and distcheck problems in nightly builds)	Morgan Deters

2012-11-02	more minor updates to inst gen and representative selection, clean up of ↵	Andrew Reynolds
	equality query
2012-10-31	cleaning up some of the equality query stuff, implemented a new ↵	Andrew Reynolds
	representative selection strategy for quantifier instantiation
2012-10-30	delta of a model-building failure case	Dejan Jovanović

2012-10-29	more updates and minor bug fixes for fmf/inst-gen quantifier instantiation	Andrew Reynolds

2012-10-29	Tweak to options configuration for turning off minisat elimination when ↵	Clark Barrett
	models are on