satisfiable-add-proof-clause-base

(in-package "LRAT")

(include-book "lrat-checker")

(include-book "truth-monotone")

(include-book "unit-propagation-implies-unsat")

(include-book "unit-propagation-monotone")

(include-book "unit-propagation-correct")

(defthm truth-monotone
  (implies (and (subsetp-equal a1 a2)
      (equal (formula-truep formula a1) t))
    (equal (formula-truep formula a2) t)))

(defthm unit-propagation-implies-unsat
  (implies (and (clause-or-assignment-p assignment)
      (formula-p formula)
      (formula-truep formula assignment)
      (index-listp indices))
    (not (equal (unit-propagation formula
          indices
          assignment)
        t))))

(defthm unit-propagation-monotone
  (implies (and (equal (unit-propagation formula
          indices
          a1)
        t)
      (clause-or-assignment-p a1)
      (clause-or-assignment-p a2)
      (subsetp-equal a1 a2)
      (formula-p formula))
    (equal (unit-propagation formula
        indices
        a2)
      t)))

(defthm unit-propagation-correct
  (implies (and (formula-p formula)
      (clause-or-assignment-p clause)
      (clause-or-assignment-p assignment)
      (formula-truep formula assignment)
      (equal (unit-propagation formula
          indices
          (negate-clause-or-assignment clause))
        t))
    (equal (evaluate-clause clause assignment)
      t)))

(defund flip-literal
  (lit assignment)
  (cons lit
    (remove-literal lit
      (remove-literal (negate lit)
        assignment))))

(defthm member-remove-literal
  (iff (member lit1
      (remove-literal lit2 x))
    (if (equal lit1 lit2)
      nil
      (member lit1 x))))

(defthm clause-or-assignment-p-flip-literal
  (implies (and (clause-or-assignment-p assignment)
      (literalp lit))
    (clause-or-assignment-p (flip-literal lit assignment)))
  :hints (("Goal" :in-theory (enable flip-literal))))

(defthm member-flip-literal
  (member lit
    (flip-literal lit assignment))
  :hints (("Goal" :in-theory (enable flip-literal))))