Module Language.SMTLIB.Goodies

declVars :: [(String,Sort)] -> [Command]   

Declare a list of variables

tint :: Int -> Term   

Construct SMT-LIB term from given integer

tfloat :: Float -> Term   

Construct SMT-LIB term from given float

tchar :: Char -> Term   

Construct SMT-LIB term from given character

tvar :: Int -> Term   

Construct SMT-LIB term from given variable index

var :: String -> Term   

Construct SMT-LIB term from a string

Further infos:

• solution complete, i.e., able to compute all solutions

tcomb :: String -> [Term] -> Term   

Construct SMT-LIB constructor term

Further infos:

• solution complete, i.e., able to compute all solutions

qtcomb :: QIdent -> [Term] -> Term   

Construct qualified SMT-LIB constructor term

Further infos:

• solution complete, i.e., able to compute all solutions

forAll :: [Int] -> [Sort] -> Term -> Term   

Construct universally quantified SMT-LIB term

tneg :: Term -> Term   

Negate given numeral SMT-LIB term

Further infos:

• solution complete, i.e., able to compute all solutions

tabs :: Term -> Term   

Absolute value of an SMT-LIB term

Further infos:

• solution complete, i.e., able to compute all solutions

(+%) :: Term -> Term -> Term   

Add two SMT-LIB terms

Further infos:

• defined as left-associative infix operator with precedence 6
• solution complete, i.e., able to compute all solutions

(-%) :: Term -> Term -> Term   

Subtract an SMT-LIB term from another one

Further infos:

• defined as left-associative infix operator with precedence 6
• solution complete, i.e., able to compute all solutions

(*%) :: Term -> Term -> Term   

Multiply two SMT-LIB terms

Further infos:

• defined as left-associative infix operator with precedence 7
• solution complete, i.e., able to compute all solutions

(/%) :: Term -> Term -> Term   

Divide an SMT-LIB term by another one

Further infos:

• solution complete, i.e., able to compute all solutions

true :: Term   

SMT-LIB term true

Further infos:

• solution complete, i.e., able to compute all solutions

false :: Term   

SMT-LIB term false

Further infos:

• solution complete, i.e., able to compute all solutions

(=%) :: Term -> Term -> Term   

Constrain two SMT-LIB terms to be equal

Further infos:

• defined as non-associative infix operator with precedence 4
• solution complete, i.e., able to compute all solutions

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

Constrain two SMT-LIB terms to be different

Further infos:

• defined as non-associative infix operator with precedence 4
• solution complete, i.e., able to compute all solutions

(<%) :: Term -> Term -> Term   

Constrain two SMT-LIB terms with a less-than-relation

Further infos:

• defined as non-associative infix operator with precedence 4
• solution complete, i.e., able to compute all solutions

(<=%) :: Term -> Term -> Term   

Constrain two SMT-LIB terms with a less-than-or-equal-relation

Further infos:

• defined as non-associative infix operator with precedence 4
• solution complete, i.e., able to compute all solutions

(>%) :: Term -> Term -> Term   

Constrain two SMT-LIB terms with a greater-than-relation

Further infos:

• defined as non-associative infix operator with precedence 4
• solution complete, i.e., able to compute all solutions

(>=%) :: Term -> Term -> Term   

Constrain two SMT-LIB terms with a greater-than-or-equal-relation

Further infos:

• defined as non-associative infix operator with precedence 4
• solution complete, i.e., able to compute all solutions

tand :: [Term] -> Term   

Combine a list of SMT-LIB terms using a conjunction

Further infos:

• solution complete, i.e., able to compute all solutions

tor :: [Term] -> Term   

Combine a list of SMT-LIB terms using a disjunction

Further infos:

• solution complete, i.e., able to compute all solutions

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

Logical implication

Further infos:

• solution complete, i.e., able to compute all solutions

tnot :: Term -> Term   

Logical negation of an SMT-LIB term

Further infos:

• solution complete, i.e., able to compute all solutions

scomb :: String -> [Sort] -> Sort   

Construct an SMT-LIB sort

Further infos:

• solution complete, i.e., able to compute all solutions

orderingSort :: Sort   

Representation of Ordering type as SMT-LIB sort

Further infos:

• solution complete, i.e., able to compute all solutions

boolSort :: Sort   

Representation of Bool type as SMT-LIB sort

Further infos:

• solution complete, i.e., able to compute all solutions

intSort :: Sort   

Representation of Int type as SMT-LIB sort

Further infos:

• solution complete, i.e., able to compute all solutions

floatSort :: Sort   

Representation of Float type as SMT-LIB sort

Further infos:

• solution complete, i.e., able to compute all solutions

funSC :: [Sort] -> Sort   

Representation of -> type constructor as SMT-LIB sort constructor

Further infos:

• solution complete, i.e., able to compute all solutions

nop :: Command   

Generate a nop SMT-LIB command

Further infos:

• solution complete, i.e., able to compute all solutions

assert :: [Term] -> Command   

Generate an assert SMT-LIB command

unqual :: QIdent -> String   

Get the unqualified identifier of a qualified SMT-LIB identifier

Further infos:

• solution complete, i.e., able to compute all solutions

isDeclData :: Command -> Bool   

Is given SMT-LIB command a declaration of an algebraic data type

isEcho :: Command -> Bool   

Is given SMT-LIB command an Echo

echo :: String -> Command   

Smart constructor for the Echo SMT-LIB command marking every Echo command with an initial @ character which is necessary to recognize Echos during parsing

Further infos:

• solution complete, i.e., able to compute all solutions

comment :: String -> Command   

Smart constructor to generate a comment in an SMT-LIB script

Further infos:

• solution complete, i.e., able to compute all solutions

var2SMT :: Int -> String   

Transform a FlatCurry variable index into an SMT-LIB symbol