diff options
Diffstat (limited to 'src/theory/quantifiers/instantiate.h')
| -rw-r--r-- | src/theory/quantifiers/instantiate.h | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h index cd3993756..d10a44149 100644 --- a/src/theory/quantifiers/instantiate.h +++ b/src/theory/quantifiers/instantiate.h @@ -318,6 +318,11 @@ class Instantiate : public QuantifiersUtil bool addedLem = true); /** remove instantiation from the cache */ bool removeInstantiationInternal(Node q, std::vector<Node>& terms); + /** + * Ensure that n has type tn, return a term equivalent to it for that type + * if possible. + */ + static Node ensureType(Node n, TypeNode tn); /** pointer to the quantifiers engine */ QuantifiersEngine* d_qe; |