diff options
Diffstat (limited to 'src/theory/quantifiers_engine.h')
| -rw-r--r-- | src/theory/quantifiers_engine.h | 11 |
1 files changed, 10 insertions, 1 deletions
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 5172c1554..5d4ff6afe 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -232,7 +232,16 @@ public: bool usingModelEqualityEngine() const { return d_useModelEe; } /** debug print equality engine */ void debugPrintEqualityEngine( const char * c ); - /** get internal representative */ + /** get internal representative + * + * Choose a term that is equivalent to a in the current context that is the + * best term for instantiating the index^th variable of quantified formula q. + * If no legal term can be found, we return null. This can occur if: + * - a's type is not a subtype of the type of the index^th variable of q, + * - a is in an equivalent class with all terms that are restricted not to + * appear in instantiations of q, e.g. INST_CONSTANT terms for counterexample + * guided instantiation. + */ Node getInternalRepresentative( Node a, Node q, int index ); public: |