https://stackoverflow.com/questions/23233969
italiano
english
français
española
中国
日本の
العربية
Deutsch
한국어
Português
RussianWorking With SBV
Working with SBV requires that you follow the types and realize the Predicate is just a Symbolic SBool. After that step it is important that you investigate and discover Symbolic is a monad - yay, a monad!
Now that you you know you have a monad then anything in the haddock that is Symbolic should be trivial to combine to build any SAT you desire. For your problem you just need a simple interpreter over your AST that builds a Predicate.
Code Walk-Through
The code is all included in one continuous form below but I will step through the fun parts. The entry point is solveExpr which takes expressions and produces a SAT result:
solveExpr :: Expr -> IO AllSatResult
solveExpr e0 = allSat prd
The application of SBV's allSat to the predicate is sort of obvious. To build that predicate we need to declare an existential SBool for every variable in our expression. For now lets assume we have vs :: [String] where each string corresponds to one of the Var from the expression.
prd :: Predicate
prd = do
syms <- mapM exists vs
let env = M.fromList (zip vs syms)
interpret env e0
Notice how programming language fundamentals is sneaking in here. We now need an environment that maps the expressions variable names to the symbolic booleans used by SBV.
Next we interpret the expression to produce our Predicate. The interpret function uses the environment and just applies the SBV function that matches the intent of each constructor from hatt's Expr type.
interpret :: Env -> Expr -> Predicate
interpret env expr = do
let interp = interpret env
case expr of
Variable v -> return (envLookup v env)
Negation e -> bnot `fmap` interp e
Conjunction e1 e2 ->
do r1 <- interp e1
r2 <- interp e2
return (r1 &&& r2)
Disjunction e1 e2 ->
do r1 <- interp e1
r2 <- interp e2
return (r1 ||| r2)
Conditional e1 e2 -> error "And so on"
Biconditional e1 e2 -> error "And so on"
And that is it! The rest is just boiler-plate.
Complete Code
import Data.Logic.Propositional hiding (interpret)
import Data.SBV
import Text.Parsec.Error (ParseError)
import qualified Data.Map as M
import qualified Data.Set as Set
import Data.Foldable (foldMap)
import Control.Monad ((<=<))
testParse :: Either ParseError Expr
testParse = parseExpr "test source" "((X | ~Z) & (Y | ~Z))"
type Env = M.Map String SBool
envLookup :: Var -> Env -> SBool
envLookup (Var v) e = maybe (error $ "Var not found: " ++ show v) id
(M.lookup [v] e)
solveExpr :: Expr -> IO AllSatResult
solveExpr e0 = allSat go
where
vs :: [String]
vs = map (\(Var c) -> [c]) (variables e0)
go :: Predicate
go = do
syms <- mapM exists vs
let env = M.fromList (zip vs syms)
interpret env e0
interpret :: Env -> Expr -> Predicate
interpret env expr = do
let interp = interpret env
case expr of
Variable v -> return (envLookup v env)
Negation e -> bnot `fmap` interp e
Conjunction e1 e2 ->
do r1 <- interp e1
r2 <- interp e2
return (r1 &&& r2)
Disjunction e1 e2 ->
do r1 <- interp e1
r2 <- interp e2
return (r1 ||| r2)
Conditional e1 e2 -> error "And so on"
Biconditional e1 e2 -> error "And so on"
main :: IO ()
main = do
let expr = testParse
putStrLn $ "Solving expr: " ++ show expr
either (error . show) (print <=< solveExpr) expr
