From 914bf2ff3b8e0c0bde7e05e97cd4d40272d33df5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 24 Jun 2016 07:43:05 -0700 Subject: [PATCH 1/3] extend constant folding for bit-vector overflow/underflow operators, #657 Signed-off-by: Nikolaj Bjorner --- src/ast/array_decl_plugin.cpp | 2 +- src/ast/rewriter/bit_blaster/bit_blaster.h | 4 +- src/ast/rewriter/bv_rewriter.cpp | 96 +++++++++ src/ast/rewriter/bv_rewriter.h | 3 + src/smt/params/smt_params_helper.pyg | 3 +- src/smt/smt_solver.cpp | 45 +++- src/solver/mus.cpp | 226 ++++++++++++++++----- src/solver/mus.h | 4 + src/solver/solver_na2as.h | 1 + src/solver/tactic2solver.cpp | 5 +- 10 files changed, 332 insertions(+), 57 deletions(-) diff --git a/src/ast/array_decl_plugin.cpp b/src/ast/array_decl_plugin.cpp index 9634e17cb..4ae66707d 100644 --- a/src/ast/array_decl_plugin.cpp +++ b/src/ast/array_decl_plugin.cpp @@ -522,7 +522,7 @@ void array_decl_plugin::get_sort_names(svector& sort_names, symbol void array_decl_plugin::get_op_names(svector& op_names, symbol const & logic) { op_names.push_back(builtin_name("store",OP_STORE)); op_names.push_back(builtin_name("select",OP_SELECT)); - if (logic == symbol::null) { + if (true || logic == symbol::null) { // none of the SMT2 logics support these extensions op_names.push_back(builtin_name("const",OP_CONST_ARRAY)); op_names.push_back(builtin_name("map",OP_ARRAY_MAP)); diff --git a/src/ast/rewriter/bit_blaster/bit_blaster.h b/src/ast/rewriter/bit_blaster/bit_blaster.h index 6221eeaf9..4feeb6f5a 100644 --- a/src/ast/rewriter/bit_blaster/bit_blaster.h +++ b/src/ast/rewriter/bit_blaster/bit_blaster.h @@ -20,8 +20,8 @@ Revision History: #define BIT_BLASTER_H_ #include"bool_rewriter.h" -#include"bit_blaster_params.h" -#include"bit_blaster_tpl.h" +#include"bit_blaster/bit_blaster_params.h" +#include"bit_blaster/bit_blaster_tpl.h" #include"bv_decl_plugin.h" #include"rational.h" diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp index def05f014..d876dc8cb 100644 --- a/src/ast/rewriter/bv_rewriter.cpp +++ b/src/ast/rewriter/bv_rewriter.cpp @@ -20,6 +20,7 @@ Notes: #include"bv_rewriter_params.hpp" #include"poly_rewriter_def.h" #include"ast_smt2_pp.h" +#include"bit_blaster/bit_blaster.h" void bv_rewriter::updt_local_params(params_ref const & _p) { @@ -189,6 +190,15 @@ br_status bv_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * cons return mk_bv_comp(args[0], args[1], result); case OP_MKBV: return mk_mkbv(num_args, args, result); + case OP_BUMUL_NO_OVFL: + SASSERT(num_args == 2); + return mk_bv_umul_no_ovfl(args[0], args[1], result); + case OP_BSMUL_NO_OVFL: + SASSERT(num_args == 2); + return mk_bv_smul_no_ovfl(args[0], args[1], result); + case OP_BSMUL_NO_UDFL: + SASSERT(num_args == 2); + return mk_bv_smul_no_udfl(args[0], args[1], result); default: return BR_FAILED; } @@ -1100,6 +1110,92 @@ br_status bv_rewriter::mk_concat(unsigned num_args, expr * const * args, expr_re return BR_DONE; } +br_status bv_rewriter::mk_bv_umul_no_ovfl(expr * arg1, expr * arg2, expr_ref& result) { + rational val1, val2; + unsigned bv_size; + bool is_num1 = is_numeral(arg1, val1, bv_size); + bool is_num2 = is_numeral(arg2, val2, bv_size); + if (is_num1 && (val1.is_zero() || val1.is_one())) { + result = m().mk_true(); + return BR_DONE; + } + if (is_num2 && (val2.is_zero() || val2.is_one())) { + result = m().mk_true(); + return BR_DONE; + } + if (is_num1 && is_num2) { + SASSERT(!val1.is_neg()); + SASSERT(!val2.is_neg()); + rational r = val1 * val2; + result = m().mk_bool_val(r < rational(2).expt(bv_size)); + return BR_DONE; + } + return BR_FAILED; +} + +br_status bv_rewriter::mk_bv_smul_no_ovfl(expr * arg1, expr * arg2, expr_ref& result) { + rational val1, val2; + unsigned bv_size; + bool is_num1 = is_numeral(arg1, val1, bv_size); + bool is_num2 = is_numeral(arg2, val2, bv_size); + if (is_num1 && (val1.is_zero() || val1.is_one())) { + result = m().mk_true(); + return BR_DONE; + } + if (is_num2 && (val2.is_zero() || val2.is_one())) { + result = m().mk_true(); + return BR_DONE; + } + if (is_num1 && is_num2) { + bit_blaster_params params; + bit_blaster blaster(m(), params); + SASSERT(!val1.is_neg()); + SASSERT(!val2.is_neg()); + expr_ref_vector bits1(m()), bits2(m()); + for (unsigned i = 0; i < bv_size; ++i) { + bits1.push_back(m().mk_bool_val(!val1.is_even())); + bits2.push_back(m().mk_bool_val(!val2.is_even())); + val1 = div(val1, rational(2)); + val2 = div(val2, rational(2)); + } + blaster.mk_smul_no_overflow(bits1.size(), bits1.c_ptr(), bits2.c_ptr(), result); + return BR_DONE; + } + return BR_FAILED; +} + +br_status bv_rewriter::mk_bv_smul_no_udfl(expr * arg1, expr * arg2, expr_ref& result) { + rational val1, val2; + unsigned bv_size; + bool is_num1 = is_numeral(arg1, val1, bv_size); + bool is_num2 = is_numeral(arg2, val2, bv_size); + if (is_num1 && (val1.is_zero() || val1.is_one())) { + result = m().mk_true(); + return BR_DONE; + } + if (is_num2 && (val2.is_zero() || val2.is_one())) { + result = m().mk_true(); + return BR_DONE; + } + if (is_num1 && is_num2) { + bit_blaster_params params; + bit_blaster blaster(m(), params); + SASSERT(!val1.is_neg()); + SASSERT(!val2.is_neg()); + expr_ref_vector bits1(m()), bits2(m()); + for (unsigned i = 0; i < bv_size; ++i) { + bits1.push_back(m().mk_bool_val(!val1.is_even())); + bits2.push_back(m().mk_bool_val(!val2.is_even())); + val1 = div(val1, rational(2)); + val2 = div(val2, rational(2)); + } + blaster.mk_smul_no_underflow(bits1.size(), bits1.c_ptr(), bits2.c_ptr(), result); + return BR_DONE; + } + return BR_FAILED; +} + + br_status bv_rewriter::mk_zero_extend(unsigned n, expr * arg, expr_ref & result) { if (n == 0) { result = arg; diff --git a/src/ast/rewriter/bv_rewriter.h b/src/ast/rewriter/bv_rewriter.h index 7135c52ba..0b449d006 100644 --- a/src/ast/rewriter/bv_rewriter.h +++ b/src/ast/rewriter/bv_rewriter.h @@ -114,6 +114,9 @@ class bv_rewriter : public poly_rewriter { br_status mk_bv_srem_i(expr * arg1, expr * arg2, expr_ref & result) { return mk_bv_srem_core(arg1, arg2, true, result); } br_status mk_bv_urem_i(expr * arg1, expr * arg2, expr_ref & result) { return mk_bv_urem_core(arg1, arg2, true, result); } br_status mk_bv_smod_i(expr * arg1, expr * arg2, expr_ref & result) { return mk_bv_smod_core(arg1, arg2, true, result); } + br_status mk_bv_umul_no_ovfl(expr * arg1, expr * arg2, expr_ref& result); + br_status mk_bv_smul_no_ovfl(expr * arg1, expr * arg2, expr_ref& result); + br_status mk_bv_smul_no_udfl(expr * arg1, expr * arg2, expr_ref& result); br_status mk_int2bv(unsigned bv_size, expr * arg, expr_ref & result); br_status mk_bv2int(expr * arg, expr_ref & result); br_status mk_bv_redor(expr * arg, expr_ref & result); diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index a9f6ccc18..153d948f5 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -61,5 +61,6 @@ def_module_params(module_name='smt', ('dack.gc', UINT, 2000, 'Dynamic ackermannization garbage collection frequency (per conflict)'), ('dack.gc_inv_decay', DOUBLE, 0.8, 'Dynamic ackermannization garbage collection decay'), ('dack.threshold', UINT, 10, ' number of times the congruence rule must be used before Leibniz\'s axiom is expanded'), - ('core.validate', BOOL, False, 'validate unsat core produced by SMT context') + ('core.validate', BOOL, False, 'validate unsat core produced by SMT context'), + ('core.minimize', BOOL, False, 'minimize unsat core produced by SMT context') )) diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index 59c08006b..d7764ac64 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -20,19 +20,25 @@ Notes: #include"smt_kernel.h" #include"reg_decl_plugins.h" #include"smt_params.h" +#include"smt_params_helper.hpp" +#include"mus.h" namespace smt { class solver : public solver_na2as { - smt_params m_params; + smt_params m_smt_params; + params_ref m_params; smt::kernel m_context; progress_callback * m_callback; symbol m_logic; + bool m_minimizing_core; public: solver(ast_manager & m, params_ref const & p, symbol const & l): solver_na2as(m), + m_smt_params(p), m_params(p), - m_context(m, m_params) { + m_context(m, m_smt_params), + m_minimizing_core(false) { m_logic = l; if (m_logic != symbol::null) m_context.set_logic(m_logic); @@ -48,7 +54,8 @@ namespace smt { } virtual void updt_params(params_ref const & p) { - m_params.updt_params(p); + m_smt_params.updt_params(p); + m_params.copy(p); m_context.updt_params(p); } @@ -77,10 +84,40 @@ namespace smt { return m_context.check(num_assumptions, assumptions); } + struct scoped_minimize_core { + solver& s; + expr_ref_vector m_assumptions; + scoped_minimize_core(solver& s): s(s), m_assumptions(s.m_assumptions) { + s.m_minimizing_core = true; + s.m_assumptions.reset(); + } + + ~scoped_minimize_core() { + s.m_minimizing_core = false; + s.m_assumptions.append(m_assumptions); + } + }; + virtual void get_unsat_core(ptr_vector & r) { unsigned sz = m_context.get_unsat_core_size(); - for (unsigned i = 0; i < sz; i++) + for (unsigned i = 0; i < sz; i++) { r.push_back(m_context.get_unsat_core_expr(i)); + } + + if (m_minimizing_core || smt_params_helper(m_params).core_minimize() == false) { + return; + } + scoped_minimize_core scm(*this); + mus mus(*this); + + for (unsigned i = 0; i < r.size(); ++i) { + VERIFY(i == mus.add_soft(r[i])); + } + ptr_vector r2; + if (l_true == mus.get_mus(r2)) { + r.reset(); + r.append(r2); + } } virtual void get_model(model_ref & m) { diff --git a/src/solver/mus.cpp b/src/solver/mus.cpp index 4960a3d2a..5f856cd80 100644 --- a/src/solver/mus.cpp +++ b/src/solver/mus.cpp @@ -26,6 +26,9 @@ Notes: struct mus::imp { + + typedef obj_hashtable expr_set; + solver& m_solver; ast_manager& m; expr_ref_vector m_lit2expr; @@ -64,66 +67,73 @@ struct mus::imp { SASSERT(is_literal(lit)); m_assumptions.push_back(lit); } + + lbool get_mus(ptr_vector& mus) { + unsigned_vector result; + lbool r = get_mus(result); + ids2exprs(mus, result); + return r; + } - lbool get_mus(unsigned_vector& mus) { - // SASSERT: mus does not have duplicates. + lbool get_mus(unsigned_vector& mus_ids) { + // SASSERT: mus_ids does not have duplicates. m_model.reset(); - unsigned_vector core; - for (unsigned i = 0; i < m_lit2expr.size(); ++i) { - core.push_back(i); - } - if (core.size() == 1) { - mus.push_back(core.back()); + mus_ids.reset(); + + if (m_lit2expr.size() == 1) { + mus_ids.push_back(0); return l_true; } + + return get_mus1(mus_ids); + } - mus.reset(); - if (false && core.size() > 64) { - return qx(mus); + lbool get_mus1(unsigned_vector& mus_ids) { + expr_ref_vector mus(m); + lbool result = get_mus1(mus); + for (unsigned i = 0; i < mus.size(); ++i) { + mus_ids.push_back(m_expr2lit.find(mus[i].get())); } + return result; + } - expr_ref_vector assumptions(m); + + lbool get_mus1(expr_ref_vector& mus) { + ptr_vector unknown(m_lit2expr.size(), m_lit2expr.c_ptr()); ptr_vector core_exprs; - while (!core.empty()) { - IF_VERBOSE(12, verbose_stream() << "(opt.mus reducing core: " << core.size() << " new core: " << mus.size() << ")\n";); - unsigned lit_id = core.back(); - TRACE("opt", - display_vec(tout << "core: ", core); - display_vec(tout << "mus: ", mus); - ); - core.pop_back(); - expr* lit = m_lit2expr[lit_id].get(); - expr_ref not_lit(m); - not_lit = mk_not(m, lit); + while (!unknown.empty()) { + IF_VERBOSE(12, verbose_stream() << "(opt.mus reducing core: " << unknown.size() << " new core: " << mus.size() << ")\n";); + TRACE("opt", display_vec(tout << "core: ", unknown); display_vec(tout << "mus: ", mus);); + expr* lit = unknown.back(); + unknown.pop_back(); + expr_ref not_lit(mk_not(m, lit), m); lbool is_sat = l_undef; { - scoped_append _sa1(*this, assumptions, core); - scoped_append _sa2(*this, assumptions, m_assumptions); - assumptions.push_back(not_lit); - is_sat = m_solver.check_sat(assumptions); + scoped_append _sa1(*this, mus, unknown); + scoped_append _sa2(*this, mus, m_assumptions); + mus.push_back(not_lit); + is_sat = m_solver.check_sat(mus); } switch (is_sat) { case l_undef: return is_sat; case l_true: - assumptions.push_back(lit); - mus.push_back(lit_id); + mus.push_back(lit); update_model(); break; default: core_exprs.reset(); m_solver.get_unsat_core(core_exprs); if (!core_exprs.contains(not_lit)) { - // core := core_exprs \ mus - core.reset(); + // unknown := core_exprs \ mus + unknown.reset(); for (unsigned i = 0; i < core_exprs.size(); ++i) { - lit = core_exprs[i]; - if (m_expr2lit.find(lit, lit_id) && !mus.contains(lit_id)) { - core.push_back(lit_id); + if (!mus.contains(core_exprs[i])) { + unknown.push_back(core_exprs[i]); } } TRACE("opt", display_vec(tout << "core exprs:", core_exprs); - display_vec(tout << "core:", core); + display_vec(tout << "core:", unknown); display_vec(tout << "mus:", mus); ); @@ -131,19 +141,118 @@ struct mus::imp { break; } } -#if 0 - DEBUG_CODE( - assumptions.reset(); - for (unsigned i = 0; i < mus.size(); ++i) { - assumptions.push_back(m_lit2expr[mus[i]].get()); - } - lbool is_sat = m_solver.check_sat(assumptions.size(), assumptions.c_ptr()); - SASSERT(is_sat == l_false); - ); -#endif + // SASSERT(is_core(mus)); return l_true; } + // use correction sets + lbool get_mus2(expr_ref_vector& mus) { + scoped_append _sa1(*this, mus, m_assumptions); + ptr_vector unknown(m_lit2expr.size(), m_lit2expr.c_ptr()); + while (!unknown.empty()) { + expr* lit; + lbool is_sat = get_next_mcs(mus, unknown, lit); + switch (is_sat) { + case l_undef: + return is_sat; + case l_false: + mus.push_back(lit); + break; + case l_true: + break; + } + } + return l_true; + } + + // find the next literal to be a member of a core. + lbool get_next_mcs(expr_ref_vector& mus, ptr_vector& unknown, expr*& core_literal) { + ptr_vector mss, core, min_core; + bool min_core_valid = false; + expr* min_lit = 0; + while (!unknown.empty()) { + expr* lit = unknown.back(); + unknown.pop_back(); + model_ref mdl; + scoped_append assume_mss(*this, mus, mss); + scoped_append assume_lit(*this, mus, lit); + switch (m_solver.check_sat(mus)) { + case l_true: + mss.push_back(lit); + m_solver.get_model(mdl); + for (unsigned i = 0; i < unknown.size(); ) { + expr_ref tmp(m); + if (mdl->eval(unknown[i], tmp) && m.is_true(tmp)) { + mss.push_back(unknown[i]); + unknown[i] = unknown.back(); + unknown.pop_back(); + } + else { + ++i; + } + } + break; + case l_false: + core.reset(); + m_solver.get_unsat_core(core); + // ??? + if (!core.contains(lit)) { + return l_false; + } + if (!min_core_valid || core.size() < min_core.size()) { + min_core.reset(); + min_core.append(core); + min_core_valid = true; + min_lit = lit; + } + break; + case l_undef: + return l_undef; + } + } + if (!min_core_valid) { + // ??? + UNREACHABLE(); + return l_true; + } + else { + for (unsigned i = 0; i < min_core.size(); ++i) { + if (mss.contains(min_core[i]) && min_lit != min_core[i]) { + unknown.push_back(min_core[i]); + } + } + core_literal = min_lit; + } + return l_false; + } + + expr* lit2expr(unsigned lit_id) const { + return m_lit2expr[lit_id]; + } + + void ids2exprs(ptr_vector& dst, unsigned_vector const& ids) const { + for (unsigned i = 0; i < ids.size(); ++i) { + dst.push_back(lit2expr(ids[i])); + } + } + + bool is_core(unsigned_vector const& mus_ids) { + ptr_vector mus_exprs; + ids2exprs(mus_exprs, mus_ids); + return l_false == m_solver.check_sat(mus_exprs.size(), mus_exprs.c_ptr()); + } + + // dst := A \ B + void set_difference(unsigned_vector& dst, ptr_vector const& A, unsigned_vector const& B) { + dst.reset(); + for (unsigned i = 0; i < A.size(); ++i) { + unsigned lit_id; + if (m_expr2lit.find(A[i], lit_id) && !B.contains(lit_id)) { + dst.push_back(lit_id); + } + } + } + class scoped_append { expr_ref_vector& m_fmls; unsigned m_size; @@ -152,7 +261,7 @@ struct mus::imp { m_fmls(fmls1), m_size(fmls1.size()) { for (unsigned i = 0; i < fmls2.size(); ++i) { - fmls1.push_back(imp.m_lit2expr[fmls2[i]].get()); + fmls1.push_back(imp.lit2expr(fmls2[i])); } } scoped_append(imp& imp, expr_ref_vector& fmls1, uint_set const& fmls2): @@ -160,7 +269,7 @@ struct mus::imp { m_size(fmls1.size()) { uint_set::iterator it = fmls2.begin(), end = fmls2.end(); for (; it != end; ++it) { - fmls1.push_back(imp.m_lit2expr[*it].get()); + fmls1.push_back(imp.lit2expr(*it)); } } scoped_append(imp& imp, expr_ref_vector& fmls1, expr_ref_vector const& fmls2): @@ -168,6 +277,16 @@ struct mus::imp { m_size(fmls1.size()) { fmls1.append(fmls2); } + scoped_append(imp& imp, expr_ref_vector& fmls1, ptr_vector const& fmls2): + m_fmls(fmls1), + m_size(fmls1.size()) { + fmls1.append(fmls2.size(), fmls2.c_ptr()); + } + scoped_append(imp& imp, expr_ref_vector& fmls1, expr* fml): + m_fmls(fmls1), + m_size(fmls1.size()) { + fmls1.push_back(fml); + } ~scoped_append() { m_fmls.shrink(m_size); } @@ -175,7 +294,7 @@ struct mus::imp { void add_core(unsigned_vector const& core, expr_ref_vector& assumptions) { for (unsigned i = 0; i < core.size(); ++i) { - assumptions.push_back(m_lit2expr[core[i]].get()); + assumptions.push_back(lit2expr(core[i])); } } @@ -359,6 +478,17 @@ lbool mus::get_mus(unsigned_vector& mus) { return m_imp->get_mus(mus); } +lbool mus::get_mus(ptr_vector& mus) { + return m_imp->get_mus(mus); +} + +lbool mus::get_mus(expr_ref_vector& mus) { + ptr_vector result; + lbool r = m_imp->get_mus(result); + mus.append(result.size(), result.c_ptr()); + return r; +} + void mus::reset() { m_imp->reset(); diff --git a/src/solver/mus.h b/src/solver/mus.h index d2411b6ec..bb3c6508f 100644 --- a/src/solver/mus.h +++ b/src/solver/mus.h @@ -44,6 +44,10 @@ class mus { void add_assumption(expr* lit); lbool get_mus(unsigned_vector& mus); + + lbool get_mus(ptr_vector& mus); + + lbool get_mus(expr_ref_vector& mus); void reset(); diff --git a/src/solver/solver_na2as.h b/src/solver/solver_na2as.h index 019468fd7..9aeb56fb1 100644 --- a/src/solver/solver_na2as.h +++ b/src/solver/solver_na2as.h @@ -25,6 +25,7 @@ Notes: #include"solver.h" class solver_na2as : public solver { + protected: ast_manager & m; expr_ref_vector m_assumptions; unsigned_vector m_scopes; diff --git a/src/solver/tactic2solver.cpp b/src/solver/tactic2solver.cpp index 56b246c1e..2a00d7195 100644 --- a/src/solver/tactic2solver.cpp +++ b/src/solver/tactic2solver.cpp @@ -23,6 +23,7 @@ Notes: #include"tactic.h" #include"ast_pp_util.h" #include"ast_translation.h" +#include"mus.h" /** \brief Simulates the incremental solver interface using a tactic. @@ -42,6 +43,7 @@ class tactic2solver : public solver_na2as { bool m_produce_proofs; bool m_produce_unsat_cores; statistics m_stats; + public: tactic2solver(ast_manager & m, tactic * t, params_ref const & p, bool produce_proofs, bool produce_models, bool produce_unsat_cores, symbol const & logic); virtual ~tactic2solver(); @@ -203,8 +205,9 @@ void tactic2solver::collect_statistics(statistics & st) const { } void tactic2solver::get_unsat_core(ptr_vector & r) { - if (m_result.get()) + if (m_result.get()) { m_result->get_unsat_core(r); + } } void tactic2solver::get_model(model_ref & m) { From 017165c474bdbd1e7ea3994f943c7e307a7646f5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 24 Jun 2016 09:02:12 -0700 Subject: [PATCH 2/3] fix bug with model completion and remove spurious std::cout Signed-off-by: Nikolaj Bjorner --- src/ast/array_decl_plugin.cpp | 2 +- src/qe/qe_mbp.cpp | 3 +-- src/qe/qsat.cpp | 4 +++- src/solver/mus.cpp | 12 ------------ 4 files changed, 5 insertions(+), 16 deletions(-) diff --git a/src/ast/array_decl_plugin.cpp b/src/ast/array_decl_plugin.cpp index 4ae66707d..ab21c4c88 100644 --- a/src/ast/array_decl_plugin.cpp +++ b/src/ast/array_decl_plugin.cpp @@ -522,7 +522,7 @@ void array_decl_plugin::get_sort_names(svector& sort_names, symbol void array_decl_plugin::get_op_names(svector& op_names, symbol const & logic) { op_names.push_back(builtin_name("store",OP_STORE)); op_names.push_back(builtin_name("select",OP_SELECT)); - if (true || logic == symbol::null) { + if (logic == symbol::null || logic == symbol("HORN")) { // none of the SMT2 logics support these extensions op_names.push_back(builtin_name("const",OP_CONST_ARRAY)); op_names.push_back(builtin_name("map",OP_ARRAY_MAP)); diff --git a/src/qe/qe_mbp.cpp b/src/qe/qe_mbp.cpp index 219a4b45a..85371d8ef 100644 --- a/src/qe/qe_mbp.cpp +++ b/src/qe/qe_mbp.cpp @@ -454,8 +454,7 @@ public: (*p)(model, vars, fmls); } } - while (!vars.empty() && !fmls.empty()) { - std::cout << "mbp: " << var << "\n"; + while (!vars.empty() && !fmls.empty()) { var = vars.back(); vars.pop_back(); project_plugin* p = get_plugin(var); diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp index 02c6d26cd..1bfd53597 100644 --- a/src/qe/qsat.cpp +++ b/src/qe/qsat.cpp @@ -158,6 +158,8 @@ namespace qe { return; } model_evaluator eval(*mdl); + eval.set_model_completion(true); + TRACE("qe", model_v2_pp(tout, *mdl);); expr_ref val(m); for (unsigned j = 0; j < m_preds[level - 1].size(); ++j) { @@ -169,7 +171,7 @@ namespace qe { if (m.is_false(val)) { m_asms.push_back(m.mk_not(p)); } - else { + else { SASSERT(m.is_true(val)); m_asms.push_back(p); } diff --git a/src/solver/mus.cpp b/src/solver/mus.cpp index a5013cd5a..81635f906 100644 --- a/src/solver/mus.cpp +++ b/src/solver/mus.cpp @@ -475,18 +475,6 @@ lbool mus::get_mus(expr_ref_vector& mus) { return m_imp->get_mus(mus); } -lbool mus::get_mus(ptr_vector& mus) { - return m_imp->get_mus(mus); -} - -lbool mus::get_mus(expr_ref_vector& mus) { - ptr_vector result; - lbool r = m_imp->get_mus(result); - mus.append(result.size(), result.c_ptr()); - return r; -} - - void mus::reset() { m_imp->reset(); } From 30cf0d19eb4d842337bf2770587a7473ee01f8d4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 24 Jun 2016 09:11:45 -0700 Subject: [PATCH 3/3] use of mk_bool_val Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/bv_rewriter.cpp | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp index 66546f2f2..07e97364e 100644 --- a/src/ast/rewriter/bv_rewriter.cpp +++ b/src/ast/rewriter/bv_rewriter.cpp @@ -252,7 +252,7 @@ br_status bv_rewriter::mk_leq_core(bool is_signed, expr * a, expr * b, expr_ref r2 = m_util.norm(r2, sz, is_signed); if (is_num1 && is_num2) { - result = r1 <= r2 ? m().mk_true() : m().mk_false(); + result = m().mk_bool_val(r1 <= r2); return BR_DONE; } @@ -1785,7 +1785,7 @@ br_status bv_rewriter::mk_bit2bool(expr * lhs, expr * rhs, expr_ref & result) { if (is_numeral(lhs)) { SASSERT(is_numeral(rhs)); - result = lhs == rhs ? m().mk_true() : m().mk_false(); + result = m().mk_bool_val(lhs == rhs); return BR_DONE; } @@ -2134,7 +2134,7 @@ br_status bv_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) { st = cancel_monomials(lhs, rhs, false, new_lhs, new_rhs); if (st != BR_FAILED) { if (is_numeral(new_lhs) && is_numeral(new_rhs)) { - result = new_lhs == new_rhs ? m().mk_true() : m().mk_false(); + result = m().mk_bool_val(new_lhs == new_rhs); return BR_DONE; } } @@ -2213,7 +2213,7 @@ br_status bv_rewriter::mk_bvsmul_no_overflow(unsigned num, expr * const * args, if (is_num1 && is_num2) { rational mr = a0_val * a1_val; rational lim = rational::power_of_two(bv_sz-1); - result = (mr < lim) ? m().mk_true() : m().mk_false(); + result = m().mk_bool_val(mr < lim); return BR_DONE; } @@ -2239,7 +2239,7 @@ br_status bv_rewriter::mk_bvumul_no_overflow(unsigned num, expr * const * args, if (is_num1 && is_num2) { rational mr = a0_val * a1_val; rational lim = rational::power_of_two(bv_sz); - result = (mr < lim) ? m().mk_true() : m().mk_false(); + result = m().mk_bool_val(mr < lim); return BR_DONE; } @@ -2270,7 +2270,7 @@ br_status bv_rewriter::mk_bvsmul_no_underflow(unsigned num, expr * const * args, rational mr = a0_val * a1_val; rational neg_lim = -lim; TRACE("bv_rewriter_bvsmul_no_underflow", tout << "a0:" << a0_val << " a1:" << a1_val << " mr:" << mr << " neg_lim:" << neg_lim << std::endl;); - result = (mr >= neg_lim) ? m().mk_true() : m().mk_false(); + result = m().mk_bool_val(mr >= neg_lim); return BR_DONE; }