module Smtlib.Syntax.ShowSL where
import Data.List
import Smtlib.Syntax.Syntax
joinA ::(ShowSL a) => [a] -> String
joinA = unwords.fmap showSL
joinNs :: [Int] -> String
joinNs = unwords.fmap show
class ShowSL a where
showSL :: a -> String
instance ShowSL Command where
showSL (SetLogic s) = "(set-logic " ++ s ++ ")"
showSL (SetOption opt) = "(set-option " ++ showSL opt ++ ")"
showSL (SetInfo info) = "(set-info " ++ showSL info ++ ")"
showSL (DeclareSort str val) = "(declare-sort " ++ str ++
" " ++ show val ++ ")"
showSL (DefineSort str strs sort) = "(define-sort " ++ str ++
" (" ++ unwords strs ++ ") " ++ showSL sort ++ ") "
showSL (DeclareFun str sorts sort) = "(declare-fun " ++ str ++
" (" ++ joinA sorts ++ ") " ++ showSL sort ++ ") "
showSL (DefineFun str srvs sort term) = "( define-fun " ++ str ++
" (" ++ joinA srvs ++ ") " ++ showSL sort ++ " " ++ showSL term ++ ")"
showSL (Push n) = "(push " ++ show n ++ ")"
showSL (Pop n) = "(pop " ++show n ++ ")"
showSL (Assert term) = "(assert " ++ showSL term ++ ")"
showSL CheckSat = "(check-sat)"
showSL GetAssertions = "(get-assertions)"
showSL GetProof = "(get-proof)"
showSL GetUnsatCore = "(get-unsat-core)"
showSL (GetValue terms) = "( (" ++ joinA terms ++ ") )"
showSL GetAssignment = "(get-assignment)"
showSL (GetOption opt) = "(get-option " ++ opt ++ ")"
showSL (GetInfo info) = "(get-info " ++ showSL info ++ ")"
showSL Exit = "(exit)"
instance ShowSL Option where
showSL (PrintSucess b) = ":print-sucess " ++ show b
showSL (ExpandDefinitions b) = ":expand-definitions " ++ show b
showSL (InteractiveMode b) = ":interactive-mode " ++ show b
showSL (ProduceProofs b) = ":produce-proofs " ++ show b
showSL (ProduceUnsatCores b) = ":produce-unsat-cores " ++ show b
showSL (ProduceModels b) = ":produce-models " ++ show b
showSL (ProduceAssignments b) = ":produce-assignments " ++ show b
showSL (RegularOutputChannel s) = ":regular-output-channel " ++ s
showSL (DiagnosticOutputChannel s) = ":diagnostic-output-channel " ++ s
showSL (RandomSeed n) = ":random-seed " ++ show n
showSL (Verbosity n) = ":verbosity'" ++ show n
showSL (OptionAttr attr) = showSL attr
instance ShowSL InfoFlags where
showSL ErrorBehavior = ":error-behavior"
showSL Name = ":name"
showSL Authors = ":authors"
showSL Version = ":version"
showSL Status = ":status"
showSL ReasonUnknown = ":reason-unknown"
showSL AllStatistics = ":all-statistics"
showSL (InfoFlags s) = s
instance ShowSL Term where
showSL (TermSpecConstant sc) = showSL sc
showSL (TermQualIdentifier qi) = showSL qi
showSL (TermQualIdentifierT qi terms) =
"(" ++ showSL qi ++ " " ++ joinA terms ++ ")"
showSL (TermLet vb term) =
"(let (" ++ joinA vb ++ ") " ++ showSL term ++ ")"
showSL (TermForall svs term) =
"(forall (" ++ joinA svs ++ " ) " ++ showSL term ++ ")"
showSL (TermExists svs term) =
"(exists (" ++ joinA svs ++ " ) " ++ showSL term ++ ")"
showSL (TermAnnot term atts) =
"(! " ++ showSL term ++ " " ++ joinA atts ++ ")"
instance ShowSL VarBinding where
showSL (VB str term) = "("++ show str ++ " " ++ showSL term ++ ")"
instance ShowSL SortedVar where
showSL (SV str sort) = "(" ++ show str ++ " " ++ showSL sort ++ ")"
instance ShowSL QualIdentifier where
showSL (QIdentifier iden) = showSL iden
showSL (QIdentifierAs iden sort) =
"(as " ++ showSL iden ++ " " ++ showSL sort ++ ")"
instance ShowSL AttrValue where
showSL (AttrValueConstant spc) = showSL spc
showSL (AttrValueSymbol str) = str
showSL (AttrValueSexpr sexprs) = "(" ++ joinA sexprs ++ ")"
instance ShowSL Attribute where
showSL (Attribute str) = str
showSL (AttributeVal str attrVal) = str ++ " " ++ showSL attrVal
instance ShowSL Identifier where
showSL (ISymbol str) = str
showSL (I_Symbol str ns) = "( _ " ++ str ++ " " ++ joinNs ns ++ ")"
instance ShowSL Sort where
showSL (SortId iden) = showSL iden
showSL (SortIdentifiers iden sorts) =
"(" ++ show iden ++ " " ++ joinA sorts ++ ")"
instance ShowSL SpecConstant where
showSL (SpecConstantNumeral n) = show n
showSL (SpecConstantDecimal str) = str
showSL (SpecConstantHexadecimal str) = str
showSL (SpecConstantBinary str) = str
showSL (SpecConstantString str) = str
instance ShowSL Sexpr where
showSL (SexprSpecConstant sc) = showSL sc
showSL (SexprSymbol str) = str
showSL (SexprKeyword str) = str
showSL (SexprSxp srps) = "(" ++ joinA srps ++ ")"
instance ShowSL CmdResponse where
showSL (CmdGenResponse x) = showSL x
showSL (CmdGetInfoResponse x) = "(" ++ joinA x ++ ")"
showSL (CmdCheckSatResponse x) = showSL x
showSL (CmdGetAssertionsResponse x) = "(" ++ joinA x ++ ")"
showSL (CmdGetAssignmentResponse x) = "(" ++ joinA x ++ ")"
showSL (CmdGetProofResponse x) = showSL x
showSL (CmdGetUnsatCoreResponse x) = "(" ++ unwords x ++ ")"
showSL (CmdGetValueResponse x) = "(" ++ joinA x ++ ")"
showSL (CmdGetOptionResponse x) = showSL x
instance ShowSL GenResponse where
showSL Unsupported = "unsupported"
showSL Success = "Success"
showSL (Error s) = "(error " ++ s ++ ")"
instance ShowSL ErrorBehavior where
showSL ImmediateExit = "immediate-exit"
showSL ContinuedExecution = "continued-execution"
instance ShowSL ReasonUnknown where
showSL Memout = "memout"
showSL Incomplete = "imcomplete"
instance ShowSL CheckSatResponse where
showSL Sat = "sat"
showSL Unsat = "unsat"
showSL Unknown = "unknown"
instance ShowSL InfoResponse where
showSL (ResponseErrorBehavior x) = ":error-behaviour " ++ showSL x
showSL (ResponseName s) = ":name " ++ s
showSL (ResponseAuthors s) = ":authors " ++ s
showSL (ResponseVersion s) = ":version" ++ s
showSL (ResponseReasonUnknown x) = ":reason-unknown " ++ showSL x
showSL (ResponseAttribute x) = showSL x
instance ShowSL ValuationPair where
showSL (ValuationPair term1 term2) =
"(" ++ showSL term1 ++ " " ++ showSL term2 ++ ")"
instance ShowSL TValuationPair where
showSL (TValuationPair str b) = "(" ++ str ++ " " ++ show b ++ ")"