File size: 1,219 Bytes
56de343 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 | module SAT.CNF (Literal(..), Clause, CNF(..), tseitin) where
import IR.Boolean
import qualified Data.Map.Strict as Map
data Literal = Pos Int | Neg Int
deriving (Eq, Ord, Show)
type Clause = [Literal]
data CNF = CNF
{ cnfClauses :: [Clause]
, cnfNumVars :: Int
} deriving (Show)
litVar :: Literal -> Int
litVar (Pos v) = v
litVar (Neg v) = v
negate :: Literal -> Literal
negate (Pos v) = Neg v
negate (Neg v) = Pos v
type FreshVar = Int
tseitin :: BExpr -> CNF
tseitin expr = CNF clauses nextVar
where
(rootVar, nextVar, clauses) = runTseitin expr 1
runTseitin :: BExpr -> FreshVar -> (Int, FreshVar, [Clause])
runTseitin BTrue fresh = (fresh, fresh + 1, [[Pos fresh]])
runTseitin BFalse fresh = (fresh, fresh + 1, [[Neg fresh]])
runTseitin (BVar v) _ = (v, v + 1, [])
runTseitin (BNand a b) fresh =
let (aVar, fresh1, aClauses) = runTseitin a fresh
(bVar, fresh2, bClauses) = runTseitin b fresh1
outVar = fresh2
fresh3 = fresh2 + 1
nandClauses =
[ [Pos outVar, Pos aVar]
, [Pos outVar, Pos bVar]
, [Neg outVar, Neg aVar, Neg bVar]
]
in (outVar, fresh3, aClauses ++ bClauses ++ nandClauses)
|