Age | Commit message (Collapse) | Author |
|
|
|
This makes it so that we attempt evaluation + rewriting on applications of operators that do not always evaluate, and return constants in case the evaluation was successful.
This fixes warnings for check-models on 43 of our regressions, and also uncovered one regression where our model was wrong but check-models silently succeeded. I've opened CVC4/cvc4-projects#276 for fixing the latter.
|
|
This commit removes parser and printer support for old SMT-LIB standards and also converts all regression tests to 2.6.
|
|
Moves regressions taking >4 seconds (summing all configs) in debug to regress1.
|
|
Currently --check-models is implemented by replaying several preprocessing steps, including theory-specific expand definitions, and then checking whether the result evaluates to true.
However, by having --check-models rely on complex preprocessing machinery defeats its purpose, as these steps are part of its trusted base.
Moreover, issue #5645 demonstrates that this may lead to spurious errors where we incorrectly conclude that an input assertion is false, when it is not.
This PR significantly simplifies --check-models so that it only relies on define-fun expansion + rewriting + evaluation. This ensures that --check-models is "sound" i.e. it does not falsely report a formula as evaluating to false. As a consequence, this makes check-models give warnings more often, i.e. when partial operators are involved, thus -q is added to silence warnings on some regressions.
A followup PR will use a satisfiability check on the input formula post-expand-definitions to properly implement a trustworthy version of check-models that is robust for partial operators.
Fixes #5645.
|
|
This adds a net +82 regressions to regress[0-2] and adds several additional disabled regressions to regress3 and regress4. This involved fixing the status on several regressions, and ensuring CMakeLists.txt includes all files (exactly once) in the test/regress/ subdirectory.
It also moves several regressions to the proper regression levels (those that take >30 seconds in debug are moved to regress3+).
|
|
This commit removes the SMT1 parser infrastructure and adds the SMT2 translations of the SMT1 regression tests. For now this commit removes regression test regress3/pp-regfile.smt since the SMT2 translation has a file size of 887M (vs. 172K for the SMT1 version).
Fixes #2948 and fixes #1313.
|
|
|
|
|
|
Currently, we can optionally specify an *.expect file with the metadata
of a regression test. This commit removes that option because it was not
widely used, adds maintenance overhead and makes the transition to a new
build system more cumbersome. Regression files can still be fed to a
solver without removing the metadata first since they are in comments of
the corresponding input format (note that this was not always the case,
it changed in efc6163629c6c5de446eccfe81777c93829995d5).
|
|
Until now, regression tests were split across tens of different
Makefile.am, which required a lot of code duplication and does not
really seem to be in the spirit of automake. If we want to change the
LOG_COMPILER/LOG_DRIVER for example, we have to change every single
Makefile.am, which is cumbersome (I was able to get something
semi-working by exporting those variables but it didn't seem very
clean). Additionally, it made the output of the regression tests fairly
verbose and split the output across multiple log files. Finally
it also limited parallelism when running the regression tests (this fix lowers
the time it takes to run regression level 1 from 3m to 1m45s on my
machine with 16 threads).
This commit moves all the regression tests into
test/regress/Makefile.tests and changes test/regress/Makefile.am to deal
with this new structure. Finally, it changes how the test summary in
test/Makefile.am is produced: instead of relying on the log files for
the subdirectories, it greps for the test results in the log files of
the individual tests. Not the most elegant solution but we should
probably anyway delegate that task to a Python script at some point.
|
|
|
|
With the recent changes to the regress tests, some of the Makefiles were
not in sync anymore. This commit fixes that.
|
|
|
|
instead of answering unknown for benchmarks with quantifiers. Modified regressions accordingly. Minor fix for QCF regarding variable ordering. Improved relevant domain computation. Minor optimization for --mbqi=fmc
|
|
generation; fix bug 285.
* segfaults/assert-fails in proof-generation fixed, including bug 285
* added --check-proofs to automatically check proofs, like --check-models (but only for UF/SAT at present)
* proof generation now works in portfolio (but *not* --check-proofs, since LFSC code uses globals)
* proofs are *not* yet supported in incremental mode
* added --dump-proofs to dump out proofs, like --dump-models
* run_regression script now runs with --check-proofs where appropriate
* options scripts now support :link-smt for SMT options, like :link for command-line
|
|
success, nonzero error
|
|
|
|
|
|
|
|
|
|
|
|
Thanks to Peter Collingbourne for the report, and the patch!
(this commit was certified error- and warning-free by the test-and-commit script.)
|
|
should work now
|
|
* change some uses of "std::cout" to "Message()"
* change some files to use Unix newlines instead of DOS newlines
* fix compiler warning
|
|
(e.g., "make dist" produces a distribution that passes "make dist" and "make check", "make uninstall" actually uninstalls, "make distclean" actually cleans, ...)
|
|
disableing one test case in equantifiers/decision that runs long
|
|
|
|
pp-regfile.delta02.smt is the one to look at with
--decision=justificaiton, the delta minimized version of pp-regfile,
which also gives wrong answer. due to various commits/fixes, delta01
gives correct answer currently.
|
|
|
|
|
|
* remove assert iteSkolemMap gives ite-s (not true with repeatSimp)
* handle a corner case in findSplitter triggered by repeatSimp
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|