Sygus.Syntax

Documentation

data Lit

Constructors

LitNum Integer

LitDec Integer Integer

LitBool Bool

Hexidecimal String

Binary String

LitStr String

Instances

Eq Lit

Defined in Sygus.Syntax

Methods

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

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

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

Generic Lit

Defined in Sygus.Syntax

Associated Types

type Rep Lit :: Type -> Type

Methods

from :: Lit -> Rep Lit x

to :: Rep Lit x -> Lit

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.2-FhPJX0wzClvHYBu97mWxNf" 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

Eq Cmd

Defined in Sygus.Syntax

Methods

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

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

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

Generic Cmd

Defined in Sygus.Syntax

Associated Types

type Rep Cmd :: Type -> Type

Methods

from :: Cmd -> Rep Cmd x

to :: Rep Cmd x -> Cmd

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.2-FhPJX0wzClvHYBu97mWxNf" 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

Eq Identifier

Defined in Sygus.Syntax

Methods

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

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

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

Generic Identifier

Defined in Sygus.Syntax

Associated Types

type Rep Identifier :: Type -> Type

Methods

from :: Identifier -> Rep Identifier x

to :: Rep Identifier x -> Identifier

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.2-FhPJX0wzClvHYBu97mWxNf" 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

Eq Index

Defined in Sygus.Syntax

Methods

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

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

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

Generic Index

Defined in Sygus.Syntax

Associated Types

type Rep Index :: Type -> Type

Methods

from :: Index -> Rep Index x

to :: Rep Index x -> Index

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.2-FhPJX0wzClvHYBu97mWxNf" 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

Eq Sort

Defined in Sygus.Syntax

Methods

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

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

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

Generic Sort

Defined in Sygus.Syntax

Associated Types

type Rep Sort :: Type -> Type

Methods

from :: Sort -> Rep Sort x

to :: Rep Sort x -> Sort

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.2-FhPJX0wzClvHYBu97mWxNf" 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

Eq Term

Defined in Sygus.Syntax

Methods

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

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

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

Generic Term

Defined in Sygus.Syntax

Associated Types

type Rep Term :: Type -> Type

Methods

from :: Term -> Rep Term x

to :: Rep Term x -> Term

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.2-FhPJX0wzClvHYBu97mWxNf" 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

Eq BfTerm

Defined in Sygus.Syntax

Methods

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

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

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

Generic BfTerm

Defined in Sygus.Syntax

Associated Types

type Rep BfTerm :: Type -> Type

Methods

from :: BfTerm -> Rep BfTerm x

to :: Rep BfTerm x -> BfTerm

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.2-FhPJX0wzClvHYBu97mWxNf" 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

Eq SortedVar

Defined in Sygus.Syntax

Methods

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

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

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

Generic SortedVar

Defined in Sygus.Syntax

Associated Types

type Rep SortedVar :: Type -> Type

Methods

from :: SortedVar -> Rep SortedVar x

to :: Rep SortedVar x -> SortedVar

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.2-FhPJX0wzClvHYBu97mWxNf" 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

Eq VarBinding

Defined in Sygus.Syntax

Methods

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

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

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

Generic VarBinding

Defined in Sygus.Syntax

Associated Types

type Rep VarBinding :: Type -> Type

Methods

from :: VarBinding -> Rep VarBinding x

to :: Rep VarBinding x -> VarBinding

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.2-FhPJX0wzClvHYBu97mWxNf" 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

Eq Feature

Defined in Sygus.Syntax

Methods

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

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

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

Generic Feature

Defined in Sygus.Syntax

Associated Types

type Rep Feature :: Type -> Type

Methods

from :: Feature -> Rep Feature x

to :: Rep Feature x -> Feature

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.2-FhPJX0wzClvHYBu97mWxNf" 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

Eq SmtCmd

Defined in Sygus.Syntax

Methods

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

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

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

Generic SmtCmd

Defined in Sygus.Syntax

Associated Types

type Rep SmtCmd :: Type -> Type

Methods

from :: SmtCmd -> Rep SmtCmd x

to :: Rep SmtCmd x -> SmtCmd

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.2-FhPJX0wzClvHYBu97mWxNf" 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

Eq SortDecl

Defined in Sygus.Syntax

Methods

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

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

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

Generic SortDecl

Defined in Sygus.Syntax

Associated Types

type Rep SortDecl :: Type -> Type

Methods

from :: SortDecl -> Rep SortDecl x

to :: Rep SortDecl x -> SortDecl

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.2-FhPJX0wzClvHYBu97mWxNf" 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

Eq DTDec

Defined in Sygus.Syntax

Methods

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

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

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

Generic DTDec

Defined in Sygus.Syntax

Associated Types

type Rep DTDec :: Type -> Type

Methods

from :: DTDec -> Rep DTDec x

to :: Rep DTDec x -> DTDec

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.2-FhPJX0wzClvHYBu97mWxNf" False) (C1 (MetaCons "DTDec" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 [DTConsDec])))

data DTConsDec

Constructors

DTConsDec Symbol [SortedVar]

Instances

Eq DTConsDec

Defined in Sygus.Syntax

Methods

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

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

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

Generic DTConsDec

Defined in Sygus.Syntax

Associated Types

type Rep DTConsDec :: Type -> Type

Methods

from :: DTConsDec -> Rep DTConsDec x

to :: Rep DTConsDec x -> DTConsDec

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.2-FhPJX0wzClvHYBu97mWxNf" 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

Eq GrammarDef

Defined in Sygus.Syntax

Methods

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

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

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

Generic GrammarDef

Defined in Sygus.Syntax

Associated Types

type Rep GrammarDef :: Type -> Type

Methods

from :: GrammarDef -> Rep GrammarDef x

to :: Rep GrammarDef x -> GrammarDef

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.2-FhPJX0wzClvHYBu97mWxNf" 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

Eq GroupedRuleList

Defined in Sygus.Syntax

Methods

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

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

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

Generic GroupedRuleList

Defined in Sygus.Syntax

Associated Types

type Rep GroupedRuleList :: Type -> Type

Methods

from :: GroupedRuleList -> Rep GroupedRuleList x

to :: Rep GroupedRuleList x -> GroupedRuleList

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.2-FhPJX0wzClvHYBu97mWxNf" 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

Eq GTerm

Defined in Sygus.Syntax

Methods

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

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

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

Generic GTerm

Defined in Sygus.Syntax

Associated Types

type Rep GTerm :: Type -> Type

Methods

from :: GTerm -> Rep GTerm x

to :: Rep GTerm x -> GTerm

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.2-FhPJX0wzClvHYBu97mWxNf" 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))))