src/Checker/Kernel.hs

module Checker.Kernel (checkCertificate, CheckResult(..)) where

import Proof.Certificate
import SAT.CNF (Clause, Literal(..), litVar)
import Data.List (nub, sort)

data CheckResult
  = Verified String
  | Rejected String String
  deriving (Eq, Show)

checkCertificate :: ProofCertificate -> CheckResult
checkCertificate cert =
  case proofConclusion cert of
    Valid -> checkValidityProof cert
    Unsatisfiable -> checkUNSATProof cert
    CounterExample ce -> checkCounterExample cert ce

checkValidityProof :: ProofCertificate -> CheckResult
checkValidityProof cert =
  let steps = proofSteps cert
  in if all validStep steps
     then Verified (proofName cert)
     else Rejected (proofName cert) "Invalid proof step"

checkUNSATProof :: ProofCertificate -> CheckResult
checkUNSATProof cert =
  let steps = proofSteps cert
  in if derivesEmpty steps
     then Verified (proofName cert)
     else Rejected (proofName cert) "UNSAT proof does not derive empty clause"

checkCounterExample :: ProofCertificate -> [(Int, Bool)] -> CheckResult
checkCounterExample cert ce =
  if not (null ce)
  then Verified (proofName cert)
  else Rejected (proofName cert) "Empty counterexample"

validStep :: ProofStep -> Bool
validStep (Assumption _) = True
validStep (Learned _ _) = True
validStep (Resolution c1 c2 resolvent pivot) =
  case verifyResolution c1 c2 pivot of
    Just expected -> sort (nub resolvent) == sort (nub expected)
    Nothing -> False

derivesEmpty :: [ProofStep] -> Bool
derivesEmpty steps = any isEmpty (concatMap stepClauses steps)
  where
    isEmpty [] = True
    isEmpty _ = False
    stepClauses (Resolution _ _ r _) = [r]
    stepClauses (Assumption c) = [c]
    stepClauses (Learned c _) = [c]