diff options
Diffstat (limited to 'src/theory/quantifiers/quantifiers_attributes.h')
| -rw-r--r-- | src/theory/quantifiers/quantifiers_attributes.h | 30 |
1 files changed, 23 insertions, 7 deletions
diff --git a/src/theory/quantifiers/quantifiers_attributes.h b/src/theory/quantifiers/quantifiers_attributes.h index e9abbc9ed..88f291b2b 100644 --- a/src/theory/quantifiers/quantifiers_attributes.h +++ b/src/theory/quantifiers/quantifiers_attributes.h @@ -88,11 +88,24 @@ struct SygusVarToTermAttributeId typedef expr::Attribute<SygusVarToTermAttributeId, Node> SygusVarToTermAttribute; -namespace quantifiers { +/** + * Attribute true for quantifiers that have been internally generated, e.g. + * for reductions of string operators. + * + * Currently, this attribute is used for indicating that E-matching should + * not be applied, as E-matching should not be applied to quantifiers + * generated for strings reductions. + * + * This attribute can potentially be generalized to an identifier indicating + * the internal source of the quantified formula (of which strings reduction + * is one possibility). + */ +struct InternalQuantAttributeId +{ +}; +typedef expr::Attribute<InternalQuantAttributeId, bool> InternalQuantAttribute; -/** Attribute priority for rewrite rules */ -//struct RrPriorityAttributeId {}; -//typedef expr::Attribute< RrPriorityAttributeId, uint64_t > RrPriorityAttribute; +namespace quantifiers { /** This struct stores attributes for a single quantified formula */ struct QAttributes @@ -103,7 +116,8 @@ struct QAttributes d_sygus(false), d_qinstLevel(-1), d_quant_elim(false), - d_quant_elim_partial(false) + d_quant_elim_partial(false), + d_isInternal(false) { } ~QAttributes(){} @@ -123,6 +137,8 @@ struct QAttributes bool d_quant_elim; /** is this formula marked for partial quantifier elimination? */ bool d_quant_elim_partial; + /** Is this formula internally generated? */ + bool d_isInternal; /** the instantiation pattern list for this quantified formula (its 3rd child) */ Node d_ipl; @@ -192,12 +208,12 @@ public: bool isSygus( Node q ); /** get instantiation level */ int getQuantInstLevel( Node q ); - /** get rewrite rule priority */ - int getRewriteRulePriority( Node q ); /** is quant elim */ bool isQuantElim( Node q ); /** is quant elim partial */ bool isQuantElimPartial( Node q ); + /** is internal quantifier */ + bool isInternal(Node q) const; /** get quant name, which is used for :qid */ Node getQuantName(Node q) const; /** get (internal) quant id num */ |