Notice: If you are member of any public project or group, please make sure that your GitLab username is not the same as the LRZ identifier/Kennung (see https://gitlab.lrz.de/profile/account). Please change your username if necessary. For more information see the section "Public projects / Öffentliche Projekte" at https://doku.lrz.de/display/PUBLIC/GitLab . Thank you!

Solver.hs 3.08 KB
 Philipp Meyer committed May 16, 2014 1 2 ``````{-# LANGUAGE TypeSynonymInstances, FlexibleInstances #-} `````` Philipp Meyer committed May 06, 2014 3 ``````module Solver `````` Philipp Meyer committed Feb 03, 2015 4 `````` (prime,checkSat,checkSatMin,val,vals,positiveVal,zeroVal, `````` Philipp Meyer committed Dec 22, 2016 5 `````` getNames,ConstraintProblem,MinConstraintProblem) `````` Philipp Meyer committed May 06, 2014 6 7 8 9 10 ``````where import Data.SBV import qualified Data.Map as M `````` Philipp Meyer committed Dec 16, 2014 11 ``````import Util `````` Philipp Meyer committed Dec 24, 2014 12 13 ``````import Options import Control.Monad.IO.Class `````` Philipp Meyer committed Feb 03, 2015 14 ``````import Control.Applicative `````` Philipp Meyer committed Dec 16, 2014 15 `````` `````` Philipp Meyer committed Dec 16, 2014 16 ``````type ConstraintProblem a b = `````` Philipp Meyer committed Aug 08, 2018 17 `````` (String, String, [String], (String -> SBV a) -> SBool, (String -> a) -> b) `````` Philipp Meyer committed Dec 22, 2016 18 19 ``````type MinConstraintProblem a b c = (Int -> c -> String, Maybe (Int, c) -> ConstraintProblem a (b, c)) `````` Philipp Meyer committed Dec 16, 2014 20 `````` `````` Philipp Meyer committed May 09, 2014 21 ``````rebuildModel :: SymWord a => [String] -> Either String (Bool, [a]) -> `````` Philipp Meyer committed May 16, 2014 22 `````` Maybe (Model a) `````` Philipp Meyer committed May 07, 2014 23 24 ``````rebuildModel _ (Left _) = Nothing rebuildModel _ (Right (True, _)) = error "Prover returned unknown" `````` Philipp Meyer committed Dec 16, 2014 25 26 ``````rebuildModel vars (Right (False, m)) = Just \$ M.fromList \$ vars `zip` m `````` Philipp Meyer committed Aug 08, 2018 27 ``````symConstraints :: SymWord a => [String] -> ((String -> SBV a) -> SBool) -> `````` Philipp Meyer committed Dec 19, 2014 28 `````` Symbolic SBool `````` Philipp Meyer committed Aug 08, 2018 29 ``````symConstraints vars constraint = do `````` Philipp Meyer committed Dec 19, 2014 30 `````` syms <- mapM exists vars `````` Philipp Meyer committed Aug 08, 2018 31 `````` return \$ constraint \$ val \$ M.fromList \$ (vars `zip` syms) `````` Philipp Meyer committed Dec 19, 2014 32 `````` `````` Philipp Meyer committed Aug 02, 2018 33 34 35 36 37 38 39 40 ``````getSolverConfig :: BackendSolver -> Bool -> SMTConfig getSolverConfig Options.Z3 verbose = z3 { verbose=verbose } getSolverConfig Options.CVC4 verbose = cvc4 { verbose=verbose, solverSetOptions = [], solver = (solver cvc4) { Data.SBV.options = const ["--lang", "smt", "--incremental", "--no-interactive-prompt"] } } `````` Philipp Meyer committed Feb 07, 2017 41 `````` `````` Philipp Meyer committed Dec 24, 2014 42 43 ``````checkSat :: (SatModel a, SymWord a, Show a, Show b) => ConstraintProblem a b -> OptIO (Maybe b) `````` Philipp Meyer committed Aug 08, 2018 44 ``````checkSat (problemName, resultName, vars, constraint, interpretation) = do `````` Philipp Meyer committed Feb 13, 2015 45 `````` verbosePut 2 \$ "Checking SAT of " ++ problemName `````` Philipp Meyer committed Dec 24, 2014 46 `````` verbosity <- opt optVerbosity `````` Philipp Meyer committed Aug 02, 2018 47 48 `````` solver <- opt optSolver result <- liftIO (satWith (getSolverConfig solver (verbosity >= 4)) `````` Philipp Meyer committed Aug 08, 2018 49 `````` (symConstraints vars constraint)) `````` Philipp Meyer committed Aug 01, 2018 50 `````` case rebuildModel vars (getModelAssignment result) of `````` Philipp Meyer committed Dec 19, 2014 51 `````` Nothing -> do `````` Philipp Meyer committed Dec 24, 2014 52 `````` verbosePut 2 "- unsat" `````` Philipp Meyer committed Dec 19, 2014 53 54 `````` return Nothing Just rawModel -> do `````` Philipp Meyer committed Dec 24, 2014 55 `````` verbosePut 2 "- sat" `````` Philipp Meyer committed Dec 22, 2014 56 `````` let model = interpretation \$ val rawModel `````` Philipp Meyer committed Dec 24, 2014 57 58 `````` verbosePut 3 \$ "- " ++ resultName ++ ": " ++ show model verbosePut 4 \$ "- raw model: " ++ show rawModel `````` Philipp Meyer committed Dec 19, 2014 59 60 `````` return \$ Just model `````` Philipp Meyer committed Feb 11, 2015 61 ``````checkSatMin :: (SatModel a, SymWord a, Show a, Show b, Show c) => `````` Philipp Meyer committed Dec 22, 2016 62 63 `````` MinConstraintProblem a b c -> OptIO (Maybe b) checkSatMin (minMethod, minProblem) = do `````` Philipp Meyer committed Feb 03, 2015 64 65 66 67 `````` optMin <- opt optMinimizeRefinement r0 <- checkSat \$ minProblem Nothing case r0 of Nothing -> return Nothing `````` Philipp Meyer committed Feb 16, 2015 68 `````` Just (result, curSize) -> `````` Philipp Meyer committed Feb 12, 2015 69 `````` if optMin > 0 then `````` Philipp Meyer committed Feb 16, 2015 70 `````` Just <\$> findSmaller optMin result curSize `````` Philipp Meyer committed Feb 03, 2015 71 72 `````` else return \$ Just result `````` Philipp Meyer committed Feb 16, 2015 73 `````` where findSmaller optMin result curSize = do `````` Philipp Meyer committed Dec 22, 2016 74 `````` verbosePut 2 \$ "Checking for " ++ minMethod optMin curSize `````` Philipp Meyer committed Feb 16, 2015 75 `````` r1 <- checkSat \$ minProblem (Just (optMin, curSize)) `````` Philipp Meyer committed Feb 03, 2015 76 77 `````` case r1 of Nothing -> return result `````` Philipp Meyer committed Feb 16, 2015 78 `````` Just (result', curSize') -> findSmaller optMin result' curSize' `````` Philipp Meyer committed Feb 03, 2015 79