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
--- ----------------------------------------------------------------------------
--- This module provides a pretty printer for the SMT-LIB language (v2.6).
---
--- @author  Jan Tikovsky
--- @version August 2021
--- ----------------------------------------------------------------------------
module Language.SMTLIB.Pretty where

import Text.Pretty

import Language.SMTLIB.Types

--- Pretty print the given documents separated with spaces and parenthesized
parent :: [Doc] -> Doc
parent = encloseSep lparen rparen space

--- Show an SMT-LIB script
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) = dquotes $ 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

--- Pretty printing of booleans
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))]

--- Pretty printing of SMT-LIB commands.
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"