Age | Commit message (Collapse) | Author |
|
|
|
arithmetic.
|
|
DeltaRational values for lowerbounds, upperbounds, assignments and disequalities. Throws LogicException when a non-linear term is asserted and the the LogicInfo isLinear() disagrees.
|
|
circuit for division by 0; temporary fix for bug440
|
|
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.)
|
|
** 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.)
|
|
be used yet), added new totality lemma option for uf strong solver
|
|
constants for total functions.
|
|
|
|
|
|
|
|
Fixed another model bug and added previously failing fuzz testcase
|
|
|
|
--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.)
|
|
* 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.)
|
|
|
|
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.
|
|
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.)
|
|
|
|
|
|
multiplication.
|
|
LogicException for errors where the user uses a feature not permitted in the current logic (e.g., a quantifier in a QF logic)
|
|
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.)
|
|
"distclean" target error last night)
|
|
|
|
for division by 0.
|
|
|
|
* 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.)
|
|
uninterpreted functions for division by 0.
|
|
|
|
|
|
|
|
'as' qualifier
|
|
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.)
|
|
|
|
|
|
|
|
|
|
|
|
|
|
equality query
|
|
representative selection strategy for quantifier instantiation
|
|
|
|
|
|
models are on
|
|
|
|
|
|
|
|
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
not recognizing parametric datatype types as being datatype types
|