Eu quero analisar umString que descreve uma fórmula proposicional e, em seguida, encontre todos os modelos da fórmula proposicional com um solucionador SAT.

Agora eu posso analisar uma fórmula proposicional com ohatt pacote; Veja otestParse função abaixo.

Também posso executar uma chamada de solucionador SAT com a biblioteca SBV; Veja otestParse função abaixo.

Pergunta, questão: Como, em tempo de execução, giro um valor do tipoPredicate gostarmyPredicate dentro da biblioteca SBV que representa a fórmula proposicional que acabei de analisar de uma String? Eu só sei digitar manualmente oforSome_ $ \x y z -> ... expressão, mas não como escrever uma função de conversor de umExpr valor para um valor do 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. 
    -}

Informações que podem ser úteis:

Aqui está o link para o BitVectors.Data:http://hackage.haskell.org/package/sbv-3.0/docs/src/Data-SBV-BitVectors-Data.html

Aqui está o exemplo de formulário de código 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

Aqui está o tipo de dados Expr (da biblioteca hatt):

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