src/SAT/CNF.hs

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)