Math.SMT.Yices.Syntax

Haskell data type definition for the yices syntax. Yet incomplete since it does not include bit vectors. See http://yices.csl.sri.com/language.shtml for details.

Documentation

data TypY

yices types

Constructors

VarT String

SUBTYPE (String, TypY) ExpY

SUBRANGE ExpY ExpY

ARR [TypY]

TUP [TypY]

REC [(String, TypY)]

DEP (String, TypY)

DATATYPE [(String, [(String, TypY)])]

SCALAR [String]

Instances

Show TypY

data ExpY

yices expressions

Constructors

VarE String

LitB Bool

LitI Integer

LitR Rational

AND [ExpY]

OR [ExpY]

NOT ExpY

ExpY :=> ExpY

ExpY := ExpY

ExpY :/= ExpY

ExpY :< ExpY

ExpY :<= ExpY

ExpY :> ExpY

ExpY :>= ExpY

ExpY :+: ExpY

ExpY :-: ExpY

ExpY :*: ExpY

ExpY :/: ExpY

DIV ExpY ExpY

MOD ExpY ExpY

IF ExpY ExpY ExpY

ITE ExpY ExpY ExpY

LET [((String, Maybe TypY), ExpY)] ExpY

FORALL [(String, TypY)] ExpY

EXISTS [(String, TypY)] ExpY

APP ExpY [ExpY]

UPDATE_F ExpY [ExpY] ExpY

LAMBDA [(String, TypY)] ExpY

MKTUP [ExpY]

SELECT_T ExpY Integer

UPDATE_T ExpY Integer ExpY

MKREC [(String, ExpY)]

SELECT_R ExpY String

UPDATE_R ExpY String ExpY

Instances

Show ExpY

data CmdY

yices declarations and commands

Constructors

DEFTYP String (Maybe TypY)

DEFINE (String, TypY) (Maybe ExpY)

ASSERT ExpY

ASSERT_P ExpY (Maybe Integer)

RETRACT Integer

CHECK

MAXSAT

SETE Bool

SETV Integer

SETAO Bool

PUSH

POP

ECHO String

INCLUDE String

RESET

STATUS

DUMP

EXIT

Instances

Show CmdY