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

3
module Solver
4
    (prime,checkSat,ModelReader,val,vals,valMap,VarMap,
Philipp Meyer's avatar
Philipp Meyer committed
5
     getNames,makeVarMap,makeVarMapWith,
6
     IntConstraint,BoolConstraint,IntResult,BoolResult,
Philipp Meyer's avatar
Philipp Meyer committed
7
     Model,ConstraintProblem)
8
9
10
11
where

import Data.SBV
import qualified Data.Map as M
12
import Control.Monad.Reader
13

Philipp Meyer's avatar
Philipp Meyer committed
14
import Util
15

Philipp Meyer's avatar
Philipp Meyer committed
16
17
type Model a = M.Map String a
type VarMap a = M.Map a String
18

Philipp Meyer's avatar
Philipp Meyer committed
19
20
getNames :: VarMap a -> [String]
getNames = M.elems
21

22
23
24
25
26
27
type ModelReader a b = Reader (Model a) b
type IntConstraint = ModelReader SInteger SBool
type BoolConstraint = ModelReader SBool SBool
type IntResult a = ModelReader Integer a
type BoolResult a = ModelReader Bool a

Philipp Meyer's avatar
Philipp Meyer committed
28
29
30
type ConstraintProblem a b =
        (String, String, [String], ModelReader (SBV a) SBool, ModelReader a b)

31
32
33
val :: (Ord a) => VarMap a -> a -> ModelReader b b
val ma x = do
        mb <- ask
Philipp Meyer's avatar
Philipp Meyer committed
34
35
        return $ mb M.! (ma M.! x)

36
37
38
39
40
41
valMap :: (Ord a) => VarMap a -> ModelReader b (M.Map a b)
valMap ma = do
        mb <- ask
        return $ M.map (mb M.!) ma

vals :: (Ord a) => VarMap a -> ModelReader b [b]
Philipp Meyer's avatar
Philipp Meyer committed
42
43
vals ma = do
        mb <- ask
44
        return $ M.elems $ M.map (mb M.!) ma
45
46
47
48
49

makeVarMap :: (Show a, Ord a) => [a] -> VarMap a
makeVarMap = makeVarMapWith id

makeVarMapWith :: (Show a, Ord a) => (String -> String) -> [a] -> VarMap a
Philipp Meyer's avatar
Philipp Meyer committed
50
makeVarMapWith f xs = M.fromList $ xs `zip` map (f . show) xs
51

52
53
prime :: String -> String
prime = ('\'':)
Philipp Meyer's avatar
Philipp Meyer committed
54
{-
55
mVal :: Model a -> String -> a
Philipp Meyer's avatar
Philipp Meyer committed
56
mVal m x = M.findWithDefault (error ("key not found: " ++ x)) x m
57
58

mValues :: Model a -> [a]
Philipp Meyer's avatar
Philipp Meyer committed
59
mValues = M.elems
60
61

mElemsWith :: (a -> Bool) -> Model a -> [String]
Philipp Meyer's avatar
Philipp Meyer committed
62
mElemsWith f m = M.keys $ M.filter f m
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87

mElemSum :: (Num a) => Model a -> [String] -> a
mElemSum m xs = sum $ map (mVal m) xs

class SModel a where
        mElem :: Model a -> String -> SBool
        mNotElem :: Model a -> String -> SBool
        mNotElem m x = bnot $ mElem m x
class CModel a where
        cElem :: Model a -> String -> Bool
        cNotElem :: Model a -> String -> Bool
        cNotElem m x = not $ cElem m x

instance SModel SInteger where
        mElem m x = mVal m x .> 0
        mNotElem m x = mVal m x .== 0
instance SModel SBool where
        mElem = mVal
        mNotElem m x = bnot $ mVal m x
instance CModel Integer where
        cElem m x = mVal m x > 0
        cNotElem m x = mVal m x == 0
instance CModel Bool where
        cElem = mVal
        cNotElem m x = not $ mVal m x
Philipp Meyer's avatar
Philipp Meyer committed
88
-}
89
symConstraints :: SymWord a => [String] -> ModelReader (SBV a) SBool ->
90
91
        Symbolic SBool
symConstraints vars constraint = do
92
        syms <- mapM exists vars
Philipp Meyer's avatar
Philipp Meyer committed
93
        return $ runReader constraint $ M.fromList $ vars `zip` syms
94

95
rebuildModel :: SymWord a => [String] -> Either String (Bool, [a]) ->
96
        Maybe (Model a)
97
98
rebuildModel _ (Left _) = Nothing
rebuildModel _ (Right (True, _)) = error "Prover returned unknown"
Philipp Meyer's avatar
Philipp Meyer committed
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
rebuildModel vars (Right (False, m)) = Just $ M.fromList $ vars `zip` m

checkSat :: (SatModel a, SymWord a, Show a, Show b) => Int ->
        ConstraintProblem a b -> IO (Maybe b)
checkSat verbosity (problemName, resultName, vars, constraint, interpretation) = do
        verbosePut verbosity 1 $ "Checking SAT of " ++ problemName
        result <- satWith z3{verbose=verbosity >= 4} $
            symConstraints vars constraint
        case rebuildModel vars (getModel result) of
            Nothing -> do
                verbosePut verbosity 2 "- unsat"
                return Nothing
            Just rawModel -> do
                verbosePut verbosity 2 "- sat"
                let model = runReader interpretation rawModel
                verbosePut verbosity 3 $ "- " ++ resultName ++ ": " ++ show model
                return $ Just model
116