CurryInfo: smtlib-3.0.0 / Language.SMTLIB.ppCmd

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]

argument 1

deterministic operation

--- Pretty printing of SMT-LIB commands.

{Assert,CheckSat,CheckSatAssuming,DeclareConst,DeclareDatatype,DeclareDatatypes,DeclareFun,DeclareSort,DefineFun,DefineFunRec,DefineFunsRec,DefineSort,Echo,Exit,GetAssertions,GetAssignment,GetInfo,GetModel,GetOption,GetProof,GetUnsatAssumptions,GetUnsatCore,GetValue,Pop,Push,Reset,ResetAssertions,SetInfo,SetLogic,SetOption}

referentially transparent operation

no fixity defined

{({Assert}) |-> {:} || ({CheckSat}) |-> {:} || ({CheckSatAssuming}) |-> {:} || ({DeclareConst}) |-> {:} || ({DeclareDatatype}) |-> {:} || ({DeclareDatatypes}) |-> {:} || ({DeclareFun}) |-> {:} || ({DeclareSort}) |-> {:} || ({DefineFun}) |-> {:} || ({DefineFunRec}) |-> {:} || ({DefineFunsRec}) |-> {:} || ({DefineSort}) |-> {:} || ({Echo}) |-> {:} || ({Exit}) |-> {:} || ({GetAssertions}) |-> {:} || ({GetAssignment}) |-> {:} || ({GetInfo}) |-> {:} || ({GetModel}) |-> {:} || ({GetOption}) |-> {:} || ({GetProof}) |-> {:} || ({GetUnsatAssumptions}) |-> {:} || ({GetUnsatCore}) |-> {:} || ({GetValue}) |-> {:} || ({Pop}) |-> {:} || ({Push}) |-> {:} || ({Reset}) |-> {:} || ({ResetAssertions}) |-> {:} || ({SetInfo}) |-> {:} || ({SetLogic}) |-> {:} || ({SetOption}) |-> {:}}

ppCmd

no precedence defined

{:}

Language.SMTLIB.Types.Command -> [Text.PrettyImpl.Doc]

operation might suspend on free variables

possibly non-terminating

possibly non-reducible on same data term