diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-11-29 12:09:19 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-11-29 12:09:19 -0600 |
| commit | 41b38de8b059d346764cd5ca112740aa09e1d163 (patch) | |
| tree | 95f440dff149399ed29b6e93c9190fe8ade65e96 /src/theory/quantifiers/quantifiers_attributes.h | |
| parent | 43e02cedf0e2a2700a2ace23cf85cff9bb242f13 (diff) | |
Infrastructure for sygus side conditions (#2729)
Diffstat (limited to 'src/theory/quantifiers/quantifiers_attributes.h')
| -rw-r--r-- | src/theory/quantifiers/quantifiers_attributes.h | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/src/theory/quantifiers/quantifiers_attributes.h b/src/theory/quantifiers/quantifiers_attributes.h index 918269bbe..d3acc9434 100644 --- a/src/theory/quantifiers/quantifiers_attributes.h +++ b/src/theory/quantifiers/quantifiers_attributes.h @@ -73,6 +73,17 @@ struct SygusPrintProxyAttributeId typedef expr::Attribute<SygusPrintProxyAttributeId, Node> SygusPrintProxyAttribute; +/** Attribute for specifying a "side condition" for a sygus conjecture + * + * A sygus conjecture of the form exists f. forall x. P[f,x] whose side + * condition is C[f] has the semantics exists f. C[f] ^ forall x. P[f,x]. + */ +struct SygusSideConditionAttributeId +{ +}; +typedef expr::Attribute<SygusSideConditionAttributeId, Node> + SygusSideConditionAttribute; + namespace quantifiers { /** Attribute priority for rewrite rules */ @@ -109,6 +120,8 @@ struct QAttributes Node d_fundef_f; /** is this formula marked as a sygus conjecture? */ bool d_sygus; + /** side condition for sygus conjectures */ + Node d_sygusSideCondition; /** if a rewrite rule, then this is the priority value for the rewrite rule */ int d_rr_priority; /** stores the maximum instantiation level allowed for this quantified formula |