| Safe Haskell | Safe |
|---|---|
| Language | Haskell2010 |
SAT.Mios.Types
Contents
Description
(This is a part of MIOS.) Basic data types used throughout mios.
- type SolverResult = Either SolverException Certificate
- data Certificate
- data SolverException
- data CNFDescription = CNFDescription {}
- data MiosConfiguration = MiosConfiguration {
- variableDecayRate :: !Double
- clauseDecayRate :: !Double
- dumpStat :: !Int
- defaultConfiguration :: MiosConfiguration
- module SAT.Mios.Vec
- type Var = Int
- bottomVar :: Var
- int2var :: Int -> Int
- type Lit = Int
- lit2int :: Lit -> Int
- int2lit :: Int -> Lit
- bottomLit :: Lit
- positiveLit :: Lit -> Bool
- lit2var :: Lit -> Var
- var2lit :: Var -> Bool -> Lit
- negateLit :: Lit -> Lit
- type LiftedBool = Int
- lit2lbool :: Lit -> LiftedBool
- data Int :: * where
- class VarOrder o where
- data StatIndex
- data DumpMode
Interface to caller
type SolverResult = Either SolverException Certificate Source #
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
data SolverException Source #
abnormal termination flags
data CNFDescription Source #
Misc information on a CNF
Constructors
| CNFDescription | |
Fields
| |
Instances
Solver Configuration
data MiosConfiguration Source #
Solver's parameters; random decision rate was dropped.
Constructors
| MiosConfiguration | |
Fields
| |
defaultConfiguration :: MiosConfiguration Source #
dafault configuration
- Minisat-1.14 uses
(0.95, 0.999, 0.2 = 20 / 1000). - Minisat-2.20 uses
(0.95, 0.999, 0). - Gulcose-4.0 uses
(0.8 , 0.999, 0). - Mios-1.2 uses
(0.95, 0.999, 0).
internal structure
module SAT.Mios.Vec
Variable
int2var :: Int -> Int Source #
converts a usual Int as literal to an internal Var presentation.
>>>int2var 11 -- the first literal is the first variable>>>int2var 22 -- literal @2@ is variable 2>>>int2var (-2)2 -- literal @-2@ is corresponding to variable 2
Internal encoded Literal
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).
positiveLit :: Lit -> Bool Source #
returns True if the literal is positive
var2lit :: Var -> Bool -> Lit Source #
converts a Var to the corresponing literal.
>>>var2lit 1 True2>>>var2lit 1 False3>>>var2lit 2 True4>>>var2lit 2 False5
negateLit :: Lit -> Lit Source #
negates literal
>>>negateLit 23>>>negateLit 32>>>negateLit 45>>>negateLit 54
Assignment on the lifted Bool domain
type LiftedBool = Int Source #
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.
lit2lbool :: Lit -> LiftedBool Source #
returns the value of a literal as a LiftedBool
A fixed-precision integer type with at least the range [-2^29 .. 2^29-1].
The exact range for a given implementation can be determined by using
minBound and maxBound from the Bounded class.
Bundled Patterns
| pattern LiftedF :: Int | FALSE on the Lifted Bool domain |
| pattern LiftedT :: Int | TRUE on the Lifted Bool domain |
| pattern LBottom :: Int | UNDEFINED on the Lifted Bool domain |
| pattern Conflict :: Int | CONFLICT on the Lifted Bool domain |
Instances
class VarOrder o where Source #
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.
statistics
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. |