In January 2021 we will introduce a 10 GB quota for project repositories. Higher limits for individual projects will be available on request. Please see https://doku.lrz.de/display/PUBLIC/GitLab for more information.

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

3
module Solver
4
    (prime,checkSat,checkSatMin,val,vals,positiveVal,zeroVal,
5
     getNames,ConstraintProblem,MinConstraintProblem)
6 7 8 9 10
where

import Data.SBV
import qualified Data.Map as M

Philipp Meyer's avatar
Philipp Meyer committed
11
import Util
Philipp Meyer's avatar
Philipp Meyer committed
12 13
import Options
import Control.Monad.IO.Class
14
import Control.Applicative
15

Philipp Meyer's avatar
Philipp Meyer committed
16
type ConstraintProblem a b =
17
        (String, String, [String], [String], [String], (String -> SBV a) -> SBool, (String -> a) -> b)
18 19
type MinConstraintProblem a b c =
        (Int -> c -> String, Maybe (Int, c) -> ConstraintProblem a (b, c))
Philipp Meyer's avatar
Philipp Meyer committed
20

21
rebuildModel :: SymWord a => [String] -> Either String (Bool, [a]) ->
22
        Maybe (Model a)
23 24
rebuildModel _ (Left _) = Nothing
rebuildModel _ (Right (True, _)) = error "Prover returned unknown"
Philipp Meyer's avatar
Philipp Meyer committed
25 26
rebuildModel vars (Right (False, m)) = Just $ M.fromList $ vars `zip` m

27
symConstraints :: SymWord a => [String] -> [String] -> [String] -> ((String -> SBV a) -> SBool) ->
28
        Symbolic SBool
29
symConstraints vars exVars allVars constraint = do
30
        syms <- mapM exists vars
31 32 33
        exSyms <- mapM exists exVars
        allSyms <- mapM forall allVars
        return $ constraint $ val $ M.fromList $ (vars `zip` syms) ++ (exVars `zip` exSyms) ++ (allVars `zip` allSyms)
34

35 36 37 38 39 40 41 42
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"] }
        }
43

Philipp Meyer's avatar
Philipp Meyer committed
44 45
checkSat :: (SatModel a, SymWord a, Show a, Show b) =>
        ConstraintProblem a b -> OptIO (Maybe b)
46
checkSat (problemName, resultName, vars, exVars, allVars, constraint, interpretation) = do
47
        verbosePut 2 $ "Checking SAT of " ++ problemName
Philipp Meyer's avatar
Philipp Meyer committed
48
        verbosity <- opt optVerbosity
49 50
        solver <- opt optSolver
        result <- liftIO (satWith (getSolverConfig solver (verbosity >= 4))
51
                    (symConstraints vars exVars allVars constraint))
Philipp Meyer's avatar
Philipp Meyer committed
52
        case rebuildModel vars (getModelAssignment result) of
53
            Nothing -> do
Philipp Meyer's avatar
Philipp Meyer committed
54
                verbosePut 2 "- unsat"
55 56
                return Nothing
            Just rawModel -> do
Philipp Meyer's avatar
Philipp Meyer committed
57
                verbosePut 2 "- sat"
58
                let model = interpretation $ val rawModel
Philipp Meyer's avatar
Philipp Meyer committed
59 60
                verbosePut 3 $ "- " ++ resultName ++ ": " ++ show model
                verbosePut 4 $ "- raw model: " ++ show rawModel
61 62
                return $ Just model

63
checkSatMin :: (SatModel a, SymWord a, Show a, Show b, Show c) =>
64 65
        MinConstraintProblem a b c -> OptIO (Maybe b)
checkSatMin (minMethod, minProblem) = do
66 67 68 69
        optMin <- opt optMinimizeRefinement
        r0 <- checkSat $ minProblem Nothing
        case r0 of
            Nothing -> return Nothing
70
            Just (result, curSize) ->
71
                if optMin > 0 then
72
                    Just <$> findSmaller optMin result curSize
73 74
                else
                    return $ Just result
75
    where findSmaller optMin result curSize = do
76
            verbosePut 2 $ "Checking for " ++ minMethod optMin curSize
77
            r1 <- checkSat $ minProblem (Just (optMin, curSize))
78 79
            case r1 of
                Nothing -> return result
80
                Just (result', curSize') -> findSmaller optMin result' curSize'
81