src/Proof/Certificate.hs

module Proof.Certificate where

import SAT.CNF (Clause, Literal(..))
import qualified Data.ByteString as BS
import Data.Word (Word8)

data ProofStep
  = Resolution Clause Clause Clause Int
  | Assumption Clause
  | Learned Clause [Int]
  deriving (Eq, Show)

data ProofCertificate = ProofCertificate
  { proofName :: String
  , proofSteps :: [ProofStep]
  , proofConclusion :: ProofConclusion
  , proofHash :: [Word8]
  } deriving (Show)

data ProofConclusion
  = Valid
  | Unsatisfiable
  | CounterExample [(Int, Bool)]
  deriving (Eq, Show)

emptyProof :: String -> ProofConclusion -> ProofCertificate
emptyProof name conclusion = ProofCertificate
  { proofName = name
  , proofSteps = []
  , proofConclusion = conclusion
  , proofHash = sha256Stub name
  }

addStep :: ProofCertificate -> ProofStep -> ProofCertificate
addStep cert step = cert { proofSteps = proofSteps cert ++ [step] }

sha256Stub :: String -> [Word8]
sha256Stub s = take 32 $ cycle $ map (fromIntegral . fromEnum) s

verifyResolution :: Clause -> Clause -> Int -> Maybe Clause
verifyResolution c1 c2 pivot =
  let withoutPivot1 = filter (\l -> litVar' l /= pivot) c1
      withoutPivot2 = filter (\l -> litVar' l /= pivot) c2
      hasPosInC1 = Pos pivot `elem` c1
      hasNegInC2 = Neg pivot `elem` c2
  in if hasPosInC1 && hasNegInC2
     then Just (withoutPivot1 ++ withoutPivot2)
     else if Neg pivot `elem` c1 && Pos pivot `elem` c2
     then Just (withoutPivot1 ++ withoutPivot2)
     else Nothing

litVar' :: Literal -> Int
litVar' (Pos v) = v
litVar' (Neg v) = v