diff options
Diffstat (limited to 'src/theory/quantifiers/quantifiers_attributes.h')
| -rw-r--r-- | src/theory/quantifiers/quantifiers_attributes.h | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/src/theory/quantifiers/quantifiers_attributes.h b/src/theory/quantifiers/quantifiers_attributes.h index 189c79470..cadf0b0d6 100644 --- a/src/theory/quantifiers/quantifiers_attributes.h +++ b/src/theory/quantifiers/quantifiers_attributes.h @@ -126,9 +126,9 @@ struct QAttributes /** the instantiation pattern list for this quantified formula (its 3rd child) */ Node d_ipl; - /** the name of this quantified formula */ + /** The name of this quantified formula, used for :qid */ Node d_name; - /** the quantifier id associated with this formula */ + /** The (internal) quantifier id associated with this formula */ Node d_qid_num; /** is this quantified formula a function definition? */ bool isFunDef() const { return !d_fundef_f.isNull(); } @@ -198,9 +198,11 @@ public: bool isQuantElim( Node q ); /** is quant elim partial */ bool isQuantElimPartial( Node q ); - /** get quant id num */ + /** get quant name, which is used for :qid */ + Node getQuantName(Node q) const; + /** get (internal) quant id num */ int getQuantIdNum( Node q ); - /** get quant id num */ + /** get (internal)quant id num */ Node getQuantIdNumNode( Node q ); /** set instantiation level attr */ |