src/Proof/Produce.hs

module Proof.Produce (proveValidity, proveUNSAT) where

import IR.Boolean
import SAT.CNF
import SAT.DPLL (dpll)
import qualified SAT.DPLL as DPLL
import Proof.Certificate
import qualified Data.Map.Strict as Map

proveValidity :: String -> BExpr -> ProofCertificate
proveValidity name expr =
  let negated = BNand expr expr
      cnf = tseitin negated
  in case dpll cnf of
       DPLL.UNSAT ->
         emptyProof name Valid
       DPLL.SAT counterexample ->
         let ce = Map.toList counterexample
         in (emptyProof name (CounterExample ce))
           { proofSteps = [Assumption [Neg 0]] }

proveUNSAT :: String -> BExpr -> ProofCertificate
proveUNSAT name expr =
  let cnf = tseitin expr
  in case dpll cnf of
       DPLL.UNSAT ->
         emptyProof name Unsatisfiable
       DPLL.SAT _ ->
         emptyProof name Valid