| Age | Commit message (Collapse) | Author |
|---|
|
Fixes #1736.
|
|
#1791 removed config/tap-driver.sh from the repo, as ./autogen.sh adds it automatically.
The current PR prevents this file from being added to the untracked changes list when doing git status.
|
|
This commit refactors the pbRewrites preprocessing pass into the new
style. This commit is essentially just a code move and adds a regression
test for the preprocessing pass. It also makes use of the
AssertionPipeline::replace function to do proper dependency tracking.
|
|
The autogen.sh script that we use causes the tap-driver.sh script to be
copied from automake installed on the system, so we do not have to
include it in our git repository. This also avoids ping-ponging between
different versions of the tap-driver script if different people have
different versions and commit them as part of their PRs.
|
|
This commit adds the option to run regressions with a timeout using the
`TEST_TIMEOUT` environment variable. The default timeout is set to 10
minutes. This should make it less likely that our nightly builds hang
and makes it easier to sort out slow tests.
Default timeout tested with regression level 2 on a debug build with
proofs.
|
|
|
|
Disabling proof checking/unsat core checking for the two benchmarks in
question, reduces the time to run regressions significantly. After the
change, regression level 2 takes 7m30s to run on my machine and
regression level 1 takes just below 3m (16 threads). Individually, the
tests take over 7m each when checking proofs/unsat cores, so they add
significant overhead.
|
|
|
|
|
|
|
|
|
|
|
|
This was a new utility, only used so far by the extended rewriter in EqChain simplification.
|
|
|
|
This commit changes the regression script to look for status patterns or
get-unsat-core/get-unsat-assumption commands in the benchmark file
instead of the metadata file (i.e. the .expect file if it exists or the
benchmark file otherwise). This fix is not strictly necessary for our
current regressions but might have lead to surprising outcomes in the
future.
|
|
Due to a typo in the regression script, the (get-unsat-core) command was
not recognized (the script was looking for (get-unsat-cores)), so it
tried to run a regression script containing (get-unsat-core) even when
CVC4 was compiled without proof support. This commit fixes the typo.
|
|
|
|
There was a use-after-free in the eager bitblaster: the context used by
the SAT solver was destroyed before the solver. This lead to a
use-after-free in the destructor of the SAT solver when destroying
context-dependent objects. This commit fixes the issue by changing the
desctruction order such that the context is destroyed after the SAT
solver.
Note: This issue was introduced in commit
a917cc2ab4956b542b1f565abf0e62b197692f8d because d_nullContext and
d_satSolver were changed to be std::unique_ptrs.
|
|
|
|
There were two issues in the new Python regression script when proofs
were enabled: It would try to run "--check-proofs" on SAT benchmarks and
the parameters added to check unsat cores were wrong. This commit fixes
both issues.
|
|
|
|
|
|
|
|
|
|
|
|
Commit 629824db3911ab11ae286e4b14151a537602ba5a added options when
introducing the pseudo boolean processor that were never used. This
commit removes them.
|
|
|
|
|
|
|
|
|
|
|
|
(#1757)
|
|
|
|
|
|
|
|
|
|
|
|
Until now, we have been using a bash script for the running the
regressions. That script had several issues, e.g. it was creating many
temprorary files and it was calling itself recursively, making it
difficult to maintain. This commit replaces the script with a Python
script. The Python script uses the TAP protocol, which allows us to
display the results of multiple tests per file (e.g. with --check-models
and without) separately and with more details. It also outputs whenever it starts running
a test, which allows finding "stuck" regression tests on Travis. As recommended in the
automake documentation [0], the commit copies the TAP driver to enable
TAP support for the test driver.
Note: the commit also changes some of the regressions slightly because
we were using "%" for the test directives in SMT files which does not
correspond to the comment character ";". Using the comment character
simplifies the handling and makes it easier for users to reproduce a
failure (they can simply run CVC4 on the regression file).
[0]
https://www.gnu.org/software/automake/manual/html_node/Use-TAP-with-the-Automake-test-harness.html
|
|
This also adds an additional check in processAssertions to ensure that all
assertions are guaranteed to be rewritten (there was only a comment stating
this).
|
|
|
|
|
|
|
|
|
|
|
|
|
|
This commit refactors the IntToBV preprocessing pass into the new style.
This commit is essentially just a code move, it does not attempt to fix
issues (e.g. #1715).
|
|
Preprocessing pass that turns an arbitrary (e.g. smt2) input into a sygus conjecture, which is helpful for Horn clause solving.
This includes improvements to the robustness of the sygus solver.
|
|
If analyzeFinal() in BVMiniSat was called with a literal that also
occurred in the trail, it could happen that the set of assumptions that
led to the assignment of `p` contained `p` twice.
BitVectorProof::endBVConflict would then register that conflict with the
duplicate literal but at the same time compute a conflict expression
with the duplicate removed. LFSCSatProof::printAssumptionsResolution
would then output two resolutions for the same literal, which made the
simplify_clause side condition fail because it couldn't find the literal
in the clause anymore after the first removal.
The fix simply avoid adding `p` to the set of assumptions if it is found
in the trail. In this situation, `p` is guaranteed to be in the set of
assumptions already because it has been added at the beginning of
analyzeFinal(). This issue originally came up in PR #1384. With this fix
the regression tests pass in #1384.
|
|
|
|
(#1742)
|
