Age | Commit message (Collapse) | Author |
|
|
|
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.)
|
|
Also fix bug 421 relating to incrementality and models.
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
|
|
* fix minor issue with s-expr parsing in CVC and SMT grammars
* other minor things
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
be turned off by --disable-dt-rewrite-error-sel. changed regression answer to reflect new default behavior.
|
|
417. oops. also fix spelling on "rewritting" test
|
|
|
|
* Fix error message if you POP beyond the bottom user stack frame.
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
* Ensure Rewriter::init() is called before ::rewrite().
The array type enumerator recently gave us an end-run around
::init(). TheoryEngine no longer calls these, they're done
via static initialization.
* Respect scope for declare-sort/declare-fun/define-sort/define-fun... (resolves bug 412).
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
* ITE removal fixed to be context-dependent (on UserContext).
Resolves incrementality bugs 376 and 396 (which had given wrong answers).
* some bugfixes for incrementality that Dejan found (fixes bug 394)
* fix for bug in SmtEngine::getValue() where definitions weren't respected
(partially resolves bug 411, but get-model is still broken).
* change status of microwave21.ec.minimized.smt2 (it's actually unsat, but
was labeled sat); re-enable it for "make regress"
Also:
* --check-model doesn't fail if quantified assertions don't simplify away.
* fix some examples, and the Java system test, for the disappearance of the
BoolExpr class
* add copy constructor to array type enumerator (the type enumerator
framework requires copy ctors, and the automatically-generated copy ctor
was copying pointers that were then deleted, leaving dangling pointers in
the copy and causing segfaults)
* --dump=assertions now implies --dump=skolems
* --dump=assertions:pre-<PASS> and --dump=assertions:post-<PASS> now allow
you to dump before/after a particular preprocessing pass. E.g.,
--dump=assertions:pre-ite-removal or --dump=assertions:post-static-learning.
"--dump=assertions" by itself is after all preprocessing, just before CNF
conversion.
* minor fixes to dumping output
* include Model in language bindings
Minor refactoring/misc:
* fix compiler warning in src/theory/model.cpp
* remove unnecessary SmtEngine::printModel().
* mkoptions script doesn't give progress output if stdout isn't a terminal
(e.g., if it's written to a log, or piped through less(1), or whatever).
* add some type enumerator unit tests
* de-emphasize --parse-only and --preprocess-only (they aren't really "common"
options)
* fix some exception throw() specifications in SmtEngine
* minor documentation clarifications
|
|
* Change --lang smt to mean SMT-LIBv2
* --lang smt1 now means SMT-LIBv1
* SMT-LIBv2 parser now gives helpful error if input looks like v1
* SMT-LIBv1 parser now gives helpful error if input looks like v2
* CVC presentation language parser now gives helpful error if input
looks like either SMT-LIB v1 or v2
* Other associated changes
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
bug attachments from bugzilla and put them in the tree
|
|
regress, because the bug was fixed.
Also make QuantifiersModule's destructor virtual (it has virtual members).
(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.)
|
|
* chainability of =, <, <=, >, >= via the new CHAINABLE kind and
TheoryBuiltin rewriter support (resolves bug #383)
* with --smtlib2, force interactive mode off by default
Also:
* fix a few bugs causing crashes
* better "alias" processing for options
* configure-time fixes to readline detection
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
Thanks to Peter Collingbourne for the report, and the patch!
(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.)
|
|
|
|
was only used by the compatibility layer.
Make SmtEngine::internalPop() delay popping. This fixes a bug in model generation.
|
|
collectModelInfo with fullModel argument, most theory-specific implementation out of the model class, model printer relegated to printer classes. Also updates to finite mode finding, modifications to datatypes making them compatible with theory combination, support for theory-specific handling of user attributes, refactoring of uf models
|
|
should work now
|
|
problem so they're no longer failing (in the quantifiers rewriter). Resolves bug #381.
* Added LAMBDA kind and type rule, and Node::isClosure().
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
|
|
|
|
CVC4 differ in the answer), so it doesn't really test anything
|