| Safe Haskell | Safe |
|---|---|
| Language | Haskell2010 |
SAT.Mios.Solver
Description
(This is a part of MIOS.) Solver, the main data structure
- data Solver = Solver {
- clauses :: !ClauseExtManager
- learnts :: !ClauseExtManager
- watches :: !WatcherList
- assigns :: !(Vec Int)
- phases :: !(Vec Int)
- trail :: !Stack
- trailLim :: !Stack
- qHead :: !Int'
- reason :: !ClauseVector
- level :: !(Vec Int)
- conflicts :: !Stack
- activities :: !(Vec Double)
- order :: !VarHeap
- config :: !MiosConfiguration
- nVars :: !Int
- claInc :: !Double'
- varInc :: !Double'
- rootLevel :: !Int'
- learntSAdj :: Double'
- learntSCnt :: Int'
- maxLearnts :: Double'
- ok :: !Int'
- an'seen :: !(Vec Int)
- an'toClear :: !Stack
- an'stack :: !Stack
- an'lastDL :: !Stack
- clsPool :: ClausePool
- litsLearnt :: !Stack
- stats :: !(Vec [Int])
- lbd'seen :: !(Vec Int)
- lbd'key :: !Int'
- emaDFast :: !Double'
- emaDSlow :: !Double'
- emaAFast :: !Double'
- emaASlow :: !Double'
- nextRestart :: !Int'
- restartMode :: Int'
- 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
- setAssign :: Solver -> Int -> LiftedBool -> IO ()
- enqueue :: Solver -> Lit -> Clause -> IO Bool
- assume :: Solver -> Lit -> IO Bool
- cancelUntil :: Solver -> Int -> IO ()
- data StatIndex
- getStat :: Solver -> StatIndex -> IO Int
- setStat :: Solver -> StatIndex -> Int -> IO ()
- incrementStat :: Solver -> StatIndex -> Int -> IO ()
- getStats :: Solver -> IO [(StatIndex, Int)]
- dumpSolver :: DumpMode -> Solver -> IO ()
Solver
Fig. 2.(p.9) Internal State of the solver
Constructors
| Solver | |
Fields
| |
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
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).
Stats
stat index
Constructors
| NumOfBackjump | the number of backjump |
| NumOfRestart | the number of restart |
| NumOfBlockRestart | the number of blacking start |
| NumOfGeometricRestart | the number of classic restart |
| NumOfPropagation | the number of propagation |
| NumOfReduction | the number of reduction |
| NumOfClause | the number of |
| NumOfLearnt | the number of |
| NumOfVariable | the number of |
| NumOfAssigned | the number of assigned variables |
| EndOfStatIndex | Don't use this dummy. |