diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-03-27 11:53:49 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-03-27 11:53:49 -0500 |
| commit | 9dcaaeba4880a8f145df00289ff1b092a7e3dd47 (patch) | |
| tree | 97c6ffc45fd906e8f1b84726653cdac52bdc2f26 /src/theory/quantifiers/dynamic_rewrite.h | |
| parent | 6a656809c353776c9de9580b19a6de79ef5a76d4 (diff) | |
Filter candidate rewrites based on matching (#1682)
Diffstat (limited to 'src/theory/quantifiers/dynamic_rewrite.h')
| -rw-r--r-- | src/theory/quantifiers/dynamic_rewrite.h | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/theory/quantifiers/dynamic_rewrite.h b/src/theory/quantifiers/dynamic_rewrite.h index 2b5464151..388173829 100644 --- a/src/theory/quantifiers/dynamic_rewrite.h +++ b/src/theory/quantifiers/dynamic_rewrite.h @@ -63,6 +63,10 @@ class DynamicRewriter * a = b based on the previous equalities it has seen. */ bool addRewrite(Node a, Node b); + /** + * Check whether this class knows that the equality a = b holds. + */ + bool areEqual(Node a, Node b); private: /** pointer to the quantifiers engine */ |