diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2021-03-05 19:28:19 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-03-05 21:28:19 -0600 |
commit | 59d9aad4839e64e0f6d6b57ff112c418ffbbe9fb (patch) | |
tree | d0df100653994157bc631e9ca7fe422dd78e29ff /src/theory/bv/theory_bv.h | |
parent | c6fffe4fd328401f7f7e0757303e8dea5f6c14a4 (diff) |
Remove partial UDIV/UREM operators. (#6069)
This commit removes the partial UDIV/UREM operator handling. BITVECTOR_UDIV and BITVECTOR_UREM are now total.
Diffstat (limited to 'src/theory/bv/theory_bv.h')
-rw-r--r-- | src/theory/bv/theory_bv.h | 15 |
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; |