Add proof elaboration for MACRO_BOOL_BV_INVERT_SOLVE (cvc5#11701)

Author: ajreynol

src/rewriter/basic_rewrite_rcons.cpp

@@ -195,6 +195,12 @@ void BasicRewriteRCons::ensureProofForTheoryRewrite(CDProof* cdp,
         handledMacro = true;
       }
       break;
+    case ProofRewriteRule::MACRO_BOOL_BV_INVERT_SOLVE:
+      if (ensureProofMacroBoolBvInvertSolve(cdp, eq))
+      {
+        handledMacro = true;
+      }
+      break;
     case ProofRewriteRule::MACRO_ARITH_INT_EQ_CONFLICT:
     case ProofRewriteRule::MACRO_ARITH_INT_GEQ_TIGHTEN:
       if (ensureProofMacroArithIntRelation(cdp, eq))
@@ -370,6 +376,22 @@ bool BasicRewriteRCons::ensureProofMacroBoolNnfNorm(CDProof* cdp,
   return true;
 }
 
+bool BasicRewriteRCons::ensureProofMacroBoolBvInvertSolve(CDProof* cdp,
+                                                          const Node& eq)
+{
+  Trace("brc-macro") << "Expand Bool BV invert solve " << eq[0]
+                     << " == " << eq[1] << std::endl;
+  Assert(eq[0].getKind() == Kind::EQUAL);
+  Assert(eq[0][0].getKind() == Kind::EQUAL
+         && eq[0][1].getKind() == Kind::EQUAL);
+  std::unordered_set<Kind> disallowedKinds;
+  theory::booleans::TheoryBoolRewriter::getBvInvertSolve(
+      nodeManager(), eq[0][0], eq[0][1][0], disallowedKinds, cdp);
+  // finish proof
+  cdp->addStep(eq, ProofRule::TRUE_INTRO, {eq[0]}, {});
+  return true;
+}
+
 bool BasicRewriteRCons::ensureProofMacroArithIntRelation(CDProof* cdp,
                                                          const Node& eq)
 {

src/rewriter/basic_rewrite_rcons.h

@@ -130,6 +130,16 @@ class BasicRewriteRCons : protected EnvObj
    * @return true if added a closed proof of eq to cdp.
    */
   bool ensureProofMacroBoolNnfNorm(CDProof* cdp, const Node& eq);
+  /**
+   * Elaborate a rewrite eq that was proven by
+   * ProofRewriteRule::MACRO_BOOL_BV_INVERT_SOLVE.
+   *
+   * @param cdp The proof to add to.
+   * @param eq The rewrite proven by
+   * ProofRewriteRule::MACRO_BOOL_BV_INVERT_SOLVE.
+   * @return true if added a closed proof of eq to cdp.
+   */
+  bool ensureProofMacroBoolBvInvertSolve(CDProof* cdp, const Node& eq);
   /**
    * Elaborate a rewrite eq that was proven by
    * ProofRewriteRule::MACRO_ARITH_INT_EQ_CONFLICT or

src/theory/booleans/theory_bool_rewriter.cpp

@@ -316,7 +316,7 @@ Node TheoryBoolRewriter::getBvInvertSolve(
 {
   quantifiers::BvInverter binv;
   // solve for the variable on this path using the inverter
-  std::vector<unsigned> path;
+  std::vector<uint32_t> path;
   Node slit = binv.getPathToPv(lit, var, path);
   // check if the path had a kind that does not preserve equivalence of the
   // overall literal
@@ -331,7 +331,7 @@ Node TheoryBoolRewriter::getBvInvertSolve(
         slit = Node::null();
         break;
       }
-      unsigned p = path[npath - i - 1];
+      uint32_t p = path[npath - i - 1];
       curr = curr[p];
     }
     Assert(slit.isNull() || curr == var);
@@ -346,7 +346,7 @@ Node TheoryBoolRewriter::getBvInvertSolve(
     Node curr = lit;
     for (size_t i = 0, npath = path.size(); i < npath; i++)
     {
-      unsigned p = path[npath - i - 1];
+      uint32_t p = path[npath - i - 1];
       curr = curr[p];
       ts.push_back(curr);
     }