| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Creating LRAT proofs reuqires writing SAT problems in the DIMACS format.
Before this code was in the LRAT class.
However, since creating ER proofs will also require writing DIMACS, I
decided to extract it.
At the same time I realized that my prior representation of used clauses
was unnecessarily poor. I had chosen it to align with
`CnfProof::collectAtomsForClauses`, but the format is really bad (it
requires extra allocations & manual memory management), and I discovered
that the aforementioned method is super simple, so I'm moving to a
better format.
|
|
* LFSC ouput & unit test
* Renamed lrat unit test file
* s/DRAT/LRAT/
Thanks Andres!
Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>
* Addressed Andres' comments
1. Extracted a filter whitespace function.
2. Added @param annotations.
* Addressing Yoni's comments
Tweaked the test method name for LRAT output as LFSC
Added assertions for verifying that clause index lists are sorted during
LFSC LRAT output.
|
|
While implementing and testing LRAT proof output as LFSC, I discovered
that my implementation of LratInstruction as a tagged union was subtly
broken for reasons related to move/copy assignment/constructors.
While I could have figured out how to fix it, I decided to stop fighting
the system and use inheritance.
This PR will be followed by one using the inheritance-based
LratInstruction to implement output to LFSC.
|
|
* Fixed linking against drat2er/drat-trim
We have machinery for linking against drat2er. However, this machinery
didn't quite work because libdrat2er.a contains an (undefined) reference
to `run_drat_trim` from libdrat-trim.a.
Thus, when linking against libdrat2er.a, we also need to link against
libdrat-trim.a.
I made this change, and then tested it by actually calling a function
from the drat2er library (CheckAndConvertToLRAT) which relies on
`run_drat_trim`. Since this invocation compiles, we know that the
linking is working properly now.
* Combined the two libs, per Mathias
* drat2er configured gaurds
|
|
* [LRAT] A C++ data structure for LRAT.
Added a data structure for storing (abstract) LRAT proofs.
The constructor will take a drat binary proof and convert it to LRAT
using drat-trim. However, this is unimplemented in this PR.
Subsequent PRs will add:
* LFSC representation of LRAT
* Bitvector Proofs based on LRAT
* Enabled tests for those proofs
* Documenting LRAT constructors
* Apply suggestions from code review
Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>
* Responding to Andres' review
Consisting of
* Naming nits
* Closed fds
* Better implementation of disjoint union for LratInstruction
* DRAT -> LRAT conversion is no longer an LratProof constructor
* include reorder
* Update src/proof/lrat/lrat_proof.h
Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>
* Addressed Andres' comments
* ANonymous namespaces and name resolution?
* Remove inlines, fix i negation
Thanks Andres!
* Use `std::abs`
Credit to Andres
Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>
* Remove uneeded public
|
