Safe Haskell | Safe |
---|---|
Language | Haskell2010 |
This is a part of MIOS; main data
- data Solver = Solver {
- model :: !VecBool
- conflict :: !Stack
- clauses :: !ClauseExtManager
- learnts :: !ClauseExtManager
- watches :: !WatcherList
- assigns :: !Vec
- phases :: !Vec
- trail :: !Stack
- trailLim :: !Stack
- qHead :: !IntSingleton
- reason :: !ClauseVector
- level :: !Vec
- activities :: !VecDouble
- order :: !VarHeap
- config :: !MiosConfiguration
- nVars :: !Int
- varInc :: !DoubleSingleton
- rootLevel :: !IntSingleton
- ok :: !BoolSingleton
- an'seen :: !Vec
- an'toClear :: !Stack
- an'stack :: !Stack
- pr'seen :: !Vec
- litsLearnt :: !Stack
- lastDL :: !Stack
- stats :: !Vec
- newSolver :: MiosConfiguration -> CNFDescription -> IO Solver
- nAssigns :: Solver -> IO Int
- nClauses :: Solver -> IO Int
- nLearnts :: Solver -> IO Int
- decisionLevel :: Solver -> IO Int
- valueVar :: Solver -> Var -> IO Int
- valueLit :: Solver -> Lit -> IO Int
- locked :: Solver -> Clause -> IO Bool
- addClause :: Solver -> Vec -> IO Bool
- enqueue :: Solver -> Lit -> Clause -> IO Bool
- assume :: Solver -> Lit -> IO Bool
- cancelUntil :: Solver -> Int -> IO ()
- getModel :: Solver -> IO [Int]
- claBumpActivity :: Solver -> Clause -> IO ()
- claRescaleActivityAfterRestart :: Solver -> IO ()
- varBumpActivity :: Solver -> Var -> IO ()
- varDecayActivity :: Solver -> IO ()
- claActivityThreshold :: Double
- data StatIndex
- getStat :: Solver -> StatIndex -> IO Int
- setStat :: Solver -> StatIndex -> Int -> IO ()
- incrementStat :: Solver -> StatIndex -> Int -> IO ()
- getStats :: Solver -> IO [(StatIndex, Int)]
Solver
Fig. 2.(p.9) Internal State of the solver
Solver | |
|
newSolver :: MiosConfiguration -> CNFDescription -> IO Solver Source #
returns an everything-is-initialized solver from the arguments
Misc Accessors
valueVar :: Solver -> Var -> IO Int Source #
returns the assignment (:: LiftedBool
= [-1, 0, -1]
) from Var
valueLit :: Solver -> Lit -> IO Int Source #
returns the assignment (:: LiftedBool
= [-1, 0, -1]
) from Lit
locked :: Solver -> Clause -> IO Bool Source #
Fig. 7. (p.11)
returns True
if the clause is locked (used as a reason). Learnt clauses only
State Modifiers
addClause :: Solver -> Vec -> IO Bool Source #
returns False
if a conflict has occured.
This function is called only before the solving phase to register the given clauses.
enqueue :: Solver -> Lit -> Clause -> IO Bool Source #
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).
assume :: Solver -> Lit -> IO Bool Source #
Fig. 12 (p.17)
returns False
if immediate conflict.
Pre-condition: propagation queue is empty
cancelUntil :: Solver -> Int -> IO () Source #
#M22: Revert to the states at given level (keeping all assignment at level
but not beyond).
Activities
claRescaleActivityAfterRestart :: Solver -> IO () Source #
Fig. 14 (p.19)
varDecayActivity :: Solver -> IO () Source #
Fig. 14 (p.19)
Stats
stat index