Sygus.Syntax

Documentation

data Lit

Constructors

LitNum Integer

LitDec Integer Integer

LitBool Bool

Hexidecimal String

Binary String

LitStr String

Instances

Generic Lit

Defined in Sygus.Syntax

Associated Types

type Rep Lit :: Type -> Type

Methods

from :: Lit -> Rep Lit x

to :: Rep Lit x -> Lit

Read Lit

Defined in Sygus.Syntax

Methods

readsPrec :: Int -> ReadS Lit

readList :: ReadS [Lit]

readPrec :: ReadPrec Lit

readListPrec :: ReadPrec [Lit]

Show Lit

Defined in Sygus.Syntax

Methods

showsPrec :: Int -> Lit -> ShowS

show :: Lit -> String

showList :: [Lit] -> ShowS

Eq Lit

Defined in Sygus.Syntax

Methods

(==) :: Lit -> Lit -> Bool

(/=) :: Lit -> Lit -> Bool

Hashable Lit

Defined in Sygus.Syntax

Methods

hashWithSalt :: Int -> Lit -> Int

hash :: Lit -> Int

type Rep Lit

Defined in Sygus.Syntax

type Rep Lit = D1 ('MetaData "Lit" "Sygus.Syntax" "language-sygus-0.1.1.3-8ANx6Jkwy2873RS2baX0uE" 'False) ((C1 ('MetaCons "LitNum" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Integer)) :+: (C1 ('MetaCons "LitDec" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Integer) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Integer)) :+: C1 ('MetaCons "LitBool" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)))) :+: (C1 ('MetaCons "Hexidecimal" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)) :+: (C1 ('MetaCons "Binary" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)) :+: C1 ('MetaCons "LitStr" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)))))

type Symbol = String

data Cmd

Constructors

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

Instances

Generic Cmd

Defined in Sygus.Syntax

Associated Types

type Rep Cmd :: Type -> Type

Methods

from :: Cmd -> Rep Cmd x

to :: Rep Cmd x -> Cmd

Read Cmd

Defined in Sygus.Syntax

Methods

readsPrec :: Int -> ReadS Cmd

readList :: ReadS [Cmd]

readPrec :: ReadPrec Cmd

readListPrec :: ReadPrec [Cmd]

Show Cmd

Defined in Sygus.Syntax

Methods

showsPrec :: Int -> Cmd -> ShowS

show :: Cmd -> String

showList :: [Cmd] -> ShowS

Eq Cmd

Defined in Sygus.Syntax

Methods

(==) :: Cmd -> Cmd -> Bool

(/=) :: Cmd -> Cmd -> Bool

Hashable Cmd

Defined in Sygus.Syntax

Methods

hashWithSalt :: Int -> Cmd -> Int

hash :: Cmd -> Int

type Rep Cmd

Defined in Sygus.Syntax

type Rep Cmd = D1 ('MetaData "Cmd" "Sygus.Syntax" "language-sygus-0.1.1.3-8ANx6Jkwy2873RS2baX0uE" 'False) (((C1 ('MetaCons "CheckSynth" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Constraint" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term))) :+: (C1 ('MetaCons "DeclareVar" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Symbol) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Sort)) :+: C1 ('MetaCons "InvConstraint" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Symbol) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Symbol)) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Symbol) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Symbol))))) :+: ((C1 ('MetaCons "SetFeature" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Feature) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)) :+: C1 ('MetaCons "SynthFun" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Symbol) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [SortedVar])) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Sort) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe GrammarDef))))) :+: (C1 ('MetaCons "SynthInv" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Symbol) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [SortedVar]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe GrammarDef)))) :+: C1 ('MetaCons "SmtCmd" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 SmtCmd)))))

data Identifier

Constructors

ISymb Symbol

Indexed Symbol [Index]

Instances

Generic Identifier

Defined in Sygus.Syntax

Associated Types

type Rep Identifier :: Type -> Type

Methods

from :: Identifier -> Rep Identifier x

to :: Rep Identifier x -> Identifier

Read Identifier

Defined in Sygus.Syntax

Methods

readsPrec :: Int -> ReadS Identifier

readList :: ReadS [Identifier]

readPrec :: ReadPrec Identifier

readListPrec :: ReadPrec [Identifier]

Show Identifier

Defined in Sygus.Syntax

Methods

showsPrec :: Int -> Identifier -> ShowS

show :: Identifier -> String

showList :: [Identifier] -> ShowS

Eq Identifier

Defined in Sygus.Syntax

Methods

(==) :: Identifier -> Identifier -> Bool

(/=) :: Identifier -> Identifier -> Bool

Hashable Identifier

Defined in Sygus.Syntax

Methods

hashWithSalt :: Int -> Identifier -> Int

hash :: Identifier -> Int

type Rep Identifier

Defined in Sygus.Syntax

type Rep Identifier = D1 ('MetaData "Identifier" "Sygus.Syntax" "language-sygus-0.1.1.3-8ANx6Jkwy2873RS2baX0uE" 'False) (C1 ('MetaCons "ISymb" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Symbol)) :+: C1 ('MetaCons "Indexed" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Symbol) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Index])))

data Index

Constructors

IndNumeral Integer

IndSymb Symbol

Instances

Generic Index

Defined in Sygus.Syntax

Associated Types

type Rep Index :: Type -> Type

Methods

from :: Index -> Rep Index x

to :: Rep Index x -> Index

Read Index

Defined in Sygus.Syntax

Methods

readsPrec :: Int -> ReadS Index

readList :: ReadS [Index]

readPrec :: ReadPrec Index

readListPrec :: ReadPrec [Index]

Show Index

Defined in Sygus.Syntax

Methods

showsPrec :: Int -> Index -> ShowS

show :: Index -> String

showList :: [Index] -> ShowS

Eq Index

Defined in Sygus.Syntax

Methods

(==) :: Index -> Index -> Bool

(/=) :: Index -> Index -> Bool

Hashable Index

Defined in Sygus.Syntax

Methods

hashWithSalt :: Int -> Index -> Int

hash :: Index -> Int

type Rep Index

Defined in Sygus.Syntax

type Rep Index = D1 ('MetaData "Index" "Sygus.Syntax" "language-sygus-0.1.1.3-8ANx6Jkwy2873RS2baX0uE" 'False) (C1 ('MetaCons "IndNumeral" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Integer)) :+: C1 ('MetaCons "IndSymb" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Symbol)))

data Sort

Constructors

IdentSort Identifier

IdentSortSort Identifier [Sort]

Instances

Generic Sort

Defined in Sygus.Syntax

Associated Types

type Rep Sort :: Type -> Type

Methods

from :: Sort -> Rep Sort x

to :: Rep Sort x -> Sort

Read Sort

Defined in Sygus.Syntax

Methods

readsPrec :: Int -> ReadS Sort

readList :: ReadS [Sort]

readPrec :: ReadPrec Sort

readListPrec :: ReadPrec [Sort]

Show Sort

Defined in Sygus.Syntax

Methods

showsPrec :: Int -> Sort -> ShowS

show :: Sort -> String

showList :: [Sort] -> ShowS

Eq Sort

Defined in Sygus.Syntax

Methods

(==) :: Sort -> Sort -> Bool

(/=) :: Sort -> Sort -> Bool

Hashable Sort

Defined in Sygus.Syntax

Methods

hashWithSalt :: Int -> Sort -> Int

hash :: Sort -> Int

type Rep Sort

Defined in Sygus.Syntax

type Rep Sort = D1 ('MetaData "Sort" "Sygus.Syntax" "language-sygus-0.1.1.3-8ANx6Jkwy2873RS2baX0uE" 'False) (C1 ('MetaCons "IdentSort" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Identifier)) :+: C1 ('MetaCons "IdentSortSort" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Identifier) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Sort])))

data Term

Constructors

TermIdent Identifier

TermLit Lit

TermCall Identifier [Term]

TermExists [SortedVar] Term

TermForAll [SortedVar] Term

TermLet [VarBinding] Term

Instances

Generic Term

Defined in Sygus.Syntax

Associated Types

type Rep Term :: Type -> Type

Methods

from :: Term -> Rep Term x

to :: Rep Term x -> Term

Read Term

Defined in Sygus.Syntax

Methods

readsPrec :: Int -> ReadS Term

readList :: ReadS [Term]

readPrec :: ReadPrec Term

readListPrec :: ReadPrec [Term]

Show Term

Defined in Sygus.Syntax

Methods

showsPrec :: Int -> Term -> ShowS

show :: Term -> String

showList :: [Term] -> ShowS

Eq Term

Defined in Sygus.Syntax

Methods

(==) :: Term -> Term -> Bool

(/=) :: Term -> Term -> Bool

Hashable Term

Defined in Sygus.Syntax

Methods

hashWithSalt :: Int -> Term -> Int

hash :: Term -> Int

type Rep Term

Defined in Sygus.Syntax

type Rep Term = D1 ('MetaData "Term" "Sygus.Syntax" "language-sygus-0.1.1.3-8ANx6Jkwy2873RS2baX0uE" 'False) ((C1 ('MetaCons "TermIdent" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Identifier)) :+: (C1 ('MetaCons "TermLit" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Lit)) :+: C1 ('MetaCons "TermCall" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Identifier) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Term])))) :+: (C1 ('MetaCons "TermExists" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [SortedVar]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term)) :+: (C1 ('MetaCons "TermForAll" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [SortedVar]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term)) :+: C1 ('MetaCons "TermLet" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [VarBinding]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term)))))

data BfTerm

Constructors

BfIdentifier Identifier

BfLiteral Lit

BfIdentifierBfs Identifier [BfTerm]

Instances

Generic BfTerm

Defined in Sygus.Syntax

Associated Types

type Rep BfTerm :: Type -> Type

Methods

from :: BfTerm -> Rep BfTerm x

to :: Rep BfTerm x -> BfTerm

Read BfTerm

Defined in Sygus.Syntax

Methods

readsPrec :: Int -> ReadS BfTerm

readList :: ReadS [BfTerm]

readPrec :: ReadPrec BfTerm

readListPrec :: ReadPrec [BfTerm]

Show BfTerm

Defined in Sygus.Syntax

Methods

showsPrec :: Int -> BfTerm -> ShowS

show :: BfTerm -> String

showList :: [BfTerm] -> ShowS

Eq BfTerm

Defined in Sygus.Syntax

Methods

(==) :: BfTerm -> BfTerm -> Bool

(/=) :: BfTerm -> BfTerm -> Bool

Hashable BfTerm

Defined in Sygus.Syntax

Methods

hashWithSalt :: Int -> BfTerm -> Int

hash :: BfTerm -> Int

type Rep BfTerm

Defined in Sygus.Syntax

type Rep BfTerm = D1 ('MetaData "BfTerm" "Sygus.Syntax" "language-sygus-0.1.1.3-8ANx6Jkwy2873RS2baX0uE" 'False) (C1 ('MetaCons "BfIdentifier" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Identifier)) :+: (C1 ('MetaCons "BfLiteral" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Lit)) :+: C1 ('MetaCons "BfIdentifierBfs" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Identifier) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [BfTerm]))))

data SortedVar

Constructors

SortedVar Symbol Sort

Instances

Generic SortedVar

Defined in Sygus.Syntax

Associated Types

type Rep SortedVar :: Type -> Type

Methods

from :: SortedVar -> Rep SortedVar x

to :: Rep SortedVar x -> SortedVar

Read SortedVar

Defined in Sygus.Syntax

Methods

readsPrec :: Int -> ReadS SortedVar

readList :: ReadS [SortedVar]

readPrec :: ReadPrec SortedVar

readListPrec :: ReadPrec [SortedVar]

Show SortedVar

Defined in Sygus.Syntax

Methods

showsPrec :: Int -> SortedVar -> ShowS

show :: SortedVar -> String

showList :: [SortedVar] -> ShowS

Eq SortedVar

Defined in Sygus.Syntax

Methods

(==) :: SortedVar -> SortedVar -> Bool

(/=) :: SortedVar -> SortedVar -> Bool

Hashable SortedVar

Defined in Sygus.Syntax

Methods

hashWithSalt :: Int -> SortedVar -> Int

hash :: SortedVar -> Int

type Rep SortedVar

Defined in Sygus.Syntax

type Rep SortedVar = D1 ('MetaData "SortedVar" "Sygus.Syntax" "language-sygus-0.1.1.3-8ANx6Jkwy2873RS2baX0uE" 'False) (C1 ('MetaCons "SortedVar" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Symbol) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Sort)))

data VarBinding

Constructors

VarBinding Symbol Term

Instances

Generic VarBinding

Defined in Sygus.Syntax

Associated Types

type Rep VarBinding :: Type -> Type

Methods

from :: VarBinding -> Rep VarBinding x

to :: Rep VarBinding x -> VarBinding

Read VarBinding

Defined in Sygus.Syntax

Methods

readsPrec :: Int -> ReadS VarBinding

readList :: ReadS [VarBinding]

readPrec :: ReadPrec VarBinding

readListPrec :: ReadPrec [VarBinding]

Show VarBinding

Defined in Sygus.Syntax

Methods

showsPrec :: Int -> VarBinding -> ShowS

show :: VarBinding -> String

showList :: [VarBinding] -> ShowS

Eq VarBinding

Defined in Sygus.Syntax

Methods

(==) :: VarBinding -> VarBinding -> Bool

(/=) :: VarBinding -> VarBinding -> Bool

Hashable VarBinding

Defined in Sygus.Syntax

Methods

hashWithSalt :: Int -> VarBinding -> Int

hash :: VarBinding -> Int

type Rep VarBinding

Defined in Sygus.Syntax

type Rep VarBinding = D1 ('MetaData "VarBinding" "Sygus.Syntax" "language-sygus-0.1.1.3-8ANx6Jkwy2873RS2baX0uE" 'False) (C1 ('MetaCons "VarBinding" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Symbol) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term)))

data Feature

Constructors

Grammars

FwdDecls

Recursion

Instances

Generic Feature

Defined in Sygus.Syntax

Associated Types

type Rep Feature :: Type -> Type

Methods

from :: Feature -> Rep Feature x

to :: Rep Feature x -> Feature

Read Feature

Defined in Sygus.Syntax

Methods

readsPrec :: Int -> ReadS Feature

readList :: ReadS [Feature]

readPrec :: ReadPrec Feature

readListPrec :: ReadPrec [Feature]

Show Feature

Defined in Sygus.Syntax

Methods

showsPrec :: Int -> Feature -> ShowS

show :: Feature -> String

showList :: [Feature] -> ShowS

Eq Feature

Defined in Sygus.Syntax

Methods

(==) :: Feature -> Feature -> Bool

(/=) :: Feature -> Feature -> Bool

Hashable Feature

Defined in Sygus.Syntax

Methods

hashWithSalt :: Int -> Feature -> Int

hash :: Feature -> Int

type Rep Feature

Defined in Sygus.Syntax

type Rep Feature = D1 ('MetaData "Feature" "Sygus.Syntax" "language-sygus-0.1.1.3-8ANx6Jkwy2873RS2baX0uE" 'False) (C1 ('MetaCons "Grammars" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "FwdDecls" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Recursion" 'PrefixI 'False) (U1 :: Type -> Type)))

data SmtCmd

Constructors

DeclareDatatype Symbol DTDec

DeclareDatatypes [SortDecl] [DTDec]

DeclareSort Symbol Integer

DefineFun Symbol [SortedVar] Sort Term

DefineSort Symbol Sort

SetLogic Symbol

SetOption Symbol Lit

Instances

Generic SmtCmd

Defined in Sygus.Syntax

Associated Types

type Rep SmtCmd :: Type -> Type

Methods

from :: SmtCmd -> Rep SmtCmd x

to :: Rep SmtCmd x -> SmtCmd

Read SmtCmd

Defined in Sygus.Syntax

Methods

readsPrec :: Int -> ReadS SmtCmd

readList :: ReadS [SmtCmd]

readPrec :: ReadPrec SmtCmd

readListPrec :: ReadPrec [SmtCmd]

Show SmtCmd

Defined in Sygus.Syntax

Methods

showsPrec :: Int -> SmtCmd -> ShowS

show :: SmtCmd -> String

showList :: [SmtCmd] -> ShowS

Eq SmtCmd

Defined in Sygus.Syntax

Methods

(==) :: SmtCmd -> SmtCmd -> Bool

(/=) :: SmtCmd -> SmtCmd -> Bool

Hashable SmtCmd

Defined in Sygus.Syntax

Methods

hashWithSalt :: Int -> SmtCmd -> Int

hash :: SmtCmd -> Int

type Rep SmtCmd

Defined in Sygus.Syntax

type Rep SmtCmd = D1 ('MetaData "SmtCmd" "Sygus.Syntax" "language-sygus-0.1.1.3-8ANx6Jkwy2873RS2baX0uE" 'False) ((C1 ('MetaCons "DeclareDatatype" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Symbol) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 DTDec)) :+: (C1 ('MetaCons "DeclareDatatypes" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [SortDecl]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [DTDec])) :+: C1 ('MetaCons "DeclareSort" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Symbol) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Integer)))) :+: ((C1 ('MetaCons "DefineFun" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Symbol) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [SortedVar])) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Sort) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term))) :+: C1 ('MetaCons "DefineSort" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Symbol) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Sort))) :+: (C1 ('MetaCons "SetLogic" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Symbol)) :+: C1 ('MetaCons "SetOption" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Symbol) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Lit)))))

data SortDecl

Constructors

SortDecl Symbol Integer

Instances

Generic SortDecl

Defined in Sygus.Syntax

Associated Types

type Rep SortDecl :: Type -> Type

Methods

from :: SortDecl -> Rep SortDecl x

to :: Rep SortDecl x -> SortDecl

Read SortDecl

Defined in Sygus.Syntax

Methods

readsPrec :: Int -> ReadS SortDecl

readList :: ReadS [SortDecl]

readPrec :: ReadPrec SortDecl

readListPrec :: ReadPrec [SortDecl]

Show SortDecl

Defined in Sygus.Syntax

Methods

showsPrec :: Int -> SortDecl -> ShowS

show :: SortDecl -> String

showList :: [SortDecl] -> ShowS

Eq SortDecl

Defined in Sygus.Syntax

Methods

(==) :: SortDecl -> SortDecl -> Bool

(/=) :: SortDecl -> SortDecl -> Bool

Hashable SortDecl

Defined in Sygus.Syntax

Methods

hashWithSalt :: Int -> SortDecl -> Int

hash :: SortDecl -> Int

type Rep SortDecl

Defined in Sygus.Syntax

type Rep SortDecl = D1 ('MetaData "SortDecl" "Sygus.Syntax" "language-sygus-0.1.1.3-8ANx6Jkwy2873RS2baX0uE" 'False) (C1 ('MetaCons "SortDecl" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Symbol) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Integer)))

data DTDec

Constructors

DTDec [DTConsDec]

Instances

Generic DTDec

Defined in Sygus.Syntax

Associated Types

type Rep DTDec :: Type -> Type

Methods

from :: DTDec -> Rep DTDec x

to :: Rep DTDec x -> DTDec

Read DTDec

Defined in Sygus.Syntax

Methods

readsPrec :: Int -> ReadS DTDec

readList :: ReadS [DTDec]

readPrec :: ReadPrec DTDec

readListPrec :: ReadPrec [DTDec]

Show DTDec

Defined in Sygus.Syntax

Methods

showsPrec :: Int -> DTDec -> ShowS

show :: DTDec -> String

showList :: [DTDec] -> ShowS

Eq DTDec

Defined in Sygus.Syntax

Methods

(==) :: DTDec -> DTDec -> Bool

(/=) :: DTDec -> DTDec -> Bool

Hashable DTDec

Defined in Sygus.Syntax

Methods

hashWithSalt :: Int -> DTDec -> Int

hash :: DTDec -> Int

type Rep DTDec

Defined in Sygus.Syntax

type Rep DTDec = D1 ('MetaData "DTDec" "Sygus.Syntax" "language-sygus-0.1.1.3-8ANx6Jkwy2873RS2baX0uE" 'False) (C1 ('MetaCons "DTDec" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [DTConsDec])))

data DTConsDec

Constructors

DTConsDec Symbol [SortedVar]

Instances

Generic DTConsDec

Defined in Sygus.Syntax

Associated Types

type Rep DTConsDec :: Type -> Type

Methods

from :: DTConsDec -> Rep DTConsDec x

to :: Rep DTConsDec x -> DTConsDec

Read DTConsDec

Defined in Sygus.Syntax

Methods

readsPrec :: Int -> ReadS DTConsDec

readList :: ReadS [DTConsDec]

readPrec :: ReadPrec DTConsDec

readListPrec :: ReadPrec [DTConsDec]

Show DTConsDec

Defined in Sygus.Syntax

Methods

showsPrec :: Int -> DTConsDec -> ShowS

show :: DTConsDec -> String

showList :: [DTConsDec] -> ShowS

Eq DTConsDec

Defined in Sygus.Syntax

Methods

(==) :: DTConsDec -> DTConsDec -> Bool

(/=) :: DTConsDec -> DTConsDec -> Bool

Hashable DTConsDec

Defined in Sygus.Syntax

Methods

hashWithSalt :: Int -> DTConsDec -> Int

hash :: DTConsDec -> Int

type Rep DTConsDec

Defined in Sygus.Syntax

type Rep DTConsDec = D1 ('MetaData "DTConsDec" "Sygus.Syntax" "language-sygus-0.1.1.3-8ANx6Jkwy2873RS2baX0uE" 'False) (C1 ('MetaCons "DTConsDec" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Symbol) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [SortedVar])))

data GrammarDef

Constructors

GrammarDef [SortedVar] [GroupedRuleList]

Instances

Generic GrammarDef

Defined in Sygus.Syntax

Associated Types

type Rep GrammarDef :: Type -> Type

Methods

from :: GrammarDef -> Rep GrammarDef x

to :: Rep GrammarDef x -> GrammarDef

Read GrammarDef

Defined in Sygus.Syntax

Methods

readsPrec :: Int -> ReadS GrammarDef

readList :: ReadS [GrammarDef]

readPrec :: ReadPrec GrammarDef

readListPrec :: ReadPrec [GrammarDef]

Show GrammarDef

Defined in Sygus.Syntax

Methods

showsPrec :: Int -> GrammarDef -> ShowS

show :: GrammarDef -> String

showList :: [GrammarDef] -> ShowS

Eq GrammarDef

Defined in Sygus.Syntax

Methods

(==) :: GrammarDef -> GrammarDef -> Bool

(/=) :: GrammarDef -> GrammarDef -> Bool

Hashable GrammarDef

Defined in Sygus.Syntax

Methods

hashWithSalt :: Int -> GrammarDef -> Int

hash :: GrammarDef -> Int

type Rep GrammarDef

Defined in Sygus.Syntax

type Rep GrammarDef = D1 ('MetaData "GrammarDef" "Sygus.Syntax" "language-sygus-0.1.1.3-8ANx6Jkwy2873RS2baX0uE" 'False) (C1 ('MetaCons "GrammarDef" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [SortedVar]) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [GroupedRuleList])))

data GroupedRuleList

Constructors

GroupedRuleList Symbol Sort [GTerm]

Instances

Generic GroupedRuleList

Defined in Sygus.Syntax

Associated Types

type Rep GroupedRuleList :: Type -> Type

Methods

from :: GroupedRuleList -> Rep GroupedRuleList x

to :: Rep GroupedRuleList x -> GroupedRuleList

Read GroupedRuleList

Defined in Sygus.Syntax

Methods

readsPrec :: Int -> ReadS GroupedRuleList

readList :: ReadS [GroupedRuleList]

readPrec :: ReadPrec GroupedRuleList

readListPrec :: ReadPrec [GroupedRuleList]

Show GroupedRuleList

Defined in Sygus.Syntax

Methods

showsPrec :: Int -> GroupedRuleList -> ShowS

show :: GroupedRuleList -> String

showList :: [GroupedRuleList] -> ShowS

Eq GroupedRuleList

Defined in Sygus.Syntax

Methods

(==) :: GroupedRuleList -> GroupedRuleList -> Bool

(/=) :: GroupedRuleList -> GroupedRuleList -> Bool

Hashable GroupedRuleList

Defined in Sygus.Syntax

Methods

hashWithSalt :: Int -> GroupedRuleList -> Int

hash :: GroupedRuleList -> Int

type Rep GroupedRuleList

Defined in Sygus.Syntax

type Rep GroupedRuleList = D1 ('MetaData "GroupedRuleList" "Sygus.Syntax" "language-sygus-0.1.1.3-8ANx6Jkwy2873RS2baX0uE" 'False) (C1 ('MetaCons "GroupedRuleList" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Symbol) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Sort) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [GTerm]))))

data GTerm

Constructors

GConstant Sort

GVariable Sort

GBfTerm BfTerm

Instances

Generic GTerm

Defined in Sygus.Syntax

Associated Types

type Rep GTerm :: Type -> Type

Methods

from :: GTerm -> Rep GTerm x

to :: Rep GTerm x -> GTerm

Read GTerm

Defined in Sygus.Syntax

Methods

readsPrec :: Int -> ReadS GTerm

readList :: ReadS [GTerm]

readPrec :: ReadPrec GTerm

readListPrec :: ReadPrec [GTerm]

Show GTerm

Defined in Sygus.Syntax

Methods

showsPrec :: Int -> GTerm -> ShowS

show :: GTerm -> String

showList :: [GTerm] -> ShowS

Eq GTerm

Defined in Sygus.Syntax

Methods

(==) :: GTerm -> GTerm -> Bool

(/=) :: GTerm -> GTerm -> Bool

Hashable GTerm

Defined in Sygus.Syntax

Methods

hashWithSalt :: Int -> GTerm -> Int

hash :: GTerm -> Int

type Rep GTerm

Defined in Sygus.Syntax

type Rep GTerm = D1 ('MetaData "GTerm" "Sygus.Syntax" "language-sygus-0.1.1.3-8ANx6Jkwy2873RS2baX0uE" 'False) (C1 ('MetaCons "GConstant" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Sort)) :+: (C1 ('MetaCons "GVariable" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Sort)) :+: C1 ('MetaCons "GBfTerm" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 BfTerm))))