diff options
Diffstat (limited to 'src/theory/quantifiers_engine.h')
| -rw-r--r-- | src/theory/quantifiers_engine.h | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 28f162ddd..d05137e80 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -155,6 +155,11 @@ public: void getInstantiationTermVectors( std::map<Node, std::vector<std::vector<Node> > >& insts); /** + * Get instantiations for quantified formula q. If q is (forall ((x T)) (P x)), + * this is a list of the form (P t1) ... (P tn) for ground terms ti. + */ + void getInstantiations(Node q, std::vector<Node>& insts); + /** * Get skolemization vectors, where for each quantified formula that was * skolemized, this is the list of skolems that were used to witness the * negation of that quantified formula. |