Remove partial UDIV/UREM operators. (#6069)

This commit removes the partial UDIV/UREM operator handling. BITVECTOR_UDIV and BITVECTOR_UREM are now total.

1 files changed, 0 insertions, 15 deletions

diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index fafde0601..685f25a92 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -107,24 +107,9 @@ class TheoryBV : public Theory
  private:
   void notifySharedTerm(TNode t) override;
 
-  /**
-   * Return the UF symbol corresponding to division-by-zero for this particular
-   * bit-width.
-   * @param k should be UREM or UDIV
-   * @param width bit-width
-   */
-  Node getUFDivByZero(Kind k, unsigned width);
-
   /** Internal BV solver. */
   std::unique_ptr<BVSolver> d_internal;
 
-  /**
-   * Maps from bit-vector width to division-by-zero uninterpreted
-   * function symbols.
-   */
-  std::unordered_map<unsigned, Node> d_ufDivByZero;
-  std::unordered_map<unsigned, Node> d_ufRemByZero;
-
   /** The theory rewriter for this theory. */
   TheoryBVRewriter d_rewriter;