Module XFD.SMTLib.FromFD

This module defines operation to translate FD models into SMT-LIB models

Summary of exported operations:

(=>>) :: ([Command] -> [Command]) -> ([Command] -> [Command]) -> [Command] -> [Command]   
showSMT :: ([Command] -> [Command]) -> String   
setOptions :: Maybe [Option] -> [Command] -> [Command]   
setLogic :: String -> [Command] -> [Command]   
exit :: [Command] -> [Command]   
echo :: String -> [Command] -> [Command]   
pop :: Int -> [Command] -> [Command]   
push :: Int -> [Command] -> [Command]   
checkSat :: [Command] -> [Command]   
getModel :: [Command] -> [Command]   
getValue :: [FDExpr] -> [Command] -> [Command]   
declare :: [FDExpr] -> [Command] -> [Command]   
assert :: FDConstr -> [Command] -> [Command]   
add Assert command with the given constraint to list
declareConst :: FDExpr -> [Command] -> [Command]   
add DeclareConst command for given FDVar to list
convertConstr :: FDConstr -> Term   
convertExpr :: FDExpr -> Term   
convertCmdResponseToFD :: CmdResponse -> [FDExpr]   
convertModelResponseToFD :: ModelResponse -> FDExpr   
convertFunDefToFD :: FunDef -> FDExpr   
convertValueResponseToFD :: ValuationPair -> FDExpr   

Exported datatypes:


SMT

Type synonym: SMT = SMTLib -> SMTLib


Exported operations:

(=>>) :: ([Command] -> [Command]) -> ([Command] -> [Command]) -> [Command] -> [Command]   

Further infos:
  • defined as left-associative infix operator with precedence 1

showSMT :: ([Command] -> [Command]) -> String   

setOptions :: Maybe [Option] -> [Command] -> [Command]   

setLogic :: String -> [Command] -> [Command]   

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

exit :: [Command] -> [Command]   

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

echo :: String -> [Command] -> [Command]   

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

pop :: Int -> [Command] -> [Command]   

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

push :: Int -> [Command] -> [Command]   

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

checkSat :: [Command] -> [Command]   

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

getModel :: [Command] -> [Command]   

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

getValue :: [FDExpr] -> [Command] -> [Command]   

declare :: [FDExpr] -> [Command] -> [Command]   

assert :: FDConstr -> [Command] -> [Command]   

add Assert command with the given constraint to list

declareConst :: FDExpr -> [Command] -> [Command]   

add DeclareConst command for given FDVar to list

convertExpr :: FDExpr -> Term