other
(in-package "LRAT")
other
(include-book "lrat-checker")
lrat-verify-proof-fnfunction
(defun lrat-verify-proof-fn (cnf-file lrat-file incomplete-okp state) (declare (xargs :stobjs state :verify-guards nil)) (b* (((er formula) (time$ (parse-cnf-file cnf-file state))) ((er proof) (time$ (parse-lrat-file lrat-file state)))) (value (time$ (lrat-valid-proofp$-top formula proof incomplete-okp)))))
lrat-verify-proofmacro
(defmacro lrat-verify-proof (cnf-file lrat-file &optional (incomplete-okp 'nil)) `(lrat-verify-proof-fn ,LRAT::CNF-FILE ,LRAT::LRAT-FILE ,LRAT::INCOMPLETE-OKP state))
lrat-verify-proofmacro
(defmacro lrat-verify-proof (&rest args) `(lrat-verify-proof ,@LRAT::ARGS))