diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-03-22 09:51:05 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-03-22 09:51:05 -0500 |
| commit | 93fd4aed186c3dfa1b0fa7bec102f5b94edca322 (patch) | |
| tree | 331b0bd9dcc69c2355887db5ca5fd1a20d6a63e3 /src/expr/skolem_manager.h | |
| parent | c0d4ac3d307b13c24471da5af2f916569a7f52b9 (diff) | |
Guard for non-unique skolems in term formula removal (#6179)
In rare cases, we may reuse skolems for different terms (those that are the same up to purification) due to recent changes in how skolem are generated. This guards for this case in the term formula remover, which avoids assertion failures in cd insert hash map.
Fixes #6132.
Diffstat (limited to 'src/expr/skolem_manager.h')
| -rw-r--r-- | src/expr/skolem_manager.h | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/src/expr/skolem_manager.h b/src/expr/skolem_manager.h index 1cb048cf2..44a8f87c2 100644 --- a/src/expr/skolem_manager.h +++ b/src/expr/skolem_manager.h @@ -161,6 +161,15 @@ class SkolemManager * * Notice that a purification skolem is trivial to justify, and hence it * does not require a proof generator. + * + * Notice that in very rare cases, two different terms may have the + * same purification skolem. For example, let k be the skolem introduced to + * eliminate (ite A B C). Then, the pair of terms: + * (ite (ite A B C) D E) and (ite k D E) + * have the same purification skolem. In the implementation, this is a result + * of the fact that the above terms have the same original form. It is sound + * to use the same skolem to purify these two terms, since they are + * definitionally equivalent. */ Node mkPurifySkolem(Node t, const std::string& prefix, |