Quiero analizar unString que representa una fórmula proposicional y luego encuentra todos los modelos de la fórmula proposicional con un solucionador SAT.

Ahora puedo analizar una fórmula proposicional con elhatt paquete; ver eltestParse Funcionan a continuación.

También puedo ejecutar una llamada de solucionador SAT con la biblioteca SBV; ver eltestParse Funcionan a continuación.

Pregunta: ¿Cómo, en tiempo de ejecución, genero un valor de tipoPredicate me gustamyPredicate dentro de la biblioteca SBV que representa la fórmula proposicional que acabo de analizar de una cadena? Solo sé cómo escribir manualmenteforSome_ $ \x y z -> ... expresión, pero no cómo escribir una función de conversión desde unExpr valor a un valor de tipoPredicate.

-- 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. 
    -}

Información que puede ser útil:

Aquí está el enlace a los BitVectors.Data:http://hackage.haskell.org/package/sbv-3.0/docs/src/Data-SBV-BitVectors-Data.html

Aquí hay un ejemplo de forma de código Ejemplos.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

Aquí está el tipo de datos Expr (de la biblioteca hatt):

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