diff options
Diffstat (limited to 'src/theory/quantifiers/term_database.h')
| -rw-r--r-- | src/theory/quantifiers/term_database.h | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 7c136a186..477b964ee 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -92,6 +92,10 @@ typedef expr::Attribute< LtePartialInstAttributeId, bool > LtePartialInstAttribu struct SygusProxyAttributeId {}; typedef expr::Attribute<SygusProxyAttributeId, Node> SygusProxyAttribute; +//attribute for fun-def abstraction type +struct AbsTypeFunDefAttributeId {}; +typedef expr::Attribute<AbsTypeFunDefAttributeId, bool> AbsTypeFunDefAttribute; + class QuantifiersEngine; namespace inst{ |