From 6f689c3c1ff59d226e3fbe6c6dcf6f948afa7763 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 22 Jan 2022 12:21:20 +0100 Subject: [PATCH] updates Signed-off-by: Nikolaj Bjorner --- src/ast/bv_decl_plugin.h | 1 + src/test/polysat.cpp | 11 ++++++++++- 2 files changed, 11 insertions(+), 1 deletion(-) diff --git a/src/ast/bv_decl_plugin.h b/src/ast/bv_decl_plugin.h index 1dc2fff5f..598124c5c 100644 --- a/src/ast/bv_decl_plugin.h +++ b/src/ast/bv_decl_plugin.h @@ -376,6 +376,7 @@ public: MATCH_BINARY(is_sge); MATCH_BINARY(is_ugt); MATCH_BINARY(is_sgt); + MATCH_BINARY(is_bv_umul_no_ovfl); MATCH_BINARY(is_bv_ashr); MATCH_BINARY(is_bv_lshr); MATCH_BINARY(is_bv_shl); diff --git a/src/test/polysat.cpp b/src/test/polysat.cpp index de2e32dab..aae954cf7 100644 --- a/src/test/polysat.cpp +++ b/src/test/polysat.cpp @@ -85,7 +85,8 @@ namespace polysat { LOG(m_name << ": " << m_last_result << "\n"); statistics st; collect_statistics(st); - LOG(st << "\n" << *this << "\n"); + // LOG(st << "\n" << *this << "\n"); + std::cout << st << "\n" << *this << "\n"; } void expect_unsat() { @@ -1298,6 +1299,14 @@ public: else s.add_sle(pa, pb); } + else if (bv.is_bv_umul_no_ovfl(fm, a, b)) { + auto pa = to_pdd(m, s, expr2pdd, a); + auto pb = to_pdd(m, s, expr2pdd, b); + if (is_not) + s.add_ovfl(pa, pb); + else + s.add_noovfl(pa, pb); + } else { std::cout << "SKIP: " << mk_pp(fm, m) << "\n"; }