ToySolver.SAT.Encoder.Tseitin

The Encoder type

data Encoder m

newEncoder

newEncoderWithPBLin

setUsePB

Polarity

data Polarity

negatePolarity

polarityPos

polarityNeg

polarityBoth

polarityNone

Boolean formula type

type Formula

evalFormula

Encoding of boolean formulas

addFormula

encodeFormula

encodeFormulaWithPolarity

encodeConj

encodeConjWithPolarity

encodeDisj

encodeDisjWithPolarity

encodeITE

encodeITEWithPolarity

encodeXOR

encodeXORWithPolarity

encodeFASum

encodeFASumWithPolarity

encodeFACarry

encodeFACarryWithPolarity

Retrieving definitions

getDefinitions