Safe Haskell	Safe
Language	Haskell2010

Sygus.Syntax

Documentation

data Lit Source #

Constructors

LitNum Integer
LitDec String
LitBool Bool
Hexidecimal String
Binary String
LitStr String

Instances

Eq Lit Source #
Instance details Defined in Sygus.Syntax Methods (==) :: Lit -> Lit -> Bool # (/=) :: Lit -> Lit -> Bool #
Read Lit Source #
Instance details Defined in Sygus.Syntax Methods readsPrec :: Int -> ReadS Lit # readList :: ReadS [Lit] # readPrec :: ReadPrec Lit # readListPrec :: ReadPrec [Lit] #
Show Lit Source #
Instance details Defined in Sygus.Syntax Methods showsPrec :: Int -> Lit -> ShowS # show :: Lit -> String # showList :: [Lit] -> ShowS #

type Symbol = String Source #

data Cmd Source #

Instances

Eq Cmd Source #
Instance details Defined in Sygus.Syntax Methods (==) :: Cmd -> Cmd -> Bool # (/=) :: Cmd -> Cmd -> Bool #
Read Cmd Source #
Instance details Defined in Sygus.Syntax Methods readsPrec :: Int -> ReadS Cmd # readList :: ReadS [Cmd] # readPrec :: ReadPrec Cmd # readListPrec :: ReadPrec [Cmd] #
Show Cmd Source #
Instance details Defined in Sygus.Syntax Methods showsPrec :: Int -> Cmd -> ShowS # show :: Cmd -> String # showList :: [Cmd] -> ShowS #

data Identifier Source #

Constructors

ISymb Symbol
Indexed Symbol [Index]

Instances

Eq Identifier Source #
Instance details Defined in Sygus.Syntax Methods (==) :: Identifier -> Identifier -> Bool # (/=) :: Identifier -> Identifier -> Bool #
Read Identifier Source #
Instance details Defined in Sygus.Syntax Methods readsPrec :: Int -> ReadS Identifier # readList :: ReadS [Identifier] # readPrec :: ReadPrec Identifier # readListPrec :: ReadPrec [Identifier] #
Show Identifier Source #
Instance details Defined in Sygus.Syntax Methods showsPrec :: Int -> Identifier -> ShowS # show :: Identifier -> String # showList :: [Identifier] -> ShowS #

data Index Source #

Constructors

IndNumeral Integer
IndSymb Symbol

Instances

Eq Index Source #
Instance details Defined in Sygus.Syntax Methods (==) :: Index -> Index -> Bool # (/=) :: Index -> Index -> Bool #
Read Index Source #
Instance details Defined in Sygus.Syntax Methods readsPrec :: Int -> ReadS Index # readList :: ReadS [Index] # readPrec :: ReadPrec Index # readListPrec :: ReadPrec [Index] #
Show Index Source #
Instance details Defined in Sygus.Syntax Methods showsPrec :: Int -> Index -> ShowS # show :: Index -> String # showList :: [Index] -> ShowS #

data Sort Source #

Constructors

IdentSort Identifier
IdentSortSort Identifier [Sort]

Instances

Eq Sort Source #
Instance details Defined in Sygus.Syntax Methods (==) :: Sort -> Sort -> Bool # (/=) :: Sort -> Sort -> Bool #
Read Sort Source #
Instance details Defined in Sygus.Syntax Methods readsPrec :: Int -> ReadS Sort # readList :: ReadS [Sort] # readPrec :: ReadPrec Sort # readListPrec :: ReadPrec [Sort] #
Show Sort Source #
Instance details Defined in Sygus.Syntax Methods showsPrec :: Int -> Sort -> ShowS # show :: Sort -> String # showList :: [Sort] -> ShowS #

data Term Source #

Constructors

TermIdent Identifier
TermLit Lit
TermCall Identifier [Term]
TermExists [SortedVar] Term
TermForAll [SortedVar] Term
TermLet [VarBinding] Term

Instances

Eq Term Source #
Instance details Defined in Sygus.Syntax Methods (==) :: Term -> Term -> Bool # (/=) :: Term -> Term -> Bool #
Read Term Source #
Instance details Defined in Sygus.Syntax Methods readsPrec :: Int -> ReadS Term # readList :: ReadS [Term] # readPrec :: ReadPrec Term # readListPrec :: ReadPrec [Term] #
Show Term Source #
Instance details Defined in Sygus.Syntax Methods showsPrec :: Int -> Term -> ShowS # show :: Term -> String # showList :: [Term] -> ShowS #

data BfTerm Source #

Constructors

BfIdentifier Identifier
BfLiteral Lit
BfIdentifierBfs Identifier [BfTerm]

Instances

Eq BfTerm Source #
Instance details Defined in Sygus.Syntax Methods (==) :: BfTerm -> BfTerm -> Bool # (/=) :: BfTerm -> BfTerm -> Bool #
Read BfTerm Source #
Instance details Defined in Sygus.Syntax Methods readsPrec :: Int -> ReadS BfTerm # readList :: ReadS [BfTerm] # readPrec :: ReadPrec BfTerm # readListPrec :: ReadPrec [BfTerm] #
Show BfTerm Source #
Instance details Defined in Sygus.Syntax Methods showsPrec :: Int -> BfTerm -> ShowS # show :: BfTerm -> String # showList :: [BfTerm] -> ShowS #

data SortedVar Source #

Constructors

SortedVar Symbol Sort

Instances

Eq SortedVar Source #
Instance details Defined in Sygus.Syntax Methods (==) :: SortedVar -> SortedVar -> Bool # (/=) :: SortedVar -> SortedVar -> Bool #
Read SortedVar Source #
Instance details Defined in Sygus.Syntax Methods readsPrec :: Int -> ReadS SortedVar # readList :: ReadS [SortedVar] # readPrec :: ReadPrec SortedVar # readListPrec :: ReadPrec [SortedVar] #
Show SortedVar Source #
Instance details Defined in Sygus.Syntax Methods showsPrec :: Int -> SortedVar -> ShowS # show :: SortedVar -> String # showList :: [SortedVar] -> ShowS #

data VarBinding Source #

Constructors

VarBinding Symbol Term

Instances

Eq VarBinding Source #
Instance details Defined in Sygus.Syntax Methods (==) :: VarBinding -> VarBinding -> Bool # (/=) :: VarBinding -> VarBinding -> Bool #
Read VarBinding Source #
Instance details Defined in Sygus.Syntax Methods readsPrec :: Int -> ReadS VarBinding # readList :: ReadS [VarBinding] # readPrec :: ReadPrec VarBinding # readListPrec :: ReadPrec [VarBinding] #
Show VarBinding Source #
Instance details Defined in Sygus.Syntax Methods showsPrec :: Int -> VarBinding -> ShowS # show :: VarBinding -> String # showList :: [VarBinding] -> ShowS #

data Feature Source #

Constructors

Grammars
FwdDecls
Recursion

Instances

Eq Feature Source #
Instance details Defined in Sygus.Syntax Methods (==) :: Feature -> Feature -> Bool # (/=) :: Feature -> Feature -> Bool #
Read Feature Source #
Instance details Defined in Sygus.Syntax Methods readsPrec :: Int -> ReadS Feature # readList :: ReadS [Feature] # readPrec :: ReadPrec Feature # readListPrec :: ReadPrec [Feature] #
Show Feature Source #
Instance details Defined in Sygus.Syntax Methods showsPrec :: Int -> Feature -> ShowS # show :: Feature -> String # showList :: [Feature] -> ShowS #

data SmtCmd Source #

Instances

Eq SmtCmd Source #
Instance details Defined in Sygus.Syntax Methods (==) :: SmtCmd -> SmtCmd -> Bool # (/=) :: SmtCmd -> SmtCmd -> Bool #
Read SmtCmd Source #
Instance details Defined in Sygus.Syntax Methods readsPrec :: Int -> ReadS SmtCmd # readList :: ReadS [SmtCmd] # readPrec :: ReadPrec SmtCmd # readListPrec :: ReadPrec [SmtCmd] #
Show SmtCmd Source #
Instance details Defined in Sygus.Syntax Methods showsPrec :: Int -> SmtCmd -> ShowS # show :: SmtCmd -> String # showList :: [SmtCmd] -> ShowS #

data SortDecl Source #

Constructors

SortDecl Symbol Integer

Instances

Eq SortDecl Source #
Instance details Defined in Sygus.Syntax Methods (==) :: SortDecl -> SortDecl -> Bool # (/=) :: SortDecl -> SortDecl -> Bool #
Read SortDecl Source #
Instance details Defined in Sygus.Syntax Methods readsPrec :: Int -> ReadS SortDecl # readList :: ReadS [SortDecl] # readPrec :: ReadPrec SortDecl # readListPrec :: ReadPrec [SortDecl] #
Show SortDecl Source #
Instance details Defined in Sygus.Syntax Methods showsPrec :: Int -> SortDecl -> ShowS # show :: SortDecl -> String # showList :: [SortDecl] -> ShowS #

data DTDec Source #

Constructors

DTDec [DTConsDec]

Instances

Eq DTDec Source #
Instance details Defined in Sygus.Syntax Methods (==) :: DTDec -> DTDec -> Bool # (/=) :: DTDec -> DTDec -> Bool #
Read DTDec Source #
Instance details Defined in Sygus.Syntax Methods readsPrec :: Int -> ReadS DTDec # readList :: ReadS [DTDec] # readPrec :: ReadPrec DTDec # readListPrec :: ReadPrec [DTDec] #
Show DTDec Source #
Instance details Defined in Sygus.Syntax Methods showsPrec :: Int -> DTDec -> ShowS # show :: DTDec -> String # showList :: [DTDec] -> ShowS #

data DTConsDec Source #

Constructors

DTConsDec Symbol [SortedVar]

Instances

Eq DTConsDec Source #
Instance details Defined in Sygus.Syntax Methods (==) :: DTConsDec -> DTConsDec -> Bool # (/=) :: DTConsDec -> DTConsDec -> Bool #
Read DTConsDec Source #
Instance details Defined in Sygus.Syntax Methods readsPrec :: Int -> ReadS DTConsDec # readList :: ReadS [DTConsDec] # readPrec :: ReadPrec DTConsDec # readListPrec :: ReadPrec [DTConsDec] #
Show DTConsDec Source #
Instance details Defined in Sygus.Syntax Methods showsPrec :: Int -> DTConsDec -> ShowS # show :: DTConsDec -> String # showList :: [DTConsDec] -> ShowS #

data GrammarDef Source #

Constructors

GrammarDef [SortedVar] [GroupedRuleList]

Instances

Eq GrammarDef Source #
Instance details Defined in Sygus.Syntax Methods (==) :: GrammarDef -> GrammarDef -> Bool # (/=) :: GrammarDef -> GrammarDef -> Bool #
Read GrammarDef Source #
Instance details Defined in Sygus.Syntax Methods readsPrec :: Int -> ReadS GrammarDef # readList :: ReadS [GrammarDef] # readPrec :: ReadPrec GrammarDef # readListPrec :: ReadPrec [GrammarDef] #
Show GrammarDef Source #
Instance details Defined in Sygus.Syntax Methods showsPrec :: Int -> GrammarDef -> ShowS # show :: GrammarDef -> String # showList :: [GrammarDef] -> ShowS #

data GroupedRuleList Source #

Constructors

GroupedRuleList Symbol Sort [GTerm]

Instances

Eq GroupedRuleList Source #
Instance details Defined in Sygus.Syntax Methods (==) :: GroupedRuleList -> GroupedRuleList -> Bool # (/=) :: GroupedRuleList -> GroupedRuleList -> Bool #
Read GroupedRuleList Source #
Instance details Defined in Sygus.Syntax Methods readsPrec :: Int -> ReadS GroupedRuleList # readList :: ReadS [GroupedRuleList] # readPrec :: ReadPrec GroupedRuleList # readListPrec :: ReadPrec [GroupedRuleList] #
Show GroupedRuleList Source #
Instance details Defined in Sygus.Syntax Methods showsPrec :: Int -> GroupedRuleList -> ShowS # show :: GroupedRuleList -> String # showList :: [GroupedRuleList] -> ShowS #

data GTerm Source #

Constructors

GConstant Sort
GVariable Sort
GBfTerm BfTerm

Instances

Eq GTerm Source #
Instance details Defined in Sygus.Syntax Methods (==) :: GTerm -> GTerm -> Bool # (/=) :: GTerm -> GTerm -> Bool #
Read GTerm Source #
Instance details Defined in Sygus.Syntax Methods readsPrec :: Int -> ReadS GTerm # readList :: ReadS [GTerm] # readPrec :: ReadPrec GTerm # readListPrec :: ReadPrec [GTerm] #
Show GTerm Source #
Instance details Defined in Sygus.Syntax Methods showsPrec :: Int -> GTerm -> ShowS # show :: GTerm -> String # showList :: [GTerm] -> ShowS #

CheckSynth
Constraint Term
DeclareVar Symbol Sort
InvConstraint Symbol Symbol Symbol Symbol
SetFeature Feature Bool
SynthFun Symbol [SortedVar] Sort (Maybe GrammarDef)
SynthInv Symbol [SortedVar] (Maybe GrammarDef)
SmtCmd SmtCmd

DeclareDatatype Symbol DTDec
DeclareDatatypes [SortDecl] [DTDec]
DeclareSort Symbol Integer
DefineFun Symbol [SortedVar] Sort Term
DefineSort Symbol Sort
SetLogic Symbol
SetOption Symbol Lit