diff options
Diffstat (limited to 'src/theory/quantifiers/term_database.h')
| -rw-r--r-- | src/theory/quantifiers/term_database.h | 7 |
1 files changed, 0 insertions, 7 deletions
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 860f087dd..66b45be2f 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -60,11 +60,6 @@ typedef expr::Attribute<ModelBasisAttributeId, bool> ModelBasisAttribute; struct ModelBasisArgAttributeId {}; typedef expr::Attribute<ModelBasisArgAttributeId, uint64_t> ModelBasisArgAttribute; -struct HasBoundVarAttributeId {}; -typedef expr::Attribute<HasBoundVarAttributeId, bool> HasBoundVarAttribute; -struct HasBoundVarComputedAttributeId {}; -typedef expr::Attribute<HasBoundVarComputedAttributeId, bool> HasBoundVarComputedAttribute; - //for rewrite rules struct QRewriteRuleAttributeId {}; typedef expr::Attribute<QRewriteRuleAttributeId, Node> QRewriteRuleAttribute; @@ -210,8 +205,6 @@ public: static bool hasInstConstAttr( Node n ); //for bound variables public: - //does n have bound variables? - static bool hasBoundVarAttr( Node n ); //get bound variables in n static void getBoundVars( Node n, std::vector< Node >& bvs); //for skolem |