satisfiable-add-proof-clause

(in-package "LRAT")

(include-book "lrat-checker")

(local (encapsulate nil
    (local (include-book "satisfiable-add-proof-clause-rup"))
    (local (include-book "satisfiable-add-proof-clause-drat"))
    (set-enforce-redundancy t)
    (defthm satisfiable-add-proof-clause-rup
      (mv-let (ncls ndel new-formula)
        (verify-clause formula
          entry
          ncls
          ndel)
        (declare (ignore ncls ndel))
        (implies (and (proof-entry-p entry)
            (formula-p formula)
            (satisfiable formula)
            (equal (unit-propagation formula
                (access add-step entry :rup-indices)
                (negate-clause-or-assignment (access add-step entry :clause)))
              t))
          (satisfiable (add-proof-clause (access add-step entry :index)
              (access add-step entry :clause)
              new-formula))))
      :rule-classes nil)
    (defthm satisfiable-add-proof-clause-drat
      (mv-let (ncls ndel new-formula)
        (verify-clause formula
          entry
          ncls
          ndel)
        (declare (ignore ndel))
        (implies (and ncls
            (proof-entry-p entry)
            (not (proof-entry-deletion-p entry))
            (formula-p formula)
            (satisfiable formula)
            (not (equal (unit-propagation formula
                  (access add-step entry :rup-indices)
                  (negate-clause-or-assignment (access add-step entry :clause)))
                t))
            (consp (access add-step entry :clause)))
          (satisfiable (add-proof-clause (access add-step entry :index)
              (access add-step entry :clause)
              new-formula))))
      :rule-classes nil)))

(defthm satisfiable-add-proof-clause
  (mv-let (ncls ndel new-formula)
    (verify-clause formula
      entry
      ncls
      ndel)
    (declare (ignore ndel))
    (implies (and ncls
        (proof-entry-p entry)
        (not (proof-entry-deletion-p entry))
        (formula-p formula)
        (satisfiable formula))
      (satisfiable (add-proof-clause (access add-step entry :index)
          (access add-step entry :clause)
          new-formula))))
  :hints (("Goal" :use (satisfiable-add-proof-clause-rup satisfiable-add-proof-clause-drat)
     :in-theory (union-theories '(verify-clause)
       (theory 'minimal-theory)))))