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


-- | Bindings to the PicoSAT solver
--   
--   <a>picosat</a> provides bindings for the fast PicoSAT solver library.
@package picosat
@version 0.1.4


-- | We wish to find a solution that satisifes the following logical
--   condition.
--   
--   <pre>
--   (A v ¬B v C) ∧ (B v D v E) ∧ (D v F)
--   </pre>
--   
--   We can specify this as a zero-terminated lists of integers, with
--   integers mapping onto the variable as ordered in the condition and
--   with integer negation corresponding to logical negation of the
--   specific clause.
--   
--   <pre>
--   1 -2 3 0
--   2 4 5 0
--   4 6 0
--   </pre>
--   
--   We feed this list of clauses to the SAT solver using the <a>solve</a>
--   function.
--   
--   <pre>
--   import Picosat
--   
--   main :: IO [Int]
--   main = do
--     solve [[1, -2, 3], [2,4,5], [4,6]]
--     -- Solution [1,-2,3,4,5,6]
--   </pre>
--   
--   The solution given we can interpret as:
--   
--   <pre>
--    1  A
--   -2 ~B
--    3  C
--    4  D
--    5  E
--    6  F
--   </pre>
--   
--   To generate all satisfiable solutions, use <a>solveAll</a> function.:
--   
--   <pre>
--   import Picosat
--   
--   main :: IO [Int]
--   main = solveAll [[1,2]]
--     -- [Solution [1,2],Solution [-1,2],Solution [1,-2]]
--   </pre>
--   
--   For a higher level interface see:
--   <a>http://hackage.haskell.org/package/picologic</a>
--   
--   If you intend to solve a set of similar CNFs think about using
--   Picosat's incremental interface. It allows to push and pop sets of
--   clauses, as well as solving under assumptions.
--   
--   <pre>
--   import Picosat (evalScopedPicosat, addBaseClauses,
--                   withScopedClauses, scopedAllSolutions,
--                   scopedSolutionWithAssumptions)
--   
--   main :: IO [Int]
--   main =
--     evalScopedPicosat $ do
--       addBaseClauses [[1, 2, 3]]
--       -- == [Solution [1,2,3],
--       --     Solution [1,2,-3],
--       --     Solution [1,-2,3],
--       --     Solution [1,-2,-3],
--       --     Solution [-1,-2,3],
--       --     Solution [-1,2,-3],
--       --     Solution [-1,2,3]]
--   
--       withScopedClauses [[-2,-3]] $ do
--         sol &lt;- scopedAllSolutions
--         -- ==   [Solution [-1,2,-3],
--         --       Solution [-1,-2,3],
--         --       Solution [1,-2,-3],
--         --       Solution [1,-2,3],
--         --       Solution [1,2,-3]]
--   
--       addBaseClauses [[-1,-3]]
--   
--       withScopedClauses [[-1,-2], [1,-3]] $ do
--         sol &lt;- scopedSolutionWithAssumptions [1]
--   </pre>
module Picosat

-- | Solve a list of CNF constraints yielding the first solution.
solve :: [[Int]] -> IO Solution

-- | Solve a list of CNF constraints yielding all possible solutions.
solveAll :: [[Int]] -> IO [Solution]
unsafeSolve :: [[Int]] -> Solution
unsafeSolveAll :: [[Int]] -> [Solution]
type Picosat = Ptr ()
data Solution
Solution :: [Int] -> Solution
Unsatisfiable :: Solution
Unknown :: Solution
evalScopedPicosat :: PS a -> IO a
addBaseClauses :: [[Int]] -> PS ()
withScopedClauses :: [[Int]] -> PS a -> PS a
scopedAllSolutions :: PS [Solution]
scopedSolutionWithAssumptions :: [Int] -> PS Solution
instance GHC.Classes.Ord Picosat.Solution
instance GHC.Classes.Eq Picosat.Solution
instance GHC.Show.Show Picosat.Solution
