picologic-0.3.0: Utilities for symbolic predicate logic expressions

Picologic.Solver

Synopsis

# Documentation

Yield the solutions for an expression using the PicoSAT solver.

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

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.