From ad5fa9433f486b088e9459b85ba69510fcf2b8c6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 21 Oct 2022 09:25:45 -0700 Subject: [PATCH] add experiment with quot-rem encoding experiment seeks to determine whether quot-rem encoding can substitute the division circuit encoding. A first test suggests it makes no difference. --- src/smt/theory_bv.cpp | 10 +++++++--- src/solver/assertions/asserted_formulas.cpp | 2 +- 2 files changed, 8 insertions(+), 4 deletions(-) diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp index f195e0c9d..922eafcf6 100644 --- a/src/smt/theory_bv.cpp +++ b/src/smt/theory_bv.cpp @@ -24,6 +24,7 @@ Revision History: #include "smt/smt_model_generator.h" #include "util/stats.h" +#define ENABLE_QUOT_REM_ENCODING 0 namespace smt { @@ -898,8 +899,11 @@ namespace smt { case OP_BSUB: internalize_sub(term); return true; case OP_BMUL: internalize_mul(term); return true; case OP_BSDIV_I: internalize_sdiv(term); return true; +#if ENABLE_QUOT_REM_ENCODING + case OP_BUDIV_I: internalize_udiv_quot_rem(term); return true; +#else case OP_BUDIV_I: internalize_udiv(term); return true; - // case OP_BUDIV_I: internalize_udiv_quot_rem(term); return true; +#endif case OP_BSREM_I: internalize_srem(term); return true; case OP_BUREM_I: internalize_urem(term); return true; case OP_BSMOD_I: internalize_smod(term); return true; @@ -1394,7 +1398,7 @@ namespace smt { ctx.mark_as_relevant(n->get_arg(0)); assert_int2bv_axiom(n); } -#if 0 +#if ENABLE_QUOT_REM_ENCODING else if (m_util.is_bv_udivi(n)) { ctx.mark_as_relevant(n->get_arg(0)); ctx.mark_as_relevant(n->get_arg(1)); @@ -1994,7 +1998,7 @@ namespace smt { return true; } -#if 0 +#if ENABLE_QUOT_REM_ENCODING void theory_bv::internalize_udiv_quot_rem(app* n) { process_args(n); mk_enode(n); diff --git a/src/solver/assertions/asserted_formulas.cpp b/src/solver/assertions/asserted_formulas.cpp index 630d73945..90c84e7ee 100644 --- a/src/solver/assertions/asserted_formulas.cpp +++ b/src/solver/assertions/asserted_formulas.cpp @@ -332,8 +332,8 @@ bool asserted_formulas::invoke(simplify_fmls& s) { IF_VERBOSE(10000, verbose_stream() << "total size: " << get_total_size() << "\n";); TRACE("reduce_step_ll", ast_mark visited; display_ll(tout, visited);); CASSERT("well_sorted",check_well_sorted()); + TRACE("after_reduce", display(tout << s.id() << "\n");); if (inconsistent() || canceled()) { - TRACE("after_reduce", display(tout);); TRACE("after_reduce_ll", ast_mark visited; display_ll(tout, visited);); return false; }