Support SMT string literals and common string ops in translateTerm#1109
Open
tautschnig wants to merge 3 commits intomainfrom
Open
Support SMT string literals and common string ops in translateTerm#1109tautschnig wants to merge 3 commits intomainfrom
tautschnig wants to merge 3 commits intomainfrom
Conversation
translateSort already handles .prim .string, but translateTerm had no arm for .prim (.string _): any SMT string literal produced by the encoder would fall through to the catch-all and raise 'unsupported term'. Add the missing arm plus the two string operations already supported in Denote.lean so that the two translators agree on the end-to-end-supported subset. Specifically, add arms for: - .prim (.string s) -> (mkString, toExpr s) - .app .str_length [s] _ -> (mkInt, Int.ofNat s.length) - .app .str_concat as _ -> (mkString, leftAssocOp mkStringAppend as) mkStringAppend uses instHAppendOfAppend + instAppendString, which is the same instance chain Lean elaborates inferInstance to for HAppend String String String. Regression tests in StrataTest/DL/SMT/TranslateTests.lean cover all three arms; each fails on origin/main (catch-all throw observable via #guard_msgs mismatch) and passes with this change. I additionally verified under a Meta.check-enabled harness that the produced Expr type-checks in the kernel, so the (fst = mkString/mkInt, snd = ...) pairs are internally consistent. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Contributor
There was a problem hiding this comment.
Pull request overview
This PR extends the SMT-to-Lean translator so the supported string subset matches the string features already denoted elsewhere in the SMT layer. It adds missing translation support for string literals, string length, and string concatenation, plus regression tests covering those happy paths.
Changes:
- Add
translateTermsupport for SMT string literals. - Add translation for
str_lengthandstr_concatinto LeanExprs. - Add regression tests for string literals, length, and concatenation translation.
Reviewed changes
Copilot reviewed 2 out of 2 changed files in this pull request and generated 2 comments.
| File | Description |
|---|---|
Strata/DL/SMT/Translate.lean |
Adds the new string-expression constructors and translation arms in translateTerm. |
StrataTest/DL/SMT/TranslateTests.lean |
Adds #guard_msgs regression tests for the newly supported string cases. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Addresses the two review comments on PR #1109: 1. `.app .str_length` silently built `Int.ofNat (String.length x)` even when `x` was not a `String`. Check the operand's translated type against `mkString` via a new `expectString` helper (shape mirrors `getBitVecWidth`), so malformed terms throw rather than producing an ill-typed `Expr` that only fails much later. 2. `.app .str_concat` delegated to `leftAssocOp`, which neither rejects fewer-than-two operands (despite its error message claiming it does) nor checks that operands have the expected type. So `.app .str_concat [s]` silently translated to `s`, and a mixed-type list produced an ill-typed `HAppend.hAppend`. Both diverged from `Denote.leftAssoc`. Inline the op instead: require two or more operands explicitly and `expectString` every operand, matching what `Denote.leftAssoc` does for `str_concat`. The underlying `leftAssocOp` bug (silent-singleton) affects every other caller (`.app .add`, `.app .sub`, `.app .mul`, `.app .div`, `.app .mod`, plus the bitvec analogues); it is pre-existing and will be fixed in a separate PR so that the change set can be reviewed on its own merits. Regression tests added in StrataTest/DL/SMT/TranslateTests.lean: - A >2-ary happy-path `str_concat` to cover the foldl tail. - `str_length` applied to a non-string operand. - Singleton `str_concat`. - `str_concat` with a non-string operand in first position. Each error-path test fails on the previous commit (producing the ill-typed `Expr` or the singleton pass-through) and passes here. Tests use `.prim (.bool _)` for the non-string operand so that the expected error message is stable regardless of how `.prim (.int _)` happens to be typed (see PR #1107). Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
aqjune-aws
previously approved these changes
May 5, 2026
Contributor
aqjune-aws
left a comment
aqjune-aws
left a comment
There was a problem hiding this comment.
Looks fine to me, but probably @kondylidou or @abdoo8080's view might be helpful.
github-actions
Bot
added
Has 1 approval
Git conflicts
and removed
Waiting-For-Review
labels
Contributor
Author
|
@keyboardDrummer-bot Please resolve git conflicts. |
github-actions
Bot
added
Waiting-For-Review
and removed
Has 1 approval
Git conflicts
labels
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.
translateSort already handles .prim .string, but translateTerm had no arm for .prim (.string _): any SMT string literal produced by the encoder would fall through to the catch-all and raise 'unsupported term'. Add the missing arm plus the two string operations already supported in Denote.lean so that the two translators agree on the end-to-end-supported subset.
Specifically, add arms for:
mkStringAppend uses instHAppendOfAppend + instAppendString, which is the same instance chain Lean elaborates inferInstance to for HAppend String String String.
Regression tests in StrataTest/DL/SMT/TranslateTests.lean cover all three arms; each fails on origin/main (catch-all throw observable via #guard_msgs mismatch) and passes with this change. I additionally verified under a Meta.check-enabled harness that the produced Expr type-checks in the kernel, so the (fst = mkString/mkInt, snd = ...) pairs are internally consistent.
By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.