Module XFD.Solver

This module defines the basic options for solvers used to solve FD constraints.

Summary of exported operations:

defaultConfig :: SolverConfig   
defaultOptions :: (Int,Int,(Bool,String),(Bool,FDExpr),(Bool,FDExpr))   
getSolverOptions :: [Option] -> (Int,Int,(Bool,String),(Bool,FDExpr),(Bool,FDExpr))   
Takes a list of options and returns a tuple containing the extracted values to work with.
solveFDwith :: SolverConfig -> [Option] -> [FDExpr] -> FDConstr -> [Int]   
Get list of solutions from solver and combine them using the (?) operator to imitate non-determinism as CLP.FD.solveFD implements it.
solveFDOnewith :: SolverConfig -> [Option] -> [FDExpr] -> FDConstr -> [Int]   
Same as solveFDwith, but append option First to list of options so only one solution is returned.
solveFDAllwith :: SolverConfig -> [Option] -> [FDExpr] -> FDConstr -> [[Int]]   
Same as solveFDwith, but append option All to list of options so all solutions are returned; also returns list of solutions non-deterministically.

Exported datatypes:


SolverArgs

Type synonym: SolverArgs a = [Option] -> [FDExpr] -> FDConstr -> a


SolverImpl

Type synonym: SolverImpl = SolverConfig -> SolverArgs (IO [[Int]])


SolverConfig

Constructors:

  • Config :: String -> [String] -> SolverImpl -> (Maybe [Option]) -> String -> SolverConfig

    Fields:

    • executable :: String
    • flags :: [String]
    • solveWith :: SolverImpl
    • smtOptions :: (Maybe [Option])
    • smtLogic :: String

Option

Constructors:

  • Debug :: Int -> Option
  • All :: Option
  • First :: Option
  • FirstN :: Int -> Option
  • Persist :: String -> Option
  • Minimize :: FDExpr -> Option
  • Maximize :: FDExpr -> Option

ExtractedOptions

Type synonym: ExtractedOptions = (Int,Int,(Bool,String),(Bool,FDExpr),(Bool,FDExpr))


Exported operations:

defaultConfig :: SolverConfig   

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

defaultOptions :: (Int,Int,(Bool,String),(Bool,FDExpr),(Bool,FDExpr))   

getSolverOptions :: [Option] -> (Int,Int,(Bool,String),(Bool,FDExpr),(Bool,FDExpr))   

Takes a list of options and returns a tuple containing the extracted values to work with.

solveFDwith :: SolverConfig -> [Option] -> [FDExpr] -> FDConstr -> [Int]   

Get list of solutions from solver and combine them using the (?) operator to imitate non-determinism as CLP.FD.solveFD implements it.

solveFDOnewith :: SolverConfig -> [Option] -> [FDExpr] -> FDConstr -> [Int]   

Same as solveFDwith, but append option First to list of options so only one solution is returned.

solveFDAllwith :: SolverConfig -> [Option] -> [FDExpr] -> FDConstr -> [[Int]]   

Same as solveFDwith, but append option All to list of options so all solutions are returned; also returns list of solutions non-deterministically.