| Age | Commit message (Collapse) | Author |
|---|
|
This adds an option to change the cardinality of the alphabet of strings. The alphabet of strings is always a prefix of the interval of unicode code points in the string standard.
|
|
Our way of constructing proofs from the equality engine in very rare cases may cause cyclic proofs due to constructing double applications of SYMM, which are not recognized as assumptions in CDProof. This is due to an interplay between LazyProofChain using an underlying CDProof as its default proof generator, where the proof chain would use the proofs from the CDProof to form a cyclic proof.
This was encountered in 9 SMT-LIB benchmarks in QF_SLIA.
This makes us safer in several places related to double SYMM steps.
|
|
Fixes #6639. The issue cannot be reproduced on current master and git bisect suggests that commit adf497a
fixed the issue.
|
|
Fixes #6636, fixes #6637. When the start index was non-zero, the result of
str.indexof_re was not properly restricted to be greater or equal to
the start index. This commit fixes the issue by making the eager
reduction lemma more precise. Additionally, the commit fixes an issue
with the lower bound of the length of the match in str.indexof_re.
|
|
|
|
This commit adds --no-jh-rlv-order to two string regressions that take
over 2 minutes to run in debug after #6613, which increases the overall
regression runtime significantly.
|
|
Fixes #6057. The reductions of `str.replace_re` and `str.replace_re_all`
were not correctly enforcing that the operations replace the _first_
occurrence of some regular expression in a string. This commit fixes the
issue by introducing a new operator `str.indexof_re(s, r, n)`, which,
analoguously to `str.indexof`, returns the index of the first match of
the regular expression `r` in `s`. The commit adds basic rewrites for
evaluating the operator as well as its reduction. Additionally, it
converts the reductions of `str.replace_re` and `str.replace_re_all` to
use that new operator. This simplifies the reductions of the two
operators and ensures that the semantics are consistent between the two.
|
|
This enables the new implementation of justification heuristic by default.
Fixes #5454, fixes #5785. Fixes wishues 114, 115, 149, 160.
|
|
Fixes #6483. The benchmark in the issue was performing the following
incorrect rewrite:
Rewrite (str.replace "B" (str.replace (str.++ (str.replace "B" a "B") a) "B" "") "B") to (str.replace "B" a "B") by RPL_X_Y_X_SIMP.
The rewrite RPL_X_Y_X_SIMP rewrites terms of the form (str.replace x y x), where x is of length one and (= y "") rewrites to a
conjunction of equalities of the form (= y_i "") where y_i is some
term. The function responsible for collecting the terms y_i from this
conjunction, collectEmptyEqs(), returns a bool and a vector of
Nodes. The bool indicates whether all equalities in the conjunction
were of the form (= y_i ""). The rewrite RPL_X_Y_X_SIMP only applies
if this is true. However, collectEmptyEqs() had a bug where it would
not return false when all of the conjuncts were equalities but not all
of them were equalities with the empty string. This commit fixes
collectEmptyEqs() and adds tests.
|
|
This commit changes how defaults are set and how the SMT solver is initialized so that proofs can be used fully with (new) unsat cores. Three modes of unsat cores are established now:
the upcoming assumption-based cores, which are incompatible with producing proofs (but enable proofs for preprocessing)
cores based on the SAT proof, which are incompatible with producing proofs (but enable proofs for preprocessing and the SAT solver)
cores based on the full proof, which are unrestricted
All the modes activate proofs but lead to errors if the user requires proofs but is not in the full proofs mode for cores.
|
|
This commit removes parser and printer support for old SMT-LIB standards and also converts all regression tests to 2.6.
|
|
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+).
|
|
Fixes #5381.
|
|
|
|
This adds basic support for string/sequence updating, which has a semantics that is length preserving.
|
|
This commit adds support for the last remaining string operators from
the new SMT-LIB standard for the theory of strings. The commit adds the
kinds, type checking, reductions, and evaluation rewrites for
`str.replace_re` and `str.replace_re_all`.
|
|
This is a major refactor of how operators are eliminated in arithmetic. Currently there were (at least) two things wrong:
(1) ppRewriteTerm sent lemmas on the output channel. This behavior is incompatible with how preprocessing works. In particular, this caused unconstrained simplification to be unaware of terms from such lemmas, leading to incorrect "sat" answers.
(2) Lemmas used to eliminate certain "div-like" terms were processed in a context-independent way. However, lemmas should be cached in a user-context-dependent way. This was leading to incorrect "sat" answers in incremental.
The solution to these issues is to eliminate operators via the construction of witness terms. No lemmas are sent out, and instead these lemmas are the consequence of term formula removal in the standard way.
As a result of the refactor, 2 quantifiers regressions time out due to infinite branch and bound issues (one only during --check-unsat-cores). These appear to be random and I've changed the options to avoid these issues. 3 others now have check-model warnings, which I've added --quiet to. Improving check-model will be addressed on a future PR.
This PR is not required for SMT COMP since we have workarounds that avoid both the incorrect behaviors in our scripts.
Also notice that --rewrite-divk is effectively now enabled by default always.
Fixes #4484, fixes #4486, fixes #4481.
|
|
This PR merges --lang=smt2.6.1 and --lang=smt2.6 (default). It makes it so that 2.6 always expects the syntax of the string standard http://smtlib.cs.uiowa.edu/theories-UnicodeStrings.shtml.
I've updated the regressions so that the 2.6 benchmarks are now compliant with the standard. Some of the <=2.5 benchmarks I've updated to 2.6. Others I have left for now, in particular the ones that rely on special characters or ad-hoc escape sequences. The old formats will be supported in the release but removed shortly afterwards.
This PR is a prerequisite for the release, but not necessarily SMT-COMP (which will use --lang=smt2.6.1 if needed). Notice that we still do not have parsing support for str.replace_re or str.replace_re_all. This is required to be fully compliant.
|
|
This updates the default cardinality in strings to match the Unicode standard, 196608.
This avoids a check-model failure from 25 benchmarks in SMT-LIB, which were related to a split due to insufficient constants being required during collectModelInfo.
This also makes a few places throw an AlwaysAssert(false) that otherwise would lead to incorrect models. These regardless should never throw, but it would be better to have an assertion failure.
|
|
Towards support for the strings standard.
This modifies our interface so that we accept the SMT-LIB standard versions of re.loop and re.^. This means re.loop no longer accepts 3 arguments but 1 (with 2 indices).
This means we no longer accept re.loop with only a lower bound and no upper bound on the number of repetitions.
Also fixes #4161.
|
|
Regression `regress2/strings/issue3203.smt2` is currently timing out
depending on the version of the libraries loaded (see #3606 for more
info). This commit temporarily disables the regression to get the
nightlies to pass again.
|
|
|
|
To make sure that our `str.code` function is injectve (except for -1 in
the codomain), we send the inference that `str.code(x) == -1 v
str.code(x) != str.code(y) v x == y` for each pair of `str.code` terms.
Because of the order of disjuncts, `str.code(x) != str.code(y)` was
usually assigned true. This in turn lead to a difficult problem for the
arithmetic engine if there were more `str.code` applications than the
size of the domain. E.g. if we had `0 <= str.code(xi) < 10` for 0 <= i
<= 10, then the arithmetic engine had a difficult time finding a
conflict. This PR improves the heuristic by setting the phase of
`str.code(x) != str.code(y)` to false, so we prefer to keep the
`str.code` values equal instead of trying to make them different.
This change is also reflected in the models produced for inputs
involving `str.code`: Previously, we were producing models with
different values for the `str.code` whereas now the models are much more
uniform.
The PR adds two regressions, one testing `str.code` performance directly
and one testing it for `str.code` terms generated by `re.range`.
Signed-off-by: Andres Noetzli <anoetzli@amazon.com>
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
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.
|
|
|
|
|
