smt - SAT solving with haskell SBV library: how to generate a predicate from a parsed string?

Question

I want to parse a String that depicts a propositional formula and then find all models of the propositional formula with a SAT solver.

Now I can parse a propositional formula with the hatt package; see the testParse function below.

I can also run a SAT solver call with the SBV library; see the testParse function below.

Question: How do I, at runtime, generate a value of type Predicate like myPredicate within the SBV library that represents the propositional formula I just parsed from a String? I only know how to manually type the forSome_ $ x y z -> ... expression, but not how to write a converter function from an Expr value to a value of type Predicate.

-- cabal install sbv hatt
import Data.Logic.Propositional
import Data.SBV


-- Random test formula:
-- (x or ~z) and (y or ~z)

-- graphical depiction, see: https://www.wolframalpha.com/input/?i=%28x+or+~z%29+and+%28y+or+~z%29

testParse = parseExpr "test source" "((X | ~Z) & (Y | ~Z))"

myPredicate :: Predicate
myPredicate = forSome_ $ x y z -> ((x :: SBool) ||| (bnot z)) &&& (y ||| (bnot z))

testSat = do 
         x <- allSat $ myPredicate
         putStrLn $ show x     


main = do
       putStrLn $ show $ testParse
       testSat


    {-
       Need a function that dynamically creates a Predicate 
(as I did with the function (like "x y z -> ..") for an arbitrary expression of type "Expr" that is parsed from String. 
    -}

Information that might be helpful:

Here is the link to the BitVectors.Data: http://hackage.haskell.org/package/sbv-3.0/docs/src/Data-SBV-BitVectors-Data.html

Here is example code form Examples.Puzzles.PowerSet:

import Data.SBV

genPowerSet :: [SBool] -> SBool
genPowerSet = bAll isBool
  where isBool x = x .== true ||| x .== false

powerSet :: [Word8] -> IO ()
powerSet xs = do putStrLn $ "Finding all subsets of " ++ show xs
                 res <- allSat $ genPowerSet `fmap` mkExistVars n

Here is the Expr data type (from hatt library):

data Expr = Variable      Var
          | Negation      Expr
          | Conjunction   Expr Expr
          | Disjunction   Expr Expr
          | Conditional   Expr Expr
          | Biconditional Expr Expr
          deriving Eq

Answer 1

Working 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