KiCS2
Exported names: Imported modules:

Module ESMT

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: September 2019

Summary of exported operations:

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]   
allQIdsOfSigs :: [([String],FunSig,Term)] -> [QIdent]   
allQIdsOfAsserts :: [Command] -> [QIdent]   
allQIdsOfAssert :: 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 sort.
substTerm :: FM String Sort -> Term -> Term   
Applies a sort substitution to 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   
sortIdsOfSort :: Sort -> [String]   
sortsOfTerm :: Term -> [Sort]   
sortOfSortedVar :: SortedVar -> Sort   
unpoly :: [Command] -> [Command]   
addAllInstancesOfSigs :: [QIdent] -> [([String],FunSig,Term)] -> ([QIdent],[([String],FunSig,Term)])   
addInstancesOfSigs :: [QIdent] -> [([String],FunSig,Term)] -> ([QIdent],[([String],FunSig,Term)])   
addInstancesOfSig :: [QIdent] -> [([String],FunSig,Term)] -> ([String],FunSig,Term) -> ([QIdent],[([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 after transforming polymorphic functions into type-instanteded functions.
showSMTRaw :: [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

Exported datatypes:

SMTLib

An SMT-LIB script consists of a list of commands.

Constructors:

SVar

Type synonym: SVar = Int

Ident

Type synonym: Ident = String

Sort

Sorts

Constructors:

TLiteral

Terms A literal is a natural number, float, or string.

Constructors:

  • TInt :: Int -> TLiteral
  • TFloat :: Float -> TLiteral
  • TString :: String -> TLiteral
QIdent

An identifier possibly with a sort attached.

Constructors:

SortedVar

Sorted variables used in quantifiers.

Constructors:

Term

Terms occurring in formulas

Constructors:

DTDecl

Datatype declaration consisting of type variables and constructor decls.

Constructors:

DTCons

Constructors:

FunSig

The signature of a function declaration.

Constructors:

FunDec

The signature and arguments of a function declaration.

Constructors:

FunSigTerm

A definition of a polymorphic, possibly non-deterministic, operation. The first component is a list of type paramters which can be used in the type signature and the term. The term in the third argument 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 operations.

Type synonym: FunSigTerm = ([Ident],FunSig,Term)

Command

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 :: [FunSigTerm] -> Command
  • EmptyLine :: Command
TPSubst

A type paramter substitution.

Type synonym: TPSubst = FM Ident Sort

Exported operations:

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.

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

tComb :: String -> [Term] -> Term   

Combined term with string identifier.

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

tConj :: [Term] -> Term   

Conjunction

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

tDisj :: [Term] -> Term   

Disjunction

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

tNot :: Term -> Term   

Negation

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

tTrue :: Term   

A Boolean true.

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

tFalse :: Term   

A Boolean false.

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

tEqu :: Term -> Term -> Term   

Equality between two terms.

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

tEquVar :: Int -> Term -> Term   

Equality between a variable and a term.

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

sortedConst :: String -> Sort -> Term   

A constant with a sort declaration.

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

sAssert :: Term -> Command   

Assert a simplified formula.

allQIdsOfTerm :: Term -> [QIdent]   

allQIdsOfSigs :: [([String],FunSig,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 sort.

substTerm :: FM String Sort -> Term -> Term   

Applies a sort substitution to 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   

sortIdsOfSort :: Sort -> [String]   

sortsOfTerm :: Term -> [Sort]   

sortOfSortedVar :: SortedVar -> Sort   

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

unpoly :: [Command] -> [Command]   

addAllInstancesOfSigs :: [QIdent] -> [([String],FunSig,Term)] -> ([QIdent],[([String],FunSig,Term)])   

addInstancesOfSigs :: [QIdent] -> [([String],FunSig,Term)] -> ([QIdent],[([String],FunSig,Term)])   

addInstancesOfSig :: [QIdent] -> [([String],FunSig,Term)] -> ([String],FunSig,Term) -> ([QIdent],[([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   

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

sigNameSort :: ([String],FunSig,Term) -> (String,([String],Sort))   

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

sigTypeAsSort :: [Sort] -> Sort -> Sort   

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

showSMT :: [Command] -> String   

Show an SMT-LIB script with a newline after transforming polymorphic functions into type-instanteded functions.

showSMTRaw :: [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