Safe Haskell	Safe
Language	Haskell2010

SAT.Mios.Util.BoolExp

Contents

Class & Type
Expression contructors
List Operation
Convert function

Description

Boolean Expression module to build CNF from arbitrary expressions Tseitin translation: http://en.wikipedia.org/wiki/Tseitin_transformation

Synopsis

class BoolComponent a where
data BoolForm = Cnf (Int, Int) [[Int]]
(-|-) :: (BoolComponent a, BoolComponent b) => a -> b -> BoolForm
(-&-) :: (BoolComponent a, BoolComponent b) => a -> b -> BoolForm
(-=-) :: (BoolComponent a, BoolComponent b) => a -> b -> BoolForm
(-!-) :: (BoolComponent a, BoolComponent b) => a -> b -> BoolForm
(->-) :: (BoolComponent a, BoolComponent b) => a -> b -> BoolForm
neg :: BoolComponent a => a -> BoolForm
disjunctionOf :: [BoolForm] -> BoolForm
(-|||-) :: [BoolForm] -> BoolForm
conjunctionOf :: [BoolForm] -> BoolForm
(-&&&-) :: [BoolForm] -> BoolForm
asList :: BoolForm -> [[Int]]
asList_ :: BoolForm -> [[Int]]
asLatex :: BoolForm -> String
asLatex_ :: BoolForm -> String
numberOfVariables :: BoolForm -> Int
numberOfClauses :: BoolForm -> Int
tseitinBase :: Int

Class & Type

class BoolComponent a where Source #

class of objects that can be interpeted as a bool expression

Minimal complete definition

toBF

Methods

toBF :: a -> BoolForm Source #

Instances

BoolComponent Bool Source #
Instance details Defined in SAT.Mios.Util.BoolExp Methods toBF :: Bool -> BoolForm Source #
BoolComponent Int Source #
Instance details Defined in SAT.Mios.Util.BoolExp Methods toBF :: Int -> BoolForm Source #
BoolComponent BoolForm Source #
Instance details Defined in SAT.Mios.Util.BoolExp Methods toBF :: BoolForm -> BoolForm Source #
BoolComponent [Char] Source #
Instance details Defined in SAT.Mios.Util.BoolExp Methods toBF :: [Char] -> BoolForm Source #

data BoolForm Source #

CNF expression

Constructors

Cnf (Int, Int) [[Int]]

Instances

Eq BoolForm Source #
Instance details Defined in SAT.Mios.Util.BoolExp Methods (==) :: BoolForm -> BoolForm -> Bool # (/=) :: BoolForm -> BoolForm -> Bool #
Ord BoolForm Source #
Instance details Defined in SAT.Mios.Util.BoolExp Methods compare :: BoolForm -> BoolForm -> Ordering # (<) :: BoolForm -> BoolForm -> Bool # (<=) :: BoolForm -> BoolForm -> Bool # (>) :: BoolForm -> BoolForm -> Bool # (>=) :: BoolForm -> BoolForm -> Bool # max :: BoolForm -> BoolForm -> BoolForm # min :: BoolForm -> BoolForm -> BoolForm #
Show BoolForm Source #
Instance details Defined in SAT.Mios.Util.BoolExp Methods showsPrec :: Int -> BoolForm -> ShowS # show :: BoolForm -> String # showList :: [BoolForm] -> ShowS #
BoolComponent BoolForm Source #
Instance details Defined in SAT.Mios.Util.BoolExp Methods toBF :: BoolForm -> BoolForm Source #

Expression contructors

(-|-) :: (BoolComponent a, BoolComponent b) => a -> b -> BoolForm Source #

disjunction constructor

>>> asList $ "3" -|- "4"
[[3,4,-5],[-3,5],[-4,5]]

>>> asList (("3" -|- "4") -|- "-1")
[[3,4,-5],[-3,5],[-4,5],[5,-1,-6],[-5,6],[1,6]]

(-&-) :: (BoolComponent a, BoolComponent b) => a -> b -> BoolForm Source #

conjunction constructor

>>> asList $ "3" -&- "-2"
[[-3,2,4],[3,-4],[-2,-4]]

>>> asList $ "3" -|- ("1" -&- "2")
[[-1,-2,4],[1,-4],[2,-4],[3,4,-5],[-3,5],[-4,5]]

(-=-) :: (BoolComponent a, BoolComponent b) => a -> b -> BoolForm Source #

equal on BoolForm

(-!-) :: (BoolComponent a, BoolComponent b) => a -> b -> BoolForm Source #

negation on BoolForm

(->-) :: (BoolComponent a, BoolComponent b) => a -> b -> BoolForm Source #

implication as a short cut

>>> asList ("1" ->- "2")
[[-1,-3],[1,3],[3,2,-4],[-3,4],[-2,4]]

neg :: BoolComponent a => a -> BoolForm Source #

negate a form

>>> asList $ neg ("1" -|- "2")
[[1,2,-3],[-1,3],[-2,3],[-3,-4],[3,4]]

List Operation

disjunctionOf :: [BoolForm] -> BoolForm Source #

merge [BoolForm] by '(-|-)'

(-|||-) :: [BoolForm] -> BoolForm Source #

an alias of disjunctionOf

conjunctionOf :: [BoolForm] -> BoolForm Source #

merge [BoolForm] by '(-&-)'

(-&&&-) :: [BoolForm] -> BoolForm Source #

an alias of conjunctionOf

Convert function

asList :: BoolForm -> [[Int]] Source #

converts a *satisfied* BoolForm to "[[Int]]"

asList_ :: BoolForm -> [[Int]] Source #

converts a BoolForm to "[[Int]]"

asLatex :: BoolForm -> String Source #

make latex string from CNF, using asList

asLatex_ :: BoolForm -> String Source #

make latex string from CNF, using asList_

>>> asLatex $ "3" -|- "4"
"\\begin{displaymath}\n( x_{3} \\vee x_{4} )\n\\end{displaymath}\n"

numberOfVariables :: BoolForm -> Int Source #

returns the number of variables in the BoolForm

numberOfClauses :: BoolForm -> Int Source #

returns the number of clauses in the BoolForm

tseitinBase :: Int Source #

the start index for the generated variables by Tseitin encoding