diff options
| author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2021-01-22 13:15:43 -0300 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-01-22 13:15:43 -0300 |
| commit | 109e7e43efdeb557ff17880da83da438db35eb3e (patch) | |
| tree | 313d66098519bd3ac782a3c21a830fa41d79214a /src/smt/proof_manager.cpp | |
| parent | 98d2ca3ee48cb87e8baa7537c97016cc85ab048d (diff) | |
[proof-new] Expanding MACRO_RESOLUTION in post-processing (#5755)
Breaks down resolution, factoring and reordering. The hardest part of this process is making getting rid of the so-called "crowding literals", i.e., duplicate literals introduced during the series of resolutions and removed implicitly by the SAT solver. A naive removal via addition of premises to the chain resolution can lead to exponential behavior, so instead the removal is done by breaking the resolution and applying a factoring step midway through. This guarantees non-exponential behavior.
Diffstat (limited to 'src/smt/proof_manager.cpp')
| -rw-r--r-- | src/smt/proof_manager.cpp | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp index d82e22736..b8f68af88 100644 --- a/src/smt/proof_manager.cpp +++ b/src/smt/proof_manager.cpp @@ -38,6 +38,7 @@ PfManager::PfManager(context::UserContext* u, SmtEngine* smte) d_pfpp->setEliminateRule(PfRule::MACRO_SR_PRED_INTRO); d_pfpp->setEliminateRule(PfRule::MACRO_SR_PRED_ELIM); d_pfpp->setEliminateRule(PfRule::MACRO_SR_PRED_TRANSFORM); + d_pfpp->setEliminateRule(PfRule::MACRO_RESOLUTION); if (options::proofGranularityMode() != options::ProofGranularityMode::REWRITE) { |