Safe Haskell | Safe |
---|---|
Language | Haskell2010 |
Boolean Expression module to build CNF from arbitrary expressions Tseitin translation: http://en.wikipedia.org/wiki/Tseitin_transformation
- 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
CNF expression
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 '(-|-)'
conjunctionOf :: [BoolForm] -> BoolForm Source #
merge [BoolForm] by '(-&-)'
Convert function
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"
tseitinBase :: Int Source #
the start index for the generated variables by Tseitin encoding