2 files changed, 34 insertions, 0 deletions
diff --git a/src/expr/term_context.cpp b/src/expr/term_context.cpp
index 6974e2114..67da6d842 100644
--- a/src/expr/term_context.cpp
+++ b/src/expr/term_context.cpp
@@ -69,6 +69,22 @@ bool RtfTermContext::hasNestedTermChildren(TNode t)
          && k != kind::BITVECTOR_EAGER_ATOM;
 }
 
+uint32_t InQuantTermContext::initialValue() const { return 0; }
+
+uint32_t InQuantTermContext::computeValue(TNode t,
+                                          uint32_t tval,
+                                          size_t index) const
+{
+  return t.isClosure() ? 1 : tval;
+}
+
+uint32_t InQuantTermContext::getValue(bool inQuant) { return inQuant ? 1 : 0; }
+
+bool InQuantTermContext::inQuant(uint32_t val, bool& inQuant)
+{
+  return val == 1;
+}
+
 uint32_t PolarityTermContext::initialValue() const
 {
   // by default, we have true polarity
diff --git a/src/expr/term_context.h b/src/expr/term_context.h
index ec7b488f9..b0ce03e48 100644
--- a/src/expr/term_context.h
+++ b/src/expr/term_context.h
@@ -93,6 +93,24 @@ class RtfTermContext : public TermContext
 };
 
 /**
+ * Simpler version of above that only computes whether we are inside a
+ * quantifier.
+ */
+class InQuantTermContext : public TermContext
+{
+ public:
+  InQuantTermContext() {}
+  /** The initial value: not beneath a quantifier. */
+  uint32_t initialValue() const override;
+  /** Compute the value of the index^th child of t whose hash is tval */
+  uint32_t computeValue(TNode t, uint32_t tval, size_t index) const override;
+  /** get hash value from the flags */
+  static uint32_t getValue(bool inQuant);
+  /** get flags from the hash value */
+  static bool inQuant(uint32_t val, bool& inQuant);
+};
+
+/**
  * Polarity term context.
  *
  * This class computes the polarity of a term-context-sensitive term, which is