Notice to GitKraken users: A vulnerability has been found in the SSH key generation of GitKraken versions 7.6.0 to 8.0.0 (https://www.gitkraken.com/blog/weak-ssh-key-fix). If you use GitKraken and have generated a SSH key using one of these versions, please remove it both from your local workstation and from your LRZ GitLab profile.

21.10.2021, 9:00 - 11:00: Due to updates GitLab may be unavailable for some minutes between 09:00 and 11:00.

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

3
module Solver
4
5
    (checkSat,ModelSI,ModelSB,ModelI,ModelB,
     Model(..),mVal,mValues,mElemsWith,mElemSum,SModel(..),CModel(..))
6
7
8
9
10
where

import Data.SBV
import qualified Data.Map as M

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
38
39
40
41
42
43
44
45
46
47
48
49
50
newtype Model a = Model { getMap :: M.Map String a } deriving Show

type ModelSI = Model SInteger
type ModelSB = Model SBool
type ModelI = Model Integer
type ModelB = Model Bool

mVal :: Model a -> String -> a
mVal m x = getMap m M.! x

mValues :: Model a -> [a]
mValues m = M.elems $ getMap m

mElemsWith :: (a -> Bool) -> Model a -> [String]
mElemsWith f m = M.keys $ M.filter f $ getMap m

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
51

52
symConstraints :: SymWord a => [String] -> (Model (SBV a) -> SBool) ->
53
54
        Symbolic SBool
symConstraints vars constraint = do
55
        syms <- mapM exists vars
56
        return $ constraint $ Model $ M.fromList $ vars `zip` syms
57

58
rebuildModel :: SymWord a => [String] -> Either String (Bool, [a]) ->
59
        Maybe (Model a)
60
61
rebuildModel _ (Left _) = Nothing
rebuildModel _ (Right (True, _)) = error "Prover returned unknown"
62
rebuildModel vars (Right (False, m)) = Just $ Model $ M.fromList $ vars `zip` m
63

64
checkSat :: (SatModel a, SymWord a) =>
65
66
        ([String], Model (SBV a) -> SBool) ->
        IO (Maybe (Model a))
67
checkSat (vars, constraint) = do
68
        result <- satWith z3{verbose=False} $ symConstraints vars constraint
69
        return $ rebuildModel vars $ getModel result