diff options
| author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2021-04-09 17:30:44 -0300 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-04-09 15:30:44 -0500 |
| commit | 62f5fb8db269e12f13ce5c4e1c3f975776737836 (patch) | |
| tree | bdf16437b8c0c5ead202ac7fb08f6483aa3a9c19 /src/prop/sat_proof_manager.h | |
| parent | 6923f0cb9930332a61e187d3b4d1a7ec7e65b15c (diff) | |
[proof-new] Optimizing sat proof (#6324)
For some benchmarks, checking MACRO_RESOLUTION can be up to 80% (!!!) of the running time. This commit introduces a new rule that does not perform checking. The old rule and checker are kept for ground truth. Some miscellaneous minor changes are also made in the PR.
Diffstat (limited to 'src/prop/sat_proof_manager.h')
| -rw-r--r-- | src/prop/sat_proof_manager.h | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/prop/sat_proof_manager.h b/src/prop/sat_proof_manager.h index 4d45ce3b7..6407939c7 100644 --- a/src/prop/sat_proof_manager.h +++ b/src/prop/sat_proof_manager.h @@ -561,7 +561,8 @@ class SatProofManager /** The proof generator for resolution chains */ BufferedProofGenerator d_resChainPg; - /** The false node */ + /** The true/false nodes */ + Node d_true; Node d_false; /** All clauses added to the SAT solver, kept in a context-dependent manner. |