1 files changed, 12 insertions, 2 deletions
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index e5154476a..7b5df2ab8 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -59,6 +59,10 @@ 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;
 
 class QuantifiersEngine;
 
@@ -186,9 +190,15 @@ public:
   Node convertNodeToPattern( Node n, Node f,
                              const std::vector<Node> & vars,
                              const std::vector<Node> & nvars);
-  /** set instantiation constant attr */
-  void setInstantiationConstantAttr( Node n, Node f );
 
+  static Node getInstConstAttr( Node n );
+  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
 private:
   /** map from universal quantifiers to the list of skolem constants */