PAKCS
Exported names: Imported modules:

Module XFD.SMTLib.Build

This module defines some auxiliary operation to construct SMT-LIB formulas.

Summary of exported operations:

declareConst :: String -> String -> Command   
declareInt :: String -> Command   
termSpecConstNum :: Int -> Term   
specConstNum :: Int -> SpecConstant   
termQIdent :: String -> Term   
termQIdentT :: String -> [Term] -> Term   
qIdent :: String -> QualIdentifier   
ident :: String -> Identifier   

Exported operations:

declareConst :: String -> String -> Command   

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

declareInt :: String -> Command   

termSpecConstNum :: Int -> Term   

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

specConstNum :: Int -> SpecConstant   

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

termQIdent :: String -> Term   

termQIdentT :: String -> [Term] -> Term   

qIdent :: String -> QualIdentifier   

ident :: String -> Identifier   

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