Safe Haskell | Trustworthy |
---|---|
Language | Haskell2010 |
Basic data types used throughout mios.
- module SAT.Mios.Data.Singleton
- module SAT.Mios.Data.Vec
- class VectorFamily s t | s -> t where
- type Var = Int
- bottomVar :: Var
- int2var :: Integer -> Integer
- type Lit = Int
- lit2int :: Lit -> Int
- int2lit :: Int -> Lit
- bottomLit :: Lit
- newLit :: Var -> Lit
- positiveLit :: Lit -> Bool
- lit2var :: Lit -> Var
- var2lit :: Var -> Bool -> Lit
- negateLit :: Lit -> Lit
- data LiftedBool
- lbool :: Bool -> LiftedBool
- lFalse :: Int
- lTrue :: Int
- lBottom :: Int
- class VarOrder o where
- data CNFDescription = CNFDescription {}
Documentation
module SAT.Mios.Data.Singleton
module SAT.Mios.Data.Vec
class VectorFamily s t | s -> t where Source #
Public interface as Container
erases all elements in it
dump :: Show t => String -> s -> IO String Source #
dump the contents
asVec :: s -> IOVector Int Source #
get a raw data
asList :: s -> IO [t] Source #
converts into a list
VectorFamily Vec Int Source # | provides |
VectorFamily Stack Int Source # | |
VectorFamily ClauseVector Clause Source # | |
VectorFamily Clause Lit Source # | supports a restricted set of |
VectorFamily WatcherList Clause Source # | |
VectorFamily ClauseExtManager Clause Source # | |
Variable
int2var :: Integer -> Integer Source #
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
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 True
2>>>
var2lit 1 False
3>>>
var2lit 2 True
4>>>
var2lit 2 False
5
negateLit :: Lit -> Lit Source #
negates literal
>>>
negateLit 2
3>>>
negateLit 3
2>>>
negateLit 4
5>>>
negateLit 5
4
Assignment
data LiftedBool 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.
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.
newVarOrder :: (VectorFamily v1 Bool, VectorFamily v2 Double) => v1 -> v2 -> IO o Source #
constructor
newVar :: o -> IO Var Source #
Called when a new variable is created.
update :: o -> Var -> IO () Source #
Called when variable has increased in activity.
updateAll :: o -> IO () Source #
Called when all variables have been assigned new activities.
undo :: o -> Var -> IO () Source #
Called when variable is unbound (may be selected again).
select :: o -> IO Var Source #
Called to select a new, unassigned variable.
CNF
data CNFDescription Source #
misc information on CNF
CNFDescription | |
|