diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-09-22 23:50:43 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-09-22 23:50:43 -0500 |
| commit | cfe0fc1346c41048fa76f7e0fc582afbe95364a2 (patch) | |
| tree | aa191e07dd529b6ddad1a9e103cc75172f96f902 /src/theory/quantifiers/quantifiers_attributes.h | |
| parent | 24b44a8e559f1d89f309d611922098e667293920 (diff) | |
Allow E-matching by default when strings are enabled (#5117)
This does not disable E-matching when strings are enabled with --strings-exp, due to potential applications where strings are combined with user-provided quantified formulas.
Notice that by default, we do not want E-matching applied to quantified formulas corresponding to reductions for extended string functions. To correct this, all quantified formulas generated by strings are marked with an "internal quantified formula" attribute, which causes E-matching to ignore them. This feature can in theory be generalized later for other internal sources of quantified formulas.
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 */ |