Solver.hs 3.08 KB
Newer Older
1 2
{-# LANGUAGE TypeSynonymInstances, FlexibleInstances #-}

3
module Solver
4
    (prime,checkSat,checkSatMin,val,vals,positiveVal,zeroVal,
5
     getNames,ConstraintProblem,MinConstraintProblem)
6 7 8 9 10
where

import Data.SBV
import qualified Data.Map as M

Philipp Meyer's avatar
Philipp Meyer committed
11
import Util
Philipp Meyer's avatar
Philipp Meyer committed
12 13
import Options
import Control.Monad.IO.Class
14
import Control.Applicative
15

Philipp Meyer's avatar
Philipp Meyer committed
16
type ConstraintProblem a b =
17
        (String, String, [String], (String -> SBV a) -> SBool, (String -> a) -> b)
18 19
type MinConstraintProblem a b c =
        (Int -> c -> String, Maybe (Int, c) -> ConstraintProblem a (b, c))
Philipp Meyer's avatar
Philipp Meyer committed
20

21
rebuildModel :: SymWord a => [String] -> Either String (Bool, [a]) ->
22
        Maybe (Model a)
23 24
rebuildModel _ (Left _) = Nothing
rebuildModel _ (Right (True, _)) = error "Prover returned unknown"
Philipp Meyer's avatar
Philipp Meyer committed
25 26
rebuildModel vars (Right (False, m)) = Just $ M.fromList $ vars `zip` m

27
symConstraints :: SymWord a => [String] -> ((String -> SBV a) -> SBool) ->
28
        Symbolic SBool
29
symConstraints vars constraint = do
30
        syms <- mapM exists vars
31
        return $ constraint $ val $ M.fromList $ (vars `zip` syms)
32

33 34 35 36 37 38 39 40
getSolverConfig :: BackendSolver -> Bool -> SMTConfig
getSolverConfig Options.Z3 verbose = z3 { verbose=verbose }
getSolverConfig Options.CVC4 verbose =
        cvc4 {
            verbose=verbose,
            solverSetOptions = [],
            solver = (solver cvc4) { Data.SBV.options = const ["--lang", "smt", "--incremental", "--no-interactive-prompt"] }
        }
41

Philipp Meyer's avatar
Philipp Meyer committed
42 43
checkSat :: (SatModel a, SymWord a, Show a, Show b) =>
        ConstraintProblem a b -> OptIO (Maybe b)
44
checkSat (problemName, resultName, vars, constraint, interpretation) = do
45
        verbosePut 2 $ "Checking SAT of " ++ problemName
Philipp Meyer's avatar
Philipp Meyer committed
46
        verbosity <- opt optVerbosity
47 48
        solver <- opt optSolver
        result <- liftIO (satWith (getSolverConfig solver (verbosity >= 4))
49
                    (symConstraints vars constraint))
Philipp Meyer's avatar
Philipp Meyer committed
50
        case rebuildModel vars (getModelAssignment result) of
51
            Nothing -> do
Philipp Meyer's avatar
Philipp Meyer committed
52
                verbosePut 2 "- unsat"
53 54
                return Nothing
            Just rawModel -> do
Philipp Meyer's avatar
Philipp Meyer committed
55
                verbosePut 2 "- sat"
56
                let model = interpretation $ val rawModel
Philipp Meyer's avatar
Philipp Meyer committed
57 58
                verbosePut 3 $ "- " ++ resultName ++ ": " ++ show model
                verbosePut 4 $ "- raw model: " ++ show rawModel
59 60
                return $ Just model

61
checkSatMin :: (SatModel a, SymWord a, Show a, Show b, Show c) =>
62 63
        MinConstraintProblem a b c -> OptIO (Maybe b)
checkSatMin (minMethod, minProblem) = do
64 65 66 67
        optMin <- opt optMinimizeRefinement
        r0 <- checkSat $ minProblem Nothing
        case r0 of
            Nothing -> return Nothing
68
            Just (result, curSize) ->
69
                if optMin > 0 then
70
                    Just <$> findSmaller optMin result curSize
71 72
                else
                    return $ Just result
73
    where findSmaller optMin result curSize = do
74
            verbosePut 2 $ "Checking for " ++ minMethod optMin curSize
75
            r1 <- checkSat $ minProblem (Just (optMin, curSize))
76 77
            case r1 of
                Nothing -> return result
78
                Just (result', curSize') -> findSmaller optMin result' curSize'
79