diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-04-14 16:27:29 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-04-14 16:27:29 -0500 |
| commit | c84db60dabd8104928c7261c9df7bd9ef2917e9f (patch) | |
| tree | 25dfaeb4549fc995fddbc2940d94dfe5084e8860 /src/theory/quantifiers/instantiate.h | |
| parent | c3f7c3c9203a355a9c45bf820e3fea0e29b439de (diff) | |
Fix relevant domain computation for nested quantifiers coming from CEGQI (#4235)
Fixes #4228. That benchmark now times out.
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; |