File size: 1,770 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 47 48 49 50 51 52 53 54 55 | 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]
|