Repository navigation
smt2: lower empty_string and decimal of_int to SMT-LIB - #9469
Draft
tautschnig wants to merge 2 commits into
Draft
tautschnig wants to merge 2 commits into
tautschnig wants to merge 2 commits into
Conversation
smt2_convt lowers applications of the cprover_string_* built-ins over
SMT-LIB strings to the SMT-LIB theory of strings. Add four more
built-ins with their SMT-LIB 2.6 counterparts:
- replace_all(s, old, new) -> (str.replace_all s old new): replaces every
match; s is unchanged if old is "". (replace, which lowers to
str.replace, replaces the first match only.)
- from_code(i) -> (str.from_code i): the one-character string with code
point i, and "" unless 0 <= i <= 196607.
- to_code(s) -> (str.to_code s): the code point of s if |s| = 1, and -1
otherwise.
- from_int(n) -> (str.from_int n): the decimal representation of n, and ""
for n < 0. A front-end that needs a sign can use
ite(n < 0, "-" ++ from_int(-n), from_int(n)).
The integer operands and results are Int-sorted in SMT-LIB; applications
with operands or results of another sort, or with the wrong number of
operands, are rejected with an unsupported_operation_exceptiont rather
than producing input that the solver rejects.
No front-end in this repository emits these built-ins yet: they are meant
for front-ends that produce SMT-LIB-string applications, such as a Python
front-end in preparation, where Python's str.replace, chr, ord and str
of an integer need them. Note that the edge cases above follow SMT-LIB
and differ from those languages (e.g. Python's "abc".replace("", "x") is
"xaxbxcx"); a front-end has to handle such cases itself.
Unit tests check the lowering, the rejection of other sorts and
arities, and, using Z3, the values of the four lowerings on concrete
operands, including the edge cases above.
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
smt2_convt lowers applications of the cprover_string_* built-ins over SMT-LIB strings to the SMT-LIB theory of strings, and turns the remaining ones into uninterpreted functions. Two of the latter do have exact SMT-LIB counterparts, and leaving them uninterpreted produced spurious counterexamples: for example, x = empty_string(); assert(x == "") failed with both Z3 and cvc5. - empty_string() -> "" - of_int(n) and of_int(n, 10) -> (ite (>= n 0) (str.from_int n) (str.++ "-" (str.from_int (- n)))) as str.from_int is "" for negative n. of_int with any other radix remains uninterpreted. As for from_int, the operand of of_int must be Int-sorted; other sorts are rejected with an unsupported_operation_exceptiont. Unit tests check the lowering, the rejection of other sorts and arities, that of_int with radix 16 is not lowered, and, using Z3, the values on concrete operands, including negative ones. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## develop #9469 +/- ##
===========================================
+ Coverage 81.02% 81.03% +0.01%
===========================================
Files 1723 1723
Lines 191314 191435 +121
Branches 73 73
===========================================
+ Hits 155020 155138 +118
- Misses 36294 36297 +3 ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
This branch has not been deployed
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Depends-on: #9139
smt2_convt lowers applications of the cprover_string_* built-ins over
SMT-LIB strings to the SMT-LIB theory of strings, and turns the
remaining ones into uninterpreted functions. Two of the latter do have
exact SMT-LIB counterparts, and leaving them uninterpreted produced
spurious counterexamples: for example, x = empty_string(); assert(x == "")
failed with both Z3 and cvc5.
(ite (>= n 0) (str.from_int n) (str.++ "-" (str.from_int (- n))))
as str.from_int is "" for negative n. of_int with any other radix
remains uninterpreted.
As for from_int, the operand of of_int must be Int-sorted; other sorts
are rejected with an unsupported_operation_exceptiont.
Unit tests check the lowering, the rejection of other sorts and arities,
that of_int with radix 16 is not lowered, and, using Z3, the values on
concrete operands, including negative ones.
Co-authored-by: Kiro kiro-agent@users.noreply.github.com