picologic-0.1.2: Utilities for symbolic predicate logic expressions

Safe HaskellNone
LanguageHaskell2010

Picologic.Solver

Synopsis

Documentation

solveProp :: Expr -> IO Solutions Source

Yield the solutions for an expression using the PicoSAT solver.

solveCNF :: Expr -> IO Solutions Source

Yield the solutions for an expression using the PicoSAT solver. The Expression must be in CNF form already.

solveOneCNF :: Expr -> IO [Expr] Source

Yield one single solution for an expression using the PicoSAT solver. The Expression must be in CNF form already.

clausesExpr :: Expr -> [[Int]] Source

Yield the integer clauses given to the SAT solver.