Safe Haskell	None
Language	Haskell98

Data.Logic.Instances.SatSolver

Synopsis

Documentation

toCNF :: (Monad m, FirstOrderFormula formula atom v, PropositionalFormula formula atom, Atom atom term v, AtomEq atom p term, Term term v f, Literal formula atom, Ord formula) => formula -> NormalT formula v term m CNF Source

toLiteral :: forall m lit. (Monad m, Negatable lit, Ord lit) => lit -> LiteralMapT lit m Literal Source

Convert a [[formula]] to CNF, which means building a map from formula to Literal.