-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Pure Haskell SAT-solver
--   
--   SAT Solver implemented in Haskell.
--   
--   PureSAT uses DPLL with non-chronological backtracking and learning of
--   binaary clauses. Solver is in no-comparison to the state of the art
--   solvers, but it's fast enough to solve sudoku.
@package puresat
@version 0.1

module PureSAT
data Solver s
newSolver :: ST s (Solver s)
newtype Lit
MkLit :: Int -> Lit
newLit :: Solver s -> ST s Lit
boostScore :: Solver s -> Lit -> ST s ()
neg :: Lit -> Lit
addClause :: Solver s -> [Lit] -> ST s Bool
solve :: Solver s -> ST s Bool
simplify :: Solver s -> ST s Bool
modelValue :: Solver s -> Lit -> ST s Bool
num_vars :: Solver s -> ST s Int
num_clauses :: Solver s -> ST s Int
num_learnts :: Solver s -> ST s Int
num_learnt_literals :: Solver s -> ST s Int
num_conflicts :: Solver s -> ST s Int
num_restarts :: Solver s -> ST s Int


-- | A monadic interface to the SAT (<tt>PureSAT</tt>) solver.
--   
--   The interface is inspired by ST monad. <a>SAT</a> and <a>Lit</a> are
--   indexed by a "state" token, so you cannot mixup literals from
--   different SAT computations.
module Control.Monad.SAT

-- | Satisfiability monad.
data SAT s a

-- | Run <a>SAT</a> computation.
runSATMaybe :: (forall s. () => SAT s a) -> Maybe a

-- | Literal.
--   
--   To negate literate use <a>neg</a>.
data Lit s

-- | Create fresh literal.
newLit :: SAT s (Lit s)

-- | Boost score of the literal
boostScore :: Lit s -> SAT s ()
class Neg a
neg :: Neg a => a -> a

-- | Add a clause to the solver.
addClause :: [Lit s] -> SAT s ()

-- | At least one -constraint.
--   
--   Alias to <a>addClause</a>.
assertAtLeastOne :: [Lit s] -> SAT s ()

-- | At most one -constraint.
--   
--   Uses <tt>atMostOnePairwise</tt> for lists of length 2 to 5 and
--   <tt>atMostOneSequential</tt> for longer lists.
--   
--   The cutoff is chosen by picking encoding with least clauses: For 5
--   literals, <tt>atMostOnePairwise</tt> needs 10 clauses and
--   <a>assertAtMostOneSequential</a> needs 11 (and 4 new variables). For 6
--   literals, <tt>atMostOnePairwise</tt> needs 15 clauses and
--   <a>assertAtMostOneSequential</a> needs 14.
assertAtMostOne :: [Lit s] -> SAT s ()

-- | At most one -constraint using pairwise encoding.
--   
--   &lt;math&gt;
--   
--   &lt;math&gt; clauses, zero auxiliary variables.
assertAtMostOnePairwise :: [Lit s] -> SAT s ()

-- | At most one -constraint using sequential counter encoding.
--   
--   &lt;math&gt;
--   
--   Sinz, C.: Towards an optimal CNF encoding of Boolean cardinality
--   constraints, Proceedings of Principles and Practice of Constraint
--   Programming (CP), 827–831 (2005)
--   
--   &lt;math&gt; clauses, &lt;math&gt; auxiliary variables.
--   
--   We optimize the two literal case immediately (<a>resolution</a>) on
--   &lt;math&gt;.
--   
--   &lt;math&gt;
assertAtMostOneSequential :: [Lit s] -> SAT s ()

-- | Assert that two literals are equal.
assertEqual :: Lit s -> Lit s -> SAT s ()

-- | Assert that all literals in the list are equal.
assertAllEqual :: [Lit s] -> SAT s ()

-- | Propositional formula.
data Prop s

-- | True <a>Prop</a>.
true :: Prop s

-- | False <a>Prop</a>.
false :: Prop s

-- | Make <a>Prop</a> from a literal.
lit :: Lit s -> Prop s

-- | Disjunction of propositional formulas, or.
(\/) :: Prop s -> Prop s -> Prop s
infixr 5 \/

-- | Conjunction of propositional formulas, and.
(/\) :: Prop s -> Prop s -> Prop s
infixr 6 /\

-- | Equivalence of propositional formulas.
(<->) :: Prop s -> Prop s -> Prop s

-- | Implication of propositional formulas.
(-->) :: Prop s -> Prop s -> Prop s

-- | Exclusive or, not equal of propositional formulas.
xor :: Prop s -> Prop s -> Prop s

-- | If-then-else.
--   
--   Semantics of <tt><a>ite</a> c t f</tt> are <tt> (c <a>/\</a> t)
--   <a>\/</a> (<a>neg</a> c <a>/\</a> f)</tt>.
ite :: Prop s -> Prop s -> Prop s -> Prop s

-- | Add definition of <a>Prop</a>. The resulting literal is equivalent to
--   the argument <a>Prop</a>.
addDefinition :: Prop s -> SAT s (Lit s)

-- | Assert that given <a>Prop</a> is true.
--   
--   This is equivalent to
--   
--   <pre>
--   addProp p = do
--       l &lt;- addDefinition p
--       addClause l
--   </pre>
--   
--   but avoid creating the definition, asserting less clauses.
addProp :: Prop s -> SAT s ()

-- | True literal.
trueLit :: SAT s (Lit s)

-- | False literal
falseLit :: SAT s (Lit s)

-- | Add conjunction definition.
--   
--   <tt>addConjDefinition x ys</tt> asserts that <tt>x ↔ ⋀ yᵢ</tt>
addConjDefinition :: Lit s -> [Lit s] -> SAT s ()

-- | Add disjunction definition.
--   
--   <tt>addDisjDefinition x ys</tt> asserts that <tt>x ↔ ⋁ yᵢ</tt>
addDisjDefinition :: Lit s -> [Lit s] -> SAT s ()

-- | Search and return a model.
solve :: Traversable model => model (Lit s) -> SAT s (model Bool)

-- | Search without returning a model.
solve_ :: SAT s ()

-- | Removes already satisfied clauses.
simplify :: SAT s ()

-- | The current number of variables.
numberOfVariables :: SAT s Int

-- | The current number of original clauses.
numberOfClauses :: SAT s Int

-- | The current number of learnt clauses.
numberOfLearnts :: SAT s Int

-- | The current number of learnt literals.
numberOfLearntLiterals :: SAT s Int

-- | The current number of conflicts.
numberOfConflicts :: SAT s Int

-- | The current number of conflicts.
numberOfRestarts :: SAT s Int
instance GHC.Internal.Base.Applicative (Control.Monad.SAT.SAT s)
instance GHC.Classes.Eq (Control.Monad.SAT.Lit s)
instance GHC.Classes.Eq (Control.Monad.SAT.Prop s)
instance GHC.Classes.Eq (Control.Monad.SAT.Prop1 s)
instance GHC.Classes.Eq (Control.Monad.SAT.PropA s)
instance GHC.Internal.Base.Functor (Control.Monad.SAT.SAT s)
instance GHC.Internal.Base.Monad (Control.Monad.SAT.SAT s)
instance Control.Monad.SAT.Neg (Control.Monad.SAT.Lit s)
instance Control.Monad.SAT.Neg (Control.Monad.SAT.Prop s)
instance GHC.Classes.Ord (Control.Monad.SAT.Lit s)
instance GHC.Classes.Ord (Control.Monad.SAT.Prop s)
instance GHC.Classes.Ord (Control.Monad.SAT.Prop1 s)
instance GHC.Classes.Ord (Control.Monad.SAT.PropA s)
instance GHC.Internal.Show.Show (Control.Monad.SAT.Lit s)
instance GHC.Internal.Show.Show (Control.Monad.SAT.Prop s)
instance GHC.Internal.Show.Show (Control.Monad.SAT.Prop1 s)
instance GHC.Internal.Show.Show (Control.Monad.SAT.PropA s)
instance GHC.Internal.Show.Show Control.Monad.SAT.UnsatException
