| Age | Commit message (Collapse) | Author |
|---|
|
|
|
(cherry-picked from master 23b4fd82d1ed326cd57e9bc57ef9fab98b0b1c87)
|
|
|
|
|
|
(cherry picked from commit 25c6e1331d338c6ba8d60224711343986e11cf79)
|
|
failing regression for bug 472
|
|
also a regression for bug 411
(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.)
|
|
|
|
pattern first
just after the bindings
Do it before the release in order to not break user files later
|
|
|
|
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.)
|
|
|
|
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.)
|
|
|
|
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.)
|
|
|
|
multiplication.
|
|
for division by 0.
|
|
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.)
|
|
|
|
|
|
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.)
|
