SAT.Solver.Mios.Types

Basic data types used throughout mios.

Documentation

module SAT.Solver.Mios.Data.Singleton

module SAT.Solver.Mios.Data.Vec

class VectorFamily s t | s -> t where

Public interface as Container

Minimal complete definition

dump

Methods

clear :: s -> IO ()

erases all elements in it

dump :: Show t => String -> s -> IO String

dump the contents

asVec :: s -> IOVector Int

get a raw data

asList :: s -> IO [t]

converts into a list

Instances

VectorFamily Vec Int

provides clear and size

Methods

clear :: Vec -> IO ()

dump :: String -> Vec -> IO String

asVec :: Vec -> IOVector Int

asList :: Vec -> IO [Int]

VectorFamily ClauseVector Clause

Methods

clear :: ClauseVector -> IO ()

dump :: String -> ClauseVector -> IO String

asVec :: ClauseVector -> IOVector Int

asList :: ClauseVector -> IO [Clause]

VectorFamily Clause Lit

supports a restricted set of VectorFamily methods

Methods

clear :: Clause -> IO ()

dump :: String -> Clause -> IO String

asVec :: Clause -> IOVector Int

asList :: Clause -> IO [Lit]

VectorFamily WatcherList Clause

Methods

clear :: WatcherList -> IO ()

dump :: String -> WatcherList -> IO String

asVec :: WatcherList -> IOVector Int

asList :: WatcherList -> IO [Clause]

VectorFamily ClauseExtManager Clause

Methods

clear :: ClauseExtManager -> IO ()

dump :: String -> ClauseExtManager -> IO String

asVec :: ClauseExtManager -> IOVector Int

asList :: ClauseExtManager -> IO [Clause]

VectorFamily Stack Int

Methods

clear :: Stack -> IO ()

dump :: String -> Stack -> IO String

asVec :: Stack -> IOVector Int

asList :: Stack -> IO [Int]

Variable

type Var = Int

represents Var

bottomVar :: Var

Special constant in Var (p.7)

int2var :: Integer -> Integer

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

type Lit = Int

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).

lit2int :: Lit -> Int

converts Lit into Int as int2lit . lit2int == id

>>> lit2int 2
1
>>> lit2int 3
-1
>>> lit2int 4
2
>>> lit2int 5
-2

int2lit :: Int -> Lit

converts Int into Lit as lit2int . int2lit == id

>>> int2lit 1
2
>>> int2lit (-1)
3
>>> int2lit 2
4
>>> int2lit (-2)
5

bottomLit :: Lit

Special constant in Lit (p.7)

newLit :: Var -> Lit

converts Var into Lit

positiveLit :: Lit -> Bool

returns True if the literal is positive

lit2var :: Lit -> Var

converts Lit into Var

>>> lit2var 2
1
>>> lit2var 3
1
>>> lit2var 4
2
>>> lit2var 5
2

var2lit :: Var -> Bool -> Lit

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

negates literal

>>> negateLit 2
3
>>> negateLit 3
2
>>> negateLit 4
5
>>> negateLit 5
4

Assignment

data LiftedBool

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.

Constructors

Bottom

LFalse

LTrue

Instances

Bounded LiftedBool

Methods

minBound :: LiftedBool

maxBound :: LiftedBool

Enum LiftedBool

Methods

succ :: LiftedBool -> LiftedBool

pred :: LiftedBool -> LiftedBool

toEnum :: Int -> LiftedBool

fromEnum :: LiftedBool -> Int

enumFrom :: LiftedBool -> [LiftedBool]

enumFromThen :: LiftedBool -> LiftedBool -> [LiftedBool]

enumFromTo :: LiftedBool -> LiftedBool -> [LiftedBool]

enumFromThenTo :: LiftedBool -> LiftedBool -> LiftedBool -> [LiftedBool]

Eq LiftedBool

Methods

(==) :: LiftedBool -> LiftedBool -> Bool

(/=) :: LiftedBool -> LiftedBool -> Bool

Ord LiftedBool

Methods

compare :: LiftedBool -> LiftedBool -> Ordering

(<) :: LiftedBool -> LiftedBool -> Bool

(<=) :: LiftedBool -> LiftedBool -> Bool

(>) :: LiftedBool -> LiftedBool -> Bool

(>=) :: LiftedBool -> LiftedBool -> Bool

max :: LiftedBool -> LiftedBool -> LiftedBool

min :: LiftedBool -> LiftedBool -> LiftedBool

Read LiftedBool

Methods

readsPrec :: Int -> ReadS LiftedBool

readList :: ReadS [LiftedBool]

readPrec :: ReadPrec LiftedBool

readListPrec :: ReadPrec [LiftedBool]

Show LiftedBool

Methods

showsPrec :: Int -> LiftedBool -> ShowS

show :: LiftedBool -> String

showList :: [LiftedBool] -> ShowS

lbool :: Bool -> LiftedBool

converts Bool into LBool

lFalse :: Int

A contant representing False

lTrue :: Int

A constant representing True

lBottom :: Int

A constant for "undefined"

class VarOrder o where

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.

Methods

newVarOrder :: (VectorFamily v1 Bool, VectorFamily v2 Double) => v1 -> v2 -> IO o

constructor

newVar :: o -> IO Var

Called when a new variable is created.

update :: o -> Var -> IO ()

Called when variable has increased in activity.

updateAll :: o -> IO ()

Called when all variables have been assigned new activities.

undo :: o -> Var -> IO ()

Called when variable is unbound (may be selected again).

select :: o -> IO Var

Called to select a new, unassigned variable.

Instances

VarOrder Solver

Interfate to select a decision var based on variable activity.

Methods

newVarOrder :: (VectorFamily v1 Bool, VectorFamily v2 Double) => v1 -> v2 -> IO Solver

newVar :: Solver -> IO Var

update :: Solver -> Var -> IO ()

updateAll :: Solver -> IO ()

undo :: Solver -> Var -> IO ()

select :: Solver -> IO Var

CNF

data CNFDescription

misc information on CNF

Constructors

CNFDescription

Fields

• _numberOfVariables :: !Int

  number of variables

• _numberOfClauses :: !Int

  number of clauses

• _pathname :: Maybe FilePath

  given filename

Instances

Eq CNFDescription

Methods

(==) :: CNFDescription -> CNFDescription -> Bool

(/=) :: CNFDescription -> CNFDescription -> Bool

Ord CNFDescription

Methods

compare :: CNFDescription -> CNFDescription -> Ordering

(<) :: CNFDescription -> CNFDescription -> Bool

(<=) :: CNFDescription -> CNFDescription -> Bool

(>) :: CNFDescription -> CNFDescription -> Bool

(>=) :: CNFDescription -> CNFDescription -> Bool

max :: CNFDescription -> CNFDescription -> CNFDescription

min :: CNFDescription -> CNFDescription -> CNFDescription

Show CNFDescription

Methods

showsPrec :: Int -> CNFDescription -> ShowS

show :: CNFDescription -> String

showList :: [CNFDescription] -> ShowS