1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
|
module Language.SMTLIB.Pretty where
import Text.Pretty
import Language.SMTLIB.Types
parent :: [Doc] -> Doc
parent = encloseSep lparen rparen space
showSMT :: [Command] -> String
showSMT = pPrint . pretty . SMTLib
instance Pretty SMTLib where
pretty (SMTLib cmds) = vsep (map pretty cmds)
instance Pretty Keyword where
pretty (KW sym) = colon <> text sym
instance Pretty SpecConstant where
pretty (Num n) = int n
pretty (Dec f) = float f
pretty (Str s) = text s
instance Pretty SExpr where
pretty (SEConst c) = pretty c
pretty (SESym sym) = text sym
pretty (SEKW k) = pretty k
pretty (SEList ses) = parent (map pretty ses)
instance Pretty Sort where
pretty (SComb i ss) = parensIf (not $ null ss) $
text i <+> (hsep (map pretty ss))
instance Pretty AttrValue where
pretty (AVConst c) = pretty c
pretty (AVSym sym) = text sym
pretty (AVSExpr ses) = parent (map pretty ses)
instance Pretty Attribute where
pretty (AKW k) = pretty k
pretty (AVal k v) = pretty k <+> pretty v
instance Pretty QIdent where
pretty (Id i) = text i
pretty (As i s) = parent [text "as", text i, pretty s]
instance Pretty SortedVar where
pretty (SV sym s) = parent [text sym, pretty s]
instance Pretty Pattern where
pretty (PComb sym ss) = parensIf (not $ null ss) (hsep (map text (sym:ss)))
instance Pretty Term where
pretty (TConst c) = pretty c
pretty (TComb qi ts) = parensIf (not $ null ts) $
pretty qi <+> (hsep (map pretty ts))
pretty (Let bs t) = parent [text "let", parent (map ppBind bs), pretty t]
where ppBind (sym, t') = parent [text sym, pretty t']
pretty (Forall svs t) = parent [ text "forall"
, parent (map pretty svs)
, pretty t
]
pretty (Exists svs t) = parent [ text "exists"
, parent (map pretty svs)
, pretty t
]
pretty (Match t bs) = parent [ text "match"
, pretty t
, parent (map ppBranch bs)
]
where ppBranch (p, bt) = parent [pretty p, pretty bt]
pretty (Annot t as) = parent [char '!', pretty t, hsep (map pretty as)]
instance Pretty SortSymDecl where
pretty (SortSymDecl i n as) = parent [text i, int n, hsep (map pretty as)]
instance Pretty MetaSpecConstant where
pretty = text . show
instance Pretty FunSymDecl where
pretty (Spec c s as) = parent [pretty c, pretty s, hsep (map pretty as)]
pretty (Meta c s as) = parent [pretty c, pretty s, hsep (map pretty as)]
pretty (Ident i ss as) = parent [ text i, hsep (map pretty ss)
, hsep (map pretty as)
]
instance Pretty ParFunSymDecl where
pretty (ParFunSymDecl f syms i ss as) = pretty f <+>
parent [ text "par"
, parent (map text syms)
, parent [text i, hsep (map pretty ss), hsep (map pretty as)]]
instance Pretty TheoryAttr where
pretty (TASorts sdecls) = text ":sorts" <+> parent (map pretty sdecls)
pretty (TAFuns pdecls) = text ":funs" <+> parent (map pretty pdecls)
pretty (TASortsDesc str) = text ":sorts-description" <+> text str
pretty (TAFunsDesc str) = text ":funs-description" <+> text str
pretty (TADefinition str) = text ":definition" <+> text str
pretty (TAValues str) = text ":values" <+> text str
pretty (TANotes str) = text ":notes" <+> text str
pretty (TA a) = pretty a
instance Pretty Theory where
pretty (Theory sym tas) = parent [ text "theory"
, text sym, hsep (map pretty tas)
]
instance Pretty InfoFlag where
pretty AllStatistics = text ":all-statistics"
pretty AssertionStackLevels = text ":assertion-stack-levels"
pretty Authors = text ":authors"
pretty ErrorBehavior = text ":error-behavior"
pretty Name = text ":name"
pretty ReasonUnknown = text ":reason-unknown"
pretty Version = text ":version"
pretty (IFKW k) = pretty k
instance Pretty Option where
pretty (DiagnosticOutput s) = text ":diagnostic-output-channel" <+> text s
pretty (GlobalDecls b) = text ":global-declarations" <+> ppBool b
pretty (Interactive b) = text ":interactive-mode" <+> ppBool b
pretty (PrintSuccess b) = text ":print-success" <+> ppBool b
pretty (ProduceAssertions b) = text ":produce-assertions" <+> ppBool b
pretty (ProduceAssign b) = text ":produce-assignments" <+> ppBool b
pretty (ProduceModels b) = text ":produce-models" <+> ppBool b
pretty (ProduceProofs b) = text ":produce-proofs" <+> ppBool b
pretty (ProduceUnsatAssump b) = text ":produce-unsat-assumptions" <+> ppBool b
pretty (ProduceUnsatCores b) = text ":produce-unsat-cores" <+> ppBool b
pretty (RandomSeed n) = text ":random-seed" <+> int n
pretty (RegularOutput s) = text ":regular-output-channel" <+> text s
pretty (ReproducibleResLimit n) = text ":reproducible-resource-limit" <+> int n
pretty (Verbosity n) = text ":verbosity" <+> int n
pretty (OptAttr a) = pretty a
ppBool :: Bool -> Doc
ppBool True = text "true"
ppBool False = text "false"
instance Pretty FunDec where
pretty (FunDec sym svs s) = parent [ text sym, parent (map pretty svs)
, pretty s
]
instance Pretty FunDef where
pretty (FunDef sym svs s t) = parent [ text sym, parent (map pretty svs)
, pretty s, pretty t
]
instance Pretty PropLit where
pretty (Sym sym) = text sym
pretty (Not sym) = parent [text "not", text sym]
instance Pretty Command where
pretty cmd = case cmd of
Comment comment -> semi <+> text comment
_ -> parent $ ppCmd cmd
instance Pretty SortDecl where
pretty (SortDecl sym a) = parent [text sym, int a]
instance Pretty DTDecl where
pretty (MT cs) = parent (map pretty cs)
pretty (PT tys cs) = parent [ text "par"
, parent (map text tys)
, parent (map pretty cs)
]
instance Pretty ConsDecl where
pretty (Cons sym svs) = parent [text sym, (hsep (map pretty svs))]
ppCmd :: Command -> [Doc]
ppCmd (Assert t) = [text "assert", pretty t]
ppCmd CheckSat = [text "check-sat"]
ppCmd (CheckSatAssuming ps) = [ text "check-sat-assuming"
, parent (map pretty ps)
]
ppCmd (DeclareConst sym s) = [text "declare-const", text sym, pretty s]
ppCmd (DeclareDatatype s d) = [ text "declare-datatype"
, text s
, pretty d
]
ppCmd (DeclareDatatypes sds) = let (ss, ds) = unzip sds in
[ text "declare-datatypes"
, parent (map pretty ss)
, parent (map pretty ds)
]
ppCmd (DeclareFun sym ss s) = [ text "declare-fun"
, text sym
, parent (map pretty ss)
, pretty s
]
ppCmd (DeclareSort sym n) = [text "declare-sort", text sym, int n]
ppCmd (DefineFun f) = [text "define-fun", pretty f]
ppCmd (DefineFunRec f) = [text "define-fun-rec", pretty f]
ppCmd (DefineFunsRec fts) = let (fs, ts) = unzip fts in
[ text "define-funs-rec"
, parent (map pretty fs)
, parent (map pretty ts)
]
ppCmd (DefineSort sym syms s) = [text sym, parent (map text syms), pretty s]
ppCmd (Echo str) = [text "echo", dquotes (text str)]
ppCmd Exit = [text "exit"]
ppCmd GetAssertions = [text "get-assertions"]
ppCmd GetAssignment = [text "get-assignment"]
ppCmd (GetInfo flag) = [text "get-info", pretty flag]
ppCmd GetModel = [text "get-model"]
ppCmd (GetOption opt) = [text "get-option", pretty opt]
ppCmd GetProof = [text "get-proof"]
ppCmd GetUnsatAssumptions = [text "get-unsat-assumptions"]
ppCmd GetUnsatCore = [text "get-unsat-core"]
ppCmd (GetValue ts) = [text "get-value", parent (map pretty ts)]
ppCmd (Pop lvl) = [text "pop", int lvl]
ppCmd (Push lvl) = [text "push", int lvl]
ppCmd Reset = [text "reset"]
ppCmd ResetAssertions = [text "reset-assertions"]
ppCmd (SetInfo a) = [text "set-info", pretty a]
ppCmd (SetLogic l) = [text "set-logic", pretty l]
ppCmd (SetOption opt) = [text "set-option", pretty opt]
instance Pretty Logic where
pretty ALL = text "ALL"
pretty AUFLIA = text "AUFLIA"
pretty AUFLIRA = text "AUFLIRA"
pretty AUFNIRA = text "AUFNIRA"
pretty LIA = text "LIA"
pretty LRA = text "LRA"
pretty QFABV = text "QF_ABV"
pretty QFAUFBV = text "QF_AUFBV"
pretty QFAUFLIA = text "QF_AUFLIA"
pretty QFAX = text "QF_AX"
pretty QFBV = text "QF_BV"
pretty QFIDL = text "QF_IDL"
pretty QFLIA = text "QF_LIA"
pretty QFLRA = text "QF_LRA"
pretty QFNIA = text "QF_NIA"
pretty QFNRA = text "QF_NRA"
pretty QFRDL = text "QF_RDL"
pretty QFUF = text "QF_UF"
pretty QFUFBV = text "QF_UFBV"
pretty QFUFIDL = text "QF_UFIDL"
pretty QFUFLIA = text "QF_UFLIA"
pretty QFUFLRA = text "QF_UFLRA"
pretty QFUFNRA = text "QF_UFNRA"
pretty UFLRA = text "UFLRA"
pretty UFNIA = text "UFNIA"
instance Pretty ErrorBehavior where
pretty ImmediateExit = text "immediate-exit"
pretty ContinuedExecution = text "continued-execution"
instance Pretty ReasonUnknown where
pretty Memout = text "memout"
pretty Incomplete = text "incomplete"
pretty (SEReason se) = pretty se
instance Pretty ModelRsp where
pretty (MRFun f) = parent [text "define-fun", pretty f]
pretty (MRFunRec f) = parent [text "define-fun-rec", pretty f]
pretty (MRFunsRec fts) = let (fs, ts) = unzip fts
in parent [ text "define-funs-rec"
, parent (map pretty fs)
, parent (map pretty ts)
]
instance Pretty InfoRsp where
pretty (AssertionStackLevelsRsp n) = text ":assertion-stack-levels" <+> int n
pretty (AuthorsRsp str) = text ":authors" <+> text str
pretty (ErrorBehaviorRsp eb) = text ":error-behavior" <+> pretty eb
pretty (NameRsp str) = text ":name" <+> text str
pretty (ReasonUnknownRsp ru) = text ":reason-unknown" <+> pretty ru
pretty (VersionRsp str) = text ":version" <+> text str
pretty (AttrRsp a) = pretty a
ppValPair :: ValuationPair -> Doc
ppValPair (t1, t2) = parent [pretty t1, pretty t2]
instance Pretty CmdResponse where
pretty SuccessRsp = text "success"
pretty UnsupportedRsp = text "unsupported"
pretty (ErrorRsp str) = parens (text "error"
<+> dquotes (text str))
pretty (CheckSatRsp cs) = pretty cs
pretty (EchoRsp str) = text str
pretty (GetAssertionsRsp ts) = parent (map pretty ts)
pretty (GetAssignmentRsp tvs) = parent (map ppTValPair tvs)
where ppTValPair (sym, b) = parent [text sym, ppBool b]
pretty (GetInfoRsp is) = parent (map pretty is)
pretty (GetModelRsp ms) = parent (map pretty ms)
pretty (GetOptionRsp av) = pretty av
pretty (GetProofRsp se) = pretty se
pretty (GetUnsatAssumptionsRsp syms) = parent (map text syms)
pretty (GetUnsatCoreRsp syms) = parent (map text syms)
pretty (GetValueRsp vs) = parent (map ppValPair vs)
instance Pretty CheckSat where
pretty Sat = text "sat"
pretty Unsat = text "unsat"
pretty Unknown = text "unknown"
|