bv: Do not rewrite below BV leafs in BBProof's TConvProofGenerator. (#6869)

Introduces a TermContext class that can be used to skip rewrites below theory leafs. Fixes issues related to bit-vector leafs begin incorrectly rewritten.

2 files changed, 29 insertions, 0 deletions

diff --git a/src/expr/term_context.cpp b/src/expr/term_context.cpp
index d339a3d28..7f8aa9eac 100644
--- a/src/expr/term_context.cpp
+++ b/src/expr/term_context.cpp
@@ -15,6 +15,8 @@
 
 #include "expr/term_context.h"
 
+#include "theory/theory.h"
+
 namespace cvc5 {
 
 uint32_t TermContext::computeValueOp(TNode t, uint32_t tval) const
@@ -133,4 +135,13 @@ void PolarityTermContext::getFlags(uint32_t val, bool& hasPol, bool& pol)
   pol = val == 2;
 }
 
+uint32_t TheoryLeafTermContext::initialValue() const { return 0; }
+
+uint32_t TheoryLeafTermContext::computeValue(TNode t,
+                                             uint32_t tval,
+                                             size_t index) const
+{
+  return theory::Theory::isLeafOf(t, d_theoryId) ? 1 : tval;
+}
+
 }  // namespace cvc5
diff --git a/src/expr/term_context.h b/src/expr/term_context.h
index 37d2ef6bd..db08372ef 100644
--- a/src/expr/term_context.h
+++ b/src/expr/term_context.h
@@ -19,6 +19,7 @@
 #define CVC5__EXPR__TERM_CONTEXT_H
 
 #include "expr/node.h"
+#include "theory/theory_id.h"
 
 namespace cvc5 {
 
@@ -164,6 +165,23 @@ class PolarityTermContext : public TermContext
   static void getFlags(uint32_t val, bool& hasPol, bool& pol);
 };
 
+/**
+ * Similar to InQuantTermContext, but computes whether we are below a theory
+ * leaf of given theory id.
+ */
+class TheoryLeafTermContext : public TermContext
+{
+ public:
+  TheoryLeafTermContext(theory::TheoryId id) : d_theoryId(id) {}
+  /** The initial value: not beneath a theory leaf. */
+  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;
+
+ private:
+  theory::TheoryId d_theoryId;
+};
+
 }  // namespace cvc5
 
 #endif /* CVC5__EXPR__TERM_CONVERSION_PROOF_GENERATOR_H */