Module Verify.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: March 2024

Summary of exported operations:

showSort :: Sort -> String  Deterministic 
isTypeParameter :: Sort -> Bool  Deterministic 
Does the sort represent a type parameter (TVar i)?
anonymousType :: Sort  Deterministic 
A sort represent an anonymous type (SComb "_" []).
isAnonymousType :: Sort -> Bool  Deterministic 
Does the sort represent an anonymous type (SComb "_" [])?
qidName :: QIdent -> String  Deterministic 
The identifier of a possibly sorted identifier.
pTrue :: Pattern  Deterministic 
pFalse :: Pattern  Deterministic 
tComb :: String -> [Term] -> Term  Deterministic 
Combined term with string identifier.
tConj :: [Term] -> Term  Deterministic 
Conjunction
tDisj :: [Term] -> Term  Deterministic 
Disjunction
tNot :: Term -> Term  Deterministic 
Negation
tTrue :: Term  Deterministic 
A Boolean true.
tFalse :: Term  Deterministic 
A Boolean false.
tEqu :: Term -> Term -> Term  Deterministic 
Equality between two terms.
tEquVar :: Int -> Term -> Term  Deterministic 
Equality between a variable and a term.
tITE :: Term -> Term -> Term -> Term  Deterministic 
if-then-else expression
tLet :: [(Int,Term)] -> Term -> Term  Deterministic 
Let expression.
sortedConst :: String -> Sort -> Term  Deterministic 
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
showTPSubst :: Map String Sort -> String  Deterministic 
Shows a type substitution.
makeTPSubst :: [(String,Sort)] -> Map String Sort  Deterministic 
Create a type substitution from ident/sort pairs.
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 
Remove As-identifiers if they are functions (for better readability):
reduceAsInCmd :: Command -> Command  Deterministic 
Remove As-identifiers if they are functions (for better readability):
sortIdsOfSort :: Sort -> [String]  Deterministic 
sortsOfTerm :: Term -> [Sort]  Deterministic 
sortOfSortedVar :: SortedVar -> Sort  Deterministic 
unpoly :: [Command] -> [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 
allSigs :: [Command] -> [([String],FunSig,Term)]  Deterministic 
nameOfSig :: ([String],FunSig,Term) -> String  Deterministic 
sigNameSort :: ([String],FunSig,Term) -> (String,([String],Sort))  Deterministic 
sigTypeAsSort :: [Sort] -> Sort -> Sort  Deterministic 
showSMT :: [Command] -> String  Deterministic 
Show an SMT-LIB script with a newline after transforming polymorphic functions into type-instanteded functions.
showSMTRaw :: [Command] -> String  Deterministic 
Show an SMT-LIB script with a newline.
ppSigBody :: ([String],FunSig,Term) -> Doc  Deterministic 
ppCmd :: Command -> [Doc]  Deterministic 
Pretty printing of SMT-LIB commands.
prettyVar :: Int -> Doc  Deterministic 
parent :: [Doc] -> Doc  Deterministic 
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:

Pattern

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 parameter substitution.

Type synonym: TPSubst = Map Ident Sort

Exported operations:

showSort :: Sort -> String  Deterministic 

isTypeParameter :: Sort -> Bool  Deterministic 

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

anonymousType :: Sort  Deterministic 

A sort represent an anonymous type (SComb "_" []).

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

isAnonymousType :: Sort -> Bool  Deterministic 

Does the sort represent an anonymous type (SComb "_" [])?

qidName :: QIdent -> String  Deterministic 

The identifier of a possibly sorted identifier.

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

pTrue :: Pattern  Deterministic 

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

pFalse :: Pattern  Deterministic 

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

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

Combined term with string identifier.

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

tConj :: [Term] -> Term  Deterministic 

Conjunction

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

tDisj :: [Term] -> Term  Deterministic 

Disjunction

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

tNot :: Term -> Term  Deterministic 

Negation

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

tTrue :: Term  Deterministic 

A Boolean true.

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

tFalse :: Term  Deterministic 

A Boolean false.

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

tEqu :: Term -> Term -> Term  Deterministic 

Equality between two terms.

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

tEquVar :: Int -> Term -> Term  Deterministic 

Equality between a variable and a term.

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

tITE :: Term -> Term -> Term -> Term  Deterministic 

if-then-else expression

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

tLet :: [(Int,Term)] -> Term -> Term  Deterministic 

Let expression.

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

sortedConst :: String -> Sort -> Term  Deterministic 

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

showTPSubst :: Map String Sort -> String  Deterministic 

Shows a type substitution.

makeTPSubst :: [(String,Sort)] -> Map String Sort  Deterministic 

Create a type substitution from ident/sort pairs.

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

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

Further infos:
  • partially defined

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 

Remove As-identifiers if they are functions (for better readability):

reduceAsInCmd :: Command -> Command  Deterministic 

Remove As-identifiers if they are functions (for better readability):

sortIdsOfSort :: Sort -> [String]  Deterministic 

sortsOfTerm :: Term -> [Sort]  Deterministic 

sortOfSortedVar :: SortedVar -> Sort  Deterministic 

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

unpoly :: [Command] -> [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 

Further infos:
  • partially defined

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

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

showSMT :: [Command] -> String  Deterministic 

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

showSMTRaw :: [Command] -> String  Deterministic 

Show an SMT-LIB script with a newline.

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

ppCmd :: Command -> [Doc]  Deterministic 

Pretty printing of SMT-LIB commands.

prettyVar :: Int -> Doc  Deterministic 

parent :: [Doc] -> Doc  Deterministic 

Pretty print the given documents separated with spaces and parenthesized