Skip to content

Commit f9f3059

Browse files
kjcjohnsonkjcjohnson
committed
Annotations on sexpr output
1 parent 8956eeb commit f9f3059

1 file changed

Lines changed: 113 additions & 60 deletions

File tree

‎SemgusParser/Sexpr/SmtTermWriter.cs‎

Lines changed: 113 additions & 60 deletions
Original file line numberDiff line numberDiff line change
@@ -18,73 +18,117 @@ public SmtTermWriter(ISexprWriter sw)
1818
_sw = sw;
1919
}
2020

21+
/// <summary>
22+
/// Wraps an annotation block around the current term, if necessary
23+
/// </summary>
24+
/// <param name="term">Term to write annotations for, if any</param>
25+
/// <param name="inner">Action to call for writing the term</param>
26+
private void MaybeWriteAnnotations(SmtTerm term, Action inner)
27+
{
28+
if (term.Annotations != null && term.Annotations.Count > 0)
29+
{
30+
_sw.WriteList(() =>
31+
{
32+
_sw.WriteSymbol("annotated");
33+
inner();
34+
foreach (var ann in term.Annotations)
35+
{
36+
_sw.WriteString(ann.Keyword.Name);
37+
_sw.Write(ann.Value);
38+
}
39+
});
40+
}
41+
else
42+
{
43+
inner();
44+
}
45+
}
46+
2147
public ISexprWriter VisitBitVectorLiteral(SmtBitVectorLiteral bitVectorLiteral)
2248
{
23-
_sw.WriteBitVector(bitVectorLiteral.Value);
49+
MaybeWriteAnnotations(bitVectorLiteral, () =>
50+
{
51+
_sw.WriteBitVector(bitVectorLiteral.Value);
52+
});
2453
return _sw;
2554
}
2655

2756
public ISexprWriter VisitDecimalLiteral(SmtDecimalLiteral decimalLiteral)
2857
{
29-
_sw.WriteDecimal(decimalLiteral.Value);
58+
MaybeWriteAnnotations(decimalLiteral, () =>
59+
{
60+
_sw.WriteDecimal(decimalLiteral.Value);
61+
});
3062
return _sw;
3163
}
3264

3365
public ISexprWriter VisitExistsBinder(SmtExistsBinder existsBinder)
3466
{
35-
_sw.WriteList(() =>
67+
MaybeWriteAnnotations(existsBinder, () =>
3668
{
37-
_sw.WriteSymbol("exists");
38-
_sw.WriteKeyword("bindings");
39-
_sw.WriteList(existsBinder.NewScope.LocalBindings, b => _sw.Write(b.Id));
40-
_sw.WriteKeyword("binding-sorts");
41-
_sw.WriteList(existsBinder.NewScope.LocalBindings, b => _sw.Write(b.Sort.Name));
42-
_sw.WriteKeyword("child");
43-
existsBinder.Child.Accept(this);
69+
_sw.WriteList(() =>
70+
{
71+
_sw.WriteSymbol("exists");
72+
_sw.WriteKeyword("bindings");
73+
_sw.WriteList(existsBinder.NewScope.LocalBindings, b => _sw.Write(b.Id));
74+
_sw.WriteKeyword("binding-sorts");
75+
_sw.WriteList(existsBinder.NewScope.LocalBindings, b => _sw.Write(b.Sort.Name));
76+
_sw.WriteKeyword("child");
77+
existsBinder.Child.Accept(this);
78+
});
4479
});
4580
return _sw;
4681
}
4782

4883
public ISexprWriter VisitForallBinder(SmtForallBinder forallBinder)
4984
{
50-
_sw.WriteList(() =>
85+
MaybeWriteAnnotations(forallBinder, () =>
5186
{
52-
_sw.WriteSymbol("forall");
53-
_sw.WriteKeyword("bindings");
54-
_sw.WriteList(forallBinder.NewScope.LocalBindings, b => _sw.Write(b.Id));
55-
_sw.WriteKeyword("binding-sorts");
56-
_sw.WriteList(forallBinder.NewScope.LocalBindings, b => _sw.Write(b.Sort.Name));
57-
_sw.WriteKeyword("child");
58-
forallBinder.Child.Accept(this);
87+
_sw.WriteList(() =>
88+
{
89+
_sw.WriteSymbol("forall");
90+
_sw.WriteKeyword("bindings");
91+
_sw.WriteList(forallBinder.NewScope.LocalBindings, b => _sw.Write(b.Id));
92+
_sw.WriteKeyword("binding-sorts");
93+
_sw.WriteList(forallBinder.NewScope.LocalBindings, b => _sw.Write(b.Sort.Name));
94+
_sw.WriteKeyword("child");
95+
forallBinder.Child.Accept(this);
96+
});
5997
});
6098
return _sw;
6199
}
62100

63101
public ISexprWriter VisitFunctionApplication(SmtFunctionApplication functionApplication)
64102
{
65-
_sw.WriteList(() =>
103+
MaybeWriteAnnotations(functionApplication, () =>
66104
{
67-
_sw.WriteSymbol("application");
68-
_sw.Write(functionApplication.Definition.Name);
69-
_sw.WriteKeyword("argument-sorts");
70-
_sw.WriteList(functionApplication.Rank.ArgumentSorts, s => _sw.Write(s.Name));
71-
_sw.WriteKeyword("arguments");
72-
_sw.WriteList(functionApplication.Arguments, a => a.Accept(this));
73-
_sw.WriteKeyword("return-sort");
74-
_sw.Write(functionApplication.Rank.ReturnSort.Name);
105+
_sw.WriteList(() =>
106+
{
107+
_sw.WriteSymbol("application");
108+
_sw.Write(functionApplication.Definition.Name);
109+
_sw.WriteKeyword("argument-sorts");
110+
_sw.WriteList(functionApplication.Rank.ArgumentSorts, s => _sw.Write(s.Name));
111+
_sw.WriteKeyword("arguments");
112+
_sw.WriteList(functionApplication.Arguments, a => a.Accept(this));
113+
_sw.WriteKeyword("return-sort");
114+
_sw.Write(functionApplication.Rank.ReturnSort.Name);
115+
});
75116
});
76117
return _sw;
77118
}
78119

79120
public ISexprWriter VisitLambdaBinder(SmtLambdaBinder lambdaBinder)
80121
{
81-
_sw.WriteList(() =>
122+
MaybeWriteAnnotations(lambdaBinder, () =>
82123
{
83-
_sw.WriteSymbol("lambda");
84-
_sw.WriteKeyword("arguments");
85-
_sw.WriteList(lambdaBinder.ArgumentNames, an => _sw.Write(an));
86-
_sw.WriteKeyword("body");
87-
lambdaBinder.Child.Accept(this);
124+
_sw.WriteList(() =>
125+
{
126+
_sw.WriteSymbol("lambda");
127+
_sw.WriteKeyword("arguments");
128+
_sw.WriteList(lambdaBinder.ArgumentNames, an => _sw.Write(an));
129+
_sw.WriteKeyword("body");
130+
lambdaBinder.Child.Accept(this);
131+
});
88132
});
89133
return _sw;
90134
}
@@ -96,59 +140,68 @@ public ISexprWriter VisitLetBinder(SmtLetBinder letBinder)
96140

97141
public ISexprWriter VisitMatchBinder(SmtMatchBinder matchBinder)
98142
{
99-
_sw.WriteList(() =>
143+
MaybeWriteAnnotations(matchBinder, () =>
100144
{
101-
_sw.WriteSymbol("binder");
102-
_sw.WriteKeyword("operator");
103-
if (matchBinder.Constructor is null)
104-
{
105-
_sw.WriteNil();
106-
}
107-
else
145+
_sw.WriteList(() =>
108146
{
109-
_sw.Write(matchBinder.Constructor.Name);
110-
}
111-
_sw.WriteKeyword("arguments");
112-
_sw.WriteList(matchBinder.Bindings, b => _sw.Write(b.Binding.Id));
113-
_sw.WriteKeyword("child");
114-
matchBinder.Child.Accept(this);
147+
_sw.WriteSymbol("binder");
148+
_sw.WriteKeyword("operator");
149+
if (matchBinder.Constructor is null)
150+
{
151+
_sw.WriteNil();
152+
}
153+
else
154+
{
155+
_sw.Write(matchBinder.Constructor.Name);
156+
}
157+
_sw.WriteKeyword("arguments");
158+
_sw.WriteList(matchBinder.Bindings, b => _sw.Write(b.Binding.Id));
159+
_sw.WriteKeyword("child");
160+
matchBinder.Child.Accept(this);
161+
});
115162
});
116163
return _sw;
117164
}
118165

119166
public ISexprWriter VisitMatchGrouper(SmtMatchGrouper matchGrouper)
120167
{
121-
_sw.WriteList(() =>
168+
MaybeWriteAnnotations(matchGrouper, () =>
122169
{
123-
_sw.WriteSymbol("match");
124-
_sw.WriteKeyword("term");
125-
matchGrouper.Term.Accept(this);
126-
_sw.WriteKeyword("binders");
127-
_sw.WriteList(matchGrouper.Binders, b => b.Accept(this));
170+
_sw.WriteList(() =>
171+
{
172+
_sw.WriteSymbol("match");
173+
_sw.WriteKeyword("term");
174+
matchGrouper.Term.Accept(this);
175+
_sw.WriteKeyword("binders");
176+
_sw.WriteList(matchGrouper.Binders, b => b.Accept(this));
177+
});
128178
});
129179
return _sw;
130180
}
131181

132182
public ISexprWriter VisitNumeralLiteral(SmtNumeralLiteral numeralLiteral)
133183
{
134-
_sw.WriteNumeral(numeralLiteral.Value);
184+
MaybeWriteAnnotations(numeralLiteral, () => { _sw.WriteNumeral(numeralLiteral.Value); });
135185
return _sw;
136186
}
137187

138188
public ISexprWriter VisitStringLiteral(SmtStringLiteral stringLiteral)
139189
{
140-
_sw.WriteString(stringLiteral.Value);
190+
MaybeWriteAnnotations(stringLiteral, () => { _sw.WriteString(stringLiteral.Value); });
141191
return _sw;
142192
}
143193

144194
public ISexprWriter VisitVariable(SmtVariable variable)
145195
{
146-
_sw.WriteList(() =>
196+
MaybeWriteAnnotations(variable, () =>
147197
{
148-
_sw.WriteSymbol("variable");
149-
_sw.Write(variable.Name);
150-
_sw.WriteKeyword("sort");
151-
_sw.Write(variable.Sort.Name);
198+
_sw.WriteList(() =>
199+
{
200+
_sw.WriteSymbol("variable");
201+
_sw.Write(variable.Name);
202+
_sw.WriteKeyword("sort");
203+
_sw.Write(variable.Sort.Name);
204+
});
152205
});
153206
return _sw;
154207
}

0 commit comments

Comments
 (0)