diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-08-13 15:08:00 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-08-13 15:08:00 -0500 |
| commit | 72281a35622ae4656d3a2e4cd29e42cb96eba205 (patch) | |
| tree | 1182a067911c1d7c2314fce70b76f0171c57ee3c /src/theory/quantifiers/quantifiers_attributes.h | |
| parent | 9e654bc0105b04d08e8c0fb555a212228cab2c9d (diff) | |
Track sygus variable to term relationship via attribute (#3182)
Diffstat (limited to 'src/theory/quantifiers/quantifiers_attributes.h')
| -rw-r--r-- | src/theory/quantifiers/quantifiers_attributes.h | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/src/theory/quantifiers/quantifiers_attributes.h b/src/theory/quantifiers/quantifiers_attributes.h index 329f9d08a..827c5e7f4 100644 --- a/src/theory/quantifiers/quantifiers_attributes.h +++ b/src/theory/quantifiers/quantifiers_attributes.h @@ -84,6 +84,18 @@ struct SygusSideConditionAttributeId typedef expr::Attribute<SygusSideConditionAttributeId, Node> SygusSideConditionAttribute; +/** Attribute for indicating that a sygus variable encodes a term + * + * This is used, e.g., for abduction where the formal argument list of the + * abduct-to-synthesize corresponds to the free variables of the sygus + * problem. + */ +struct SygusVarToTermAttributeId +{ +}; +typedef expr::Attribute<SygusVarToTermAttributeId, Node> + SygusVarToTermAttribute; + namespace quantifiers { /** Attribute priority for rewrite rules */ |