feat(Core): add Str.ToLower and Str.ToUpper string operations#621
feat(Core): add Str.ToLower and Str.ToUpper string operations#621
Conversation
- Add `unaryOp` optional `axioms` parameter in IntBoolFactory.lean - Add `strToLowerFunc` and `strToUpperFunc` in Factory.lean, each with concrete evaluation (String.toLower / String.toUpper) and three SMT axioms: idempotence, length preservation, and concat distributivity - Wire both ops into the DDM grammar, ASTtoCST, and Translate passes - Skip axiom-bearing factory functions in ExprEvalTest to avoid MBQI timeouts on UF-based operations - Merge StrToLowerTest and StrToUpperTest into StrCaseTest.lean - Update ProcedureEvalTests and ProgramTypeTests expected outputs Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
shigoel
changed the title
… doc Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
| (((~Str.Concat : string → string → string) %1) %0)) | ||
| == (((~Str.Concat : string → string → string) | ||
| ((~Str.ToUpper : string → string) %1)) | ||
| ((~Str.ToUpper : string → string) %0)))] |
There was a problem hiding this comment.
Confirmed that all these axioms and their ToLower versions are indeed valid, using CVC5.
I heard ß uppercases to SS, but probably ToUpper only deals with English alphabets.
There was a problem hiding this comment.
Could you verify that idea?
There was a problem hiding this comment.
Yeah, I could test with this! :)
(set-logic QF_SLIA)
(declare-const result String)
(assert (= result (str.to_upper "\u{00DF}")))
(check-sat)
(get-value (result))
It prints:
sat <- this doesn't matter
((result "\u{df}"))
\u00df is ß.
There was a problem hiding this comment.
I think we should have a test with an unprovable or false goal to demonstrate that the axioms are not vacuous.
joehendrix
left a comment
joehendrix
left a comment
There was a problem hiding this comment.
It's be nice to see if we can reduce some of the per-operator boilerplate wrt DDM integration, but that's clearly a separate PR.
| knowledge for the solver: | ||
| - *Idempotence*: `f(f(s)) == f(s)` | ||
| - *Length preservation*: `len(f(s)) == len(s)` | ||
| - *Concat distributivity*: `f(s1 ++ s2) == f(s1) ++ f(s2)` |
There was a problem hiding this comment.
These three axioms can be trivially satisfied by the identity function. This means that having them will make "sat" no longer sound. @aqjune-aws any insight we could bring on that?
There was a problem hiding this comment.
It is true that this might lead to spurious counter examples - but I thought it was fine to raise spurious counter examples. There was a discussion suggesting that preventing cover from unsat -> sat was too strict.
MikaelMayer
left a comment
MikaelMayer
left a comment
There was a problem hiding this comment.
There seem to be redundant tests.
| assert [empty_lower]: str.tolower("") == ""; | ||
|
|
||
| // Concrete idempotence (two calls on a literal) | ||
| assert [concrete_idempotent]: |
There was a problem hiding this comment.
These tests are about concrete values, so they don't make sense since we know the result of these functions. It would be more interesting to see symbolic inputs here to see that the axioms are being picked up
5 participants
Summary
str.tolowerandstr.toupperoperations to Strata Core, each with concrete evaluation and SMT axiomsunaryOpcombinator inIntBoolFactory.leanwith an optionalaxiomsparameterExprEvalTestto avoid MBQI timeouts on UF-based operationsBy submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.