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


-- | A Minisat-based SAT solver in Haskell
--   
--   A modern and fast SAT solver written in Haskell, based on Minisat-1.14
--   and 2.2. By using CDCL, watch literals, VSIDS, restart,
--   blocking-literals, LBD and so on. The current version is only 2.0 time
--   slower than Minisat-2.2. <a>Mios</a> is an abbreviation of
--   'Minisat-based Implementation and Optimization Study on SAT solver'.
@package mios
@version 1.4.0


-- | Boolean Expression module to build CNF from arbitrary expressions
--   Tseitin translation:
--   <a>http://en.wikipedia.org/wiki/Tseitin_transformation</a>
module SAT.Mios.Util.BoolExp

-- | class of objects that can be interpeted as a bool expression
class BoolComponent a
toBF :: BoolComponent a => a -> BoolForm

-- | CNF expression
data BoolForm
Cnf :: (Int, Int) -> [[Int]] -> BoolForm

-- | disjunction constructor
--   
--   <pre>
--   &gt;&gt;&gt; asList $ "3" -|- "4"
--   [[3,4,-5],[-3,5],[-4,5]]
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; asList (("3" -|- "4") -|- "-1")
--   [[3,4,-5],[-3,5],[-4,5],[5,-1,-6],[-5,6],[1,6]]
--   </pre>
(-|-) :: (BoolComponent a, BoolComponent b) => a -> b -> BoolForm

-- | conjunction constructor
--   
--   <pre>
--   &gt;&gt;&gt; asList $ "3" -&amp;- "-2"
--   [[-3,2,4],[3,-4],[-2,-4]]
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; asList $ "3" -|- ("1" -&amp;- "2")
--   [[-1,-2,4],[1,-4],[2,-4],[3,4,-5],[-3,5],[-4,5]]
--   </pre>
(-&-) :: (BoolComponent a, BoolComponent b) => a -> b -> BoolForm

-- | equal on BoolForm
(-=-) :: (BoolComponent a, BoolComponent b) => a -> b -> BoolForm

-- | negation on BoolForm
(-!-) :: (BoolComponent a, BoolComponent b) => a -> b -> BoolForm

-- | implication as a short cut
--   
--   <pre>
--   &gt;&gt;&gt; asList ("1" -&gt;- "2")
--   [[-1,-3],[1,3],[3,2,-4],[-3,4],[-2,4]]
--   </pre>
(->-) :: (BoolComponent a, BoolComponent b) => a -> b -> BoolForm

-- | negate a form
--   
--   <pre>
--   &gt;&gt;&gt; asList $ neg ("1" -|- "2")
--   [[1,2,-3],[-1,3],[-2,3],[-3,-4],[3,4]]
--   </pre>
neg :: (BoolComponent a) => a -> BoolForm

-- | merge [BoolForm] by '(-|-)'
disjunctionOf :: [BoolForm] -> BoolForm

-- | an alias of <a>disjunctionOf</a>
(-|||-) :: [BoolForm] -> BoolForm

-- | merge [BoolForm] by '(-&amp;-)'
conjunctionOf :: [BoolForm] -> BoolForm

-- | an alias of <a>conjunctionOf</a>
(-&&&-) :: [BoolForm] -> BoolForm

-- | converts a *satisfied* BoolForm to "[[Int]]"
asList :: BoolForm -> [[Int]]

-- | converts a BoolForm to "[[Int]]"
asList_ :: BoolForm -> [[Int]]

-- | make latex string from CNF, using <a>asList</a>
asLatex :: BoolForm -> String

-- | make latex string from CNF, using <a>asList_</a>
--   
--   <pre>
--   &gt;&gt;&gt; asLatex $ "3" -|- "4"
--   "\\begin{displaymath}\n( x_{3} \\vee x_{4} )\n\\end{displaymath}\n"
--   </pre>
asLatex_ :: BoolForm -> String

-- | returns the number of variables in the <a>BoolForm</a>
numberOfVariables :: BoolForm -> Int

-- | returns the number of clauses in the <a>BoolForm</a>
numberOfClauses :: BoolForm -> Int

-- | the start index for the generated variables by Tseitin encoding
tseitinBase :: Int
instance GHC.Show.Show SAT.Mios.Util.BoolExp.BoolForm
instance GHC.Classes.Eq SAT.Mios.Util.BoolExp.BoolForm
instance SAT.Mios.Util.BoolExp.BoolComponent GHC.Types.Int
instance SAT.Mios.Util.BoolExp.BoolComponent SAT.Mios.Util.BoolExp.L
instance SAT.Mios.Util.BoolExp.BoolComponent [GHC.Types.Char]
instance SAT.Mios.Util.BoolExp.BoolComponent SAT.Mios.Util.BoolExp.BoolForm
instance SAT.Mios.Util.BoolExp.BoolComponent GHC.Types.Bool
instance GHC.Classes.Ord SAT.Mios.Util.BoolExp.BoolForm


-- | Write SAT data to DIMACS file
module SAT.Mios.Util.DIMACS.Writer

-- | Write the DIMACS to file <tt>f</tt>, using <a>toDIMACSString</a>
toFile :: FilePath -> [[Int]] -> IO ()

-- | Convert [Clause] to String, where Clause is [Int]
--   
--   <pre>
--   &gt;&gt;&gt; toDIMACSString []
--   "p cnf 0 0\n"
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; toDIMACSString [[-1, 2], [-3, -4]]
--   "p cnf 4 2\n-1 2 0\n-3 -4 0\n"
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; toDIMACSString [[1], [-2], [-3, -4], [1,2,3,4]]
--   "p cnf 4 4\n1 0\n-2 0\n-3 -4 0\n1 2 3 4 0\n"
--   </pre>
toDIMACSString :: [[Int]] -> String

-- | converts <tt>[[Int]]</tt> to a String
toString :: [[Int]] -> String -> String -> String

-- | converts <tt>[[Int]]</tt> to a LaTeX expression
toLatexString :: [[Int]] -> String


-- | Read a CNF file without haskell-platform
module SAT.Mios.Util.DIMACS.Reader

-- | read a CNF file and return: ((numbefOfVariables, numberOfClauses),
--   [Literal])
--   
--   <pre>
--   &gt;&gt;&gt; fromFile "acnf"
--   ((3, 4), [[1, 2], [-2, 3], [-1, 2, -3], [3]]
--   </pre>
fromFile :: FilePath -> IO (Maybe ((Int, Int), [[Int]]))

-- | return clauses as [[Int]] from <tt>file</tt>
--   
--   <pre>
--   &gt;&gt;&gt; clauseListFromFile "a.cnf"
--   [[1, 2], [-2, 3], [-1, 2, -3], [3]]
--   </pre>
clauseListFromFile :: FilePath -> IO [[Int]]


-- | Read an output file of minisat
module SAT.Mios.Util.DIMACS.MinisatReader

-- | read a minisat output: ((numbefOfVariables, 0), [Literal])
--   
--   <pre>
--   &gt;&gt;&gt; fromFile "result"
--   ((3, 0), [1, -2, 3])
--   </pre>
fromMinisatOutput :: FilePath -> IO (Maybe ((Int, Int), [Int]))

-- | return clauses as [[Int]] from <tt>file</tt>
--   
--   <pre>
--   &gt;&gt;&gt; clauseListFromMinisatOutput "result"
--   [1,-2,3]
--   </pre>
clauseListFromMinisatOutput :: FilePath -> IO [Int]


-- | Read/Write a CNF file only with ghc standard libraries
module SAT.Mios.Util.DIMACS

-- | read a CNF file and return: ((numbefOfVariables, numberOfClauses),
--   [Literal])
--   
--   <pre>
--   &gt;&gt;&gt; fromFile "acnf"
--   ((3, 4), [[1, 2], [-2, 3], [-1, 2, -3], [3]]
--   </pre>
fromFile :: FilePath -> IO (Maybe ((Int, Int), [[Int]]))

-- | return clauses as [[Int]] from <tt>file</tt>
--   
--   <pre>
--   &gt;&gt;&gt; clauseListFromFile "a.cnf"
--   [[1, 2], [-2, 3], [-1, 2, -3], [3]]
--   </pre>
clauseListFromFile :: FilePath -> IO [[Int]]

-- | read a minisat output: ((numbefOfVariables, 0), [Literal])
--   
--   <pre>
--   &gt;&gt;&gt; fromFile "result"
--   ((3, 0), [1, -2, 3])
--   </pre>
fromMinisatOutput :: FilePath -> IO (Maybe ((Int, Int), [Int]))

-- | return clauses as [[Int]] from <tt>file</tt>
--   
--   <pre>
--   &gt;&gt;&gt; clauseListFromMinisatOutput "result"
--   [1,-2,3]
--   </pre>
clauseListFromMinisatOutput :: FilePath -> IO [Int]

-- | Write the DIMACS to file <tt>f</tt>, using <a>toDIMACSString</a>
toFile :: FilePath -> [[Int]] -> IO ()

-- | Convert [Clause] to String, where Clause is [Int]
--   
--   <pre>
--   &gt;&gt;&gt; toDIMACSString []
--   "p cnf 0 0\n"
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; toDIMACSString [[-1, 2], [-3, -4]]
--   "p cnf 4 2\n-1 2 0\n-3 -4 0\n"
--   </pre>
--   
--   <pre>
--   &gt;&gt;&gt; toDIMACSString [[1], [-2], [-3, -4], [1,2,3,4]]
--   "p cnf 4 4\n1 0\n-2 0\n-3 -4 0\n1 2 3 4 0\n"
--   </pre>
toDIMACSString :: [[Int]] -> String

-- | String from BoolFrom
asDIMACSString :: BoolForm -> String

-- | String from BoolFrom
asDIMACSString_ :: BoolForm -> String


-- | Abstraction Layer for Mutable Vectors
module SAT.Mios.Vec

-- | Interface on vectors.
class VecFamily v a | v -> a where reset = error "no default method: reset" asUVector = error "no default method: asUVector" swapBetween = error "no default method: swapBetween" modifyNth = error "no default method: modifyNth" newVec = error "no default method: newVec" setAll = error "no default method: setAll" asList = error "no default method: asList" growBy = error "no default method: growBy"

-- | returns the <i>n</i>-th value.
getNth :: VecFamily v a => v -> Int -> IO a

-- | sets the <i>n</i>-th value.
setNth :: VecFamily v a => v -> Int -> a -> IO ()

-- | erases all elements in it.
reset :: VecFamily v a => v -> IO ()

-- | converts to an Int vector.
asUVector :: (VecFamily v a, a ~ Int) => v -> UVector Int

-- | returns the <i>n</i>-th value (index starts from zero in any case). |
--   swaps two elements.
swapBetween :: VecFamily v a => v -> Int -> Int -> IO ()

-- | calls the update function.
modifyNth :: VecFamily v a => v -> (a -> a) -> Int -> IO ()

-- | returns a new vector.
newVec :: VecFamily v a => Int -> a -> IO v

-- | sets all elements.
setAll :: VecFamily v a => v -> a -> IO ()

-- | extends the size of stack by <i>n</i>; note: values in new elements
--   aren't initialized maybe.
growBy :: VecFamily v a => v -> Int -> IO v

-- | converts to a list.
asList :: VecFamily v a => v -> IO [a]

-- | A thin abstract layer for Mutable unboxed Vector
type UVector a = IOVector a

-- | Another abstraction layer on <a>UVector</a>.
--   
--   <b>Note</b>: the 0-th element of <tt>Vec Int</tt> is reserved for
--   internal tasks. If you want to use it, use <tt>UVector Int</tt>.
newtype Vec a
Vec :: (UVector a) -> Vec a

-- | Interface for single mutable data
class SingleStorage s t | s -> t where new' = undefined modify' = undefined

-- | allocates and returns an new data.
new' :: SingleStorage s t => t -> IO s

-- | gets the value.
get' :: SingleStorage s t => s -> IO t

-- | sets the value.
set' :: SingleStorage s t => s -> t -> IO ()

-- | calls an update function on it.
modify' :: SingleStorage s t => s -> (t -> t) -> IO ()

-- | Mutable Bool
type Bool' = IOVector Bool

-- | Mutable Double
type Double' = IOVector Double

-- | Mutable Int <b>Note:</b> Int' is the same with <a>Stack</a>
type Int' = IOVector Int

-- | Interface on stacks
class SingleStorage s Int => StackFamily s t | s -> t where newStack = undefined pushTo = undefined popFrom = undefined lastOf = undefined shrinkBy = undefined

-- | returns a new stack.
newStack :: StackFamily s t => Int -> IO s

-- | pushs an value to the tail of the stack.
pushTo :: StackFamily s t => s -> t -> IO ()

-- | pops the last element.
popFrom :: StackFamily s t => s -> IO ()

-- | peeks the last element.
lastOf :: StackFamily s t => s -> IO t

-- | shrinks the stack.
shrinkBy :: StackFamily s t => s -> Int -> IO ()

-- | Alias of <tt>Vec Int</tt>. The 0-th element holds the number of
--   elements.
type Stack = Vec Int

-- | returns a new <a>Stack</a> from <tt>[Int]</tt>.
newStackFromList :: [Int] -> IO Stack
instance SAT.Mios.Vec.VecFamily (SAT.Mios.Vec.UVector GHC.Types.Int) GHC.Types.Int
instance SAT.Mios.Vec.VecFamily (SAT.Mios.Vec.UVector GHC.Types.Double) GHC.Types.Double
instance SAT.Mios.Vec.VecFamily (SAT.Mios.Vec.Vec GHC.Types.Int) GHC.Types.Int
instance SAT.Mios.Vec.VecFamily (SAT.Mios.Vec.Vec GHC.Types.Double) GHC.Types.Double
instance SAT.Mios.Vec.SingleStorage SAT.Mios.Vec.Int' GHC.Types.Int
instance SAT.Mios.Vec.SingleStorage SAT.Mios.Vec.Bool' GHC.Types.Bool
instance SAT.Mios.Vec.SingleStorage SAT.Mios.Vec.Double' GHC.Types.Double
instance SAT.Mios.Vec.SingleStorage SAT.Mios.Vec.Stack GHC.Types.Int
instance SAT.Mios.Vec.StackFamily SAT.Mios.Vec.Stack GHC.Types.Int


-- | Basic data types used throughout mios.
module SAT.Mios.Types

-- | represents <a>Var</a>.
type Var = Int

-- | Special constant in <a>Var</a> (p.7)
bottomVar :: Var

-- | converts a usual Int as literal to an internal <a>Var</a>
--   presentation.
--   
--   <pre>
--   &gt;&gt;&gt; int2var 1
--   1  -- the first literal is the first variable
--   
--   &gt;&gt;&gt; int2var 2
--   2  -- literal @2@ is variable 2
--   
--   &gt;&gt;&gt; int2var (-2)
--   2 -- literal @-2@ is corresponding to variable 2
--   </pre>
int2var :: Int -> Int

-- | The literal data has an <tt>index</tt> method which converts the
--   literal to a "small" integer suitable for array indexing. The
--   <tt>var</tt> method returns the underlying variable of the literal,
--   and the <tt>sign</tt> method if the literal is signed (False for
--   <i>x</i> and True for <i>-x</i>).
type Lit = Int

-- | converts <a>Lit</a> into <a>Int</a> as <tt>int2lit . lit2int ==
--   id</tt>.
--   
--   <pre>
--   &gt;&gt;&gt; lit2int 2
--   1
--   
--   &gt;&gt;&gt; lit2int 3
--   -1
--   
--   &gt;&gt;&gt; lit2int 4
--   2
--   
--   &gt;&gt;&gt; lit2int 5
--   -2
--   </pre>
lit2int :: Lit -> Int

-- | converts <a>Int</a> into <a>Lit</a> as <tt>lit2int . int2lit ==
--   id</tt>.
--   
--   <pre>
--   &gt;&gt;&gt; int2lit 1
--   2
--   
--   &gt;&gt;&gt; int2lit (-1)
--   3
--   
--   &gt;&gt;&gt; int2lit 2
--   4
--   
--   &gt;&gt;&gt; int2lit (-2)
--   5
--   </pre>
int2lit :: Int -> Lit

-- | Special constant in <a>Lit</a> (p.7)
bottomLit :: Lit

-- | returns <tt>True</tt> if the literal is positive
positiveLit :: Lit -> Bool

-- | converts <a>Lit</a> into <a>Var</a>.
--   
--   <pre>
--   &gt;&gt;&gt; lit2var 2
--   1
--   
--   &gt;&gt;&gt; lit2var 3
--   1
--   
--   &gt;&gt;&gt; lit2var 4
--   2
--   
--   &gt;&gt;&gt; lit2var 5
--   2
--   </pre>
lit2var :: Lit -> Var

-- | converts a <a>Var</a> to the corresponing literal.
--   
--   <pre>
--   &gt;&gt;&gt; var2lit 1 True
--   2
--   
--   &gt;&gt;&gt; var2lit 1 False
--   3
--   
--   &gt;&gt;&gt; var2lit 2 True
--   4
--   
--   &gt;&gt;&gt; var2lit 2 False
--   5
--   </pre>
var2lit :: Var -> Bool -> Lit

-- | negates literal
--   
--   <pre>
--   &gt;&gt;&gt; negateLit 2
--   3
--   
--   &gt;&gt;&gt; negateLit 3
--   2
--   
--   &gt;&gt;&gt; negateLit 4
--   5
--   
--   &gt;&gt;&gt; negateLit 5
--   4
--   </pre>
negateLit :: Lit -> Lit

-- | <i>FALSE</i> on the Lifted Bool domain
lFalse :: Int

-- | <i>TRUE</i> on the Lifted Bool domain
lTrue :: Int

-- | <i>UNDEFINED</i> on the Lifted Bool domain
lBottom :: Int

-- | Assisting ADT for the dynamic variable ordering of the solver. The
--   constructor takes references to the assignment vector and the activity
--   vector of the solver. The method <a>select</a> will return the
--   unassigned variable with the highest activity.
class VarOrder o where update _ = error "update undefined" undo _ _ = error "undo undefined" select = error "select undefined"

-- | should be called when a variable has increased in activity.
update :: VarOrder o => o -> Var -> IO ()

-- | should be called when a variable becomes unbound (may be selected
--   again).
undo :: VarOrder o => o -> Var -> IO ()

-- | returns a new, unassigned var as the next decision.
select :: VarOrder o => o -> IO Var

-- | Misc information on a CNF
data CNFDescription
CNFDescription :: !Int -> !Int -> Maybe FilePath -> CNFDescription

-- | the number of variables
[_numberOfVariables] :: CNFDescription -> !Int

-- | the number of clauses
[_numberOfClauses] :: CNFDescription -> !Int

-- | given filename
[_pathname] :: CNFDescription -> Maybe FilePath

-- | Solver's parameters; random decision rate was dropped.
data MiosConfiguration
MiosConfiguration :: !Double -> MiosConfiguration

-- | decay rate for variable activity , clauseDecayRate :: !Double -- ^
--   decay rate for clause activity
[variableDecayRate] :: MiosConfiguration -> !Double

-- | dafault configuration
--   
--   <ul>
--   <li>Minisat-1.14 uses <tt>(0.95, 0.999, 0.2 = 20 / 1000)</tt>.</li>
--   <li>Minisat-2.20 uses <tt>(0.95, 0.999, 0)</tt>.</li>
--   <li>Gulcose-4.0 uses <tt>(0.8 , 0.999, 0)</tt>.</li>
--   <li>Mios-1.2 uses <tt>(0.95, 0.999, 0)</tt>.</li>
--   </ul>
defaultConfiguration :: MiosConfiguration
instance GHC.Show.Show SAT.Mios.Types.CNFDescription
instance GHC.Classes.Ord SAT.Mios.Types.CNFDescription
instance GHC.Classes.Eq SAT.Mios.Types.CNFDescription


-- | command line option parser for mios
module SAT.Mios.OptionParser

-- | Solver's parameters; random decision rate was dropped.
data MiosConfiguration
MiosConfiguration :: !Double -> MiosConfiguration

-- | decay rate for variable activity , clauseDecayRate :: !Double -- ^
--   decay rate for clause activity
[variableDecayRate] :: MiosConfiguration -> !Double

-- | dafault configuration
--   
--   <ul>
--   <li>Minisat-1.14 uses <tt>(0.95, 0.999, 0.2 = 20 / 1000)</tt>.</li>
--   <li>Minisat-2.20 uses <tt>(0.95, 0.999, 0)</tt>.</li>
--   <li>Gulcose-4.0 uses <tt>(0.8 , 0.999, 0)</tt>.</li>
--   <li>Mios-1.2 uses <tt>(0.95, 0.999, 0)</tt>.</li>
--   </ul>
defaultConfiguration :: MiosConfiguration

-- | configuration swithces
data MiosProgramOption
MiosProgramOption :: Maybe String -> Maybe String -> !Double -> !Bool -> !Bool -> !Bool -> !Bool -> !Bool -> !Bool -> !Bool -> !Bool -> MiosProgramOption
[_targetFile] :: MiosProgramOption -> Maybe String
[_outputFile] :: MiosProgramOption -> Maybe String
[_confVariableDecayRate] :: MiosProgramOption -> !Double
[_confCheckAnswer] :: MiosProgramOption -> !Bool
[_confVerbose] :: MiosProgramOption -> !Bool
[_confTimeProbe] :: MiosProgramOption -> !Bool
[_confStatProbe] :: MiosProgramOption -> !Bool
[_confNoAnswer] :: MiosProgramOption -> !Bool
[_validateAssignment] :: MiosProgramOption -> !Bool
[_displayHelp] :: MiosProgramOption -> !Bool
[_displayVersion] :: MiosProgramOption -> !Bool

-- | default option settings
miosDefaultOption :: MiosProgramOption

-- | definition of mios option
miosOptions :: [OptDescr (MiosProgramOption -> MiosProgramOption)]

-- | generates help message
miosUsage :: String -> String

-- | builds <a>MiosProgramOption</a> from string given as command option
miosParseOptions :: String -> [String] -> IO MiosProgramOption

-- | builds <a>MiosProgramOption</a> from a String
miosParseOptionsFromArgs :: String -> IO MiosProgramOption

-- | converts <a>MiosProgramOption</a> into <a>SIHConfiguration</a>
toMiosConf :: MiosProgramOption -> MiosConfiguration


-- | Clause, supporting pointer-based equality
module SAT.Mios.Clause

-- | <b>Fig. 7.(p.11)</b> normal, null (and binary) clause. This matches
--   both of <tt>Clause</tt> and <tt>GClause</tt> in MiniSat.
data Clause
Clause :: !Bool -> !Double' -> !Bool' -> !Stack -> Clause

-- | whether this is a learnt clause , rank :: !Int' -- ^ goodness like
--   LBD; computed in <tt>Ranking</tt>
[learnt] :: Clause -> !Bool

-- | activity of this clause
[activity] :: Clause -> !Double'

-- | protected from reduce
[protected] :: Clause -> !Bool'

-- | which this clause consists of
[lits] :: Clause -> !Stack
NullClause :: Clause

-- | copies <i>vec</i> and return a new <a>Clause</a>. Since 1.0.100 DIMACS
--   reader should use a scratch buffer allocated statically.
newClauseFromStack :: Bool -> Stack -> IO Clause

-- | Mutable <a>Clause</a> Vector
type ClauseVector = IOVector Clause

-- | returns a new <a>ClauseVector</a>.
newClauseVector :: Int -> IO ClauseVector
instance GHC.Classes.Eq SAT.Mios.Clause.Clause
instance GHC.Show.Show SAT.Mios.Clause.Clause
instance SAT.Mios.Vec.VecFamily SAT.Mios.Clause.Clause SAT.Mios.Types.Lit
instance SAT.Mios.Vec.SingleStorage SAT.Mios.Clause.Clause GHC.Types.Int
instance SAT.Mios.Vec.StackFamily SAT.Mios.Clause.Clause SAT.Mios.Types.Lit
instance SAT.Mios.Vec.VecFamily SAT.Mios.Clause.ClauseVector SAT.Mios.Clause.Clause


-- | A shrinkable vector of <a>Clause</a>
module SAT.Mios.ClauseManager

-- | Resizable vector of <a>Clause</a>.
class ClauseManager a
newManager :: ClauseManager a => Int -> IO a
getClauseVector :: ClauseManager a => a -> IO ClauseVector

-- | Clause + Blocking Literal
data ClauseExtManager

-- | O(1) inserter
pushClauseWithKey :: ClauseExtManager -> Clause -> Lit -> IO ()

-- | returns the associated Int vector, which holds <i>blocking
--   literals</i>.
getKeyVector :: ClauseExtManager -> IO (UVector Int)

-- | sets the expire flag to a clause.
markClause :: ClauseExtManager -> Clause -> IO ()

-- | Immutable Vector of <a>ClauseExtManager</a>
type WatcherList = Vector ClauseExtManager

-- | <i>n</i> is the number of <a>Var</a>, <i>m</i> is default size of each
--   watcher list. | For <i>n</i> vars, we need [0 .. 2 + 2 * n - 1] slots,
--   namely <i>2 * (n + 1)</i>-length vector
newWatcherList :: Int -> Int -> IO WatcherList

-- | returns the watcher List for <a>Literal</a> <i>l</i>.
getNthWatcher :: WatcherList -> Lit -> ClauseExtManager
instance SAT.Mios.Vec.SingleStorage SAT.Mios.ClauseManager.ClauseExtManager GHC.Types.Int
instance SAT.Mios.Vec.StackFamily SAT.Mios.ClauseManager.ClauseExtManager SAT.Mios.Clause.Clause
instance SAT.Mios.ClauseManager.ClauseManager SAT.Mios.ClauseManager.ClauseExtManager
instance SAT.Mios.Vec.VecFamily SAT.Mios.ClauseManager.ClauseExtManager SAT.Mios.Clause.Clause
instance SAT.Mios.Vec.VecFamily SAT.Mios.ClauseManager.WatcherList SAT.Mios.Clause.Clause


-- | This is a part of MIOS; main data
module SAT.Mios.Solver

-- | <b>Fig. 2.(p.9)</b> Internal State of the solver
data Solver
Solver :: !(Vec Int) -> !Stack -> !ClauseExtManager -> !ClauseExtManager -> !WatcherList -> !(Vec Int) -> !(Vec Int) -> !Stack -> !Stack -> !Int' -> !ClauseVector -> !(Vec Int) -> !(Vec Double) -> !VarHeap -> !MiosConfiguration -> !Int -> !Double' -> !Int' -> !Bool' -> !(Vec Int) -> !Stack -> !Stack -> !Stack -> !Stack -> !(UVector Int) -> Solver

-- | If found, this vector has the model
[model] :: Solver -> !(Vec Int)

-- | Set of literals in the case of conflicts
[conflicts] :: Solver -> !Stack

-- | List of problem constraints.
[clauses] :: Solver -> !ClauseExtManager

-- | List of learnt clauses.
[learnts] :: Solver -> !ClauseExtManager

-- | list of constraint wathing <tt>p</tt>, literal-indexed
[watches] :: Solver -> !WatcherList

-- | The current assignments indexed on variables
[assigns] :: Solver -> !(Vec Int)

-- | The last assignments indexed on variables
[phases] :: Solver -> !(Vec Int)

-- | List of assignments in chronological order
[trail] :: Solver -> !Stack

-- | Separator indices for different decision levels in <a>trail</a>.
[trailLim] :: Solver -> !Stack

-- | <a>trail</a> is divided at qHead; assignment part and queue part
[qHead] :: Solver -> !Int'

-- | For each variable, the constraint that implied its value
[reason] :: Solver -> !ClauseVector

-- | For each variable, the decision level it was assigned
[level] :: Solver -> !(Vec Int)

-- | Heuristic measurement of the activity of a variable
[activities] :: Solver -> !(Vec Double)

-- | Keeps track of the dynamic variable order.
[order] :: Solver -> !VarHeap

-- | search paramerters
[config] :: Solver -> !MiosConfiguration

-- | number of variables
[nVars] :: Solver -> !Int

-- | Variable activity increment amount to bump with.
[varInc] :: Solver -> !Double'

-- | Separates incremental and search assumptions.
[rootLevel] :: Solver -> !Int'

-- | <i>return value</i> holder
[ok] :: Solver -> !Bool'

-- | used in <a>analyze</a>
[an'seen] :: Solver -> !(Vec Int)

-- | used in <a>analyze</a>
[an'toClear] :: Solver -> !Stack

-- | used in <a>analyze</a>
[an'stack] :: Solver -> !Stack

-- | last decision level used in <a>analyze</a>
[an'lastDL] :: Solver -> !Stack

-- | used in <a>analyze</a> and <a>search</a> to create a learnt clause
[litsLearnt] :: Solver -> !Stack

-- | statistics information holder
[stats] :: Solver -> !(UVector Int)

-- | A heap tree built from two <a>Vec</a>. This implementation is
--   identical wtih that in Minisat-1.14. Note: the zero-th element of
--   <tt>heap</tt> is used for holding the number of elements. Note:
--   VarHeap itself is not a <tt>VarOrder</tt>, because it requires a
--   pointer to solver.
data VarHeap

-- | returns an everything-is-initialized solver from the arguments.
newSolver :: MiosConfiguration -> CNFDescription -> IO Solver

-- | returns the model as a list of literal.
getModel :: Solver -> IO [Int]

-- | returns the number of current assigments.
nAssigns :: Solver -> IO Int

-- | returns the number of constraints (clauses).
nClauses :: Solver -> IO Int

-- | returns the number of learnt clauses.
nLearnts :: Solver -> IO Int

-- | returns the current decision level.
decisionLevel :: Solver -> IO Int

-- | returns the assignment (:: <tt>LiftedBool</tt> = <tt>[-1, 0, -1]</tt>)
--   from <a>Var</a>.
valueVar :: Solver -> Var -> IO Int

-- | returns the assignment (:: <tt>LiftedBool</tt> = <tt>[-1, 0, -1]</tt>)
--   from <a>Lit</a>.
valueLit :: Solver -> Lit -> IO Int

-- | <b>Fig. 7. (p.11)</b> returns <tt>True</tt> if the clause is locked
--   (used as a reason). <b>Learnt clauses only</b>
locked :: Solver -> Clause -> IO Bool

-- | returns <tt>False</tt> if a conflict has occured. This function is
--   called only before the solving phase to register the given clauses.
addClause :: Solver -> Stack -> IO Bool

-- | <b>Fig. 9 (p.14)</b> Puts a new fact on the propagation queue, as well
--   as immediately updating the variable's value in the assignment vector.
--   If a conflict arises, <tt>False</tt> is returned and the propagation
--   queue is cleared. The parameter <tt>from</tt> contains a reference to
--   the constraint from which <tt>p</tt> was propagated (defaults to
--   <tt>Nothing</tt> if omitted).
enqueue :: Solver -> Lit -> Clause -> IO Bool

-- | <b>Fig. 12 (p.17)</b> returns <tt>False</tt> if immediate conflict.
--   
--   <b>Pre-condition:</b> propagation queue is empty
assume :: Solver -> Lit -> IO Bool

-- | #M22: Revert to the states at given level (keeping all assignment at
--   <a>level</a> but not beyond).
cancelUntil :: Solver -> Int -> IO ()

-- | <b>Fig. 14 (p.19)</b>
claBumpActivity :: Solver -> Clause -> IO ()

-- | <b>Fig. 14 (p.19)</b>
claRescaleActivityAfterRestart :: Solver -> IO ()

-- | <b>Fig. 14 (p.19)</b> Bumping of clause activity
varBumpActivity :: Solver -> Var -> IO ()

-- | <b>Fig. 14 (p.19)</b>
varDecayActivity :: Solver -> IO ()

-- | value for rescaling clause activity.
claActivityThreshold :: Double

-- | stat index
data StatIndex

-- | the number of backjump
NumOfBackjump :: StatIndex

-- | the number of restart
NumOfRestart :: StatIndex

-- | Don't use this dummy.
EndOfStatIndex :: StatIndex

-- | returns the value of <a>StatIndex</a>.
getStat :: Solver -> StatIndex -> IO Int

-- | sets to <a>StatIndex</a>.
setStat :: Solver -> StatIndex -> Int -> IO ()

-- | increments a stat data corresponding to <a>StatIndex</a>.
incrementStat :: Solver -> StatIndex -> Int -> IO ()

-- | returns the statistics as a list.
getStats :: Solver -> IO [(StatIndex, Int)]
instance GHC.Show.Show SAT.Mios.Solver.StatIndex
instance GHC.Read.Read SAT.Mios.Solver.StatIndex
instance GHC.Classes.Ord SAT.Mios.Solver.StatIndex
instance GHC.Classes.Eq SAT.Mios.Solver.StatIndex
instance GHC.Enum.Enum SAT.Mios.Solver.StatIndex
instance GHC.Enum.Bounded SAT.Mios.Solver.StatIndex
instance SAT.Mios.Types.VarOrder SAT.Mios.Solver.Solver


-- | This is a part of MIOS; main heuristics.
module SAT.Mios.Main

-- | #M22
--   
--   simplify : [void] -&gt; [bool]
--   
--   <b>Description:</b> Simplify the clause database according to the
--   current top-level assigment. Currently, the only thing done here is
--   the removal of satisfied clauses, but more things can be put here.
simplifyDB :: Solver -> IO Bool

-- | <b>Fig. 16. (p.20)</b> Main solve method.
--   
--   <b>Pre-condition:</b> If assumptions are used, <a>simplifyDB</a> must
--   be called right before using this method. If not, a top-level conflict
--   (resulting in a non-usable internal state) cannot be distinguished
--   from a conflict under assumptions.
solve :: (Foldable t) => Solver -> t Lit -> IO Bool


-- | validate an assignment
module SAT.Mios.Validator

-- | validates the assignment even if the implementation of <a>Solver</a>
--   is wrong; we re-implement some functions here.
validate :: Traversable t => Solver -> t Int -> IO Bool


-- | Minisat-based Implementation and Optimization Study on SAT solver
module SAT.Mios

-- | version name
versionId :: String

-- | Misc information on a CNF
data CNFDescription
CNFDescription :: !Int -> !Int -> Maybe FilePath -> CNFDescription

-- | the number of variables
[_numberOfVariables] :: CNFDescription -> !Int

-- | the number of clauses
[_numberOfClauses] :: CNFDescription -> !Int

-- | given filename
[_pathname] :: CNFDescription -> Maybe FilePath

-- | new top-level interface that returns:
--   
--   <ul>
--   <li>conflicting literal set :: Left [Int]</li>
--   <li>satisfiable assignment :: Right [Int]</li>
--   </ul>
runSolver :: Traversable t => MiosConfiguration -> CNFDescription -> t [Int] -> IO (Either [Int] [Int])

-- | The easiest interface for Haskell programs. This returns the result
--   <tt>::[[Int]]</tt> for a given <tt>(CNFDescription, [[Int]])</tt>. The
--   first argument <tt>target</tt> can be build by <tt>Just target &lt;-
--   cnfFromFile targetfile</tt>. The second part of the first argument is
--   a list of vector, which 0th element is the number of its real
--   elements.
solveSAT :: Traversable m => CNFDescription -> m [Int] -> IO [Int]

-- | solves the problem (2rd arg) under the configuration (1st arg). and
--   returns an assignment as list of literals :: Int.
solveSATWithConfiguration :: Traversable m => MiosConfiguration -> CNFDescription -> m [Int] -> IO [Int]

-- | <b>Fig. 16. (p.20)</b> Main solve method.
--   
--   <b>Pre-condition:</b> If assumptions are used, <a>simplifyDB</a> must
--   be called right before using this method. If not, a top-level conflict
--   (resulting in a non-usable internal state) cannot be distinguished
--   from a conflict under assumptions.
solve :: (Foldable t) => Solver -> t Lit -> IO Bool

-- | returns the model as a list of literal.
getModel :: Solver -> IO [Int]

-- | returns True if a given assignment (2nd arg) satisfies the problem
--   (1st arg). if you want to check the <tt>answer</tt> which a
--   <tt>slover</tt> returned, run <tt>solver <a>validate</a> answer</tt>,
--   where <a>validate</a> <tt> :: Traversable t =&gt; Solver -&gt; t Lit
--   -&gt; IO Bool</tt>.
validateAssignment :: (Traversable m, Traversable n) => CNFDescription -> m [Int] -> n Int -> IO Bool

-- | validates the assignment even if the implementation of <a>Solver</a>
--   is wrong; we re-implement some functions here.
validate :: Traversable t => Solver -> t Int -> IO Bool

-- | executes a solver on the given CNF file. This is the simplest entry to
--   standalone programs; not for Haskell programs.
executeSolverOn :: FilePath -> IO ()

-- | executes a solver on the given 'arg :: MiosConfiguration'. This is
--   another entry point for standalone programs.
executeSolver :: MiosProgramOption -> IO ()

-- | validates a given assignment from STDIN for the CNF file (2nd arg).
--   this is the entry point for standalone programs.
executeValidatorOn :: FilePath -> IO ()

-- | validates a given assignment for the problem (2nd arg). This is
--   another entry point for standalone programs; see app/mios.hs.
executeValidator :: MiosProgramOption -> IO ()

-- | dumps an assigment to file. 2nd arg is
--   
--   <ul>
--   <li><tt>True</tt> if the assigment is satisfiable assigment</li>
--   <li><tt>False</tt> if not</li>
--   </ul>
--   
--   <pre>
--   &gt;&gt;&gt; do y &lt;- solve s ... ; dumpAssigmentAsCNF "result.cnf" y &lt;$&gt; model s
--   </pre>
dumpAssigmentAsCNF :: FilePath -> Bool -> [Int] -> IO ()