File size: 1,600 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 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
|