diff options
Diffstat (limited to 'src/theory/quantifiers/quantifiers_attributes.h')
| -rw-r--r-- | src/theory/quantifiers/quantifiers_attributes.h | 12 |
1 files changed, 11 insertions, 1 deletions
diff --git a/src/theory/quantifiers/quantifiers_attributes.h b/src/theory/quantifiers/quantifiers_attributes.h index 9a18d13fb..87315de7c 100644 --- a/src/theory/quantifiers/quantifiers_attributes.h +++ b/src/theory/quantifiers/quantifiers_attributes.h @@ -55,6 +55,11 @@ typedef expr::Attribute< SygusAttributeId, bool > SygusAttribute; struct SynthesisAttributeId {}; typedef expr::Attribute< SynthesisAttributeId, bool > SynthesisAttribute; +struct InstLevelAttributeId +{ +}; +typedef expr::Attribute<InstLevelAttributeId, uint64_t> InstLevelAttribute; + /** Attribute for setting printing information for sygus variables * * For variable d of sygus datatype type, if @@ -185,7 +190,12 @@ public: /** get quant id num */ Node getQuantIdNumNode( Node q ); -private: + /** set instantiation level attr */ + static void setInstantiationLevelAttr(Node n, uint64_t level); + /** set instantiation level attr */ + static void setInstantiationLevelAttr(Node n, Node qn, uint64_t level); + + private: /** pointer to quantifiers engine */ QuantifiersEngine * d_quantEngine; /** cache of attributes */ |