| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Due to issues in the current proof code, this commit also disables proof
checking for five QF_LRA benchmarks (see issue #2855).
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
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).
|
|
|
|
|
|
|
|
In MiniSat's analyze(), we were taking a reference of a clause that
could be invalidated by a call to resolveOutUnit(). resolveOutUnit() can
lead to allocation of clauses which in turn can lead to clauses being
reallocated, making the reference stale. The commit encloses the
reference in a code block that makes the lifetime of the reference more
obvious and removes uses of the potentially stale reference.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
This commit refactors code generation for options. It uses a new configuration format for defining options (*.toml) and a new Python script mkoptions.py to generate the source code and option documentation.
The option behavior did not change for most of the options, except that for bool --enable-/--disable- long options enable/disable was removed. E.g. --enable-miplib-trick and --disable-miplib-trick got changed to --miplib-trick and --no-miplib-trick.
This commit fixes also an issues with set-option/get-option via the SMT2 interface. Before long options were only accessible if the name included the =ARG part.
|
|
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.
|
|
While reorganizing the regression tests, I found three tests with a
wrong status, one that CVC4 reported unknown for and some regression
tests that had command line options set in the Makefile.am instead of
the tests themselves. This commit fixes the status of the three
regression tests (verified the status with Z3), adds command line
options to make the previously "unknown" test work, and moves the
command line options from the Makefile.am into the individual regression
tests. The latter also required some minor changes to the regression
script because it would not try to determine the expected output from
the (set-info :status ...) command if there was one directive (such as
EXPECT/COMMAND-LINE/etc.). This was an issue with the tests that now
have a COMMAND-LINE directive.
|
|
|
|
|
|
|
|
|
|
|
|
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
|
|
|
|
|
|
|
|
should work now
|
|
back in) by doing "make regress RUN_REGRESSION_ARGS=--dump"
|
|
|
|
|
