| Age | Commit message (Collapse) | Author |
|---|
|
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 is work towards eliminating global calls to getCurrentSmtEngine()->expandDefinition.
The next step will be to add Rewriter::expandDefinition.
|
|
This PR refactors how we collect statistics.
It splits the current statistic values into the values and a proxy object. The actual values now live inside the registry (making the ownership model way easier) while the proxy object are handed to whoever wants to collect a new statistic.
It also extends the C++ API to obtain and inspect the statistics.
To change the ownership, this PR needs to touch every single statistic in the whole codebase and change how it is registered.
|
|
|
|
|
|
|
|
|
|
|
|
This PR uses IntegralHistogramStat instead of HistogramStat when appropriate, that is everywhere.
|
|
|
|
This PR updates the update-copyright.pl script to also update/add copyright headers to CMake specific files. It further fixes a small typo in the header.
|
|
This PR adds support for seq.nth operator by eliminating it during expandDefinitions, based on sub-sequences.
Tests that use this operator are also included.
|
|
This adds support for skeleton proofs in the rewriter (REWRITE -> THEORY_REWRITE).
It adds "extended equality rewrite" as a new method of the rewriter/theory rewriters.
The unit test of this feature should be added on a followup PR.
Co-authored-by: Andres Noetzli <andres.noetzli@gmail.com>
|
|
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 adds basic infrastructure for the sequence type, including its type rules, type enumerator and extensions to type functions.
The next step will be to finalize the support in TheoryStrings for sequences and then add front end support for sequences in the API/parsers.
|
|
This commit adds statistics for string rewrites. This is work towards proof
support in the string solver. At a high level, this commit adds a pointer to a
`SequenceStatistics` in the rewriters and modifies
`SequencesRewriter::returnRewrite()` to count the rewrites done. In practice,
to make this work requires a couple of changes, some of them temporary:
- We can't have a single `Rewriter` instance shared between different
`SmtEngine` instances anymore. Thus the `Rewriter` is now owned by the
`SmtEngine` and calling the rewriter retrieves the rewriter associated with
the current `SmtEngine`. This is a temporary workaround before we get rid of
singletons.
- Methods in the `SequencesRewriter` and the `StringsRewriter` are made
non-`static` because they need access to the statistics instance.
- `StringsEntail` now has non-`static` methods because it needs a reference to
the sequences rewriter that it can call.
- The interaction between the `StringsRewriter` and the `SequencesRewriter`
changed: the `StringsRewriter` is now a proper `TheoryRewriter` that inherits
from `SequencesRewriter` and calls its `postRewrite()` before applying its
own rewrites (this is essentially a reversal of roles from before: the
`SequencesRewriter` used to call `static` methods in the `StringsRewriter`).
- The theory rewriters are now owned by the individual theories. This design
mirrors the `EqualityEngine`s owned by the individual theories.
|
|
This is in preparation for making the strings rewriter configurable for stats.
This moves all utility functions from SequencesRewriter to a proper place. This includes three new groupings of utility functions: those involving arithmetic entailments, those involving string entailments, those involving regular expression entailments. Here, "entailments" loosely means any question regarding a (set of) terms or formulas.
No major code changes. Added some missing documentation and lightly cleaned a few blocks of code in cpp.
|
|
Towards theory of sequences.
|
|
Towards proofs for string rewrites. All return statements all now associated with an enum value.
An indentation in a block of code changed in rewriteMembership.
|
|
In preparation for string proof infrastructure.
This introduces an enumeration type to track string rewrites.
It also makes inference printing more consistent.
|
|
Organization towards theory of sequences.
The motivation of this PR is to ensure that string-specific operators in the rewriter are in their own file; thus the use of mkConst<String> / getConst<String> is allowable in rewriter_str.cpp.
|
