Picologic.Solver

Documentation

solveProp :: Expr -> IO Solutions

Yield the solutions for an expression using the PicoSAT solver.

solveCNF :: Expr -> IO Solutions

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

solveOneCNF :: Expr -> IO (Maybe [Expr])

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

clausesExpr :: Expr -> [[Int]]

Yield the integer clauses given to the SAT solver.

addVarsToSolutions :: [Ident] -> Solutions -> Solutions