SMT2: encode mathematical and string/regex types and operations#9074
Open
tautschnig wants to merge 1 commit into
Open
SMT2: encode mathematical and string/regex types and operations#9074tautschnig wants to merge 1 commit into
tautschnig wants to merge 1 commit into
Conversation
Convert mathematical integer/real types to SMT-LIB Int/Real (type2id, convert_type), encode mathematical mod/div semantics, string/regex types, string constants, and map Strata's Str.*/Re.* function applications to the corresponding SMT-LIB string/regex operators in convert_expr. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
tautschnig
requested review from
TGWDB,
kroening,
martin-cs and
peterschrammel
as code owners
There was a problem hiding this comment.
Pull request overview
Note
Copilot was unable to run its full agentic suite in this review.
Extends the SMT2 converter to support Strata mathematical Int/Real types plus SMT-LIB string/regex types, constants, and common Str.* / Re.* operations.
Changes:
- Encode
integer,real,string, and regex sorts intype2id/convert_type - Map selected
Str.*andRe.*function applications to SMT-LIB string/regex operators - Adjust integer
div/modencoding and add SMT-LIB string constant emission
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Comment on lines
+3880
to
+3894
| else if(expr_type.id()==ID_string) | ||
| { | ||
| const std::string &value = id2string(expr.get_value()); | ||
| out << "\""; | ||
| for(char c : value) | ||
| { | ||
| if(c == '"') | ||
| out << "\"\""; | ||
| else if(c == '\\') | ||
| out << "\\\\"; | ||
| else | ||
| out << c; | ||
| } | ||
| out << "\""; | ||
| } |
Comment on lines
+3929
to
+3942
| else if(expr.type().id() == ID_integer) | ||
| { | ||
| // SMT-LIB2 mod for mathematical integers (truncation semantics) | ||
| // Use (- a (* (div a b) b)) to get truncation mod | ||
| out << "(- "; | ||
| convert_expr(expr.op0()); | ||
| out << " (* (div "; | ||
| convert_expr(expr.op0()); | ||
| out << " "; | ||
| convert_expr(expr.op1()); | ||
| out << ") "; | ||
| convert_expr(expr.op1()); | ||
| out << "))"; | ||
| } |
Comment on lines
+2718
to
+2751
| // Map Strata function names to SMT-LIB names for string/regex ops | ||
| std::string smt_name; | ||
| if(fn_name == "Str.Concat") | ||
| smt_name = "str.++"; | ||
| else if(fn_name == "Str.Length") | ||
| smt_name = "str.len"; | ||
| else if(fn_name == "Str.Substr") | ||
| smt_name = "str.substr"; | ||
| else if(fn_name == "Str.ToRegEx") | ||
| smt_name = "str.to_re"; | ||
| else if(fn_name == "Str.InRegEx") | ||
| smt_name = "str.in_re"; | ||
| else if(fn_name == "Re.AllChar") | ||
| smt_name = "re.allchar"; | ||
| else if(fn_name == "Re.All") | ||
| smt_name = "re.all"; | ||
| else if(fn_name == "Re.Range") | ||
| smt_name = "re.range"; | ||
| else if(fn_name == "Re.Concat") | ||
| smt_name = "re.concat"; | ||
| else if(fn_name == "Re.Star") | ||
| smt_name = "re.*"; | ||
| else if(fn_name == "Re.Plus") | ||
| smt_name = "re.+"; | ||
| else if(fn_name == "Re.Loop") | ||
| smt_name = "re.loop"; | ||
| else if(fn_name == "Re.Union") | ||
| smt_name = "re.union"; | ||
| else if(fn_name == "Re.Inter") | ||
| smt_name = "re.inter"; | ||
| else if(fn_name == "Re.Comp") | ||
| smt_name = "re.comp"; | ||
| else if(fn_name == "Re.None") | ||
| smt_name = "re.none"; |
Comment on lines
+4479
to
+4483
| if( | ||
| expr.type().id() == ID_integer || expr.type().id() == ID_natural) | ||
| { | ||
| out << "(div "; | ||
| } |
kroening
reviewed
Jun 18, 2026
| fn_name = id2string( | ||
| to_symbol_expr(function_application_expr.function()).get_identifier()); | ||
|
|
||
| // Map Strata function names to SMT-LIB names for string/regex ops |
Collaborator
There was a problem hiding this comment.
We should introduce expressions for these at some point.
kroening
approved these changes
Jun 18, 2026
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.
Convert mathematical integer/real types to SMT-LIB Int/Real (type2id, convert_type), encode mathematical mod/div semantics, string/regex types, string constants, and map Strata's Str./Re. function applications to the corresponding SMT-LIB string/regex operators in convert_expr.