diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-04-27 16:25:11 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-04-27 21:25:11 +0000 |
| commit | d524948b58c4c3f61c623649049f6209b7756ed6 (patch) | |
| tree | ed35c98dbcb5428b9e4ba6db18f891df985ab1a3 /src/expr | |
| parent | 187bbe04f54798f84b404dc61d2a9d221130109d (diff) | |
Fix refutational soundness bug in quantifier prenexing (#6448)
This bug can be triggered by define-fun, quantifier macros or inferred substitutions whose RHS contain quantified formulas.
This corrects the issue by ensuring that bound variables introduced for prenexing are fresh for distinct quantified formula subterms that may share quantified variables.
This was reported by Geoff Sutcliffe via a TPTP run.
Diffstat (limited to 'src/expr')
| -rw-r--r-- | src/expr/bound_var_manager.cpp | 4 | ||||
| -rw-r--r-- | src/expr/bound_var_manager.h | 2 |
2 files changed, 6 insertions, 0 deletions
diff --git a/src/expr/bound_var_manager.cpp b/src/expr/bound_var_manager.cpp index fa7e4305d..e4b1be691 100644 --- a/src/expr/bound_var_manager.cpp +++ b/src/expr/bound_var_manager.cpp @@ -37,6 +37,10 @@ Node BoundVarManager::getCacheValue(TNode cv1, TNode cv2) { return NodeManager::currentNM()->mkNode(kind::SEXPR, cv1, cv2); } +Node BoundVarManager::getCacheValue(TNode cv1, TNode cv2, TNode cv3) +{ + return NodeManager::currentNM()->mkNode(kind::SEXPR, cv1, cv2, cv3); +} Node BoundVarManager::getCacheValue(TNode cv1, TNode cv2, size_t i) { diff --git a/src/expr/bound_var_manager.h b/src/expr/bound_var_manager.h index 4c9c0af20..3330decff 100644 --- a/src/expr/bound_var_manager.h +++ b/src/expr/bound_var_manager.h @@ -83,6 +83,8 @@ class BoundVarManager //---------------------------------- utilities for computing Node hash /** get cache value from two nodes, returns SEXPR */ static Node getCacheValue(TNode cv1, TNode cv2); + /** get cache value from three nodes, returns SEXPR */ + static Node getCacheValue(TNode cv1, TNode cv2, TNode cv3); /** get cache value from two nodes and a size_t, returns SEXPR */ static Node getCacheValue(TNode cv1, TNode cv2, size_t i); /** get cache value, returns a constant rational node */ |