-- 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 1.8 time -- slower than Minisat-1.14. Mios is an abbreviation of -- Minisat-based Implementation and Optimization Study on SAT -- solver. @package mios @version 1.2.1 -- | Read an output file of minisat module SAT.Util.CNFIO.MinisatReader -- | read a minisat output: ((numbefOfVariables, 0), [Literal]) -- -- 
--   >>> fromFile "result"
--   ((3, 0), [1, -2, 3])
--
fromMinisatOutput :: FilePath -> IO (Maybe ((Int, Int), [Int])) -- | return clauses as [[Int]] from file -- -- 
--   >>> clauseListFromMinisatOutput "result"
--   [1,-2,3]
--
clauseListFromMinisatOutput :: FilePath -> IO [Int] -- | Write SAT data to CNF file module SAT.Util.CNFIO.Writer -- | Write the CNF to file f, using toCNFString toFile :: FilePath -> [[Int]] -> IO () -- | Convert [Clause] to String, where Clause is [Int] -- -- 
--   >>> toCNFString []
--   "p cnf 0 0\n"
--
-- -- 
--   >>> toCNFString [[-1, 2], [-3, -4]]
--   "p cnf 4 2\n-1 2 0\n-3 -4 0\n"
--
-- -- 
--   >>> toCNFString [[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"
--
toCNFString :: [[Int]] -> String -- | converts [[Int]] to a String toString :: [[Int]] -> String -> String -> String -- | converts [[Int]] to a LaTeX expression toLatexString :: [[Int]] -> String -- | Read a CNF file without haskell-platform module SAT.Util.CNFIO.Reader -- | read a CNF file and return: ((numbefOfVariables, numberOfClauses), -- [Literal]) -- -- 
--   >>> fromFile "acnf"
--   ((3, 4), [[1, 2], [-2, 3], [-1, 2, -3], [3]]
--
fromFile :: FilePath -> IO (Maybe ((Int, Int), [[Int]])) -- | return clauses as [[Int]] from file -- -- 
--   >>> clauseListFromFile "a.cnf"
--   [[1, 2], [-2, 3], [-1, 2, -3], [3]]
--
clauseListFromFile :: FilePath -> IO [[Int]] -- | Boolean Expression module to build CNF from arbitrary expressions -- Tseitin translation: -- http://en.wikipedia.org/wiki/Tseitin_transformation module SAT.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 -- -- 
--   >>> asList $ "3" -|- "4"
--   [[3,4,-5],[-3,5],[-4,5]]
--
-- -- 
--   >>> asList (("3" -|- "4") -|- "-1")
--   [[3,4,-5],[-3,5],[-4,5],[5,-1,-6],[-5,6],[1,6]]
--
(-|-) :: (BoolComponent a, BoolComponent b) => a -> b -> BoolForm -- | conjunction constructor -- -- 
--   >>> asList $ "3" -&- "-2"
--   [[-3,2,4],[3,-4],[-2,-4]]
--
-- -- 
--   >>> asList $ "3" -|- ("1" -&- "2")
--   [[-1,-2,4],[1,-4],[2,-4],[3,4,-5],[-3,5],[-4,5]]
--
(-&-) :: (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 -- -- 
--   >>> asList ("1" ->- "2")
--   [[-1,-3],[1,3],[3,2,-4],[-3,4],[-2,4]]
--
(->-) :: (BoolComponent a, BoolComponent b) => a -> b -> BoolForm -- | negate a form -- -- 
--   >>> asList $ neg ("1" -|- "2")
--   [[1,2,-3],[-1,3],[-2,3],[-3,-4],[3,4]]
--
neg :: (BoolComponent a) => a -> BoolForm -- | merge [BoolForm] by '(-|-)' disjunctionOf :: [BoolForm] -> BoolForm -- | an alias of disjunctionOf (-|||-) :: [BoolForm] -> BoolForm -- | merge [BoolForm] by '(-&-)' conjunctionOf :: [BoolForm] -> BoolForm -- | an alias of conjunctionOf (-&&&-) :: [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 asList asLatex :: BoolForm -> String -- | make latex string from CNF, using asList_ -- -- 
--   >>> asLatex $ "3" -|- "4"
--   "\\begin{displaymath}\n( x_{3} \\vee x_{4} )\n\\end{displaymath}\n"
--
asLatex_ :: BoolForm -> String -- | returns the number of variables in the BoolForm numberOfVariables :: BoolForm -> Int -- | returns the number of clauses in the BoolForm numberOfClauses :: BoolForm -> Int -- | the start index for the generated variables by Tseitin encoding tseitinBase :: Int instance GHC.Show.Show SAT.Util.BoolExp.BoolForm instance GHC.Classes.Eq SAT.Util.BoolExp.BoolForm instance SAT.Util.BoolExp.BoolComponent GHC.Types.Int instance SAT.Util.BoolExp.BoolComponent SAT.Util.BoolExp.L instance SAT.Util.BoolExp.BoolComponent [GHC.Types.Char] instance SAT.Util.BoolExp.BoolComponent SAT.Util.BoolExp.BoolForm instance SAT.Util.BoolExp.BoolComponent GHC.Types.Bool instance GHC.Classes.Ord SAT.Util.BoolExp.BoolForm -- | Read/Write a CNF file only with ghc standard libraries module SAT.Util.CNFIO -- | read a CNF file and return: ((numbefOfVariables, numberOfClauses), -- [Literal]) -- -- 
--   >>> fromFile "acnf"
--   ((3, 4), [[1, 2], [-2, 3], [-1, 2, -3], [3]]
--
fromFile :: FilePath -> IO (Maybe ((Int, Int), [[Int]])) -- | return clauses as [[Int]] from file -- -- 
--   >>> clauseListFromFile "a.cnf"
--   [[1, 2], [-2, 3], [-1, 2, -3], [3]]
--
clauseListFromFile :: FilePath -> IO [[Int]] -- | read a minisat output: ((numbefOfVariables, 0), [Literal]) -- -- 
--   >>> fromFile "result"
--   ((3, 0), [1, -2, 3])
--
fromMinisatOutput :: FilePath -> IO (Maybe ((Int, Int), [Int])) -- | return clauses as [[Int]] from file -- -- 
--   >>> clauseListFromMinisatOutput "result"
--   [1,-2,3]
--
clauseListFromMinisatOutput :: FilePath -> IO [Int] -- | Write the CNF to file f, using toCNFString toFile :: FilePath -> [[Int]] -> IO () -- | Convert [Clause] to String, where Clause is [Int] -- -- 
--   >>> toCNFString []
--   "p cnf 0 0\n"
--
-- -- 
--   >>> toCNFString [[-1, 2], [-3, -4]]
--   "p cnf 4 2\n-1 2 0\n-3 -4 0\n"
--
-- -- 
--   >>> toCNFString [[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"
--
toCNFString :: [[Int]] -> String -- | String from BoolFrom asCNFString :: BoolForm -> String -- | String from BoolFrom asCNFString_ :: BoolForm -> String -- | A fast(est) mutable data module SAT.Solver.Mios.Data.Singleton -- | mutable Bool type BoolSingleton = IOVector Bool -- | returns a new BoolSingleton newBool :: Bool -> IO BoolSingleton -- | returns the value getBool :: BoolSingleton -> IO Bool -- | sets the value setBool :: BoolSingleton -> Bool -> IO () -- | modifies the value modifyBool :: BoolSingleton -> (Bool -> Bool) -> IO () -- | mutable Int type IntSingleton = IOVector Int -- | returns a new IntSingleton newInt :: Int -> IO IntSingleton -- | returns the value getInt :: IntSingleton -> IO Int -- | sets the value setInt :: IntSingleton -> Int -> IO () -- | modifies the value modifyInt :: IntSingleton -> (Int -> Int) -> IO () -- | mutable Double type DoubleSingleton = IOVector Double -- | returns a new DoubleSingleton newDouble :: Double -> IO DoubleSingleton -- | returns the value getDouble :: DoubleSingleton -> IO Double -- | sets the value setDouble :: DoubleSingleton -> Double -> IO () -- | modifies the value modifyDouble :: DoubleSingleton -> (Double -> Double) -> IO () -- | The fundamental data structure: Fixed Mutable Unboxed Int Vector module SAT.Solver.Mios.Data.Vec -- | Costs of all operations are O(1) type Vec = IOVector Int -- | returns the size of Vec sizeOfVector :: Vec -> IO Int -- | gets the nth value getNth :: Vec -> Int -> IO Int -- | sets the nth value setNth :: Vec -> Int -> Int -> IO () -- | swaps two elements swapBetween :: Vec -> Int -> Int -> IO () -- | modify the nth value modifyNth :: Vec -> (Int -> Int) -> Int -> IO () -- | sets all elements setAll :: Vec -> Int -> IO () -- | returns a new Vec newVec :: Int -> IO Vec -- | returns a new Vec filled with an Int newVecWith :: Int -> Int -> IO Vec -- | returns a new Vec from a [Int] newSizedVecIntFromList :: [Int] -> IO Vec -- | returns a new Vec from a Unboxed Int Vector newSizedVecIntFromUVector :: Vector Int -> IO Vec -- | calls unasfeGrow vecGrow :: Vec -> Int -> IO Vec -- | Basic data types used throughout mios. module SAT.Solver.Mios.Types -- | Public interface as Container class VectorFamily s t | s -> t where clear = error "no default method for clear" dump msg _ = error $ msg ++ ": no defalut method for dump" asVec = error "asVector undefined" asList = error "asList undefined" -- | erases all elements in it clear :: VectorFamily s t => s -> IO () -- | dump the contents dump :: (VectorFamily s t, Show t) => String -> s -> IO String -- | get a raw data asVec :: VectorFamily s t => s -> IOVector Int -- | converts into a list asList :: VectorFamily s t => s -> IO [t] -- | represents Var type Var = Int -- | Special constant in Var (p.7) bottomVar :: Var -- | converts a usual Int as literal to an internal Var presentation -- -- 
--   >>> int2var 1
--   1  -- the first literal is the first variable
--   
--   >>> int2var 2
--   2  -- literal @2@ is variable 2
--   
--   >>> int2var (-2)
--   2 -- literal @-2@ is corresponding to variable 2
--
int2var :: Integer -> Integer -- | The literal data has an index method which converts the -- literal to a "small" integer suitable for array indexing. The -- var method returns the underlying variable of the literal, -- and the sign method if the literal is signed (False for -- x and True for -x). type Lit = Int -- | converts Lit into Int as int2lit . lit2int == -- id -- -- 
--   >>> lit2int 2
--   1
--   
--   >>> lit2int 3
--   -1
--   
--   >>> lit2int 4
--   2
--   
--   >>> lit2int 5
--   -2
--
lit2int :: Lit -> Int -- | converts Int into Lit as lit2int . int2lit == -- id -- -- 
--   >>> int2lit 1
--   2
--   
--   >>> int2lit (-1)
--   3
--   
--   >>> int2lit 2
--   4
--   
--   >>> int2lit (-2)
--   5
--
int2lit :: Int -> Lit -- | Special constant in Lit (p.7) bottomLit :: Lit -- | converts Var into Lit newLit :: Var -> Lit -- | returns True if the literal is positive positiveLit :: Lit -> Bool -- | converts Lit into Var -- -- 
--   >>> lit2var 2
--   1
--   
--   >>> lit2var 3
--   1
--   
--   >>> lit2var 4
--   2
--   
--   >>> lit2var 5
--   2
--
lit2var :: Lit -> Var -- | converts a Var to the corresponing literal -- -- 
--   >>> var2lit 1 True
--   2
--   
--   >>> var2lit 1 False
--   3
--   
--   >>> var2lit 2 True
--   4
--   
--   >>> var2lit 2 False
--   5
--
var2lit :: Var -> Bool -> Lit -- | negates literal -- -- 
--   >>> negateLit 2
--   3
--   
--   >>> negateLit 3
--   2
--   
--   >>> negateLit 4
--   5
--   
--   >>> negateLit 5
--   4
--
negateLit :: Lit -> Lit -- | Lifted Boolean domain (p.7) that extends Bool with "⊥" means -- undefined design note: _|_ should be null = 0; True literals -- are coded to even numbers. So it should be 2. data LiftedBool Bottom :: LiftedBool LFalse :: LiftedBool LTrue :: LiftedBool -- | converts Bool into LBool lbool :: Bool -> LiftedBool -- | A contant representing False lFalse :: Int -- | A constant representing True lTrue :: Int -- | A constant for "undefined" 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 select will return the -- unassigned variable with the highest activity. class VarOrder o where newVarOrder _ _ = error "newVarOrder undefined" newVar = error "newVar undefined" update _ = error "update undefined" updateAll = error "updateAll undefined" undo _ _ = error "undo undefined" select = error "select undefined" -- | constructor newVarOrder :: (VarOrder o, VectorFamily v1 Bool, VectorFamily v2 Double) => v1 -> v2 -> IO o -- | Called when a new variable is created. newVar :: VarOrder o => o -> IO Var -- | Called when variable has increased in activity. update :: VarOrder o => o -> Var -> IO () -- | Called when all variables have been assigned new activities. updateAll :: VarOrder o => o -> IO () -- | Called when variable is unbound (may be selected again). undo :: VarOrder o => o -> Var -> IO () -- | Called to select a new, unassigned variable. select :: VarOrder o => o -> IO Var -- | misc information on CNF data CNFDescription CNFDescription :: !Int -> !Int -> Maybe FilePath -> CNFDescription -- | number of variables [_numberOfVariables] :: CNFDescription -> !Int -- | number of clauses [_numberOfClauses] :: CNFDescription -> !Int -- | given filename [_pathname] :: CNFDescription -> Maybe FilePath instance GHC.Show.Show SAT.Solver.Mios.Types.CNFDescription instance GHC.Classes.Ord SAT.Solver.Mios.Types.CNFDescription instance GHC.Classes.Eq SAT.Solver.Mios.Types.CNFDescription instance GHC.Show.Show SAT.Solver.Mios.Types.LiftedBool instance GHC.Read.Read SAT.Solver.Mios.Types.LiftedBool instance GHC.Classes.Ord SAT.Solver.Mios.Types.LiftedBool instance GHC.Classes.Eq SAT.Solver.Mios.Types.LiftedBool instance GHC.Enum.Bounded SAT.Solver.Mios.Types.LiftedBool instance SAT.Solver.Mios.Types.VectorFamily SAT.Solver.Mios.Data.Vec.Vec GHC.Types.Int instance GHC.Enum.Enum SAT.Solver.Mios.Types.LiftedBool -- | Clause, a data supporting pointer-based equality module SAT.Solver.Mios.Clause -- | Fig. 7.(p.11) clause, null, binary clause. This matches both of -- Clause and GClause in MiniSat TODO: GADTs is better? data Clause Clause :: !Bool -> !DoubleSingleton -> !BoolSingleton -> !IntSingleton -> !Vec -> Clause -- | whether this is a learnt clause [learnt] :: Clause -> !Bool -- | activity of this clause [activity] :: Clause -> !DoubleSingleton -- | protected from reduce [protected] :: Clause -> !BoolSingleton -- | storing the LBD; values are computed in Solver [lbd] :: Clause -> !IntSingleton -- | which this clause consists of [lits] :: Clause -> !Vec NullClause :: Clause -- | drop the last N literals in a Clause to eliminate -- unsatisfied literals shrinkClause :: Int -> Clause -> IO () -- | copies vec and return a new Clause Since 1.0.100 DIMACS -- reader should use a scratch buffer allocated statically. newClauseFromVec :: Bool -> Vec -> IO Clause -- | returns the number of literals in a clause, even if the given clause -- is a binary clause sizeOfClause :: Clause -> IO Int -- | Mutable Clause Vector type ClauseVector = IOVector Clause -- | returns a new ClauseVector newClauseVector :: Int -> IO ClauseVector -- | returns the nth Clause getNthClause :: ClauseVector -> Int -> IO Clause -- | sets the nth Clause setNthClause :: ClauseVector -> Int -> Clause -> IO () -- | swaps the two Clauses swapClauses :: ClauseVector -> Int -> Int -> IO () instance GHC.Classes.Eq SAT.Solver.Mios.Clause.Clause instance GHC.Show.Show SAT.Solver.Mios.Clause.Clause instance SAT.Solver.Mios.Types.VectorFamily SAT.Solver.Mios.Clause.Clause SAT.Solver.Mios.Types.Lit instance SAT.Solver.Mios.Types.VectorFamily SAT.Solver.Mios.Clause.ClauseVector SAT.Solver.Mios.Clause.Clause -- | A shrinkable VectorFamily of Clause module SAT.Solver.Mios.ClauseManager -- | resizable clause vector class ClauseManager a newManager :: ClauseManager a => Int -> IO a numberOfClauses :: ClauseManager a => a -> IO Int clearManager :: ClauseManager a => a -> IO () shrinkManager :: ClauseManager a => a -> Int -> IO () getClauseVector :: ClauseManager a => a -> IO ClauseVector pushClause :: ClauseManager a => a -> Clause -> IO () -- | Clause + Blocking Literal data ClauseExtManager -- | O(1) inserter pushClauseWithKey :: ClauseExtManager -> Clause -> Lit -> IO () -- | returns the associated Int vector getKeyVector :: ClauseExtManager -> IO Vec -- | sets the expire flag to a clause markClause :: ClauseExtManager -> Clause -> IO () -- | Vector of ClauseExtManager type WatcherList = Vector ClauseExtManager -- | n is the number of Var, m is default size of each -- watcher list | For n vars, we need [0 .. 2 + 2 * n - 1] slots, -- namely 2 * (n + 1)-length vector newWatcherList :: Int -> Int -> IO WatcherList -- | returns the watcher List :: ClauseManager for Literal -- l getNthWatcher :: WatcherList -> Lit -> ClauseExtManager -- | purges all expirable clauses in WatcherList garbageCollect :: WatcherList -> IO () instance SAT.Solver.Mios.ClauseManager.ClauseManager SAT.Solver.Mios.ClauseManager.ClauseExtManager instance SAT.Solver.Mios.Types.VectorFamily SAT.Solver.Mios.ClauseManager.ClauseExtManager SAT.Solver.Mios.Clause.Clause instance SAT.Solver.Mios.Types.VectorFamily SAT.Solver.Mios.ClauseManager.WatcherList SAT.Solver.Mios.Clause.Clause -- | Mutable Unboxed Boolean Vector -- -- module SAT.Solver.Mios.Data.VecBool -- | Mutable unboxed Bool Vector type VecBool = IOVector Bool -- | returns a new VecBool newVecBool :: Int -> Bool -> IO VecBool -- | returns the nth value in VecBool getNthBool :: VecBool -> Int -> IO Bool -- | sets the nth value setNthBool :: VecBool -> Int -> Bool -> IO () -- | sets the nth value modifyNthBool :: VecBool -> (Bool -> Bool) -> Int -> IO () instance SAT.Solver.Mios.Types.VectorFamily SAT.Solver.Mios.Data.VecBool.VecBool GHC.Types.Bool -- | Mutable Unboxed Double Vector module SAT.Solver.Mios.Data.VecDouble -- | Mutable unboxed Double Vector type VecDouble = IOVector Double -- | returns a new VecDouble newVecDouble :: Int -> Double -> IO VecDouble -- | returns the nth value in VecDouble getNthDouble :: Int -> VecDouble -> IO Double -- | sets the nth value setNthDouble :: Int -> VecDouble -> Double -> IO () -- | updates the nth value modifyNthDouble :: Int -> VecDouble -> (Double -> Double) -> IO () instance SAT.Solver.Mios.Types.VectorFamily SAT.Solver.Mios.Data.VecDouble.VecDouble GHC.Types.Double -- | stack of Int, by adding the length field as the zero-th element to a -- Vec module SAT.Solver.Mios.Data.Stack -- | Unboxed mutable stack for Int. data Stack -- | returns a new stack which size is size newStack :: Int -> IO Stack -- | clear stack clearStack :: Stack -> IO () -- | returns the number of elements sizeOfStack :: Stack -> IO Int -- | pushs an int to Stack pushToStack :: Stack -> Int -> IO () -- | drops the first element from Stack popFromStack :: Stack -> IO () -- | peeks the last element in Stack lastOfStack :: Stack -> IO Int -- | Shrink the stack. The given arg means the number of discards. -- therefore, shrink s n == for [1 .. n] $ _ -> pop s shrinkStack :: Stack -> Int -> IO () -- | converts Stack to sized Vec; this is the method to get the internal -- vector asSizedVec :: Stack -> Vec -- | isomorphic conversion to Vec -- -- Note: asVec drops the 1st element and no copy (unsafe -- operation); isoVec really copies the real elements isoVec :: Stack -> IO Vec instance SAT.Solver.Mios.Types.VectorFamily SAT.Solver.Mios.Data.Stack.Stack GHC.Types.Int -- | Internal Settings module SAT.Solver.Mios.Internal -- | version name versionId :: String -- | solver's parameters; random decision rate was dropped. data MiosConfiguration MiosConfiguration :: Double -> Double -> Bool -> MiosConfiguration -- | decay rate for variable activity [variableDecayRate] :: MiosConfiguration -> Double -- | decay rate for clause activity [clauseDecayRate] :: MiosConfiguration -> Double -- | whether collect and report statistics [collectStats] :: MiosConfiguration -> Bool -- | dafault configuration -- -- defaultConfiguration :: MiosConfiguration -- | This is a part of MIOS module SAT.Solver.Mios.Solver -- | Fig. 2.(p.9) Internal State of the solver data Solver Solver :: !VecBool -> !Stack -> !ClauseExtManager -> !ClauseExtManager -> !WatcherList -> !Vec -> !Vec -> !Stack -> !Stack -> !IntSingleton -> !ClauseVector -> !Vec -> !VecDouble -> !VarHeap -> !MiosConfiguration -> !Int -> !DoubleSingleton -> !DoubleSingleton -> !IntSingleton -> !BoolSingleton -> !Vec -> !Stack -> !Stack -> !Vec -> !Vec -> !IntSingleton -> !Stack -> !Stack -> !Vec -> Solver -- | If found, this vector has the model [model] :: Solver -> !VecBool -- | set of literals in the case of conflicts Clause Database [conflict] :: Solver -> !Stack -- | List of problem constraints. [clauses] :: Solver -> !ClauseExtManager -- | List of learnt clauses. [learnts] :: Solver -> !ClauseExtManager -- | a list of constraint wathing p, literal-indexed Assignment -- Management [watches] :: Solver -> !WatcherList -- | The current assignments indexed on variables; var-indexed [assigns] :: Solver -> !Vec -- | The last assignments indexed on variables; var-indexed [phases] :: Solver -> !Vec -- | List of assignments in chronological order; var-indexed [trail] :: Solver -> !Stack -- | Separator indices for different decision levels in trail. [trailLim] :: Solver -> !Stack -- | trail is divided at qHead; assignments and queue [qHead] :: Solver -> !IntSingleton -- | For each variable, the constraint that implied its value; var-indexed [reason] :: Solver -> !ClauseVector -- | For each variable, the decision level it was assigned; var-indexed -- Variable Order [level] :: Solver -> !Vec -- | Heuristic measurement of the activity of a variable; var-indexed [activities] :: Solver -> !VecDouble -- | Keeps track of the dynamic variable order. Configuration [order] :: Solver -> !VarHeap -- | search paramerters [config] :: Solver -> !MiosConfiguration -- | number of variables [nVars] :: Solver -> !Int -- | Clause activity increment amount to bump with. , varDecay :: -- !DoubleSingleton -- ^ used to set varInc [claInc] :: Solver -> !DoubleSingleton -- | Variable activity increment amount to bump with. [varInc] :: Solver -> !DoubleSingleton -- | Separates incremental and search assumptions. Working Memory [rootLevel] :: Solver -> !IntSingleton -- | return value holder [ok] :: Solver -> !BoolSingleton -- | scratch var for analyze; var-indexed [an'seen] :: Solver -> !Vec -- | ditto [an'toClear] :: Solver -> !Stack -- | ditto [an'stack] :: Solver -> !Stack -- | used in propagate [pr'seen] :: Solver -> !Vec -- | used in lbd computation [lbd'seen] :: Solver -> !Vec -- | used in lbd computation [lbd'key] :: Solver -> !IntSingleton -- | used to create a learnt clause [litsLearnt] :: Solver -> !Stack -- | last decision level used in analyze [lastDL] :: Solver -> !Stack -- | statistics information holder [stats] :: Solver -> !Vec -- | 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 (:: LiftedBool = [-1, 0, -1]) -- from Var valueVar :: Solver -> Var -> IO Int -- | returns the assignment (:: LiftedBool = [-1, 0, -1]) -- from Lit valueLit :: Solver -> Lit -> IO Int -- | Fig. 7. (p.11) returns True if the clause is locked -- (used as a reason). Learnt clauses only locked :: Solver -> Clause -> IO Bool -- | VarHeap is a heap tree built from two Vec This -- implementation is identical wtih that in Minisat-1.14 Note: the -- zero-th element of heap is used for holding the number of -- elements Note: VarHeap itself is not a VarOrder, because it -- requires a pointer to solver data VarHeap -- | returns False if a conflict has occured. This function is -- called only before the solving phase to register the given clauses. addClause :: Solver -> Vec -> IO Bool -- | Fig. 9 (p.14) 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, False is returned and the propagation -- queue is cleared. The parameter from contains a reference to -- the constraint from which p was propagated (defaults to -- Nothing if omitted). enqueue :: Solver -> Lit -> Clause -> IO Bool -- | Fig. 12 (p.17) returns False if immediate conflict. -- -- Pre-condition: propagation queue is empty assume :: Solver -> Lit -> IO Bool -- | #M22: Revert to the states at given level (keeping all assignment at -- level but not beyond). cancelUntil :: Solver -> Int -> IO () -- | return the model as a list of literal getModel :: Solver -> IO [Int] -- | Fig. 14 (p.19) claBumpActivity :: Solver -> Clause -> IO () -- | Fig. 14 (p.19) claDecayActivity :: Solver -> IO () -- | Fig. 14 (p.19) Bumping of clause activity varBumpActivity :: Solver -> Var -> IO () -- | Fig. 14 (p.19) varDecayActivity :: Solver -> IO () -- | stats data StatIndex NumOfBackjump :: StatIndex NumOfRestart :: StatIndex -- | increments a stat data corresponding to StatIndex incrementStat :: Solver -> StatIndex -> Int -> IO () -- | returns the statistics as list getStats :: Solver -> IO [(StatIndex, Int)] instance GHC.Show.Show SAT.Solver.Mios.Solver.StatIndex instance GHC.Read.Read SAT.Solver.Mios.Solver.StatIndex instance GHC.Classes.Ord SAT.Solver.Mios.Solver.StatIndex instance GHC.Classes.Eq SAT.Solver.Mios.Solver.StatIndex instance GHC.Enum.Enum SAT.Solver.Mios.Solver.StatIndex instance GHC.Enum.Bounded SAT.Solver.Mios.Solver.StatIndex instance SAT.Solver.Mios.Types.VarOrder SAT.Solver.Mios.Solver.Solver -- | validate an assignment module SAT.Solver.Mios.Validator -- | validates the assignment even if the implementation of Solver -- is wrong; we re-implement some functions here. validate :: Traversable t => Solver -> t Int -> IO Bool -- | This is a part of MIOS module SAT.Solver.Mios.Glucose -- | returns the LBD vaule for 'Vec[1 ..]' computeLBD :: Solver -> Vec -> IO Int -- | returns the LBD value of Clause lbdOf :: Solver -> Clause -> IO Int -- | update the LBD field in Clause setLBD :: Solver -> Clause -> IO () -- | update the lbd field of c updateLBD :: Solver -> Clause -> IO () -- | 0 based -- -- 
--   >>> nextReduction 0
--   20000
--   
--   >>> nextReduction 1
--   40000 + 200 = 20000 + 20000 + 200
--   
--   >>> nextReduction 2
--   6000 + 600 = 20000 + 20200 + 20000 + 400
--   
--   >>> nextReduction 3
--   80000 + 1200 = 20000 + 20200 + 20400 + 20000 + 600
--
nextReduction :: Int -> Int -> Int -- | This is a part of MIOS module SAT.Solver.Mios.M114 -- | #M22 -- -- simplify : [void] -> [bool] -- -- Description: 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 -- | Fig. 16. (p.20) Main solve method. -- -- Pre-condition: If assumptions are used, simplifyDB 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 -- | command line option parser for mios module SAT.Solver.Mios.OptionParser -- | solver's parameters; random decision rate was dropped. data MiosConfiguration MiosConfiguration :: Double -> Double -> Bool -> MiosConfiguration -- | decay rate for variable activity [variableDecayRate] :: MiosConfiguration -> Double -- | decay rate for clause activity [clauseDecayRate] :: MiosConfiguration -> Double -- | whether collect and report statistics [collectStats] :: MiosConfiguration -> Bool -- | dafault configuration -- -- defaultConfiguration :: MiosConfiguration -- | configuration swithces data MiosProgramOption MiosProgramOption :: Maybe String -> Maybe String -> Double -> Double -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> MiosProgramOption [_targetFile] :: MiosProgramOption -> Maybe String [_outputFile] :: MiosProgramOption -> Maybe String [_confVariableDecayRate] :: MiosProgramOption -> Double [_confClauseDecayRate] :: 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 MiosProgramOption from string given as command option miosParseOptions :: String -> [String] -> IO MiosProgramOption -- | builds MiosProgramOption from a String miosParseOptionsFromArgs :: String -> IO MiosProgramOption -- | converts MiosProgramOption into SIHConfiguration toMiosConf :: MiosProgramOption -> MiosConfiguration -- | Minisat-based Implementation and Optimization Study on SAT solver module SAT.Solver.Mios -- | version name versionId :: String -- | misc information on CNF data CNFDescription CNFDescription :: !Int -> !Int -> Maybe FilePath -> CNFDescription -- | number of variables [_numberOfVariables] :: CNFDescription -> !Int -- | number of clauses [_numberOfClauses] :: CNFDescription -> !Int -- | given filename [_pathname] :: CNFDescription -> Maybe FilePath -- | new top-level interface that returns -- -- runSolver :: Traversable t => MiosConfiguration -> CNFDescription -> t [Int] -> IO (Either [Int] [Int]) -- | the easiest interface for Haskell programs This returns the result -- ::[[Int]] for a given (CNFDescription, [[Int]]) The -- first argument target can be build by Just target <- -- cnfFromFile targetfile. 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] -- | Fig. 16. (p.20) Main solve method. -- -- Pre-condition: If assumptions are used, simplifyDB 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 -- | return 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 answer which a -- slover returned, run solver validate answer, -- where validate :: Traversable t => Solver -> t Lit -- -> IO Bool validateAssignment :: (Traversable m, Traversable n) => CNFDescription -> m [Int] -> n Int -> IO Bool -- | validates the assignment even if the implementation of Solver -- 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 -- -- -- -- 
--   >>> do y <- solve s ... ; dumpAssigmentAsCNF "result.cnf" y <$> model s
--
dumpAssigmentAsCNF :: FilePath -> Bool -> [Int] -> IO ()