diff options
author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2021-02-04 11:59:56 -0300 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-02-04 08:59:56 -0600 |
commit | 18e8b81b8eb4c4e313b03f4616271a0ea8e65e9b (patch) | |
tree | b48324201876336ec351f3128d0850160df71ff9 /src/prop/sat_proof_manager.cpp | |
parent | ac998a45ae64c589aeb79c5fd72234468e40451c (diff) |
[proof-new] Catch trivial cycles in SAT proof generation (#5853)
Evaluating the proof infrastructure in SMT-LIB has uncovered a rare
case (i.e., not previously in our regressions!!) in which we generate
a trivial cycle during SAT proof generation, which can lead to
problematic cycles when expanding MACRO_RESOLUTION steps. For example,
we can go from
l1 v l2 ~l1 v l3 ~l2 v l3
(ok) ------------------------------
l3
in which l3 = l1 v l2, to
l1 v l2 ~l1 v l3 ~l2 v l3
(bad) ------------------------------
l3 v l3
---------
l3
This commit now catches the trivial cycle before it's generated.
Diffstat (limited to 'src/prop/sat_proof_manager.cpp')
-rw-r--r-- | src/prop/sat_proof_manager.cpp | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/src/prop/sat_proof_manager.cpp b/src/prop/sat_proof_manager.cpp index aae11ae51..dd7e94f03 100644 --- a/src/prop/sat_proof_manager.cpp +++ b/src/prop/sat_proof_manager.cpp @@ -228,6 +228,17 @@ void SatProofManager::endResChain(Node conclusion, << children[0] << "\n"; return; } + // whether trivial cycle + for (const Node& child : children) + { + if (conclusion == child) + { + Trace("sat-proof") + << "SatProofManager::endResChain: no-op. The conclusion " + << conclusion << " is equal to a premise\n"; + return; + } + } if (Trace.isOn("sat-proof") && d_resChains.hasGenerator(conclusion)) { Trace("sat-proof") << "SatProofManager::endResChain: replacing proof of " |