diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-11-12 11:00:44 +0100 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-11-12 11:00:44 +0100 |
| commit | ada1fc44c9b5b8746a2e1e4046032282149768b5 (patch) | |
| tree | efb350f7729004fedb4d7d872d5ff7e8d5d1fdc4 /src/theory/quantifiers/term_database.h | |
| parent | 97470da31e14104f807fb33b2b3423e583e10726 (diff) | |
Minor fixes and improvements to purify quant, relational triggers.
Diffstat (limited to 'src/theory/quantifiers/term_database.h')
| -rw-r--r-- | src/theory/quantifiers/term_database.h | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index f809aa5b8..8ce6aeaf0 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -59,6 +59,9 @@ typedef expr::Attribute< NoMatchAttributeId, struct InstConstantAttributeId {}; typedef expr::Attribute<InstConstantAttributeId, Node> InstConstantAttribute; +struct BoundVarAttributeId {}; +typedef expr::Attribute<BoundVarAttributeId, Node> BoundVarAttribute; + struct InstLevelAttributeId {}; typedef expr::Attribute<InstLevelAttributeId, uint64_t> InstLevelAttribute; @@ -262,6 +265,8 @@ public: static Node getInstConstAttr( Node n ); static bool hasInstConstAttr( Node n ); + static Node getBoundVarAttr( Node n ); + static bool hasBoundVarAttr( Node n ); //for skolem |