This module provides some goodies and utility functions for SMTLIB.
Author: Jan Tikovsky
Version: January 2018
declVars
:: [(String,Sort)] > [Command]
Declare a list of variables 
tint
:: Int > Term
Construct SMTLIB term from given integer 
tfloat
:: Float > Term
Construct SMTLIB term from given float 
tchar
:: Char > Term
Construct SMTLIB term from given character 
tvar
:: Int > Term
Construct SMTLIB term from given variable index 
var
:: String > Term
Construct SMTLIB term from a string 
tcomb
:: String > [Term] > Term
Construct SMTLIB constructor term 
qtcomb
:: QIdent > [Term] > Term
Construct qualified SMTLIB constructor term 
forAll
:: [Int] > [Sort] > Term > Term
Construct universally quantified SMTLIB term 
tneg
:: Term > Term
Negate given numeral SMTLIB term 
tabs
:: Term > Term
Absolute value of an SMTLIB term 
(+%)
:: Term > Term > Term
Add two SMTLIB terms 
(%)
:: Term > Term > Term
Subtract an SMTLIB term from another one 
(*%)
:: Term > Term > Term
Multiply two SMTLIB terms 
(/%)
:: Term > Term > Term
Divide an SMTLIB term by another one 
true
:: Term
SMTLIB term true

false
:: Term
SMTLIB term false

(=%)
:: Term > Term > Term
Constrain two SMTLIB terms to be equal 
(/=%)
:: Term > Term > Term
Constrain two SMTLIB terms to be different 
(<%)
:: Term > Term > Term
Constrain two SMTLIB terms with a lessthanrelation 
(<=%)
:: Term > Term > Term
Constrain two SMTLIB terms with a lessthanorequalrelation 
(>%)
:: Term > Term > Term
Constrain two SMTLIB terms with a greaterthanrelation 
(>=%)
:: Term > Term > Term
Constrain two SMTLIB terms with a greaterthanorequalrelation 
tand
:: [Term] > Term
Combine a list of SMTLIB terms using a conjunction 
tor
:: [Term] > Term
Combine a list of SMTLIB terms using a disjunction 
(==>)
:: Term > Term > Term
Logical implication 
tnot
:: Term > Term
Logical negation of an SMTLIB term 
scomb
:: String > [Sort] > Sort
Construct an SMTLIB sort 
orderingSort
:: Sort
Representation of Ordering type as SMTLIB sort 
boolSort
:: Sort
Representation of Bool type as SMTLIB sort 
intSort
:: Sort
Representation of Int type as SMTLIB sort 
floatSort
:: Sort
Representation of Float type as SMTLIB sort 
funSC
:: [Sort] > Sort
Representation of > type constructor as SMTLIB sort constructor 
nop
:: Command
Generate a nop
SMTLIB command

assert
:: [Term] > Command
Generate an assert
SMTLIB command

unqual
:: QIdent > String
Get the unqualified identifier of a qualified SMTLIB identifier 
isDeclData
:: Command > Bool
Is given SMTLIB command a declaration of an algebraic data type 
isEcho
:: Command > Bool
Is given SMTLIB command an Echo 
echo
:: String > Command
Smart constructor for the Echo SMTLIB command marking every Echo command with an initial @ character which is necessary to recognize Echos during parsing 
comment
:: String > Command
Smart constructor to generate a comment in an SMTLIB script 
var2SMT
:: Int > String
Transform a FlatCurry variable index into an SMTLIB symbol 
Construct SMTLIB term from a string

Construct SMTLIB constructor term

Construct qualified SMTLIB constructor term

Negate given numeral SMTLIB term

Absolute value of an SMTLIB term

Add two SMTLIB terms

Subtract an SMTLIB term from another one

Multiply two SMTLIB terms

Divide an SMTLIB term by another one

SMTLIB term

SMTLIB term

Constrain two SMTLIB terms to be equal

Constrain two SMTLIB terms to be different

Constrain two SMTLIB terms with a lessthanrelation

Constrain two SMTLIB terms with a lessthanorequalrelation

Constrain two SMTLIB terms with a greaterthanrelation

Constrain two SMTLIB terms with a greaterthanorequalrelation

Combine a list of SMTLIB terms using a conjunction

Combine a list of SMTLIB terms using a disjunction

Logical implication

Logical negation of an SMTLIB term

Construct an SMTLIB sort

Representation of Ordering type as SMTLIB sort

Representation of Bool type as SMTLIB sort

Representation of Int type as SMTLIB sort

Representation of Float type as SMTLIB sort

Representation of > type constructor as SMTLIB sort constructor

Generate a

Get the unqualified identifier of a qualified SMTLIB identifier

Is given SMTLIB command a declaration of an algebraic data type 
Smart constructor for the Echo SMTLIB command marking every Echo command with an initial @ character which is necessary to recognize Echos during parsing

Smart constructor to generate a comment in an SMTLIB script

Transform a FlatCurry variable index into an SMTLIB symbol 