Module XFD.SMTLib.FromFD

(=>>) :: ([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

convertConstr :: FDConstr -> Term   

convertExpr :: FDExpr -> Term   

convertCmdResponseToFD :: CmdResponse -> [FDExpr]   

convertModelResponseToFD :: ModelResponse -> FDExpr   

convertFunDefToFD :: FunDef -> FDExpr   

convertValueResponseToFD :: ValuationPair -> FDExpr