Ich möchte aString das zeigt eine aussagenformel und findet dann alle modelle der aussagenformel mit einem SAT-löser.

Jetzt kann ich eine aussagekräftige Formel mit derhatt Paket; siehe dietestParse Funktion unten.

Ich kann auch einen SAT-Solver-Aufruf mit der SBV-Bibliothek ausführen. siehe dietestParse Funktion unten.

Frage: Wie erstelle ich zur Laufzeit einen Wert vom Typ?Predicate mögenmyPredicate innerhalb der SBV-Bibliothek, die die Satzformel darstellt, die ich gerade aus einem String analysiert habe? Ich weiß nur, wie man das manuell schreibtforSome_ $ \x y z -> ... Ausdruck, aber nicht, wie man eine Konverterfunktion aus einerExpr value auf einen Wert vom TypPredicate.

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

Informationen, die hilfreich sein könnten:

Hier ist der Link zu den BitVectors.Data:http://hackage.haskell.org/package/sbv-3.0/docs/src/Data-SBV-BitVectors-Data.html

Hier ist ein Beispielcode für 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

Hier ist der Expr-Datentyp (aus der Hutbibliothek):

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