Filtering...

lrat-checker

books/projects/sat/lrat/list-based/lrat-checker
other
(in-package "LRAT")
literalpfunction
(defun literalp
  (x)
  (declare (xargs :guard t))
  (and (integerp x) (not (equal x 0))))
other
(defthm literalp-compound-recognizer
  (equal (literalp x)
    (and (integerp x) (not (equal x 0))))
  :rule-classes :compound-recognizer)
other
(in-theory (disable literalp))
literal-listpfunction
(defun literal-listp
  (x)
  (declare (xargs :guard t))
  (if (atom x)
    (null x)
    (and (literalp (car x))
      (literal-listp (cdr x)))))
negatemacro
(defmacro negate (x) `(- ,LRAT::X))
unique-literalspfunction
(defun unique-literalsp
  (x)
  (declare (xargs :guard (literal-listp x)))
  (if (atom x)
    t
    (and (not (member (car x) (cdr x)))
      (unique-literalsp (cdr x)))))
conflicting-literalspfunction
(defun conflicting-literalsp
  (x)
  (declare (xargs :guard (literal-listp x)))
  (if (atom x)
    nil
    (or (member (negate (car x)) (cdr x))
      (conflicting-literalsp (cdr x)))))
clause-or-assignment-pfunction
(defun clause-or-assignment-p
  (clause)
  (declare (xargs :guard t))
  (and (literal-listp clause)
    (unique-literalsp clause)
    (not (conflicting-literalsp clause))))
duplicate-literalfunction
(defun duplicate-literal
  (x)
  (declare (xargs :guard (literal-listp x)))
  (if (atom x)
    (er hard?
      'duplicate-literal
      "Implementation error: Failed to find a duplicate literal!")
    (if (member (car x) (cdr x))
      (car x)
      (duplicate-literal (cdr x)))))
conflicting-literalsfunction
(defun conflicting-literals
  (x)
  (declare (xargs :guard (literal-listp x)))
  (if (atom x)
    (er hard?
      'duplicate-literal
      "Implementation error: Failed to find conflicting literals!")
    (if (member (negate (car x)) (cdr x))
      (car x)
      (conflicting-literals (cdr x)))))
clause-or-assignment-p-error-msgfunction
(defun clause-or-assignment-p-error-msg
  (clause)
  (declare (xargs :guard t))
  (cond ((not (literal-listp clause)) (msg "the alleged clause ~x0, which is not a list of literals."
        clause))
    ((not (unique-literalsp clause)) (msg "the alleged clause ~x0, whcih contains ~x1 as a duplicate literal."
        clause
        (duplicate-literal clause)))
    ((conflicting-literalsp clause) (let ((lit (conflicting-literals clause)))
        (msg "the alleged clause ~x0, which contains conflicting literals ~
                 ~x1 and ~x2."
          clause
          lit
          (negate lit))))
    (t (er hard?
        'clause-or-assignment-p-error-msg
        "Implementation error: Expected the following to be nil, but ~
                apparently it is not:~|~x0"
        `(clause-or-assignment-p ',LRAT::CLAUSE)))))
other
(defthm clause-or-assignment-p-forward-to-literal-listp
  (implies (clause-or-assignment-p x)
    (literal-listp x))
  :rule-classes :forward-chaining)
other
(defthm literal-listp-forward-to-eqlable-listp
  (implies (literal-listp x)
    (eqlable-listp x))
  :rule-classes :forward-chaining)
other
(defconst *deleted-clause* :deleted)
deleted-clause-pmacro
(defmacro deleted-clause-p
  (val)
  `(eq ,LRAT::VAL *deleted-clause*))
formula-pfunction
(defun formula-p
  (fal)
  (declare (xargs :guard t))
  (if (atom fal)
    (null fal)
    (let ((pair (car fal)))
      (and (consp pair)
        (posp (car pair))
        (let ((val (cdr pair)))
          (or (deleted-clause-p val)
            (clause-or-assignment-p val)))
        (formula-p (cdr fal))))))
formula-p-error-msgfunction
(defun formula-p-error-msg
  (fal)
  (declare (xargs :guard t))
  (if (atom fal)
    (msg "The alleged formula is not a true-list")
    (let ((pair (car fal)))
      (cond ((not (consp pair)) (msg "A formula is represented internally as a list of pairs, ~
                    but the following is not a pair: ~x0"
            pair))
        ((not (posp (car pair))) (msg "A formula is represented internally as a list of pairs.  ~
                    The following pair is invalid, however, because its first ~
                    element is expected to be a positive integer but is ~
                    not:~|~x0"
            pair))
        ((and (not (deleted-clause-p (cdr pair)))
           (not (clause-or-assignment-p (cdr pair)))) (msg "The formula contains ~@0"
            (clause-or-assignment-p-error-msg (cdr pair))))
        (t (formula-p-error-msg (cdr fal)))))))
clause-listpfunction
(defun clause-listp
  (x)
  (declare (xargs :guard t))
  (if (atom x)
    (null x)
    (and (clause-or-assignment-p (car x))
      (clause-listp (cdr x)))))
index-listpmacro
(defmacro index-listp
  (x)
  `(pos-listp ,LRAT::X))
drat-hint-pfunction
(defun drat-hint-p
  (x)
  (declare (xargs :guard t))
  (and (consp x)
    (posp (car x))
    (index-listp (cdr x))))
drat-hint-listpfunction
(defun drat-hint-listp
  (x)
  (declare (xargs :guard t))
  (cond ((atom x) (null x))
    (t (and (drat-hint-p (car x))
        (drat-hint-listp (cdr x))))))
other
(defthm drat-hint-listp-forward-to-alistp
  (implies (drat-hint-listp x)
    (alistp x))
  :rule-classes :forward-chaining)
other
(defrec add-step
  ((index . clause) rup-indices . drat-hints)
  t)
add-step-pfunction
(defun add-step-p
  (x)
  (declare (xargs :guard t))
  (and (weak-add-step-p x)
    (posp (access add-step x :index))
    (clause-or-assignment-p (access add-step x :clause))
    (index-listp (access add-step x :rup-indices))
    (drat-hint-listp (access add-step x :drat-hints))))
proof-entry-pfunction
(defun proof-entry-p
  (entry)
  (declare (xargs :guard t))
  (cond ((and (consp entry) (eq (car entry) t)) (index-listp (cdr entry)))
    (t (add-step-p entry))))
proof-entry-deletion-pmacro
(defmacro proof-entry-deletion-p
  (entry)
  `(eq (car ,LRAT::ENTRY) t))
proof-entry-deletion-indicesmacro
(defmacro proof-entry-deletion-indices
  (entry)
  `(cdr ,LRAT::ENTRY))
proofpfunction
(defun proofp
  (proof)
  (declare (xargs :guard t))
  (if (atom proof)
    (null proof)
    (and (proof-entry-p (car proof))
      (proofp (cdr proof)))))
other
(defthm proofp-forward-to-true-listp
  (implies (proofp x)
    (true-listp x))
  :rule-classes :forward-chaining)
negate-clause-or-assignment-recfunction
(defun negate-clause-or-assignment-rec
  (clause acc)
  (declare (xargs :guard (and (literal-listp clause)
        (literal-listp acc))))
  (if (endp clause)
    acc
    (negate-clause-or-assignment-rec (cdr clause)
      (cons (negate (car clause)) acc))))
other
(defund negate-clause-or-assignment
  (clause)
  (declare (xargs :guard (literal-listp clause)))
  (negate-clause-or-assignment-rec clause nil))
other
(defun-inline undefp
  (x)
  (declare (xargs :guard t))
  (not (booleanp x)))
evaluate-literalfunction
(defun evaluate-literal
  (literal assignment)
  (declare (xargs :guard (and (literalp literal)
        (clause-or-assignment-p assignment))))
  (cond ((member literal assignment) t)
    ((member (negate literal) assignment) nil)
    (t 0)))
evaluate-clausefunction
(defun evaluate-clause
  (clause assignment)
  (declare (xargs :guard (and (clause-or-assignment-p clause)
        (clause-or-assignment-p assignment))))
  (if (atom clause)
    nil
    (let* ((literal (car clause)) (literal-value (evaluate-literal literal assignment)))
      (if (eq literal-value t)
        t
        (let* ((remaining-clause (cdr clause)) (remaining-clause-value (evaluate-clause remaining-clause
                assignment)))
          (cond ((eq remaining-clause-value t) t)
            ((undefp literal-value) 0)
            (t remaining-clause-value)))))))
other
(in-theory (disable clause-or-assignment-p))
other
(defthm clause-or-assignment-p-cdr
  (implies (clause-or-assignment-p clause)
    (clause-or-assignment-p (cdr clause)))
  :hints (("Goal" :in-theory (enable clause-or-assignment-p))))
is-unit-clausefunction
(defun is-unit-clause
  (clause assignment)
  (declare (xargs :guard (and (clause-or-assignment-p clause)
        (clause-or-assignment-p assignment))
      :guard-hints (("Goal" :in-theory (enable clause-or-assignment-p)))))
  (if (atom clause)
    t
    (let ((val (evaluate-literal (car clause) assignment)))
      (cond ((eq val t) nil)
        ((undefp val) (if (null (evaluate-clause (cdr clause) assignment))
            (car clause)
            nil))
        (t (is-unit-clause (cdr clause) assignment))))))
other
(defthm booleanp-evaluate-clause-monotone
  (implies (booleanp (evaluate-clause cl a))
    (booleanp (evaluate-clause cl (cons lit a)))))
unit-propagation-errormacro
(defmacro unit-propagation-error
  (msg formula indices assignment)
  `(prog2$ (er hard?
      'unit-propagation
      "~@0"
      ,LRAT::MSG)
    (unit-propagation ,LRAT::FORMULA
      (cdr ,LRAT::INDICES)
      ,LRAT::ASSIGNMENT)))
other
(defun-notinline my-hons-get
  (key alist)
  (declare (xargs :guard t))
  (hons-get key alist))
unit-propagationfunction
(defun unit-propagation
  (formula indices assignment)
  (declare (xargs :guard (and (formula-p formula)
        (index-listp indices)
        (clause-or-assignment-p assignment))
      :verify-guards nil))
  (cond ((endp indices) assignment)
    (t (let* ((pair (my-hons-get (car indices) formula)) (clause (and pair
              (not (deleted-clause-p (cdr pair)))
              (cdr pair)))
          (unit-literal (and clause
              (is-unit-clause clause assignment))))
        (cond ((not unit-literal) (unit-propagation-error (msg "Unit-propagation has failed for index ~x0 because ~
                      ~@1."
                (car indices)
                (cond ((null pair) "no formula was found for that index")
                  ((null clause) "that clause had been deleted")
                  (t "that clause is not a unit")))
              formula
              indices
              assignment))
          ((eq unit-literal t) t)
          (t (unit-propagation formula
              (cdr indices)
              (add-to-set unit-literal assignment))))))))
other
(defthm literalp-is-unit-clause
  (implies (force (literal-listp clause))
    (or (literalp (is-unit-clause clause assignment))
      (booleanp (is-unit-clause clause assignment))))
  :rule-classes :type-prescription)
other
(defthm clause-or-assignment-p-cdr-hons-assoc-equal
  (let ((clause (cdr (hons-assoc-equal index fal))))
    (implies (and (formula-p fal)
        (not (deleted-clause-p clause)))
      (clause-or-assignment-p clause))))
other
(defthm backchain-to-clause-or-assignment-p
  (implies (clause-or-assignment-p clause)
    (and (literal-listp clause)
      (unique-literalsp clause)
      (not (conflicting-literalsp clause))))
  :hints (("Goal" :in-theory (enable clause-or-assignment-p))))
other
(defthm not-member-complement-unit-clause-assignment
  (implies (and (clause-or-assignment-p clause)
      (clause-or-assignment-p assignment))
    (not (member-equal (negate (is-unit-clause clause assignment))
        assignment)))
  :hints (("Goal" :in-theory (enable clause-or-assignment-p))))
other
(verify-guards unit-propagation
  :hints (("Goal" :in-theory (enable clause-or-assignment-p))))
remove-literalfunction
(defun remove-literal
  (literal clause)
  (declare (xargs :guard (and (literalp literal)
        (clause-or-assignment-p clause))))
  (if (atom clause)
    nil
    (if (equal (car clause) literal)
      (remove-literal literal (cdr clause))
      (cons (car clause)
        (remove-literal literal (cdr clause))))))
other
(defthm literal-listp-union-equal
  (implies (true-listp x)
    (equal (literal-listp (union-equal x y))
      (and (literal-listp x)
        (literal-listp y)))))
other
(defthm member-equal-remove-literal
  (implies (not (member-equal a x))
    (not (member-equal a
        (remove-literal b x)))))
other
(defthm clause-or-assignment-p-remove-literal
  (implies (clause-or-assignment-p y)
    (clause-or-assignment-p (remove-literal x y)))
  :hints (("Goal" :in-theory (enable clause-or-assignment-p))))
other
(defthm literal-listp-remove-literal
  (implies (literal-listp x)
    (literal-listp (remove-literal a x))))
other
(defthm literal-listp-negate-clause-or-assignment-rec
  (implies (and (literal-listp x)
      (literal-listp y))
    (literal-listp (negate-clause-or-assignment-rec x y))))
other
(defthm literal-listp-negate-clause-or-assignment
  (implies (literal-listp x)
    (literal-listp (negate-clause-or-assignment x)))
  :hints (("Goal" :in-theory (enable negate-clause-or-assignment))))
other
(defthm unique-literalsp-remove-literal
  (implies (unique-literalsp x)
    (unique-literalsp (remove-literal a x))))
other
(defthm member-equal-negate-clause-or-assignment-rec-lemma
  (implies (member-equal lit x2)
    (member-equal lit
      (negate-clause-or-assignment-rec x1 x2))))
other
(defthm member-equal-negate-clause-or-assignment-rec
  (implies (literalp lit)
    (iff (member-equal lit
        (negate-clause-or-assignment-rec x1 x2))
      (or (member-equal (negate lit) x1)
        (member-equal lit x2)))))
other
(defthm member-equal-negate-clause-or-assignment
  (implies (literalp x1)
    (iff (member-equal x1
        (negate-clause-or-assignment x2))
      (member-equal (negate x1) x2)))
  :hints (("Goal" :in-theory (enable negate-clause-or-assignment))))
other
(defthm member-equal-union-equal
  (iff (member-equal a
      (union-equal x y))
    (or (member-equal a x)
      (member-equal a y))))
other
(defthm unique-literalsp-union-equal
  (implies (and (unique-literalsp x)
      (unique-literalsp y))
    (unique-literalsp (union-equal x y))))
intersectp-complementaryfunction
(defun intersectp-complementary
  (x y)
  (cond ((endp x) nil)
    (t (or (member-equal (negate (car x)) y)
        (intersectp-complementary (cdr x) y)))))
other
(defthm intersectp-complementary-cons-2
  (implies (literalp a)
    (iff (intersectp-complementary x
        (cons a y))
      (or (member-equal (negate a) x)
        (intersectp-complementary x y))))
  :hints (("Goal" :in-theory (disable (force)))))
other
(defthm negate-negate
  (implies (literalp lit)
    (equal (negate (negate lit)) lit)))
other
(defthm unique-literalsp-negate-clause-or-assignment-rec
  (implies (and (literal-listp x)
      (unique-literalsp x)
      (unique-literalsp y)
      (not (intersectp-complementary x y)))
    (unique-literalsp (negate-clause-or-assignment-rec x y)))
  :hints (("Goal" :induct (negate-clause-or-assignment-rec x y))))
other
(defthm not-intersectp-complementary-nil
  (not (intersectp-complementary x nil)))
other
(defthm unique-literalsp-negate-clause-or-assignment
  (implies (and (literal-listp x)
      (unique-literalsp x))
    (unique-literalsp (negate-clause-or-assignment x)))
  :hints (("Goal" :in-theory (enable negate-clause-or-assignment))))
rat-assignmentfunction
(defun rat-assignment
  (assignment nlit clause)
  (declare (xargs :guard (and (clause-or-assignment-p assignment)
        (literalp nlit)
        (clause-or-assignment-p clause))
      :guard-hints (("Goal" :in-theory (enable clause-or-assignment-p)))))
  (cond ((endp clause) assignment)
    ((or (eql (car clause) nlit)
       (member (negate (car clause)) assignment)) (rat-assignment assignment
        nlit
        (cdr clause)))
    ((member (car clause) assignment) t)
    (t (rat-assignment (cons (negate (car clause)) assignment)
        nlit
        (cdr clause)))))
other
(defthm minus-minus
  (implies (acl2-numberp x)
    (equal (- (- x)) x)))
other
(defthm clause-or-assignment-p-rat-assignment
  (implies (and (clause-or-assignment-p assignment)
      (clause-or-assignment-p clause)
      (not (equal (rat-assignment assignment
            nlit
            clause)
          t)))
    (clause-or-assignment-p (rat-assignment assignment
        nlit
        clause)))
  :hints (("Goal" :in-theory (enable clause-or-assignment-p))))
ratp1function
(defun ratp1
  (alist formula
    nlit
    drat-hints
    assignment)
  (declare (xargs :guard (and (formula-p alist)
        (formula-p formula)
        (literalp nlit)
        (drat-hint-listp drat-hints)
        (clause-or-assignment-p assignment))
      :verify-guards nil
      :guard-hints (("Goal" :in-theory (enable clause-or-assignment-p)))))
  (if (endp alist)
    t
    (let* ((index (caar alist)) (clause (cdar alist)))
      (cond ((deleted-clause-p clause) (ratp1 (cdr alist)
            formula
            nlit
            drat-hints
            assignment))
        ((eql index (caar drat-hints)) (let ((new-assignment (rat-assignment assignment
                 nlit
                 clause)))
            (cond ((eq new-assignment t) (ratp1 (cdr alist)
                  formula
                  nlit
                  (cdr drat-hints)
                  assignment))
              ((eq t
                 (unit-propagation formula
                   (cdar drat-hints)
                   new-assignment)) (ratp1 (cdr alist)
                  formula
                  nlit
                  (cdr drat-hints)
                  assignment))
              (t (list 'unit-propagation-failure
                  index
                  clause
                  nlit)))))
        ((or (not (member nlit clause))
           (deleted-clause-p (cdr (my-hons-get index formula)))) (ratp1 (cdr alist)
            formula
            nlit
            drat-hints
            assignment))
        (t (list 'index-failure
            index
            clause
            nlit))))))
other
(defthm intersectp-equal-cons-2
  (iff (intersectp-equal x (cons a y))
    (or (member-equal a x)
      (intersectp-equal x y))))
other
(defthm not-conflicting-literalsp-negate-clause-or-assignment-rec
  (implies (and (literal-listp x)
      (not (conflicting-literalsp x))
      (not (conflicting-literalsp y))
      (not (intersectp x y)))
    (not (conflicting-literalsp (negate-clause-or-assignment-rec x y))))
  :hints (("Goal" :induct (negate-clause-or-assignment-rec x y))))
other
(defthm not-intersectp-equal-nil
  (not (intersectp-equal x nil)))
other
(defthm not-conflicting-literalsp-negate-clause-or-assignment
  (implies (and (literal-listp x)
      (not (conflicting-literalsp x)))
    (not (conflicting-literalsp (negate-clause-or-assignment x))))
  :hints (("Goal" :in-theory (enable negate-clause-or-assignment))))
other
(defthm clause-or-assignment-p-negate-clause-or-assignment
  (implies (clause-or-assignment-p x)
    (clause-or-assignment-p (negate-clause-or-assignment x)))
  :hints (("Goal" :in-theory (enable clause-or-assignment-p))))
other
(defthm clause-or-assignment-p-union-equal
  (implies (and (clause-or-assignment-p x)
      (clause-or-assignment-p y)
      (not (conflicting-literalsp (union-equal x y))))
    (clause-or-assignment-p (union-equal x y)))
  :hints (("Goal" :in-theory (enable clause-or-assignment-p))))
other
(defthm clause-or-assignment-p-unit-propagation
  (implies (and (formula-p formula)
      (clause-or-assignment-p x)
      (not (equal (unit-propagation formula indices x)
          t)))
    (clause-or-assignment-p (unit-propagation formula indices x)))
  :hints (("Goal" :in-theory (enable clause-or-assignment-p))))
other
(defthm true-listp-lookup-formula-index
  (implies (formula-p x)
    (or (true-listp (cdr (hons-assoc-equal index x)))
      (equal (cdr (hons-assoc-equal index x))
        *deleted-clause*)))
  :rule-classes :type-prescription)
other
(verify-guards ratp1)
ratpfunction
(defun ratp
  (formula literal
    drat-hints
    assignment)
  (declare (xargs :guard (and (formula-p formula)
        (literalp literal)
        (drat-hint-listp drat-hints)
        (clause-or-assignment-p assignment))))
  (ratp1 formula
    formula
    (negate literal)
    drat-hints
    assignment))
remove-deleted-clausesfunction
(defun remove-deleted-clauses
  (fal acc)
  (declare (xargs :guard (alistp fal)))
  (cond ((endp fal) (make-fast-alist acc))
    (t (remove-deleted-clauses (cdr fal)
        (if (deleted-clause-p (cdar fal))
          acc
          (cons (car fal) acc))))))
other
(defthm formula-p-forward-to-alistp
  (implies (formula-p x)
    (alistp x))
  :rule-classes :forward-chaining)
other
(defthm alistp-fast-alist-fork
  (implies (and (alistp x) (alistp y))
    (alistp (fast-alist-fork x y))))
other
(local (defthm cdr-last-of-alistp
    (implies (alistp x)
      (equal (cdr (last x)) nil))))
other
(defund shrink-formula
  (fal)
  (declare (xargs :guard (formula-p fal)))
  (let ((fal2 (fast-alist-clean fal)))
    (fast-alist-free-on-exit fal2
      (remove-deleted-clauses fal2 nil))))
maybe-shrink-formulafunction
(defun maybe-shrink-formula
  (ncls ndel formula factor)
  (declare (xargs :guard (and (integerp ncls)
        (natp ndel)
        (formula-p formula)
        (rationalp factor))))
  (cond ((> ndel (* factor ncls)) (let ((new-formula (shrink-formula formula)))
        (mv ncls 0 new-formula)))
    (t (mv ncls ndel formula))))
other
(defthm formula-p-remove-deleted-clauses
  (implies (and (formula-p fal1)
      (formula-p fal2))
    (formula-p (remove-deleted-clauses fal1 fal2))))
other
(defthm formula-p-fast-alist-fork
  (implies (and (formula-p fal1)
      (formula-p fal2))
    (formula-p (fast-alist-fork fal1 fal2))))
other
(defthm formula-p-shrink-formula
  (implies (formula-p fal)
    (formula-p (shrink-formula fal)))
  :hints (("Goal" :in-theory (enable shrink-formula))))
verify-clausefunction
(defun verify-clause
  (formula add-step ncls ndel)
  (declare (xargs :guard (and (formula-p formula)
        (add-step-p add-step)
        (integerp ncls)
        (natp ndel))
      :guard-hints (("Goal" :in-theory (enable clause-or-assignment-p)))))
  (let* ((proof-clause (access add-step add-step :clause)) (assignment (negate-clause-or-assignment proof-clause))
      (rup-indices (access add-step add-step :rup-indices))
      (assignment (unit-propagation formula
          rup-indices
          assignment)))
    (cond ((eq assignment t) (maybe-shrink-formula ncls
          ndel
          formula
          10))
      ((consp proof-clause) (mv-let (ncls ndel formula)
          (maybe-shrink-formula ncls
            ndel
            formula
            1/3)
          (cond ((eq (ratp formula
                 (car proof-clause)
                 (access add-step add-step :drat-hints)
                 assignment)
               t) (mv ncls ndel formula))
            (t (prog2$ (let* ((current-index (access add-step add-step :index)) (er-type/index/clause/nlit (ratp formula
                        (car proof-clause)
                        (access add-step add-step :drat-hints)
                        assignment))
                    (er-type (nth 0 er-type/index/clause/nlit))
                    (earlier-index (nth 1 er-type/index/clause/nlit))
                    (clause (nth 2 er-type/index/clause/nlit))
                    (nlit (nth 3 er-type/index/clause/nlit)))
                  (declare (ignore clause))
                  (case er-type
                    (unit-propagation-failure (er hard?
                        'verify-clause
                        "Unit propagation failure has cause the RAT check to fail ~
                     when attempting to add proof clause #~x0 for earlier RAT ~
                     clause #~x1."
                        current-index
                        earlier-index))
                    (index-failure (er hard?
                        'verify-clause
                        "The RAT check has failed for proof clause #~x0, because ~
                     literal ~x1 belongs to earlier proof clause #~x2 but no ~
                     hint for that clause is given with proof clause #~x0."
                        current-index
                        nlit
                        earlier-index))
                    (otherwise (er hard?
                        'verify-clause
                        "Unexpected error for RAT check, proof clause #~x0; the ~
                     error is probably a true error but the checker needs to ~
                     be fixed to print a more useful error in this case."
                        current-index))))
                (mv nil nil nil))))))
      (t (prog2$ (er hard?
            'verify-clause
            "The unit-propagation check failed at proof clause #~x0, which ~
              is the empty clause."
            (access add-step add-step :index))
          (mv nil nil nil))))))
delete-clausesfunction
(defun delete-clauses
  (index-list fal)
  (declare (xargs :guard (index-listp index-list)))
  (cond ((endp index-list) fal)
    (t (delete-clauses (cdr index-list)
        (hons-acons (car index-list)
          *deleted-clause*
          fal)))))
add-proof-clausefunction
(defun add-proof-clause
  (index clause formula)
  (declare (xargs :guard (and (posp index)
        (formula-p formula))))
  (hons-acons index clause formula))
verify-proof-recfunction
(defun verify-proof-rec
  (ncls ndel formula proof)
  (declare (xargs :guard (and (integerp ncls)
        (natp ndel)
        (formula-p formula)
        (proofp proof))))
  (cond ((atom proof) t)
    (t (let* ((entry (car proof)) (delete-flg (proof-entry-deletion-p entry)))
        (cond (delete-flg (let* ((indices (proof-entry-deletion-indices entry)) (new-formula (delete-clauses indices formula))
                (len (length indices))
                (ncls (- ncls len))
                (ndel (+ ndel len)))
              (verify-proof-rec ncls
                ndel
                new-formula
                (cdr proof))))
          (t (mv-let (ncls ndel new-formula)
              (verify-clause formula
                entry
                ncls
                ndel)
              (and ncls
                (verify-proof-rec (1+ ncls)
                  ndel
                  (add-proof-clause (access add-step entry :index)
                    (access add-step entry :clause)
                    new-formula)
                  (cdr proof))))))))))
verify-prooffunction
(defun verify-proof
  (formula proof)
  (declare (xargs :guard (and (formula-p formula)
        (proofp proof))))
  (verify-proof-rec (fast-alist-len formula)
    0
    formula
    proof))
proof-contradiction-pfunction
(defun proof-contradiction-p
  (proof)
  (declare (xargs :guard (proofp proof)))
  (if (endp proof)
    nil
    (or (let ((entry (car proof)))
        (and (not (proof-entry-deletion-p entry))
          (null (access add-step entry :clause))))
      (proof-contradiction-p (cdr proof)))))
valid-proofpfunction
(defun valid-proofp
  (formula proof)
  (declare (xargs :guard (formula-p formula)))
  (let ((p (proofp proof)))
    (mv (and p (verify-proof formula proof))
      (and p (proof-contradiction-p proof)))))
refutation-pfunction
(defun refutation-p
  (proof formula)
  (declare (xargs :guard (formula-p formula)))
  (mv-let (v c)
    (valid-proofp formula proof)
    (and v c)))
other
(defun-sk formula-truep
  (formula assignment)
  (forall index
    (let ((pair (hons-get index formula)))
      (implies (and pair
          (not (deleted-clause-p (cdr pair))))
        (equal (evaluate-clause (cdr pair) assignment)
          t)))))
solution-pfunction
(defun solution-p
  (assignment formula)
  (and (clause-or-assignment-p assignment)
    (formula-truep formula assignment)))
other
(defun-sk satisfiable
  (formula)
  (exists assignment
    (solution-p assignment formula)))
other
(in-theory (disable maybe-shrink-formula
    formula-truep
    satisfiable))