1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37

module XFD (

  -- solve functions
  solveFD, solveFDwith,

  -- FD constraints
  module XFD.FD,

  -- SMTLib
  --module SMTFD.SMTLib

  module XFD.Solver
  ) where

import Unsafe
import XFD.FD
import XFD.SMTLib
import XFD.Solver hiding (solveFDwith, solveFDAllwith, solveFDOnewith)

import XFD.Solvers.Z3
import XFD.Solvers.CVC4

data Solvers = Z3 | CVC4
type SolverOptions = [Option]

-- solveFD :: Solvers -> [FDExpr] -> FDConstr -> [[Int]]
-- solveFD Z3   exs c = unsafePerformIO $ solveSMT z3Config exs c
-- solveFD CVC4 exs c = unsafePerformIO $ solveSMT cvc4Config exs c
solveFD :: SolverOptions -> [FDExpr] -> FDConstr -> [[Int]]
solveFD = solveFDwith Z3

solveFDwith :: Solvers -> SolverOptions -> [FDExpr] -> FDConstr -> [[Int]]
solveFDwith s opt exs c =
  let (sol, cfg) = case s of
                    Z3    -> (solveSMT, z3Config)
                    CVC4  -> (solveSMT, cvc4Config)
  in unsafePerformIO $ sol cfg opt exs c