This module provides an abstract representation of a variant of the SMT-LIB language appropriate for checking Curry programs. In particular, polymorphic function declarations are supported.
It might be later replaced by an extended version of the
SMT-LIB language specified in the package smtlib
.
Author: Michael Hanus
Version: March 2019
showSort
:: Sort -> String
|
isTypeParameter
:: Sort -> Bool
Does the sort represent a type parameter ( TVar i )?
|
qidName
:: QIdent -> String
The identifier of a possibly sorted identifier. |
tComb
:: String -> [Term] -> Term
Combined term with string identifier. |
tConj
:: [Term] -> Term
Conjunction |
tDisj
:: [Term] -> Term
Disjunction |
tNot
:: Term -> Term
Negation |
tTrue
:: Term
A Boolean true. |
tFalse
:: Term
A Boolean false. |
tEqu
:: Term -> Term -> Term
Equality between two terms. |
tEquVar
:: Int -> Term -> Term
Equality between a variable and a term. |
sortedConst
:: String -> Sort -> Term
A constant with a sort declaration. |
sAssert
:: Term -> Command
Assert a simplified formula. |
allQIdsOfTerm
:: Term -> [QIdent]
|
allQIdsOfAsserts
:: [Command] -> [QIdent]
|
typeParamsOfSort
:: Sort -> [String]
All type parameters occurring in a sort. |
typeParamsOfTerm
:: Term -> [String]
All type parameters contained in a term. |
typeParamsOfQId
:: QIdent -> [String]
|
typeParamsOfSV
:: SortedVar -> [String]
|
typeParamsOfFunSig
:: FunSig -> [String]
|
emptyTPSubst
:: FM String Sort
The empty substitution |
matchSort
:: Sort -> Sort -> Maybe (FM String Sort)
Compute sort matching, i.e., if matchSort t1 t2 = s , then t2 = s(t1) .
|
matchSorts
:: [Sort] -> [Sort] -> Maybe (FM String Sort)
|
substSort
:: FM String Sort -> Sort -> Sort
Applies a sort substitution to a term. |
substTerm
:: FM String Sort -> Term -> Term
All type parameters contained in a term. |
substQId
:: FM String Sort -> QIdent -> QIdent
|
substSV
:: FM String Sort -> SortedVar -> SortedVar
|
substFunSig
:: FM String Sort -> FunSig -> FunSig
|
substDefSig
:: FM String Sort -> ([String],FunSig,Term) -> ([String],FunSig,Term)
|
rnmTerm
:: (String -> String) -> Term -> Term
|
rnmQId
:: (String -> String) -> QIdent -> QIdent
|
rnmFunSig
:: (String -> String) -> FunSig -> FunSig
|
rnmDefSig
:: (String -> String) -> ([String],FunSig,Term) -> ([String],FunSig,Term)
|
simpTerm
:: Term -> Term
|
reduceAsInTerm
:: Term -> Term
|
unpoly
:: [Command] -> [Command]
|
addSigInstances
:: [QIdent] -> ([String],FunSig,Term) -> [([String],FunSig,Term)]
|
rnmQIdWithTInst
:: [(String,([String],Sort))] -> QIdent -> QIdent
|
rnmQIdWithTInstTerm
:: [(String,([String],Sort))] -> Term -> Term
|
toTInstName
:: String -> [String] -> FM String Sort -> String -> String
|
addTInstName
:: [String] -> FM String Sort -> String -> String
|
allSigs
:: [Command] -> [([String],FunSig,Term)]
|
nameOfSig
:: ([String],FunSig,Term) -> String
|
sigNameSort
:: ([String],FunSig,Term) -> (String,([String],Sort))
|
sigTypeAsSort
:: [Sort] -> Sort -> Sort
|
showSMT
:: [Command] -> String
Show an SMT-LIB script with a newline |
ppSigBody
:: ([String],FunSig,Term) -> Doc
|
ppCmd
:: Command -> [Doc]
Pretty printing of SMT-LIB commands. |
prettyVar
:: Int -> Doc
|
parent
:: [Doc] -> Doc
Pretty print the given documents separated with spaces and parenthesized |
An SMT-LIB script consists of a list of commands.
Constructors:
SMTLib
:: [Command] -> SMTLib
Type synonym: SVar = Int
Type synonym: Ident = String
Sorts
Constructors:
Terms A literal is a natural number, float, or string.
Constructors:
TInt
:: Int -> TLiteral
TFloat
:: Float -> TLiteral
TString
:: String -> TLiteral
An identifier possibly with a sort attached.
Constructors:
Sorted variables used in quantifiers.
Constructors:
Terms occurring in formulas
Constructors:
TConst
:: TLiteral -> Term
TSVar
:: SVar -> Term
TComb
:: QIdent -> [Term] -> Term
Let
:: [(SVar,Term)] -> Term -> Term
Forall
:: [SortedVar] -> Term -> Term
Exists
:: [SortedVar] -> Term -> Term
Datatype declaration consisting of type variables and constructor decls.
Constructors:
Constructors:
The signature of a function declaration.
Constructors:
The signature and arguments of a function declaration.
Constructors:
Commands in SMT script.
The command DefineSigsRec
is new. It is similar to DefineFunsRec
,
but the associated term is the axiomatization of the function
definition. Thus, it contains all quantifiers and the equation
(= (f x1...xn) rhs-term)
so that it can also be used to specify,
by exploiting disjunctions, the meaning of non-deterministic functions.
Moreover, it supports parametric polymoprhism by providing a list
of type paramters which can be used in the type signature and term.
Such polymorphic declarations are replaced by type-instantiated
monomorphic definitions before printing an SMT script.
Constructors:
Assert
:: Term -> Command
CheckSat
:: Command
Comment
:: String -> Command
DeclareVar
:: SortedVar -> Command
DeclareDatatypes
:: [(Ident,Int,DTDecl)] -> Command
DeclareFun
:: Ident -> [Sort] -> Sort -> Command
DeclareSort
:: Ident -> Int -> Command
DefineFunsRec
:: [(FunDec,Term)] -> Command
DefineSigsRec
:: [([Ident],FunSig,Term)] -> Command
EmptyLine
:: Command
A type paramter substitution.
Type synonym: TPSubst = FM Ident Sort
Does the sort represent a type parameter ( |
The identifier of a possibly sorted identifier.
|
Combined term with string identifier.
|
Conjunction
|
Disjunction
|
A Boolean false.
|
Equality between two terms.
|
Equality between a variable and a term.
|
A constant with a sort declaration.
|
|
|
All type parameters occurring in a sort. |
All type parameters contained in a term. |
|
|
|
The empty substitution |
Compute sort matching, i.e., if |
|
|
|
|
|
|
|
|
|
|