Module Language.SMTLIB.Goodies

This module provides some goodies and utility functions for SMT-LIB.

Author: Jan Tikovsky

Version: January 2018

Summary of exported operations:

declVars :: [(String,Sort)] -> [Command]  Deterministic 
Declare a list of variables
tint :: Int -> Term  Deterministic 
Construct SMT-LIB term from given integer
tfloat :: Float -> Term  Deterministic 
Construct SMT-LIB term from given float
tchar :: Char -> Term  Deterministic 
Construct SMT-LIB term from given character
tvar :: Int -> Term  Deterministic 
Construct SMT-LIB term from given variable index
var :: String -> Term  Deterministic 
Construct SMT-LIB term from a string
tcomb :: String -> [Term] -> Term  Deterministic 
Construct SMT-LIB constructor term
qtcomb :: QIdent -> [Term] -> Term  Deterministic 
Construct qualified SMT-LIB constructor term
forAll :: [Int] -> [Sort] -> Term -> Term  Deterministic 
Construct universally quantified SMT-LIB term
tneg :: Term -> Term  Deterministic 
Negate given numeral SMT-LIB term
tabs :: Term -> Term  Deterministic 
Absolute value of an SMT-LIB term
(+%) :: Term -> Term -> Term  Deterministic 
Add two SMT-LIB terms
(-%) :: Term -> Term -> Term  Deterministic 
Subtract an SMT-LIB term from another one
(*%) :: Term -> Term -> Term  Deterministic 
Multiply two SMT-LIB terms
(/%) :: Term -> Term -> Term  Deterministic 
Divide an SMT-LIB term by another one
true :: Term  Deterministic 
SMT-LIB term true
false :: Term  Deterministic 
SMT-LIB term false
(=%) :: Term -> Term -> Term  Deterministic 
Constrain two SMT-LIB terms to be equal
(/=%) :: Term -> Term -> Term  Deterministic 
Constrain two SMT-LIB terms to be different
(<%) :: Term -> Term -> Term  Deterministic 
Constrain two SMT-LIB terms with a less-than-relation
(<=%) :: Term -> Term -> Term  Deterministic 
Constrain two SMT-LIB terms with a less-than-or-equal-relation
(>%) :: Term -> Term -> Term  Deterministic 
Constrain two SMT-LIB terms with a greater-than-relation
(>=%) :: Term -> Term -> Term  Deterministic 
Constrain two SMT-LIB terms with a greater-than-or-equal-relation
tand :: [Term] -> Term  Deterministic 
Combine a list of SMT-LIB terms using a conjunction
tor :: [Term] -> Term  Deterministic 
Combine a list of SMT-LIB terms using a disjunction
(==>) :: Term -> Term -> Term  Deterministic 
Logical implication
tnot :: Term -> Term  Deterministic 
Logical negation of an SMT-LIB term
scomb :: String -> [Sort] -> Sort  Deterministic 
Construct an SMT-LIB sort
orderingSort :: Sort  Deterministic 
Representation of Ordering type as SMT-LIB sort
boolSort :: Sort  Deterministic 
Representation of Bool type as SMT-LIB sort
intSort :: Sort  Deterministic 
Representation of Int type as SMT-LIB sort
floatSort :: Sort  Deterministic 
Representation of Float type as SMT-LIB sort
funSC :: [Sort] -> Sort  Deterministic 
Representation of -> type constructor as SMT-LIB sort constructor
nop :: Command  Deterministic 
Generate a nop SMT-LIB command
assert :: [Term] -> Command  Deterministic 
Generate an assert SMT-LIB command
unqual :: QIdent -> String  Deterministic 
Get the unqualified identifier of a qualified SMT-LIB identifier
isDeclData :: Command -> Bool  Deterministic 
Is given SMT-LIB command a declaration of an algebraic data type
isEcho :: Command -> Bool  Deterministic 
Is given SMT-LIB command an Echo
echo :: String -> Command  Deterministic 
Smart constructor for the Echo SMT-LIB command marking every Echo command with an initial @ character which is necessary to recognize Echos during parsing
comment :: String -> Command  Deterministic 
Smart constructor to generate a comment in an SMT-LIB script
var2SMT :: Int -> String  Deterministic 
Transform a FlatCurry variable index into an SMT-LIB symbol

Exported operations:

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

Declare a list of variables

tint :: Int -> Term  Deterministic 

Construct SMT-LIB term from given integer

tfloat :: Float -> Term  Deterministic 

Construct SMT-LIB term from given float

tchar :: Char -> Term  Deterministic 

Construct SMT-LIB term from given character

tvar :: Int -> Term  Deterministic 

Construct SMT-LIB term from given variable index

var :: String -> Term  Deterministic 

Construct SMT-LIB term from a string

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

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

Construct SMT-LIB constructor term

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

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

Construct qualified SMT-LIB constructor term

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

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

Construct universally quantified SMT-LIB term

tneg :: Term -> Term  Deterministic 

Negate given numeral SMT-LIB term

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

tabs :: Term -> Term  Deterministic 

Absolute value of an SMT-LIB term

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

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

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  Deterministic 

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  Deterministic 

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  Deterministic 

Divide an SMT-LIB term by another one

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

true :: Term  Deterministic 

SMT-LIB term true

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

false :: Term  Deterministic 

SMT-LIB term false

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

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

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  Deterministic 

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  Deterministic 

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  Deterministic 

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  Deterministic 

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  Deterministic 

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  Deterministic 

Combine a list of SMT-LIB terms using a conjunction

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

tor :: [Term] -> Term  Deterministic 

Combine a list of SMT-LIB terms using a disjunction

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

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

Logical implication

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

tnot :: Term -> Term  Deterministic 

Logical negation of an SMT-LIB term

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

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

Construct an SMT-LIB sort

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

orderingSort :: Sort  Deterministic 

Representation of Ordering type as SMT-LIB sort

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

boolSort :: Sort  Deterministic 

Representation of Bool type as SMT-LIB sort

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

intSort :: Sort  Deterministic 

Representation of Int type as SMT-LIB sort

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

floatSort :: Sort  Deterministic 

Representation of Float type as SMT-LIB sort

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

funSC :: [Sort] -> Sort  Deterministic 

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

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

nop :: Command  Deterministic 

Generate a nop SMT-LIB command

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

assert :: [Term] -> Command  Deterministic 

Generate an assert SMT-LIB command

unqual :: QIdent -> String  Deterministic 

Get the unqualified identifier of a qualified SMT-LIB identifier

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

isDeclData :: Command -> Bool  Deterministic 

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

isEcho :: Command -> Bool  Deterministic 

Is given SMT-LIB command an Echo

echo :: String -> Command  Deterministic 

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  Deterministic 

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  Deterministic 

Transform a FlatCurry variable index into an SMT-LIB symbol