Starting from 2021-07-01, all LRZ GitLab users will be required to explicitly accept the GitLab Terms of Service. Please see the detailed information at https://doku.lrz.de/display/PUBLIC/GitLab and make sure that your projects conform to the requirements.

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

3
module Solver
4 5
    (checkSat,checkSatInt,checkSatBool,MModelS,MModelI,MModelB,
     MModel(..),mVal,mValues,mElemsWith,mElemSum,CModel(..),
6
     Z3Type(..),mkOr',mkAnd',mkAdd',mkSub',mkMul')
7 8
where

9 10
import Z3.Monad
import Control.Monad
11
import qualified Data.Map as M
12

13
newtype MModel a = MModel { getMap :: M.Map String a }
14

15
instance Show a => Show (MModel a) where
16
        show = show . M.toList . getMap
17

18 19
type MModelS = MModel AST
type MModelI = MModel Integer
20
type MModelB = MModel (Maybe Bool)
21

22
class Z3Type a where
23
        mkVal :: a -> Z3 AST
24
        getVal :: AST -> Z3 a
25 26

instance Z3Type Integer where
27 28 29 30 31 32 33 34 35
        mkVal = mkInt
        getVal = getInt

instance Z3Type (Maybe Bool) where
        mkVal x = case x of
                      Nothing -> error "can not make undefined constant"
                      Just True -> mkTrue
                      Just False -> mkFalse
        getVal  = getBool
36 37

mVal :: MModel a -> String -> a
38
mVal m x = M.findWithDefault (error ("key not found: " ++ x)) x (getMap m)
39

40
mValues :: MModel a -> [a]
41 42
mValues m = M.elems $ getMap m

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

46
mElemSum :: (Num a) => MModel a -> [String] -> a
47 48
mElemSum m xs = sum $ map (mVal m) xs

49 50 51 52 53 54 55 56
mkOr' :: [AST] -> Z3 AST
mkOr' [] = mkFalse
mkOr' xs = mkOr xs

mkAnd' :: [AST] -> Z3 AST
mkAnd' [] = mkTrue
mkAnd' xs = mkAnd xs

57 58 59 60 61 62 63 64 65 66 67 68
mkAdd' :: [AST] -> Z3 AST
mkAdd' [] = mkInt (0::Integer)
mkAdd' xs = mkAdd xs

mkSub' :: [AST] -> Z3 AST
mkSub' [] = mkInt (0::Integer)
mkSub' xs = mkSub xs

mkMul' :: [AST] -> Z3 AST
mkMul' [] = mkInt (1::Integer)
mkMul' xs = mkMul xs

69 70 71 72
--class SMModel a where
--        mElem :: MModel a -> String -> Z3 AST
--        mNotElem :: MModel a -> String -> Z3 AST
--        mNotElem m x = mkNot =<< mElem m x
73
class CModel a where
74 75
        cElem :: MModel a -> String -> Bool
        cNotElem :: MModel a -> String -> Bool
76 77
        cNotElem m x = not $ cElem m x

78 79 80 81 82 83
--instance SMModel AST where
--        mElem m x = (mVal m x `mkGt`) =<< mkInt 0
--        mNotElem m x = mkEq (mVal m x) =<< mkInt 0
--instance SMModel AST where
--        mElem = mVal
--        mNotElem m x = mkNot $ mVal m x
84 85 86 87 88 89
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
90

91 92 93 94 95 96 97 98 99 100 101 102 103 104
checkSat :: Z3Type a => Z3 Sort -> ([String], MModel AST -> Z3 ()) ->
        Z3 (Maybe (MModel a))
checkSat mkSort (vars, constraint) = do
        sort <- mkSort
        syms <- mapM (mkStringSymbol >=> flip mkConst sort) vars
        let smodel = MModel $ M.fromList $ vars `zip` syms
        constraint smodel
        result <- getModel
        case result of
            (Unsat, Nothing) -> return Nothing
            (Sat, Just m) -> do
                ms <- evalT m syms
                case ms of
                    Just xs -> do
105
                        vals <- mapM getVal xs
106 107 108 109 110 111
                        let cmodel = MModel $ M.fromList $ vars `zip` vals
                        return $ Just cmodel
                    Nothing -> error "Prover returned incomplete model"
            (Undef, _) -> error "Prover returned unknown"
            (Unsat, Just _) -> error "Prover returned unsat but a model"
            (Sat, Nothing) -> error "Prover returned sat but no model"
112

113
checkSatInt :: ([String], MModel AST -> Z3 ()) -> IO (Maybe (MModel Integer))
114 115 116 117
checkSatInt = evalZ3 . checkSat mkIntSort

checkSatBool :: ([String], MModel AST -> Z3 ()) -> IO (Maybe (MModel (Maybe Bool)))
checkSatBool = evalZ3 . checkSat mkBoolSort