diff options
| author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2021-07-13 15:38:23 -0300 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-07-13 13:38:23 -0500 |
| commit | 912be5c60f194c3b0d52c1d06a1339fb6cb13a9c (patch) | |
| tree | d82fa967ecf45342133369c8641aac02ca633016 /src/prop | |
| parent | 36d01a7fd74c6dff52bf9dcba490ff7ded29ad5d (diff) | |
[rewriter] Add rewrite to order IFF (equality for Booleans) (#6872)
Not doing this rewrite for Booleans is probably an artifact of the old IFF kind being removed. This rewrite is important to simplify the generation of proofs for the SAT solver, as clarified in the new comment in the SAT proof manager.
Diffstat (limited to 'src/prop')
| -rw-r--r-- | src/prop/sat_proof_manager.cpp | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/prop/sat_proof_manager.cpp b/src/prop/sat_proof_manager.cpp index 5bec41e2b..0f8ad8e69 100644 --- a/src/prop/sat_proof_manager.cpp +++ b/src/prop/sat_proof_manager.cpp @@ -336,6 +336,10 @@ void SatProofManager::explainLit(SatLiteral lit, Trace("sat-proof") << push << "SatProofManager::explainLit: Lit: " << lit; Node litNode = getClauseNode(lit); Trace("sat-proof") << " [" << litNode << "]\n"; + // Note that if we had two literals for (= a b) and (= b a) and we had already + // a proof for (= a b) this test would return true for (= b a), which could + // lead to open proof. However we should never have two literals like this in + // the SAT solver since they'd be rewritten to the same one if (d_resChainPg.hasProofFor(litNode)) { Trace("sat-proof") << "SatProofManager::explainLit: already justified " |