[acl2/acl2] a65f5a: Added linear DRAT checker, with soundness proof an...

[GitHub]

Branch: refs/heads/master
Home: https://github.com/acl2/acl2
Commit: a65f5ac8e0238c558071b091daebf947310a0c16
https://github.com/acl2/acl2/commit/a65f5ac8e0238c558071b091daebf947310a0c16
Author: Matt Kaufmann <kauf...@cs.utexas.edu>
Date: 2016-12-01 (Thu, 01 Dec 2016)

Changed paths:
A books/projects/sat/lrat/lrat-checker.lisp
A books/projects/sat/lrat/lrat-parser.lisp
A books/projects/sat/lrat/sat-drat-claim-1.lisp
A books/projects/sat/lrat/sat-drat-claim-2-3.lisp
A books/projects/sat/lrat/sat-drat-claim-2.lisp
A books/projects/sat/lrat/satisfiable-add-proof-clause-base.lisp
A books/projects/sat/lrat/satisfiable-add-proof-clause-drat.lisp
A books/projects/sat/lrat/satisfiable-add-proof-clause-rup.lisp
A books/projects/sat/lrat/satisfiable-add-proof-clause.lisp
A books/projects/sat/lrat/satisfiable-maybe-shrink-formula.lisp
A books/projects/sat/lrat/soundness.lisp
A books/projects/sat/lrat/tests/LICENSE
A books/projects/sat/lrat/tests/README
A books/projects/sat/lrat/tests/driver.lisp
A books/projects/sat/lrat/tests/example-4-vars.cnf
A books/projects/sat/lrat/tests/example-4-vars.lrat
A books/projects/sat/lrat/tests/uuf-100-1.cnf
A books/projects/sat/lrat/tests/uuf-100-1.lrat
A books/projects/sat/lrat/tests/uuf-100-2.cnf
A books/projects/sat/lrat/tests/uuf-100-2.lrat
A books/projects/sat/lrat/tests/uuf-100-3.cnf
A books/projects/sat/lrat/tests/uuf-100-3.lrat
A books/projects/sat/lrat/tests/uuf-100-4.cnf
A books/projects/sat/lrat/tests/uuf-100-4.lrat
A books/projects/sat/lrat/tests/uuf-100-5.cnf
A books/projects/sat/lrat/tests/uuf-100-5.lrat
A books/projects/sat/lrat/tests/uuf-30-1.cnf
A books/projects/sat/lrat/tests/uuf-30-1.lrat
A books/projects/sat/lrat/top.lisp
A books/projects/sat/lrat/truth-monotone.lisp
A books/projects/sat/lrat/unit-propagation-correct.lisp
A books/projects/sat/lrat/unit-propagation-implies-unsat.lisp
A books/projects/sat/lrat/unit-propagation-monotone.lisp

Log Message:
-----------
Added linear DRAT checker, with soundness proof and small tests.

[GitHub]

Branch: refs/heads/testing

Commit: d2b2cf482564f71a4f2f9c853c02220570b2c800
https://github.com/acl2/acl2/commit/d2b2cf482564f71a4f2f9c853c02220570b2c800
Author: David L. Rager <rag...@gmail.com>

Merge commit 'a65f5ac8e0238c558071b091daebf947310a0c16' into HEAD


Compare: https://github.com/acl2/acl2/compare/c22bcf311812...d2b2cf482564