Add a translator from SMT.Term to SMTDDM.Term #177

aqjune-aws · 2025-10-31T17:01:56Z

This patch adds

A translator from SMT.Term -> SMTDDM.Term as well as
A string converter from SMTDDM.Term -> String
Hooks the converter to SMT/DL/Encoder.lean, only when it is encoding a primitive term (as a small-step start!)
Adds the get-option SMT command and relevant syntax categories (mentioned in the previous pull request).
Slightly changes the .real constructor of the old SMT Term, from String to Decimal.

After 3, I checked the generated .smt2 files at vcs/ dir, and confirmed that they are equivalent modulo spaces! :)

There are a few features in the string converters that are unimplemented; they will be added later when Encoder.lean uses the DDM string converter more.

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

This patch adds a translator from SMT.Term to SMTDDM.Term, and also has a small code snippet that prints the SMTDDM.Term into the format. There are missing features, which will be addressed in the following commits. - Whitespaces must exist between the printed subterms(!) - Option types, triggers, real-number/bit-vector constants are left as unimplemented.

Strata/DL/SMT/DDMTransform/Translate.lean

…e new toString

Strata/DDM/Format.lean

aqjune-aws · 2025-11-06T20:42:57Z

Strata/DL/SMT/DDMTransform/Parse.lean

+// This collides with the ':named' term attribute. This file has the example.
+// op info_flag_name () : InfoFlag => ":name";
+op info_flag_reasonu () : InfoFlag => ":reason-unknown";
+op info_flag_version () : InfoFlag => ":version";


This and below are updates for the requested option related SMT commands.

Strata/DL/SMT/DDMTransform/Parse.lean

Strata/Languages/Boogie/DDMTransform/Parse.lean

StrataTest/Languages/C_Simp/Examples/Coprime.lean

…paces

…cimal_neg and sc_numeral_neg to separately treat negative numerals Note that negative integers like '-1231' are symbols in Std! (Sec 3.1. Lexicon) The only way to create a unary symbol is through idenitifers, but this makes its DDM format wrapped with pipes, like '|-1231|`. Since such representation cannot be recognized by Z3, make a workaround which is to have separate `*_neg` categories for sc_numeral.

aqjune-aws · 2026-01-02T22:34:25Z

Strata/DL/SMT/Term.lean

  | bool   : Bool → TermPrim
  | int    : Int → TermPrim
-  | real   : String → TermPrim
+  | real   : Decimal → TermPrim


This finally changes the argument of SMT .real term from String to Decimal!

…qX syntax categories to SMT DDM

MikaelMayer

I would like to be able to parse ":pattern" as well for quantifiers, I think that will be necessary to convert the B3 dialect.

MikaelMayer · 2026-01-05T12:23:25Z

Strata/DL/SMT/DDMTransform/Parse.lean

+// sign is not a part of the standard, but it seems CVC5 and Z3
+// support this for convenience.
+// Note that negative integers like '-1231' are symbols in Std! (Sec 3.1. Lexicon)
+// The only way to create a unary symbol is through idenitifers, but this


Suggested change

// The only way to create a unary symbol is through idenitifers, but this

// The only way to create a unary symbol is through identifiers, but this

Nice catch, thanks!

MikaelMayer · 2026-01-05T12:25:06Z

Strata/DL/SMT/DDMTransform/Parse.lean

+// The only way to create a unary symbol is through idenitifers, but this
+// makes its DDM format wrapped with pipes, like '|-1231|`. Since such
+// representation cannot be recognized by Z3, make a workaround which is to have
+// separate `*_neg` categories for sc_numeral.


That makes sense, same as for the + operator. Thanks for the clarification.

MikaelMayer · 2026-01-05T12:26:35Z

Strata/DL/SMT/DDMTransform/Parse.lean

 op se_keyword (s:Keyword) : SExpr => s;

-op se_ls (s:Seq SExpr) : SExpr => "(" s ")";
+category SeqPSExpr; // For spacing, P for "+"


Yeah, excellent workaround until we have a SpaceSepBy type one day (which I would approve)

MikaelMayer · 2026-01-05T12:27:32Z

Strata/DL/SMT/DDMTransform/Parse.lean



-// 3. Identifier
+// 3. Identifier. Use 'SMTIdentifier' because the 'Identifier' category is


Is this possible to move the declaration of category SMTIdentifier up so that it's just below this comment?

I moved this in the new commit.

MikaelMayer · 2026-01-05T12:29:09Z

Strata/DL/SMT/DDMTransform/Parse.lean

-op iden_simple (s:Symbol) : Identifier => s;
-op iden_indexed (s:Symbol, i0:Index, il:Seq Index) : Identifier =>
-  "(" "_" s i0 il ")";
+op iden_indexed (s:Symbol, si:SeqPIndex) : SMTIdentifier =>


What is the difference between SeqPSExpr and SeqPIndex? Since it's the concrete syntax tree, can we use only one of both?

It seems the existing syntax rule of Identifier is using <index>+ like this (page 102):

⟨identifier ⟩ ::= ⟨symbol ⟩ | ( _ ⟨symbol ⟩ ⟨index ⟩+ )

Probably SeqPSExpr will be a bit more general than SeqPIndex.

MikaelMayer · 2026-01-05T12:36:32Z

Strata/DL/SMT/Term.lean

  | .bool b₁, .bool b₂         => b₁ < b₂
  | .int  i₁, .int i₂          => i₁ < i₂
-  | .real r₁, .real r₂         => r₁ < r₂ -- TODO
+  | .real r₁, .real r₂         => r₁.toRat < r₂.toRat -- TODO


Is the TODO still applicable? If so, can you tell what the TODO is about, if not can you remove it?

MikaelMayer · 2026-01-05T12:40:00Z

Strata/DL/SMT/DDMTransform/Parse.lean

+op exists_smt (svs: SeqPSortedVar, t:Term) : Term =>
+  "(" "exists" "(" svs ")" t ")";
+op bang (t:Term, attrs:SeqPAttribute) : Term =>
+  "(" "!" t " " attrs ")";


Oh interesting how we can give parsing errors directly on these constructs rather than decoding general S-Expressions. I like it.

This also follows the definition of <term> category in the doc (link) . :) Page 103 has this.

aqjune-aws · 2026-01-05T17:01:01Z

I would like to be able to parse ":pattern" as well for quantifiers, I think that will be necessary to convert the B3 dialect.

I added an example that has :pattern. It seems there is no explicit Pattern syntax category in DDM, but it can still be still parsed as a part of Term.

joscoh · 2026-01-05T20:26:02Z

Strata/DL/SMT/DDMTransform/Parse.lean

 op declare_datatype (s:Symbol, so:SMTSort) : Command =>
-  "(" "declare-datatype" s so ")";
+  "(" "declare-datatype " s so ")";
 // TODO: declare-datatypes; what is ^(n+1)?


Not directly related to this PR, but I think it just means that there are k $\geq$ 1 datatype declarations following the declare-datatypes syntax.

Makes sense..! I will fix this in the following commit.

joscoh · 2026-01-05T20:42:18Z

Strata/DL/SMT/DDMTransform/Translate.lean

+      return .smtsort_param srnone (mkIdentifier id) argtys
+
+-- List of SortedVar to SeqPSortedVar.
+-- Hope this could be elided away later. :(


What do you mean by this being elided away? Maybe separately, this and the next function are basically the same thing, so they could be combined into something like the following:

def list_to_ne_gen {nelist : Type → Type} (single : α → nelist α) (cons: α → nelist α → nelist α) (l: List α) (Hl: ¬l.isEmpty = true) : nelist α := match h: l with | [] => by grind | [x] => single x | x :: y :: t => cons x (list_to_ne_gen single cons (y :: t) (by grind)) def list_to_optlist {nelist : Type → Type} (single : α → nelist α) (cons: α → nelist α → nelist α) (l: List α) : Option (nelist α) := if h: l.isEmpty then .none else .some (list_to_ne_gen single cons l h)

And then this can be instantiated for both functions. Not sure which is better, don't feel strongly one way or the other.

I meant I wanted to ~~have~~ remove these separate definitions of SeqP* to describe nonempty lists in DDM. :)
That being said, I think the 'SeqP' prefix doesn't seem straightforward to understand; I will fix SeqPSortedVar to SortedVarList.

This makes me think that it might be worth it to have a more convenient way to work with nonempty lists in the DDM. This shows up all over the place, including for datatype constructors.

…nt types

…ard 'List' suffix

shigoel · 2026-01-06T02:29:06Z

Strata/DL/SMT/DDMTransform/Parse.lean

Feel free to tackle this in a subsequent PR, but may I request you to add some file-level comments that describe what's going on in general in the file?
https://github.com/strata-org/Strata/blob/main/CONTRIBUTING.md#file-organization

Sure, I added one. :) I must have added this in advance to avoid making approvals stale :)

aqjune-aws commented Oct 31, 2025

View reviewed changes

Strata/DL/SMT/DDMTransform/Translate.lean Outdated Show resolved Hide resolved

Merge branch 'main' into jlee/smt2

c28190c

aqjune-aws mentioned this pull request Nov 3, 2025

Printer Program.toString misses whitespaces between terminals #179

Closed

aqjune-aws and others added 3 commits November 6, 2025 10:15

Merge branch 'main' into jlee/smt2

576cbdd

Update DDM formatter to insert spaces, hook DL/SMT/Encoder.lean to th…

1d5cb91

…e new toString

Update lake test targets

bf3ba56

aqjune-aws marked this pull request as ready for review November 6, 2025 20:42

aqjune-aws requested review from MikaelMayer, andrewmwells-amazon, atomb, joehendrix and shigoel as code owners November 6, 2025 20:42

aqjune-aws commented Nov 6, 2025

View reviewed changes

Strata/DDM/Format.lean Outdated Show resolved Hide resolved

aqjune-aws commented Nov 6, 2025

View reviewed changes

Strata/DL/SMT/DDMTransform/Parse.lean Show resolved Hide resolved

aqjune-aws commented Nov 6, 2025

View reviewed changes

Strata/Languages/Boogie/DDMTransform/Parse.lean Show resolved Hide resolved

aqjune-aws commented Nov 6, 2025

View reviewed changes

StrataTest/Languages/C_Simp/Examples/Coprime.lean Outdated Show resolved Hide resolved

aqjune-aws and others added 12 commits November 6, 2025 15:51

Merge branch 'main' into jlee/smt2

a800b54

Merge branch 'main' into jlee/smt2

fd8013c

Merge branch 'main' into jlee/smt2

003e703

consider new .regex, fix a bug in type printer

78169d3

Merge branch 'main' into jlee/smt2

7edd299

Merge branch 'main' into jlee/smt2

c080d18

Merge branch 'main' into jlee/smt2

4094735

Merge branch 'main' into jlee/smt2

a3dca73

Merge branch 'main' into jlee/smt2

dc6f2b9

Merge branch 'main' into jlee/smt2

dc0209a

Resolve failure

26bf6fb

Merge branch 'main' into jlee/smt2

78bc637

Turn a few DDM operations to have more visible option

f429a03

aqjune-aws force-pushed the jlee/smt2 branch from e3fe7bf to f429a03 Compare January 2, 2026 17:11

aqjune-aws requested a review from a team as a code owner January 2, 2026 17:11

aqjune-aws mentioned this pull request Jan 2, 2026

feat(DDM): Add pipe-delimited identifier support #285

Merged

aqjune-aws added 2 commits January 2, 2026 15:24

Smarter space insertion algorithm, update B3 grammar to avoid extra s…

3352cb0

…paces

aqjune-aws commented Jan 2, 2026

View reviewed changes

aqjune-aws added 2 commits January 2, 2026 16:39

Minor changes

5d287de

Rollback space insertion patch, bite the bullet and insert space & Se…

1f0ee9c

…qX syntax categories to SMT DDM

MikaelMayer requested changes Jan 5, 2026

View reviewed changes

Reflect comments

7337fe0

joscoh reviewed Jan 5, 2026

View reviewed changes

aqjune-aws added 2 commits January 5, 2026 15:57

Add declare-datatypes as well as examples, fix a few incorrect argume…

6fe591b

…nt types

Replace the 'SeqP' prefixes of syntax category with more straightforw…

1a541e3

…ard 'List' suffix

shigoel reviewed Jan 6, 2026

View reviewed changes

shigoel previously approved these changes Jan 6, 2026

View reviewed changes

joscoh previously approved these changes Jan 6, 2026

View reviewed changes

Add header comment

9e5751d

aqjune-aws dismissed stale reviews from joscoh and shigoel via 9e5751d January 6, 2026 15:51

aqjune-aws added 2 commits January 6, 2026 15:24

Merge branch 'main' into jlee/smt2

cba2e6f

Merge branch 'main' into jlee/smt2

cfc8a4a

	// The only way to create a unary symbol is through idenitifers, but this
	// The only way to create a unary symbol is through identifiers, but this



		// 3. Identifier
		// 3. Identifier. Use 'SMTIdentifier' because the 'Identifier' category is

Add a translator from SMT.Term to SMTDDM.Term #177

Are you sure you want to change the base?

Add a translator from SMT.Term to SMTDDM.Term #177

Conversation

aqjune-aws commented Oct 31, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

MikaelMayer left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

aqjune-aws commented Jan 5, 2026

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

joscoh Jan 5, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

aqjune-aws Jan 5, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

shigoel Jan 6, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

aqjune-aws commented Oct 31, 2025 •

edited

Loading

joscoh Jan 5, 2026 •

edited

Loading

aqjune-aws Jan 5, 2026 •

edited

Loading

shigoel Jan 6, 2026 •

edited

Loading