diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-11-04 16:22:51 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-11-04 16:22:51 -0600 |
| commit | e5ac2503afc1879808a8809e9b9498ba08217328 (patch) | |
| tree | 61b27f5e68be461d38ab767b97aa1deeeac9772a /src/theory/uf/ho_extension.h | |
| parent | 9ca190a3a2f7f952e1452efb69c78803ec302dd6 (diff) | |
Fix ho extensionality in collect model info (#3435)
Diffstat (limited to 'src/theory/uf/ho_extension.h')
| -rw-r--r-- | src/theory/uf/ho_extension.h | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/src/theory/uf/ho_extension.h b/src/theory/uf/ho_extension.h index a38d1803a..47336e085 100644 --- a/src/theory/uf/ho_extension.h +++ b/src/theory/uf/ho_extension.h @@ -127,8 +127,12 @@ class HoExtension * * Given disequality deq f != g, this returns the disequality: * (f k) != (g k) for fresh constant(s) k. + * + * If isCached is true, then this returns the same k for all calls to this + * method with the same deq. If it is false, it creates fresh k and does not + * cache the result. */ - Node getExtensionalityDeq(TNode deq); + Node getExtensionalityDeq(TNode deq, bool isCached = true); /** * Check whether extensionality should be applied for any pair of terms in the |