| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
In TSatProof<Solver>::finalizeProof(), we got a clause from the clause
allocator, called resolveUnit() and then size() on the clause. The problem is
that resolveUnit() can reallocate memory (and there is even a comment warning
about that in finalizeProof()), which invalidates the clause. This commit gets
the clause again from the clause allocator before calling size().
|
|
This commit fixes bug 819 by making d_unitConflictId context dependent and adds a test case.
|
|
This commit fixes an issue where the ResChain in `d_resolutionChains` gets
deleted here:
https://github.com/CVC4/CVC4/blob/master/src/proof/sat_proof_implementation.h#L729
The condition immediately after is false because the condition on line 727 is
true. Thus, `d_resolutionChains` now has a deleted entry for `id`.
When CVC4 afterwards gets the ResChain associated with `id` in
`checkResolution()`, it accesses the deleted entry:
https://github.com/CVC4/CVC4/blob/master/src/proof/sat_proof_implementation.h#L303
|
|
|
|
Before, in some cases, e.g. when printing sorts and in resolution
proofs, the proofs contained redundant and/or missing spaces. With this
commit, CVC4 now prints out `(trust_f (= (Array Index Element) let10
let12)` instead of `(trust_f (= (Array Index Element )let10 let12))`.
|
|
|
|
core. Currently, lemmas that are not conjunctions and their own weakest implicants; but for lemmas that *are* conjunctions, we may return only a subset of the conjuncts.
|
|
|
|
|
|
This reverts commit 89ba584531115b7f6d47088d7614368ea05ab9d8.
|
|
|
|
|
|
implementation. As a part of tracking this down, I've modified a number of accessor functions in TSatProof to be const. An expert in this code will need to do a pass over this.
|
|
|
|
|
|
|
|
|
