Module ESMT

This module provides some utility functions for the SMT-LIB language defined in the package smtlib that are needed for checking Curry programs. For example, functions for substituting sorts in terms, simplifying terms and removing polymorphism in SMT-LIB scripts are provided.

Author: Michael Hanus

Version: Juli 2021

Summary of exported operations:

showSort :: Sort -> String  Deterministic 
Sorts
isTypeParameter :: Sort -> Bool  Deterministic 
Does the sort represent a type parameter (TVar i)?
sortedConst :: String -> Sort -> Term  Deterministic 
Terms A constant with a sort declaration.
sAssert :: Term -> Command  Deterministic 
Assert a simplified formula.
allQIdsOfTerm :: Term -> [QIdent]  Deterministic 
allQIdsOfSigs :: [([String],FunSig,Term)] -> [QIdent]  Deterministic 
allQIdsOfAsserts :: [Command] -> [QIdent]  Deterministic 
allQIdsOfAssert :: Command -> [QIdent]  Deterministic 
typeParamsOfSort :: Sort -> [String]  Deterministic 
All type parameters occurring in a sort.
typeParamsOfTerm :: Term -> [String]  Deterministic 
All type parameters contained in a term.
typeParamsOfQId :: QIdent -> [String]  Deterministic 
typeParamsOfSV :: SortedVar -> [String]  Deterministic 
typeParamsOfFunSig :: FunSig -> [String]  Deterministic 
emptyTPSubst :: Map String Sort  Deterministic 
The empty substitution
matchSort :: Sort -> Sort -> Maybe (Map String Sort)  Deterministic 
Compute sort matching, i.e., if matchSort t1 t2 = s, then t2 = s(t1).
matchSorts :: [Sort] -> [Sort] -> Maybe (Map String Sort)  Deterministic 
substSort :: Map String Sort -> Sort -> Sort  Deterministic 
Applies a sort substitution to a sort.
substTerm :: Map String Sort -> Term -> Term  Deterministic 
Applies a sort substitution to a term.
substQId :: Map String Sort -> QIdent -> QIdent  Deterministic 
substSV :: Map String Sort -> SortedVar -> SortedVar  Deterministic 
substFunSig :: Map String Sort -> FunSig -> FunSig  Deterministic 
substDefSig :: Map String Sort -> ([String],FunSig,Term) -> ([String],FunSig,Term)  Deterministic 
rnmTerm :: (String -> String) -> Term -> Term  Deterministic 
rnmQId :: (String -> String) -> QIdent -> QIdent  Deterministic 
rnmFunSig :: (String -> String) -> FunSig -> FunSig  Deterministic 
rnmDefSig :: (String -> String) -> ([String],FunSig,Term) -> ([String],FunSig,Term)  Deterministic 
simpTerm :: Term -> Term  Deterministic 
reduceAsInTerm :: Term -> Term  Deterministic 
sortIdsOfSort :: Sort -> [String]  Deterministic 
sortsOfTerm :: Term -> [Sort]  Deterministic 
sortOfSortedVar :: SortedVar -> Sort  Deterministic 
unpoly :: [Either [([String],FunSig,Term)] Command] -> [Command]  Deterministic 
funSigTermsToCommands :: [([String],FunSig,Term)] -> [Command]  Deterministic 
addAllInstancesOfSigs :: [QIdent] -> [([String],FunSig,Term)] -> ([QIdent],[([String],FunSig,Term)])  Deterministic 
addInstancesOfSigs :: [QIdent] -> [([String],FunSig,Term)] -> ([QIdent],[([String],FunSig,Term)])  Deterministic 
addInstancesOfSig :: [QIdent] -> [([String],FunSig,Term)] -> ([String],FunSig,Term) -> ([QIdent],[([String],FunSig,Term)])  Deterministic 
rnmQIdWithTInst :: [(String,([String],Sort))] -> QIdent -> QIdent  Deterministic 
rnmQIdWithTInstTerm :: [(String,([String],Sort))] -> Term -> Term  Deterministic 
toTInstName :: String -> [String] -> Map String Sort -> String -> String  Deterministic 
addTInstName :: [String] -> Map String Sort -> String -> String  Deterministic 
nameOfSig :: ([String],FunSig,Term) -> String  Deterministic 
sigNameSort :: ([String],FunSig,Term) -> (String,([String],Sort))  Deterministic 
sigTypeAsSort :: [Sort] -> Sort -> Sort  Deterministic 

Exported datatypes:


FunSig

Function signatures The signature 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)


TPSubst

A type parameter substitution.

Type synonym: TPSubst = Map Ident Sort


Exported operations:

showSort :: Sort -> String  Deterministic 

Sorts

isTypeParameter :: Sort -> Bool  Deterministic 

Does the sort represent a type parameter (TVar i)?

sortedConst :: String -> Sort -> Term  Deterministic 

Terms A constant with a sort declaration.

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

sAssert :: Term -> Command  Deterministic 

Assert a simplified formula.

allQIdsOfTerm :: Term -> [QIdent]  Deterministic 

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

allQIdsOfAsserts :: [Command] -> [QIdent]  Deterministic 

typeParamsOfSort :: Sort -> [String]  Deterministic 

All type parameters occurring in a sort.

typeParamsOfTerm :: Term -> [String]  Deterministic 

All type parameters contained in a term.

typeParamsOfQId :: QIdent -> [String]  Deterministic 

typeParamsOfSV :: SortedVar -> [String]  Deterministic 

typeParamsOfFunSig :: FunSig -> [String]  Deterministic 

emptyTPSubst :: Map String Sort  Deterministic 

The empty substitution

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

matchSort :: Sort -> Sort -> Maybe (Map String Sort)  Deterministic 

Compute sort matching, i.e., if matchSort t1 t2 = s, then t2 = s(t1).

matchSorts :: [Sort] -> [Sort] -> Maybe (Map String Sort)  Deterministic 

substSort :: Map String Sort -> Sort -> Sort  Deterministic 

Applies a sort substitution to a sort.

substTerm :: Map String Sort -> Term -> Term  Deterministic 

Applies a sort substitution to a term.

substQId :: Map String Sort -> QIdent -> QIdent  Deterministic 

substSV :: Map String Sort -> SortedVar -> SortedVar  Deterministic 

substFunSig :: Map String Sort -> FunSig -> FunSig  Deterministic 

substDefSig :: Map String Sort -> ([String],FunSig,Term) -> ([String],FunSig,Term)  Deterministic 

rnmTerm :: (String -> String) -> Term -> Term  Deterministic 

rnmQId :: (String -> String) -> QIdent -> QIdent  Deterministic 

rnmFunSig :: (String -> String) -> FunSig -> FunSig  Deterministic 

rnmDefSig :: (String -> String) -> ([String],FunSig,Term) -> ([String],FunSig,Term)  Deterministic 

simpTerm :: Term -> Term  Deterministic 

reduceAsInTerm :: Term -> Term  Deterministic 

sortIdsOfSort :: Sort -> [String]  Deterministic 

sortsOfTerm :: Term -> [Sort]  Deterministic 

sortOfSortedVar :: SortedVar -> Sort  Deterministic 

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

unpoly :: [Either [([String],FunSig,Term)] Command] -> [Command]  Deterministic 

funSigTermsToCommands :: [([String],FunSig,Term)] -> [Command]  Deterministic 

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

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

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

rnmQIdWithTInst :: [(String,([String],Sort))] -> QIdent -> QIdent  Deterministic 

rnmQIdWithTInstTerm :: [(String,([String],Sort))] -> Term -> Term  Deterministic 

toTInstName :: String -> [String] -> Map String Sort -> String -> String  Deterministic 

addTInstName :: [String] -> Map String Sort -> String -> String  Deterministic 

nameOfSig :: ([String],FunSig,Term) -> String  Deterministic 

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

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

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

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

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