diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-12-08 00:38:14 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-12-08 00:38:14 -0600 |
| commit | 0309ef4aa7462c6fa2a65c1ef408dc9063bb1f21 (patch) | |
| tree | 6a5165e43890811a91d01bce0ff7cb3893a4257c /src/theory/strings/kinds | |
| parent | 3223d3c765b87db9d87a7ca65c4b7cf5dc9a7885 (diff) | |
Proper implementation of expand definitions for sequences (#5616)
Expand definitions for sequences was wrong in two ways: (1) we replaced str.from_code with a witness term. This led to it being unevaluatable in models. (2) we did not handle seq.nth, meaning its model value was unevaluatable if it was out of bounds. Now it evaluates the value of the uninterpreted function we replace with.
This corrects both issues and adds a regression to demonstrate both kinds of terms evaluate correctly.
To do this, I added a helper function to skolem cache as well as a new (internal-only) kind SEQ_NTH_TOTAL. Notice applications of this kind should only be used for model evaluation.
Notice this fixes several check-model warnings in the regressions. It still does not fix others since other things must be corrected for model evaluation (e.g. expandDefinitions must be applied on theory assertions for --debug-check-models). This will be done in later PRs.
Diffstat (limited to 'src/theory/strings/kinds')
| -rw-r--r-- | src/theory/strings/kinds | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds index 020cedb30..427e2e4e6 100644 --- a/src/theory/strings/kinds +++ b/src/theory/strings/kinds @@ -84,6 +84,7 @@ constant CONST_SEQUENCE \ operator SEQ_UNIT 1 "a sequence of length one" operator SEQ_NTH 2 "The nth element of a sequence" +operator SEQ_NTH_TOTAL 2 "The nth element of a sequence (internal, for responses to expand definitions only)" # equal equal / less than / output operator STRING_TO_REGEXP 1 "convert string to regexp" @@ -171,5 +172,6 @@ typerule STRING_TOLOWER "SimpleTypeRule<RString, AString>" typerule CONST_SEQUENCE ::CVC4::theory::strings::ConstSequenceTypeRule typerule SEQ_UNIT ::CVC4::theory::strings::SeqUnitTypeRule typerule SEQ_NTH ::CVC4::theory::strings::SeqNthTypeRule +typerule SEQ_NTH_TOTAL ::CVC4::theory::strings::SeqNthTypeRule endtheory |