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


-- | A Minisat-based CDCL SAT solver in Haskell
--   
--   A modern and very fast SAT solver written in Haskell, using CDCL,
--   watch literals, VSIDS, blocking-literals, phase saving, LBD,
--   Glucose-like restart and so on. <a>Mios</a> is an abbreviation of
--   'Minisat-based Implementation and Optimization Study on SAT solver'.
@package mios
@version 1.6.2


-- | 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


-- | 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 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]]


-- | 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/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


-- | (This is a part of MIOS.) Abstraction Layer for Mutable Vectors
module SAT.Mios.Vec

-- | The interface on vectors.
class VecFamily v a | v -> a

-- | 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 ()

-- | 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]

-- | Another abstraction layer on <tt>Vector</tt> which reserves zero
--   element for internal use. <b>Note</b>: If you want to use the 0-th
--   element, use <tt>UVector Int</tt>.

-- | Interface for single (one-length vector) mutable data
class SingleStorage s t | s -> t

-- | 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' = ByteArrayDouble

-- | Mutable Int <b>Note:</b> Int' is identical to <a>Stack</a>
type Int' = ByteArrayInt

-- | Interface on stacks
class SingleStorage s Int => StackFamily s t | s -> t

-- | 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 ()

-- | Stack of Int, an alias of <tt>Vec Int</tt>
type Stack = Vec Int

-- | returns a new <a>Stack</a> from <tt>[Int]</tt>.
newStackFromList :: [Int] -> IO Stack

-- | returns the number of allocated slots
realLength :: Vec Int -> Int

-- | sort the content of a stack, in small-to-large order.
sortStack :: Stack -> IO ()
instance SAT.Mios.Vec.StackFamily SAT.Mios.Vec.ByteArrayInt GHC.Types.Int
instance SAT.Mios.Vec.SingleStorage SAT.Mios.Vec.Bool' GHC.Types.Bool
instance SAT.Mios.Vec.SingleStorage SAT.Mios.Vec.ByteArrayInt GHC.Types.Int
instance SAT.Mios.Vec.SingleStorage SAT.Mios.Vec.ByteArrayDouble GHC.Types.Double
instance SAT.Mios.Vec.VecFamily SAT.Mios.Vec.ByteArrayDouble GHC.Types.Double
instance SAT.Mios.Vec.VecFamily SAT.Mios.Vec.ByteArrayInt GHC.Types.Int
instance SAT.Mios.Vec.VecFamily (SAT.Mios.Vec.UVector GHC.Types.Int) GHC.Types.Int


-- | (This is a part of MIOS.) Basic data types used throughout mios.
module SAT.Mios.Types

-- | the type that Mios returns This captures the following three cases: *
--   solved with a satisfiable assigment, * proved that it's an
--   unsatisfiable problem, and * aborted due to Mios specification or an
--   internal error
type SolverResult = Either SolverException Certificate

-- | terminate and find an SAT/UNSAT answer
data Certificate
SAT :: [Int] -> Certificate
UNSAT :: [Int] -> Certificate

-- | abnormal termination flags
data SolverException
StateUNSAT :: SolverException
StateSAT :: SolverException
OutOfMemory :: SolverException
TimeOut :: SolverException
InternalInconsistent :: SolverException
UndescribedError :: SolverException

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

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

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

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

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

-- | decay rate for variable activity
[variableDecayRate] :: MiosConfiguration -> !Double

-- | decay rate for clause activity
[clauseDecayRate] :: MiosConfiguration -> !Double

-- | dump stats data during solving
[dumpSolverStatMode] :: MiosConfiguration -> !Int

-- | the coefficients for restarts
[emaCoeffs] :: MiosConfiguration -> !(Int, Int)

-- | restart expansion factor
[restartExpansion] :: MiosConfiguration -> !Double

-- | static Steps between restarts
[restartStep] :: 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

-- | 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

-- | Lifted Boolean domain (p.7) that extends <a>Bool</a> with "⊥" means
--   <i>undefined</i> design note: _|_ should be null = 0; True literals
--   are coded to even numbers. So it should be 2.
type LiftedBool = Int

-- | returns the value of a literal as a <a>LiftedBool</a>
lit2lbool :: Lit -> LiftedBool

-- | A fixed-precision integer type with at least the range <tt>[-2^29 ..
--   2^29-1]</tt>. The exact range for a given implementation can be
--   determined by using <a>minBound</a> and <a>maxBound</a> from the
--   <a>Bounded</a> class.
data 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 <tt>select</tt> will return the
--   unassigned variable with the highest activity.
class VarOrder o

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

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

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

-- | Exponential Moving Average, EMA
type EMA = (Double', Maybe Double', Double)

-- | returns a new EMA from a flag (slow or fast) and a window size
newEMA :: Bool -> Int -> IO EMA

-- | returns an EMA value
getEMA :: EMA -> IO Double

-- | updates an EMA
updateEMA :: EMA -> Double -> IO Double

-- | stat index
data StatIndex

-- | the number of backjump
NumOfBackjump :: StatIndex

-- | the number of restart
NumOfRestart :: StatIndex

-- | the number of blacking start
NumOfBlockRestart :: StatIndex

-- | the number of classic restart
NumOfGeometricRestart :: StatIndex

-- | the number of propagation
NumOfPropagation :: StatIndex

-- | the number of reduction
NumOfReduction :: StatIndex

-- | the number of <tt>alive</tt> given clauses
NumOfClause :: StatIndex

-- | the number of <tt>alive</tt> learnt clauses
NumOfLearnt :: StatIndex

-- | the number of <tt>alive</tt> variables
NumOfVariable :: StatIndex

-- | the number of assigned variables
NumOfAssigned :: StatIndex

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

-- | formats of state dump
data DumpMode
NoDump :: DumpMode
DumpCSVHeader :: DumpMode
DumpCSV :: DumpMode
DumpJSON :: DumpMode
instance GHC.Show.Show SAT.Mios.Types.MiosDump
instance GHC.Read.Read SAT.Mios.Types.MiosDump
instance GHC.Classes.Ord SAT.Mios.Types.MiosDump
instance GHC.Classes.Eq SAT.Mios.Types.MiosDump
instance GHC.Show.Show SAT.Mios.Types.MiosStats
instance GHC.Read.Read SAT.Mios.Types.MiosStats
instance GHC.Classes.Ord SAT.Mios.Types.MiosStats
instance GHC.Classes.Eq SAT.Mios.Types.MiosStats
instance GHC.Show.Show SAT.Mios.Types.DumpTag
instance GHC.Read.Read SAT.Mios.Types.DumpTag
instance GHC.Classes.Ord SAT.Mios.Types.DumpTag
instance GHC.Classes.Eq SAT.Mios.Types.DumpTag
instance GHC.Enum.Enum SAT.Mios.Types.DumpTag
instance GHC.Enum.Bounded SAT.Mios.Types.DumpTag
instance GHC.Show.Show SAT.Mios.Types.DumpMode
instance GHC.Read.Read SAT.Mios.Types.DumpMode
instance GHC.Classes.Ord SAT.Mios.Types.DumpMode
instance GHC.Classes.Eq SAT.Mios.Types.DumpMode
instance GHC.Enum.Enum SAT.Mios.Types.DumpMode
instance GHC.Enum.Bounded SAT.Mios.Types.DumpMode
instance GHC.Show.Show SAT.Mios.Types.StatIndex
instance GHC.Read.Read SAT.Mios.Types.StatIndex
instance GHC.Classes.Ord SAT.Mios.Types.StatIndex
instance GHC.Classes.Eq SAT.Mios.Types.StatIndex
instance GHC.Enum.Enum SAT.Mios.Types.StatIndex
instance GHC.Enum.Bounded SAT.Mios.Types.StatIndex
instance GHC.Show.Show SAT.Mios.Types.MiosConfiguration
instance GHC.Read.Read SAT.Mios.Types.MiosConfiguration
instance GHC.Classes.Ord SAT.Mios.Types.MiosConfiguration
instance GHC.Classes.Eq SAT.Mios.Types.MiosConfiguration
instance GHC.Show.Show SAT.Mios.Types.CNFDescription
instance GHC.Read.Read SAT.Mios.Types.CNFDescription
instance GHC.Classes.Ord SAT.Mios.Types.CNFDescription
instance GHC.Classes.Eq SAT.Mios.Types.CNFDescription
instance GHC.Show.Show SAT.Mios.Types.SolverException
instance GHC.Classes.Ord SAT.Mios.Types.SolverException
instance GHC.Classes.Eq SAT.Mios.Types.SolverException
instance GHC.Enum.Enum SAT.Mios.Types.SolverException
instance GHC.Enum.Bounded SAT.Mios.Types.SolverException
instance GHC.Show.Show SAT.Mios.Types.Certificate
instance GHC.Read.Read SAT.Mios.Types.Certificate
instance GHC.Classes.Ord SAT.Mios.Types.Certificate
instance GHC.Classes.Eq SAT.Mios.Types.Certificate


-- | (This is a part of MIOS.) Command line option parser
module SAT.Mios.OptionParser

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

-- | decay rate for variable activity
[variableDecayRate] :: MiosConfiguration -> !Double

-- | decay rate for clause activity
[clauseDecayRate] :: MiosConfiguration -> !Double

-- | dump stats data during solving
[dumpSolverStatMode] :: MiosConfiguration -> !Int

-- | the coefficients for restarts
[emaCoeffs] :: MiosConfiguration -> !(Int, Int)

-- | restart expansion factor
[restartExpansion] :: MiosConfiguration -> !Double

-- | static Steps between restarts
[restartStep] :: 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 :: Either String String -> [String] -> Maybe String -> Double -> Double -> Double -> Double -> Bool -> Bool -> Integer -> Int -> Bool -> Int -> Bool -> Bool -> Bool -> MiosProgramOption
[_targetFile] :: MiosProgramOption -> Either String String
[_targets] :: MiosProgramOption -> [String]
[_outputFile] :: MiosProgramOption -> Maybe String
[_confVariableDecayRate] :: MiosProgramOption -> Double
[_confClauseDecayRate] :: MiosProgramOption -> Double
[_confRestartE] :: MiosProgramOption -> Double
[_confRestartS] :: MiosProgramOption -> Double
[_confCheckAnswer] :: MiosProgramOption -> Bool
[_confVerbose] :: MiosProgramOption -> Bool
[_confBenchmark] :: MiosProgramOption -> Integer
[_confBenchSeq] :: MiosProgramOption -> Int
[_confNoAnswer] :: MiosProgramOption -> Bool
[_confDumpStat] :: MiosProgramOption -> Int
[_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


-- | (This is a part of MIOS.) 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 :: !Stack -> !Int' -> !Double' -> Clause

-- | literals and rank
[lits] :: Clause -> !Stack

-- | another metrics of this clause
[rank] :: Clause -> !Int'

-- | activity of this clause , protected :: !Bool' -- ^ protected from
--   reduce
[activity] :: Clause -> !Double'
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

-- | returns the rank, a goodness, of a given clause
getRank :: Clause -> IO Int

-- | sets the rank of a given clause
setRank :: Clause -> Int -> IO ()

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

-- | returns a new <a>ClauseVector</a>.
newClauseVector :: Int -> IO ClauseVector
instance SAT.Mios.Vec.VecFamily SAT.Mios.Clause.ClauseVector SAT.Mios.Clause.Clause
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


-- | (This is a part of MIOS.) 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 ClauseSimpleManager

-- | 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 (Vec 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 FIXME: sometimes n &gt; 1M
newWatcherList :: Int -> Int -> IO WatcherList

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


-- | (This is a part of MIOS.) Recycling clauses
module SAT.Mios.ClausePool

-- | an immutable Vector of <tt>ClauseSimpleManager</tt>
type ClausePool = Vector ClauseSimpleManager

-- | returns a new <a>ClausePool</a>
newClausePool :: Int -> IO ClausePool

-- | If a nice candidate as a learnt is stored, return it. Otherwise
--   allocate a new clause in heap then return it.
makeClauseFromStack :: ClausePool -> Stack -> IO Clause

-- | Note: only not-too-large and learnt clauses are recycled.
putBackToPool :: ClausePool -> Clause -> IO ()


-- | (This is a part of MIOS.) Solver, the main data structure
module SAT.Mios.Solver

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

-- | 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)

-- | For each variable, the number of depending decisions
[ndd] :: Solver -> !(Vec Int)

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

-- | 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

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

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

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

-- | used in <a>search</a>
[learntSAdj] :: Solver -> Double'

-- | used in <a>search</a>
[learntSCnt] :: Solver -> Int'

-- | used in <a>search</a>
[maxLearnts] :: Solver -> Double'

-- | internal flag
[ok] :: Solver -> !Int'

-- | 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

-- | clause recycler
[clsPool] :: Solver -> ClausePool

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

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

-- | used in lbd computation
[lbd'seen] :: Solver -> !(Vec Int)

-- | used in lbd computation
[lbd'key] :: Solver -> !Int'

-- | Number of Assignments Fast
[emaAFast] :: Solver -> !EMA

-- | Number of Assignments Slow
[emaASlow] :: Solver -> !EMA

-- | Backjumped and Restart Dicision Level
[emaBDLvl] :: Solver -> !EMA

-- | Conflicting Level
[emaCDLvl] :: Solver -> !EMA

-- | (Literal Block) Distance Fast
[emaDFast] :: Solver -> !EMA

-- | (Literal Block) Distance Slow
[emaDSlow] :: Solver -> !EMA

-- | next restart in number of conflict
[nextRestart] :: Solver -> !Int'

-- | incremented by blocking
[restartExp] :: Solver -> !Double'

-- | average phase of restart
[emaRstBias] :: Solver -> !EMA

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

-- | 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 (:: <a>LiftedBool</a> = <tt>[-1, 0, -1]</tt>)
--   from <a>Var</a>.
valueVar :: Solver -> Var -> IO Int

-- | returns the assignment (:: <a>LiftedBool</a> = <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

-- | assigns a value to the <i>n</i>-th variable
setAssign :: Solver -> Int -> LiftedBool -> IO ()

-- | <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 ()

-- | stat index
data StatIndex

-- | the number of backjump
NumOfBackjump :: StatIndex

-- | the number of restart
NumOfRestart :: StatIndex

-- | the number of blacking start
NumOfBlockRestart :: StatIndex

-- | the number of classic restart
NumOfGeometricRestart :: StatIndex

-- | the number of propagation
NumOfPropagation :: StatIndex

-- | the number of reduction
NumOfReduction :: StatIndex

-- | the number of <tt>alive</tt> given clauses
NumOfClause :: StatIndex

-- | the number of <tt>alive</tt> learnt clauses
NumOfLearnt :: StatIndex

-- | the number of <tt>alive</tt> variables
NumOfVariable :: StatIndex

-- | the number of assigned variables
NumOfAssigned :: 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 SAT.Mios.Types.VarOrder SAT.Mios.Solver.Solver


-- | (This is a part of MIOS.) 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


-- | (This is a part of MIOS.) Advanced heuristics library for <a>Main</a>
module SAT.Mios.Criteria

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

-- | <b>Fig. 14 (p.19)</b>
claDecayActivity :: 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 ()

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

-- | returns a POSIVITE value of Literal Block Distance
lbdOf :: Solver -> Stack -> IO Int

-- | updates all assigned vars' ndl
updateNDD :: Solver -> IO ()

-- | returns the NDL
nddOf :: Solver -> Stack -> IO Int

-- | 74, #91
checkRestartCondition :: Solver -> Int -> Int -> IO Bool

-- | print statatistic data to stdio. This should be called after each
--   restart.
dumpStats :: DumpMode -> Solver -> IO ()


-- | (This is a part of MIOS.) Main part of solving satisfiability problem.
module SAT.Mios.Main

-- | <b>Fig. 2.(p.9)</b> Internal State of the solver
data Solver

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

-- | assigns a value to the <i>n</i>-th variable
setAssign :: Solver -> Int -> LiftedBool -> IO ()

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

-- | print statatistic data to stdio. This should be called after each
--   restart.
dumpStats :: DumpMode -> Solver -> IO ()

-- | #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 SolverResult


-- | (This file is a part of MIOS.) 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 -> !FilePath -> CNFDescription

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

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

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

-- | the type that Mios returns This captures the following three cases: *
--   solved with a satisfiable assigment, * proved that it's an
--   unsatisfiable problem, and * aborted due to Mios specification or an
--   internal error
type SolverResult = Either SolverException Certificate

-- | terminate and find an SAT/UNSAT answer
data Certificate
SAT :: [Int] -> Certificate
UNSAT :: [Int] -> Certificate

-- | returns a MiosProgramOption for the target
buildOption :: Either FilePath String -> MiosProgramOption

-- | returns a new solver injected a problem
buildSolver :: MiosProgramOption -> IO Solver

-- | returns the data on a given CNF file. Only solver knows it.
buildDescription :: FilePath -> Solver -> IO CNFDescription

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

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

-- | NOT MAINTAINED NOW 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]

-- | executes a solver on the given 'arg :: MiosConfiguration'. This is
--   another entry point for standalone programs.
showAnswerFromString :: String -> IO String

-- | 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

-- | 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

-- | FIXME: swtich to DRAT
--   
--   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 (Just "result.cnf") y &lt;$&gt; model s
--   </pre>
dumpAssigmentAsCNF :: MiosProgramOption -> Certificate -> IO String