Solver.hs 3.62 KB
 Philipp Meyer committed May 16, 2014 1 2 ``````{-# LANGUAGE TypeSynonymInstances, FlexibleInstances #-} `````` Philipp Meyer committed May 06, 2014 3 ``````module Solver `````` Philipp Meyer committed Dec 16, 2014 4 `````` (prime,checkSat,ModelReader,val,vals,valMap,VarMap, `````` Philipp Meyer committed Dec 16, 2014 5 `````` getNames,makeVarMap,makeVarMapWith, `````` Philipp Meyer committed Dec 16, 2014 6 `````` IntConstraint,BoolConstraint,IntResult,BoolResult, `````` Philipp Meyer committed Dec 16, 2014 7 `````` Model,ConstraintProblem) `````` Philipp Meyer committed May 06, 2014 8 9 10 11 ``````where import Data.SBV import qualified Data.Map as M `````` Philipp Meyer committed Dec 16, 2014 12 ``````import Control.Monad.Reader `````` Philipp Meyer committed May 06, 2014 13 `````` `````` Philipp Meyer committed Dec 16, 2014 14 ``````import Util `````` Philipp Meyer committed Dec 16, 2014 15 `````` `````` Philipp Meyer committed Dec 16, 2014 16 17 ``````type Model a = M.Map String a type VarMap a = M.Map a String `````` Philipp Meyer committed Jul 15, 2014 18 `````` `````` Philipp Meyer committed Dec 16, 2014 19 20 ``````getNames :: VarMap a -> [String] getNames = M.elems `````` Philipp Meyer committed May 16, 2014 21 `````` `````` Philipp Meyer committed Dec 16, 2014 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 committed Dec 16, 2014 28 29 30 ``````type ConstraintProblem a b = (String, String, [String], ModelReader (SBV a) SBool, ModelReader a b) `````` Philipp Meyer committed Dec 16, 2014 31 32 33 ``````val :: (Ord a) => VarMap a -> a -> ModelReader b b val ma x = do mb <- ask `````` Philipp Meyer committed Dec 16, 2014 34 35 `````` return \$ mb M.! (ma M.! x) `````` Philipp Meyer committed Dec 16, 2014 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 committed Dec 16, 2014 42 43 ``````vals ma = do mb <- ask `````` Philipp Meyer committed Dec 16, 2014 44 `````` return \$ M.elems \$ M.map (mb M.!) ma `````` Philipp Meyer committed Dec 16, 2014 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 committed Dec 16, 2014 50 ``````makeVarMapWith f xs = M.fromList \$ xs `zip` map (f . show) xs `````` Philipp Meyer committed May 16, 2014 51 `````` `````` Philipp Meyer committed Dec 02, 2014 52 53 ``````prime :: String -> String prime = ('\'':) `````` Philipp Meyer committed Dec 16, 2014 54 ``````{- `````` Philipp Meyer committed May 16, 2014 55 ``````mVal :: Model a -> String -> a `````` Philipp Meyer committed Dec 16, 2014 56 ``````mVal m x = M.findWithDefault (error ("key not found: " ++ x)) x m `````` Philipp Meyer committed May 16, 2014 57 58 `````` mValues :: Model a -> [a] `````` Philipp Meyer committed Dec 16, 2014 59 ``````mValues = M.elems `````` Philipp Meyer committed May 16, 2014 60 61 `````` mElemsWith :: (a -> Bool) -> Model a -> [String] `````` Philipp Meyer committed Dec 16, 2014 62 ``````mElemsWith f m = M.keys \$ M.filter f m `````` Philipp Meyer committed May 16, 2014 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 committed Dec 16, 2014 88 ``````-} `````` Philipp Meyer committed Dec 16, 2014 89 ``````symConstraints :: SymWord a => [String] -> ModelReader (SBV a) SBool -> `````` Philipp Meyer committed May 07, 2014 90 91 `````` Symbolic SBool symConstraints vars constraint = do `````` Philipp Meyer committed May 06, 2014 92 `````` syms <- mapM exists vars `````` Philipp Meyer committed Dec 16, 2014 93 `````` return \$ runReader constraint \$ M.fromList \$ vars `zip` syms `````` Philipp Meyer committed May 07, 2014 94 `````` `````` Philipp Meyer committed May 09, 2014 95 ``````rebuildModel :: SymWord a => [String] -> Either String (Bool, [a]) -> `````` Philipp Meyer committed May 16, 2014 96 `````` Maybe (Model a) `````` Philipp Meyer committed May 07, 2014 97 98 ``````rebuildModel _ (Left _) = Nothing rebuildModel _ (Right (True, _)) = error "Prover returned unknown" `````` Philipp Meyer committed Dec 16, 2014 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 `````` Philipp Meyer committed Dec 16, 2014 116