diff options
Diffstat (limited to 'src/theory/arrays/skolem_cache.h')
| -rw-r--r-- | src/theory/arrays/skolem_cache.h | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/theory/arrays/skolem_cache.h b/src/theory/arrays/skolem_cache.h index 12578c01f..17a5c6975 100644 --- a/src/theory/arrays/skolem_cache.h +++ b/src/theory/arrays/skolem_cache.h @@ -43,6 +43,13 @@ class SkolemCache */ static Node getExtIndexSkolem(Node deq); + /** + * Get the bound variable for given EQ_RANGE operator. This bound variable + * is unique for `eqr`. Calling this method will always return the same bound + * variable over the lifetime of `eqr`. + */ + static Node getEqRangeVar(TNode eqr); + private: /** * Get the bound variable x of the witness term above for disequality deq |