Solver.hs 3.13 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], [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] -> [String] -> ((String -> SBV a) -> SBool) ->
28
        Symbolic SBool
29
symConstraints vars exVars allVars constraint = do
30
        syms <- mapM exists vars
31
32
33
        exSyms <- mapM exists exVars
        allSyms <- mapM forall allVars
        return $ constraint $ val $ M.fromList $ (vars `zip` syms) ++ (exVars `zip` exSyms) ++ (allVars `zip` allSyms)
34

35
36
37
38
39
getSolverConfig :: Bool -> Bool -> SMTConfig
getSolverConfig verbose auto =
        let tweaks = if auto then [] else ["(set-option :auto_config false)"]
        in  z3{ verbose=verbose, solverTweaks=tweaks }

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

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