More

src/CMakeLists.txt

@@ -643,6 +643,8 @@ libcvc5_add_sources(
   theory/bv/bitblast/node_bitblaster.h
   theory/bv/bitblast/proof_bitblaster.cpp
   theory/bv/bitblast/proof_bitblaster.h
+  theory/bv/bv_pp_assert.cpp
+  theory/bv/bv_pp_assert.h
   theory/bv/bv_solver.h
   theory/bv/bv_solver_bitblast.cpp
   theory/bv/bv_solver_bitblast.h

src/theory/bv/bv_pp_assert.cpp

@@ -0,0 +1,100 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2024 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Method for handling cases of TheoryBv::ppAssert.
+ */
+
+#include "theory/bv/bv_pp_assert.h"
+
+#include "theory/bv/theory_bv_utils.h"
+#include "proof/proof.h"
+#include "theory/trust_substitutions.h"
+#include "expr/skolem_manager.h"
+
+namespace cvc5::internal {
+namespace theory {
+namespace bv {
+
+BvPpAssert::BvPpAssert(Env& env,
+              Valuation val) : EnvObj(env), d_valuation(val){}
+BvPpAssert::~BvPpAssert() {}
+bool BvPpAssert::ppAssert(TrustNode tin,
+                        TrustSubstitutionMap& outSubstitutions)
+{
+  /**
+    * Eliminate extract over bit-vector variables.
+    *
+    * Given x[h:l] = c, where c is a constant and x is a variable.
+    *
+    * We rewrite to:
+    *
+    * x = sk1::c       if l == 0, where bw(sk1) = bw(x)-1-h
+    * x = c::sk2       if h == bw(x)-1, where bw(sk2) = l
+    * x = sk1::c::sk2  otherwise, where bw(sk1) = bw(x)-1-h and bw(sk2) = l
+    */
+  Node node = rewrite(tin.getNode());
+  if ((node[0].getKind() == Kind::BITVECTOR_EXTRACT && node[1].isConst())
+      || (node[1].getKind() == Kind::BITVECTOR_EXTRACT && node[0].isConst()))
+  {
+    Node extract = node[0].isConst() ? node[1] : node[0];
+    if (extract[0].isVar())
+    {
+      Node c = node[0].isConst() ? node[0] : node[1];
+
+      uint32_t high = utils::getExtractHigh(extract);
+      uint32_t low = utils::getExtractLow(extract);
+      uint32_t var_bw = utils::getSize(extract[0]);
+      std::vector<Node> children;
+
+      SkolemManager* sm = nodeManager()->getSkolemManager();
+      // create sk1 with size bw(x)-1-h
+      if (low == 0 || high != var_bw - 1)
+      {
+        Assert(high != var_bw - 1);
+        Node ext = utils::mkExtract(extract[0], var_bw - 1, high + 1);
+        Node skolem = sm->mkPurifySkolem(ext);
+        children.push_back(skolem);
+      }
+
+      children.push_back(c);
+
+      // create sk2 with size l
+      if (high == var_bw - 1 || low != 0)
+      {
+        Assert(low != 0);
+        Node ext = utils::mkExtract(extract[0], low - 1, 0);
+        Node skolem = sm->mkPurifySkolem(ext);
+        children.push_back(skolem);
+      }
+
+      Node concat = utils::mkConcat(children);
+      Assert(utils::getSize(concat) == utils::getSize(extract[0]));
+      if (d_valuation.isLegalElimination(extract[0], concat))
+      {
+        outSubstitutions.addSubstitutionSolved(extract[0], concat, tin);
+        return true;
+      }
+    }
+  }
+  return false;
+}
+std::shared_ptr<ProofNode> BvPpAssert::getProofFor(Node fact) 
+{
+  return nullptr;
+}
+
+std::string BvPpAssert::identify() const { return "BvPpAssert"; }
+
+
+}
+}
+}  // namespace cvc5::internal

src/theory/bv/bv_pp_assert.h

@@ -0,0 +1,60 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2024 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Method for handling cases of TheoryBv::ppAssert.
+ */
+
+#include "cvc5_private.h"
+
+#ifndef CVC5__THEORY__BV__BV_PP_ASSERT_H
+#define CVC5__THEORY__BV__BV_PP_ASSERT_H
+
+#include "smt/env_obj.h"
+#include "theory/valuation.h"
+#include "proof/trust_node.h"
+#include "proof/proof_generator.h"
+
+namespace cvc5::internal {
+namespace theory {
+
+class TrustSubstitutionMap;
+
+namespace bv {
+
+class BvPpAssert : protected EnvObj, public ProofGenerator
+{
+ public:
+  /**
+   * Constructor.
+   */
+  BvPpAssert(Env& env,
+              Valuation val);
+  ~BvPpAssert();
+  /**
+   */
+  bool ppAssert(TrustNode tin,
+                          TrustSubstitutionMap& outSubstitutions);
+  /**
+   */
+  std::shared_ptr<ProofNode> getProofFor(Node fact) override;
+  /** identify */
+  std::string identify() const override;
+private:
+  /** The valuation proxy. */
+  Valuation d_valuation;
+};
+
+}
+}
+}  // namespace cvc5::internal
+
+#endif /* CVC5__THEORY__BV__BV_PP_ASSERT_H */

src/theory/bv/rewrites

@@ -58,6 +58,8 @@
   (extract j i (concat x xs y))
   (extract j i (concat xs y)))
 
+; Motivated by TheoryBv::ppAssert, which turns an equality involving
+; extract into a solved form for the variable we are extracting from.
 (define-cond-rule bv-eq-extract-elim
   ((x ?BitVec) (y ?BitVec) (i Int) (j Int) (wm1 Int) (jp1 Int) (im1 Int))
   (and (= wm1 (- (@bvsize x) 1)) (= jp1 (+ j 1)) (= im1 (- i 1)))

src/theory/bv/theory_bv.cpp

@@ -25,7 +25,6 @@
 #include "theory/bv/theory_bv_rewrite_rules_simplification.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/ee_setup_info.h"
-#include "theory/trust_substitutions.h"
 #include "theory/uf/equality_engine.h"
 
 namespace cvc5::internal {
@@ -38,6 +37,7 @@ TheoryBV::TheoryBV(Env& env,
                    std::string name)
     : Theory(THEORY_BV, env, out, valuation, name),
       d_internal(nullptr),
+      d_ppAssert(env, valuation),
       d_rewriter(nodeManager()),
       d_state(env, valuation),
       d_im(env, *this, d_state, "theory::bv::"),
@@ -191,61 +191,6 @@ Theory::PPAssertStatus TheoryBV::ppAssert(
     {
       return status;
     }
-    /**
-     * Eliminate extract over bit-vector variables.
-     *
-     * Given x[h:l] = c, where c is a constant and x is a variable.
-     *
-     * We rewrite to:
-     *
-     * x = sk1::c       if l == 0, where bw(sk1) = bw(x)-1-h
-     * x = c::sk2       if h == bw(x)-1, where bw(sk2) = l
-     * x = sk1::c::sk2  otherwise, where bw(sk1) = bw(x)-1-h and bw(sk2) = l
-     */
-    Node node = rewrite(tin.getNode());
-    if ((node[0].getKind() == Kind::BITVECTOR_EXTRACT && node[1].isConst())
-        || (node[1].getKind() == Kind::BITVECTOR_EXTRACT && node[0].isConst()))
-    {
-      Node extract = node[0].isConst() ? node[1] : node[0];
-      if (extract[0].isVar())
-      {
-        Node c = node[0].isConst() ? node[0] : node[1];
-
-        uint32_t high = utils::getExtractHigh(extract);
-        uint32_t low = utils::getExtractLow(extract);
-        uint32_t var_bw = utils::getSize(extract[0]);
-        std::vector<Node> children;
-
-        SkolemManager* sm = nodeManager()->getSkolemManager();
-        // create sk1 with size bw(x)-1-h
-        if (low == 0 || high != var_bw - 1)
-        {
-          Assert(high != var_bw - 1);
-          Node ext = utils::mkExtract(extract[0], var_bw - 1, high + 1);
-          Node skolem = sm->mkPurifySkolem(ext);
-          children.push_back(skolem);
-        }
-
-        children.push_back(c);
-
-        // create sk2 with size l
-        if (high == var_bw - 1 || low != 0)
-        {
-          Assert(low != 0);
-          Node ext = utils::mkExtract(extract[0], low - 1, 0);
-          Node skolem = sm->mkPurifySkolem(ext);
-          children.push_back(skolem);
-        }
-
-        Node concat = utils::mkConcat(children);
-        Assert(utils::getSize(concat) == utils::getSize(extract[0]));
-        if (isLegalElimination(extract[0], concat))
-        {
-          outSubstitutions.addSubstitutionSolved(extract[0], concat, tin);
-          return Theory::PP_ASSERT_STATUS_SOLVED;
-        }
-      }
-    }
   }
   return Theory::PP_ASSERT_STATUS_UNSOLVED;
 }

src/theory/bv/theory_bv.h

@@ -19,6 +19,7 @@
 #define CVC5__THEORY__BV__THEORY_BV_H
 
 #include "theory/bv/proof_checker.h"
+#include "theory/bv/bv_pp_assert.h"
 #include "theory/bv/theory_bv_rewriter.h"
 #include "theory/theory.h"
 #include "theory/theory_eq_notify.h"
@@ -106,6 +107,9 @@ class TheoryBV : public Theory
   /** Internal BV solver. */
   std::unique_ptr<BVSolver> d_internal;
 
+  /** The preprocess assertion utility */
+  BvPpAssert d_ppAssert;
+
   /** The theory rewriter for this theory. */
   TheoryBVRewriter d_rewriter;