other
(in-package "LRAT")
other
(local (include-book "../list-based/lrat-checker"))
other
(local (include-book "../stobj-based/lrat-checker"))
other
(local (include-book "lrat-checker-support"))
other
(set-enforce-redundancy t)
literalpfunction
(defun literalp (x) (declare (xargs :guard t)) (and (integerp x) (not (equal x 0))))
literal-listpfunction
(defun literal-listp (x) (declare (xargs :guard t)) (if (atom x) (null x) (and (literalp (car x)) (literal-listp (cdr 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))))
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))))))
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))))))
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)))))
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)))))))
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))))))
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
(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))))))
intersectp-complementaryfunction
(defun intersectp-complementary (x y) (cond ((endp x) nil) (t (or (member-equal (negate (car x)) y) (intersectp-complementary (cdr x) y)))))
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)))))
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
(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
(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))))
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
(include-book "std/util/bstar" :dir :system)
other
(defstobj a$ (a$ptr :type (integer 0 *) :initially 0) (a$stk :type (array t (1)) :resizable t) (a$arr :type (array t (1)) :initially 0 :resizable t) :renaming ((a$arrp a$arrp-weak) (a$p a$p-weak)) :non-memoizable t :inline t)
clausepmacro
(defmacro clausep (x) `(clause-or-assignment-p ,LRAT::X))
varp$function
(defun varp$ (var a$) (declare (xargs :stobjs a$ :guard t)) (and (varp var) (< (abs var) (a$arr-length a$))))
literalp$function
(defun literalp$ (lit a$) (declare (xargs :stobjs a$ :guard t)) (and (literalp lit) (< (abs lit) (a$arr-length a$))))
literal-listp$function
(defun literal-listp$ (x a$) (declare (xargs :stobjs a$ :guard t)) (if (atom x) (null x) (and (literalp$ (car x) a$) (literal-listp$ (cdr x) a$))))
clausep$function
(defun clausep$ (x a$) (declare (xargs :stobjs a$ :guard t)) (and (literal-listp$ x a$) (unique-literalsp x) (not (conflicting-literalsp x))))
find-var-on-stkfunction
(defun find-var-on-stk (var i a$) (declare (xargs :stobjs a$ :guard (and (varp var) (natp i) (<= i (a$ptr a$)) (<= (a$ptr a$) (a$stk-length a$))))) (cond ((zp i) nil) (t (let* ((i (1- i)) (var2 (a$stki i a$))) (cond ((eql var var2) t) (t (find-var-on-stk var i a$)))))))
good-stk-pfunction
(defun good-stk-p (i a$) (declare (xargs :stobjs a$ :guard (and (natp i) (<= i (a$ptr a$)) (<= (a$ptr a$) (a$stk-length a$))))) (cond ((zp i) t) (t (let* ((i (1- i)) (var (a$stki i a$))) (and (varp$ var a$) (not (find-var-on-stk var i a$)) (good-stk-p i a$))))))
arr-matches-stkfunction
(defun arr-matches-stk (i a$) (declare (xargs :stobjs a$ :guard (and (natp i) (<= i (a$arr-length a$)) (<= (a$ptr a$) (a$stk-length a$))))) (cond ((or (zp i) (= i 1)) t) (t (let ((var (1- i))) (and (eq (booleanp (a$arri var a$)) (find-var-on-stk var (a$ptr a$) a$)) (arr-matches-stk var a$))))))
a$arrp-recfunction
(defun a$arrp-rec (i a$) (declare (xargs :stobjs a$ :guard (and (natp i) (<= i (a$arr-length a$))))) (cond ((zp i) t) (t (let* ((i (1- i)) (v (a$arri i a$))) (and (or (booleanp v) (eql v 0)) (a$arrp-rec i a$))))))
a$arrpfunction
(defun a$arrp (a$) (declare (xargs :stobjs a$)) (a$arrp-rec (a$arr-length a$) a$))
a$pfunction
(defun a$p (a$) (declare (xargs :stobjs a$)) (and (a$p-weak a$) (<= (a$ptr a$) (a$stk-length a$)) (equal (a$arr-length a$) (1+ (a$stk-length a$))) (good-stk-p (a$ptr a$) a$) (a$arrp a$) (arr-matches-stk (a$arr-length a$) a$)))
other
(defun-inline negate-value (val) (declare (xargs :guard t)) (if (booleanp val) (not val) val))
other
(defun-inline evaluate-literal$ (lit a$) (declare (xargs :stobjs a$ :guard (literalp$ lit a$))) (if (< 0 lit) (a$arri lit a$) (negate-value (a$arri (negate lit) a$))))
push-literalfunction
(defun push-literal (lit a$) (declare (xargs :stobjs a$ :guard (and (a$p a$) (literalp$ lit a$)) :verify-guards nil)) (let* ((var (abs lit)) (old (a$arri var a$)) (lit-posp (eql var lit))) (cond ((eq old t) (mv (not lit-posp) a$)) ((eq old nil) (mv lit-posp a$)) (t (let* ((ptr (a$ptr a$)) (a$ (update-a$stki ptr var a$)) (a$ (update-a$ptr (1+ ptr) a$)) (a$ (update-a$arri var lit-posp a$))) (mv nil a$))))))
other
(verify-guards push-literal)
negate-clausefunction
(defun negate-clause (clause a$) (declare (xargs :stobjs a$ :guard (and (a$p a$) (clausep$ clause a$)) :guard-hints (("Goal" :in-theory (enable clausep$))))) (cond ((atom clause) (mv nil a$)) (t (mv-let (flg a$) (push-literal (negate (car clause)) a$) (cond (flg (mv flg a$)) (t (negate-clause (cdr clause) a$)))))))
evaluate-clause$function
(defun evaluate-clause$ (clause a$) (declare (xargs :stobjs a$ :guard (and (a$p a$) (clausep$ clause a$)) :verify-guards nil)) (if (atom clause) nil (let* ((literal (car clause)) (literal-value (evaluate-literal$ literal a$))) (if (eq literal-value t) t (let* ((remaining-clause (cdr clause)) (remaining-clause-value (evaluate-clause$ remaining-clause a$))) (cond ((eq remaining-clause-value t) t) ((undefp literal-value) 0) (t remaining-clause-value)))))))
other
(verify-guards evaluate-clause$)
is-unit-clause$function
(defun is-unit-clause$ (clause a$) (declare (xargs :stobjs a$ :guard (and (a$p a$) (clausep$ clause a$)))) (if (atom clause) t (let ((val (evaluate-literal$ (car clause) a$))) (cond ((eq val t) nil) ((undefp val) (if (null (evaluate-clause$ (cdr clause) a$)) (car clause) nil)) (t (is-unit-clause$ (cdr clause) a$))))))
unit-propagation$-error$macro
(defmacro unit-propagation$-error$ (msg formula indices a$) `(prog2$ (er hard? 'unit-propagation "~@0" ,LRAT::MSG) (unit-propagation$ ,LRAT::FORMULA (cdr ,LRAT::INDICES) ,LRAT::A$)))
formula-p$function
(defun formula-p$ (formula a$) (declare (xargs :stobjs a$ :guard (a$p a$))) (if (atom formula) (null formula) (let ((pair (car formula))) (and (consp pair) (posp (car pair)) (let ((val (cdr pair))) (or (deleted-clause-p val) (clausep$ val a$))) (formula-p$ (cdr formula) a$)))))
unit-propagation$function
(defun unit-propagation$ (formula indices a$) (declare (xargs :stobjs a$ :guard (and (a$p a$) (formula-p$ formula a$) (index-listp indices)) :verify-guards nil)) (cond ((endp indices) (mv nil a$)) (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 a$)))) (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 a$)) ((eq unit-literal t) (mv t a$)) (t (mv-let (flg a$) (push-literal unit-literal a$) (assert$ (null flg) (unit-propagation$ formula (cdr indices) a$)))))))))
other
(verify-guards unit-propagation$)
rat-assignment$function
(defun rat-assignment$ (a$ nlit clause) (declare (xargs :stobjs a$ :guard (and (a$p a$) (literalp$ nlit a$) (clausep$ clause a$)))) (cond ((endp clause) (mv nil a$)) ((eql (car clause) nlit) (rat-assignment$ a$ nlit (cdr clause))) (t (mv-let (flg a$) (push-literal (negate (car clause)) a$) (cond (flg (mv flg a$)) (t (rat-assignment$ a$ nlit (cdr clause))))))))
pop-literalsfunction
(defun pop-literals (old-ptr a$) (declare (xargs :stobjs a$ :guard (and (a$p a$) (natp old-ptr) (<= old-ptr (a$ptr a$))) :verify-guards nil :measure (nfix (a$ptr a$)) :hints (("Goal" :in-theory (enable a$p))))) (cond ((and (mbt (and (a$p a$) (natp old-ptr) (<= old-ptr (a$ptr a$)))) (not (= old-ptr (a$ptr a$)))) (let* ((index (1- (a$ptr a$))) (var (a$stki index a$)) (a$ (update-a$ptr index a$)) (a$ (update-a$arri var 0 a$))) (pop-literals old-ptr a$))) (t a$)))
other
(verify-guards pop-literals)
ratp1$function
(defun ratp1$ (alist formula nlit drat-hints a$) (declare (xargs :stobjs a$ :guard (and (a$p a$) (formula-p$ alist a$) (formula-p$ formula a$) (literalp$ nlit a$) (drat-hint-listp drat-hints)) :verify-guards nil)) (if (endp alist) (mv t a$) (let* ((index (caar alist)) (clause (cdar alist))) (cond ((deleted-clause-p clause) (ratp1$ (cdr alist) formula nlit drat-hints a$)) ((eql index (caar drat-hints)) (b* ((old-ptr (a$ptr a$)) ((mv flg a$) (rat-assignment$ a$ nlit clause))) (cond (flg (let ((a$ (pop-literals old-ptr a$))) (ratp1$ (cdr alist) formula nlit (cdr drat-hints) a$))) (t (mv-let (flg a$) (unit-propagation$ formula (cdar drat-hints) a$) (let ((a$ (pop-literals old-ptr a$))) (cond (flg (ratp1$ (cdr alist) formula nlit (cdr drat-hints) a$)) (t (mv (list 'unit-propagation-failure index clause nlit) a$))))))))) ((or (not (member nlit clause)) (deleted-clause-p (cdr (my-hons-get index formula)))) (ratp1$ (cdr alist) formula nlit drat-hints a$)) (t (mv (list 'index-failure index clause nlit) a$))))))
other
(verify-guards ratp1$ :hints (("Goal" :in-theory (enable formula-p$))))
ratp$function
(defun ratp$ (formula literal drat-hints a$) (declare (xargs :stobjs a$ :guard (and (a$p a$) (formula-p$ formula a$) (literalp$ literal a$) (drat-hint-listp drat-hints)))) (ratp1$ formula formula (negate literal) drat-hints a$))
verify-clause$function
(defun verify-clause$ (formula add-step ncls ndel a$) (declare (xargs :stobjs a$ :guard (and (a$p a$) (= (a$ptr a$) 0) (formula-p$ formula a$) (add-step-p add-step) (clausep$ (access add-step add-step :clause) a$) (integerp ncls) (natp ndel)) :verify-guards nil)) (b* ((proof-clause (access add-step add-step :clause)) (old-ptr (a$ptr a$)) ((mv flg0 a$) (negate-clause proof-clause a$)) ((when flg0) (prog2$ (er hard? 'verify-clause$ "Implementation error?! Note that a$ptr is ~x0." (a$ptr a$)) (let ((a$ (pop-literals old-ptr a$))) (mv nil nil nil a$)))) (rup-indices (access add-step add-step :rup-indices)) ((mv flg a$) (unit-propagation$ formula rup-indices a$))) (cond ((eq flg t) (b* ((a$ (pop-literals old-ptr a$)) ((mv ncls nlit new-formula) (maybe-shrink-formula ncls ndel formula 10))) (mv ncls nlit new-formula a$))) ((consp proof-clause) (b* (((mv ncls ndel formula) (maybe-shrink-formula ncls ndel formula 1/3)) ((mv flg a$) (ratp$ formula (car proof-clause) (access add-step add-step :drat-hints) a$)) (a$ (pop-literals old-ptr a$))) (cond ((eq flg t) (mv ncls ndel formula a$)) (t (prog2$ (b* ((current-index (access add-step add-step :index)) ((list er-type earlier-index & nlit) flg)) (case er-type (unit-propagation-failure (er hard? 'verify-clause$ "Unit propagation failure has caused 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 a$)))))) (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)) (b* ((a$ (pop-literals old-ptr a$))) (mv nil nil nil a$)))))))
other
(verify-guards verify-clause$)
proofp$function
(defun proofp$ (proof a$) (declare (xargs :stobjs a$ :guard (a$p a$))) (if (atom proof) (null proof) (and (proof-entry-p (car proof)) (or (proof-entry-deletion-p (car proof)) (clausep$ (access add-step (car proof) :clause) a$)) (proofp$ (cdr proof) a$))))
verify-proof$-recfunction
(defun verify-proof$-rec (ncls ndel formula proof a$) (declare (xargs :stobjs a$ :guard (and (a$p a$) (= (a$ptr a$) 0) (integerp ncls) (natp ndel) (formula-p$ formula a$) (proofp$ proof a$)) :verify-guards nil)) (cond ((atom proof) (mv t a$)) (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) a$))) (t (mv-let (ncls ndel new-formula a$) (verify-clause$ formula entry ncls ndel a$) (cond (ncls (verify-proof$-rec (1+ ncls) ndel (add-proof-clause (access add-step entry :index) (access add-step entry :clause) new-formula) (cdr proof) a$)) (t (mv nil a$))))))))))
other
(defun-nx lst= (ptr lst1 lst2) (if (zp ptr) t (let ((ptr (1- ptr))) (and (equal (nth ptr lst1) (nth ptr lst2)) (lst= ptr lst1 lst2)))))
other
(defun-nx a$= (a1 a2) (or (equal a1 a2) (and (a$p a1) (a$p a2) (equal (nth *a$ptr* a1) (nth *a$ptr* a2)) (equal (nth *a$arri* a1) (nth *a$arri* a2)) (lst= (nth *a$ptr* a1) (nth *a$stki* a1) (nth *a$stki* a2)))))
other
(verify-guards verify-proof$-rec)
verify-proof$function
(defun verify-proof$ (formula proof a$) (declare (xargs :stobjs a$ :guard (and (a$p a$) (= (a$ptr a$) 0) (formula-p$ formula a$) (proofp$ proof a$)))) (verify-proof$-rec (fast-alist-len formula) 0 formula proof a$))
other
(defund initialize-a$ (max-var a$) (declare (xargs :stobjs a$ :guard (varp max-var))) (let* ((a$ (update-a$ptr 0 a$)) (a$ (resize-a$stk 0 a$)) (a$ (resize-a$stk max-var a$)) (a$ (resize-a$arr 0 a$)) (a$ (resize-a$arr (1+ max-var) a$))) a$))
clause-max-varfunction
(defun clause-max-var (clause acc) (declare (xargs :guard (and (literal-listp clause) (natp acc)))) (cond ((endp clause) acc) (t (clause-max-var (cdr clause) (max (abs (car clause)) acc)))))
formula-max-varfunction
(defun formula-max-var (fal acc) (declare (xargs :guard (and (formula-p fal) (natp acc)))) (cond ((atom fal) acc) (t (formula-max-var (cdr fal) (if (deleted-clause-p (cdar fal)) acc (clause-max-var (cdar fal) acc))))))
proof-max-varfunction
(defun proof-max-var (proof acc) (declare (xargs :guard (and (proofp proof) (natp acc)))) (cond ((endp proof) acc) (t (proof-max-var (cdr proof) (let ((entry (car proof))) (if (proof-entry-deletion-p entry) acc (clause-max-var (access add-step entry :clause) acc)))))))
valid-proofp$function
(defun valid-proofp$ (formula proof a$) (declare (xargs :stobjs a$ :guard (formula-p formula) :verify-guards nil)) (let* ((formula (make-fast-alist formula)) (max-var (and (proofp proof) (proof-max-var proof (formula-max-var formula 0))))) (cond ((varp max-var) (let ((a$ (initialize-a$ max-var a$))) (mv-let (v a$) (verify-proof$ formula proof a$) (mv v (proof-contradiction-p proof) a$)))) (t (mv nil nil a$)))))
other
(verify-guards valid-proofp$)
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)))))
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)))))))
valid-proofp$-topfunction
(defun valid-proofp$-top (formula proof incomplete-okp) (declare (xargs :guard t)) (if (formula-p formula) (with-local-stobj a$ (mv-let (v c a$) (valid-proofp$ formula proof a$) (if v (or incomplete-okp c (er hard? 'valid-proofp$-top "Incomplete proof!")) (er hard? 'valid-proofp$-top "Invalid proof!")))) (er hard? 'valid-proofp$-top "Invalid formula!~|~@0" (formula-p-error-msg formula))))
refutation-p$function
(defun refutation-p$ (proof formula) (declare (xargs :guard t)) (valid-proofp$-top formula proof nil))
ordered-literalspfunction
(defun ordered-literalsp (x) (declare (xargs :guard (literal-listp x))) (cond ((endp x) t) (t (or (null (cdr x)) (and (< (abs (car x)) (abs (cadr x))) (ordered-literalsp (cdr x)))))))
lrat-clausepfunction
(defun lrat-clausep (x) (declare (xargs :guard t)) (or (null x) (and (literal-listp x) (not (member (car x) (cdr x))) (not (member (negate (car x)) (cdr x))) (ordered-literalsp (cdr x)))))
lrat-add-step-pfunction
(defun lrat-add-step-p (x) (declare (xargs :guard t :guard-hints (("Goal" :use (:guard-theorem add-step-p))))) (and (weak-add-step-p x) (posp (access add-step x :index)) (lrat-clausep (access add-step x :clause)) (index-listp (access add-step x :rup-indices)) (drat-hint-listp (access add-step x :drat-hints))))
lrat-proof-entry-pfunction
(defun lrat-proof-entry-p (entry) (declare (xargs :guard t)) (cond ((and (consp entry) (eq (car entry) t)) (index-listp (cdr entry))) (t (lrat-add-step-p entry))))
lrat-proofpfunction
(defun lrat-proofp (proof) (declare (xargs :guard t)) (if (atom proof) (null proof) (and (lrat-proof-entry-p (car proof)) (lrat-proofp (cdr proof)))))
lrat-valid-proofp$function
(defun lrat-valid-proofp$ (formula proof a$) (declare (xargs :stobjs a$ :guard (formula-p formula) :guard-hints (("Goal" :use (:guard-theorem valid-proofp$))))) (let* ((formula (make-fast-alist formula)) (max-var (and (lrat-proofp proof) (proof-max-var proof (formula-max-var formula 0))))) (cond ((varp max-var) (let ((a$ (initialize-a$ max-var a$))) (mv-let (v a$) (verify-proof$ formula proof a$) (mv v (proof-contradiction-p proof) a$)))) (t (mv nil nil a$)))))
lrat-valid-proofp$-topfunction
(defun lrat-valid-proofp$-top (formula proof incomplete-okp) (declare (xargs :guard t)) (and (formula-p formula) (with-local-stobj a$ (mv-let (v c a$) (lrat-valid-proofp$ formula proof a$) (and v (or incomplete-okp c))))))
lrat-refutation-p$function
(defun lrat-refutation-p$ (proof formula) (declare (xargs :guard t)) (lrat-valid-proofp$-top formula proof nil))