smtLib 1.0.7 → 1.0.8
raw patch · 4 files changed
+36/−22 lines, 4 files
Files
- smtLib.cabal +2/−2
- src/SMTLib1/AST.hs +16/−10
- src/SMTLib2/AST.hs +16/−10
- src/SMTLib2/PP.hs +2/−0
smtLib.cabal view
@@ -1,5 +1,5 @@ Name: smtLib-Version: 1.0.7+Version: 1.0.8 License: BSD3 License-file: LICENSE Author: Iavor S. Diatchki@@ -34,7 +34,7 @@ SMTLib2.PP build-depends:- base < 5,+ base >= 4.5 && < 5, pretty
src/SMTLib1/AST.hs view
@@ -8,22 +8,24 @@ -- URL: -- http://goedel.cs.uiowa.edu/smtlib/papers/format-v1.2-r06.08.05.pdf -{-# LANGUAGE OverloadedStrings, Safe #-}+{-# LANGUAGE OverloadedStrings, Safe, DeriveDataTypeable #-} module SMTLib1.AST where +import Data.Typeable+import Data.Data import Data.String(IsString(..)) newtype Name = N String- deriving (Eq,Ord,Show)+ deriving (Eq,Ord,Show,Data,Typeable) data Ident = I Name [Integer]- deriving (Eq,Ord,Show)+ deriving (Eq,Ord,Show,Data,Typeable) data Quant = Exists | Forall- deriving (Eq,Ord,Show)+ deriving (Eq,Ord,Show,Data,Typeable) data Conn = Not | Implies | And | Or | Xor | Iff | IfThenElse- deriving (Eq,Ord,Show)+ deriving (Eq,Ord,Show,Data,Typeable) data Formula = FTrue | FFalse@@ -34,40 +36,43 @@ | Let Name Term Formula | FLet Name Formula Formula | FAnnot Formula [Annot]- deriving (Eq,Ord,Show)+ deriving (Eq,Ord,Show,Data,Typeable) type Sort = Ident data Binder = Bind { bindVar :: Name, bindSort :: Sort }- deriving (Eq,Ord,Show)+ deriving (Eq,Ord,Show,Data,Typeable) data Term = Var Name | App Ident [Term] | Lit Literal | ITE Formula Term Term | TAnnot Term [Annot]- deriving (Eq,Ord,Show)+ deriving (Eq,Ord,Show,Data,Typeable) data Literal = LitNum Integer | LitFrac Rational | LitStr String- deriving (Eq,Ord,Show)+ deriving (Eq,Ord,Show,Data,Typeable) data Annot = Attr { attrName :: Name, attrVal :: Maybe String }- deriving (Eq,Ord,Show)+ deriving (Eq,Ord,Show,Data,Typeable) data FunDecl = FunDecl { funName :: Ident , funArgs :: [Sort] , funRes :: Sort , funAnnots :: [Annot] }+ deriving (Data,Typeable) data PredDecl = PredDecl { predName :: Ident , predArgs :: [Sort] , predAnnots :: [Annot] }+ deriving (Data,Typeable) data Status = Sat | Unsat | Unknown+ deriving (Data,Typeable) data Command = CmdLogic Ident@@ -79,6 +84,7 @@ | CmdExtraPreds [ PredDecl ] | CmdNotes String | CmdAnnot Annot+ deriving (Data,Typeable) -- aka "benchmark" data Script = Script { scrName :: Ident, scrCommands :: [Command] }
src/SMTLib2/AST.hs view
@@ -8,45 +8,47 @@ -- URL: -- http://goedel.cs.uiowa.edu/smtlib/papers/smt-lib-reference-v2.0-r10.12.21.pdf -{-# LANGUAGE OverloadedStrings, Safe #-}+{-# LANGUAGE OverloadedStrings, Safe, DeriveDataTypeable #-} module SMTLib2.AST where +import Data.Typeable+import Data.Data import Data.String(IsString(..)) newtype Name = N String- deriving (Eq,Ord,Show)+ deriving (Eq,Ord,Show,Data,Typeable) data Ident = I Name [Integer]- deriving (Eq,Ord,Show)+ deriving (Eq,Ord,Show,Data,Typeable) data Quant = Exists | Forall- deriving (Eq,Ord,Show)+ deriving (Eq,Ord,Show,Data,Typeable) data Binder = Bind { bindVar :: Name, bindType :: Type }- deriving (Eq,Ord,Show)+ deriving (Eq,Ord,Show,Data,Typeable) data Defn = Defn { defVar :: Name, defExpr :: Expr }- deriving (Eq,Ord,Show)+ deriving (Eq,Ord,Show,Data,Typeable) data Literal = LitBV Integer Integer -- ^ value, width (in bits) | LitNum Integer | LitFrac Rational | LitStr String- deriving (Eq,Ord,Show)+ deriving (Eq,Ord,Show,Data,Typeable) data Type = TApp Ident [Type] | TVar Name- deriving (Eq,Ord,Show)+ deriving (Eq,Ord,Show,Data,Typeable) data Expr = Lit Literal | App Ident (Maybe Type) [Expr] | Quant Quant [Binder] Expr | Let [Defn] Expr | Annot Expr [Attr]- deriving (Eq,Ord,Show)+ deriving (Eq,Ord,Show,Data,Typeable) data Attr = Attr { attrName :: Name , attrVal :: Maybe AttrVal }- deriving (Eq,Ord,Show)+ deriving (Eq,Ord,Show,Data,Typeable) type AttrVal = Expr -- A bit of an approximation.... @@ -64,6 +66,7 @@ | OptRandomSeed Integer | OptVerbosity Integer | OptAttr Attr+ deriving (Data,Typeable) data InfoFlag = InfoAllStatistics@@ -74,6 +77,7 @@ | InfoStatus | InfoReasonUnknown | InfoAttr Attr+ deriving (Data,Typeable) data Command = CmdSetLogic Name@@ -93,7 +97,9 @@ | CmdGetUnsatCore | CmdGetInfo InfoFlag | CmdGetOption Name+ | CmdComment String | CmdExit+ deriving (Data,Typeable) newtype Script = Script [Command]
src/SMTLib2/PP.hs view
@@ -156,11 +156,13 @@ CmdGetUnsatCore -> one "get-unsat-core" CmdGetInfo i -> std "get-info" i CmdGetOption n -> std "get-option" n+ CmdComment s -> vcat (map comment (lines s)) CmdExit -> one "exit" where mk x d = parens (text x <+> d) one x = mk x empty std x a = mk x (pp a) fun x y as d = mk x (pp y <+> parens (fsep (map pp as)) <+> d)+ comment s = text ";" <+> text s instance PP Script where pp (Script cs) = vcat (map pp cs)