Age | Commit message (Collapse) | Author |
|
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.)
|
|
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.)
|
|
Also some fixes to parametric datatypes I found, and fixes for a handful of bugs, including some observed with --check-models --incremental on together.
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
tests to sanity check both versions CLN and GMP versions of length.
|
|
|
|
|
|
strong, and was broken by r4620. This commit resolves bug463. Adding a previously triggering test case.
|
|
in debug mode. This is too long for a regress0 test.
|
|
|
|
|
|
|
|
|
|
* some bindings cleanup
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
ALL_SUPPORTED logic
* Java bindings fixes: fixed access to ostreams, iterators
* Make SmtEngine::setUserAttribute() (and others) take a const string&
* Also a few compliance fixes
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
|
|
Also refactored some header file includes to reduce compile time
|
|
|
|
|
|
similar to arrays - limit the set of terms reported to those relevant in the
current context. Also removed collectModelInfo from sharedTermsDatabase -
doesn't seem to be needed any more.
|
|
|
|
printer now properly prints LAMBDAs. Model builing now gives bound variables names that can be parsed bypresentation language.
|
|
be in the final total order.
|
|
|
|
|
|
|
|
|
|
arithmetic.
|
|
DeltaRational values for lowerbounds, upperbounds, assignments and disequalities. Throws LogicException when a non-linear term is asserted and the the LogicInfo isLinear() disagrees.
|
|
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.)
|
|
|
|
multiplication.
|
|
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.)
|
|
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.)
|
|
|
|
|
|
|
|
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
applied selector terms, this effects two regression test where TCC fails, using --disable-dt-rewrite-error-sel changes answer of both regression tests
|
|
* not all asserted units were tracked in the user trail, moved the tracking into uncheckedEnqueue
|
|
dejan@church:~/workspace/fuzz/problems$ ./check.sh arith_lra_01.smt2
z3: sat sat sat sat sat sat sat sat sat unsat sat sat sat sat sat unsat sat
cvc4: sat sat sat sat sat sat sat sat sat unsat sat sat sat sat sat unsat unsat
dejan@church:~/workspace/fuzz/problems$ ./check.sh arith_lra_02.smt2
z3: sat sat sat sat sat sat sat sat sat sat sat sat sat sat sat unsat unsat sat
cvc4: sat sat sat sat sat sat sat sat sat sat sat sat sat sat sat unsat unsat unsat
|
|
and improved. this update fixes bug 428, also changes the result for 2 benchmarks where tcc in cvc3 fails (cvc4 had previously had been answering correctly by accident).
|
|
|
|
with --check-models (which caused the same bug, for a different reason,
due to some unintended interaction between the checkModel() function and
the UserContext, which rolled back the Model object. (Groan...)
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
just the header comments at the top, though. Don't update to this rev if
you don't have time for a complete rebuild, and exclude this rev if you
want to see what's new across a range of commits.
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
Also fix bug 421 relating to incrementality and models.
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
|