From 8491b3bebe2fb756e257b96dae14c9a0ae68dbc1 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sat, 31 Oct 2015 18:51:32 +0000 Subject: [PATCH 01/21] Revert "Fixed use of mk_th_axiom in theory_fpa." This reverts commit 89e99c7b4b1b4d75d016e53bee434d9b4cff6939. --- src/smt/theory_fpa.cpp | 16 +--------------- 1 file changed, 1 insertion(+), 15 deletions(-) diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp index 15caae296..7b8a83520 100644 --- a/src/smt/theory_fpa.cpp +++ b/src/smt/theory_fpa.cpp @@ -560,21 +560,7 @@ namespace smt { SASSERT(is_app(bv_atom) && m.is_bool(bv_atom)); bv_atom = m.mk_and(bv_atom, mk_side_conditions()); - // CMW: Do not use assert_cnstr here; the internalizer expects normalized expressions. - // See GitHub issue #227 - // assert_cnstr(m.mk_iff(atom, bv_atom)); - - ctx.internalize(atom, false); - ctx.internalize(bv_atom, false); - literal lit1(ctx.get_literal(atom)); - literal lit2(ctx.get_literal(bv_atom)); - ctx.mark_as_relevant(lit1); - ctx.mark_as_relevant(lit2); - literal lits1[2] = { lit1, ~lit2 }; - literal lits2[2] = { ~lit1, lit2 }; - ctx.mk_th_axiom(get_id(), 2, lits1); - ctx.mk_th_axiom(get_id(), 2, lits2); - + assert_cnstr(m.mk_iff(atom, bv_atom)); return true; } From 1d7aa9ba2ff1dfd0f1419361b4d595ab7fb69616 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sat, 31 Oct 2015 18:53:40 +0000 Subject: [PATCH 02/21] Fixed rewriter bug in theory_fpa. --- src/smt/theory_fpa.cpp | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp index 7b8a83520..100ece48c 100644 --- a/src/smt/theory_fpa.cpp +++ b/src/smt/theory_fpa.cpp @@ -558,9 +558,10 @@ namespace smt { expr_ref bv_atom(m); bv_atom = convert_atom(atom); SASSERT(is_app(bv_atom) && m.is_bool(bv_atom)); - bv_atom = m.mk_and(bv_atom, mk_side_conditions()); - - assert_cnstr(m.mk_iff(atom, bv_atom)); + expr_ref constr(m); + constr = m.mk_iff(atom, m.mk_and(bv_atom, mk_side_conditions())); + m_th_rw(constr); + assert_cnstr(constr); return true; } From 88064fc172172f4de62a21c38d835791e6c2beea Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sat, 31 Oct 2015 19:16:09 +0000 Subject: [PATCH 03/21] minor theory_fpa refactoring --- src/smt/theory_fpa.cpp | 12 +++++------- 1 file changed, 5 insertions(+), 7 deletions(-) diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp index 100ece48c..7c637309f 100644 --- a/src/smt/theory_fpa.cpp +++ b/src/smt/theory_fpa.cpp @@ -555,13 +555,11 @@ namespace smt { literal l(ctx.mk_bool_var(atom)); ctx.set_var_theory(l.var(), get_id()); - expr_ref bv_atom(m); - bv_atom = convert_atom(atom); - SASSERT(is_app(bv_atom) && m.is_bool(bv_atom)); - expr_ref constr(m); - constr = m.mk_iff(atom, m.mk_and(bv_atom, mk_side_conditions())); - m_th_rw(constr); - assert_cnstr(constr); + expr_ref bv_atom(convert_atom(atom)); + expr_ref bv_atom_w_side_c(m); + bv_atom_w_side_c = m.mk_and(bv_atom, mk_side_conditions()); + m_th_rw(bv_atom_w_side_c); + assert_cnstr(m.mk_eq(atom, bv_atom_w_side_c)); return true; } From 653416153dd34345b8453e2b0f02cd4cb33c855e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 2 Nov 2015 08:18:51 -0800 Subject: [PATCH 04/21] use appropriate MaxSAT solver even if there are no soft constraints. Also avoid PB constraints when all soft constraints are false. Reported by Klaus Becker Signed-off-by: Nikolaj Bjorner --- src/opt/maxres.cpp | 7 +++---- src/opt/maxsmt.cpp | 7 +------ 2 files changed, 4 insertions(+), 10 deletions(-) diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp index 7c470f552..f776fa3e9 100644 --- a/src/opt/maxres.cpp +++ b/src/opt/maxres.cpp @@ -188,6 +188,7 @@ public: } lbool mus_solver() { + lbool is_sat = l_true; init(); init_local(); trace(); @@ -198,7 +199,7 @@ public: tout << "\n"; display(tout); ); - lbool is_sat = check_sat_hill_climb(m_asms); + is_sat = check_sat_hill_climb(m_asms); if (m_cancel) { return l_undef; } @@ -833,9 +834,7 @@ public: s().assert_expr(m_asms[i].get()); } } - else { - maxsmt_solver_base::commit_assignment(); - } + // else: there is only a single assignment to these soft constraints. } void verify_core(exprs const& core) { diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp index 6b518edfa..2d3a60ea8 100644 --- a/src/opt/maxsmt.cpp +++ b/src/opt/maxsmt.cpp @@ -159,12 +159,7 @@ namespace opt { symbol const& maxsat_engine = m_c.maxsat_engine(); IF_VERBOSE(1, verbose_stream() << "(maxsmt)\n";); TRACE("opt", tout << "maxsmt\n";); - if (m_soft_constraints.empty()) { - TRACE("opt", tout << "no constraints\n";); - m_msolver = 0; - is_sat = s().check_sat(0, 0); - } - else if (maxsat_engine == symbol("maxres")) { + if (m_soft_constraints.empty() || maxsat_engine == symbol("maxres")) { m_msolver = mk_maxres(m_c, m_weights, m_soft_constraints); } else if (maxsat_engine == symbol("pd-maxres")) { From feba64b739af18fcbb0df65966b45d77fc84649c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 2 Nov 2015 10:18:25 -0800 Subject: [PATCH 05/21] Enable model construction and evaluation for theory functions that may be uninterpreted. To fix issue #237 Signed-off-by: Nikolaj Bjorner --- src/model/model_evaluator.cpp | 100 ++++++++++++++++---------------- src/smt/smt_model_generator.cpp | 7 ++- src/smt/smt_theory.h | 4 ++ src/smt/theory_bv.cpp | 15 +++++ src/smt/theory_bv.h | 1 + 5 files changed, 75 insertions(+), 52 deletions(-) diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp index d649ac236..245a09f5e 100644 --- a/src/model/model_evaluator.cpp +++ b/src/model/model_evaluator.cpp @@ -101,31 +101,21 @@ struct evaluator_cfg : public default_rewriter_cfg { br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { result_pr = 0; family_id fid = f->get_family_id(); - if (fid == null_family_id) { - if (num == 0) { - expr * val = m_model.get_const_interp(f); - if (val != 0) { - result = val; - return BR_DONE; - } - - if (m_model_completion) { - sort * s = f->get_range(); - expr * val = m_model.get_some_value(s); - m_model.register_decl(f, val); - result = val; - return BR_DONE; - } - return BR_FAILED; - } - SASSERT(num > 0); - func_interp * fi = m_model.get_func_interp(f); - if (fi != 0 && eval_fi(fi, num, args, result)) { - TRACE("model_evaluator", tout << "reduce_app " << f->get_name() << "\n"; - for (unsigned i = 0; i < num; i++) tout << mk_ismt2_pp(args[i], m()) << "\n"; - tout << "---->\n" << mk_ismt2_pp(result, m()) << "\n";); + if (fid == null_family_id && num == 0) { + expr * val = m_model.get_const_interp(f); + if (val != 0) { + result = val; return BR_DONE; } + + if (m_model_completion) { + sort * s = f->get_range(); + expr * val = m_model.get_some_value(s); + m_model.register_decl(f, val); + result = val; + return BR_DONE; + } + return BR_FAILED; } if (fid == m_b_rw.get_fid()) { @@ -160,42 +150,50 @@ struct evaluator_cfg : public default_rewriter_cfg { return m_pb_rw.mk_app_core(f, num, args, result); if (fid == m_f_rw.get_fid()) return m_f_rw.mk_app_core(f, num, args, result); + + func_interp * fi = m_model.get_func_interp(f); + if (fi != 0 && eval_fi(fi, num, args, result)) { + TRACE("model_evaluator", tout << "reduce_app " << f->get_name() << "\n"; + for (unsigned i = 0; i < num; i++) tout << mk_ismt2_pp(args[i], m()) << "\n"; + tout << "---->\n" << mk_ismt2_pp(result, m()) << "\n";); + return BR_DONE; + } + TRACE("model_evaluator", tout << f->get_name() << "\n";); + return BR_FAILED; } bool get_macro(func_decl * f, expr * & def, quantifier * & q, proof * & def_pr) { - if (f->get_family_id() == null_family_id) { - func_interp * fi = m_model.get_func_interp(f); - - if (fi != 0) { - if (fi->is_partial()) { - if (m_model_completion) { - sort * s = f->get_range(); - expr * val = m_model.get_some_value(s); - fi->set_else(val); - } - else { - return false; - } + + func_interp * fi = m_model.get_func_interp(f); + if (fi != 0) { + if (fi->is_partial()) { + if (m_model_completion) { + sort * s = f->get_range(); + expr * val = m_model.get_some_value(s); + fi->set_else(val); } - - def = fi->get_interp(); - SASSERT(def != 0); - return true; - } - - if (m_model_completion) { - sort * s = f->get_range(); - expr * val = m_model.get_some_value(s); - func_interp * new_fi = alloc(func_interp, m(), f->get_arity()); - new_fi->set_else(val); - m_model.register_decl(f, new_fi); - def = val; - return true; - } + else { + return false; + } + } + def = fi->get_interp(); + SASSERT(def != 0); + return true; + } + + if (f->get_family_id() == null_family_id && m_model_completion) { + sort * s = f->get_range(); + expr * val = m_model.get_some_value(s); + func_interp * new_fi = alloc(func_interp, m(), f->get_arity()); + new_fi->set_else(val); + m_model.register_decl(f, new_fi); + def = val; + return true; } return false; } + bool max_steps_exceeded(unsigned num_steps) const { cooperate("model evaluator"); diff --git a/src/smt/smt_model_generator.cpp b/src/smt/smt_model_generator.cpp index 6c138fd57..98d982b7a 100644 --- a/src/smt/smt_model_generator.cpp +++ b/src/smt/smt_model_generator.cpp @@ -400,7 +400,12 @@ namespace smt { \brief Return true if the interpretation of the function should be included in the model. */ bool model_generator::include_func_interp(func_decl * f) const { - return f->get_family_id() == null_family_id; + family_id fid = f->get_family_id(); + if (fid == null_family_id) return true; + if (fid == m_manager.get_basic_family_id()) return false; + theory * th = m_context->get_theory(fid); + if (!th) return true; + return th->include_func_interp(f); } /** diff --git a/src/smt/smt_theory.h b/src/smt/smt_theory.h index 242ad7c17..c5fb80a1e 100644 --- a/src/smt/smt_theory.h +++ b/src/smt/smt_theory.h @@ -412,6 +412,10 @@ namespace smt { return 0; } + virtual bool include_func_interp(func_decl* f) { + return false; + } + // ----------------------------------- // // Model checker diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp index 6bcae6f60..dcf06e1e5 100644 --- a/src/smt/theory_bv.cpp +++ b/src/smt/theory_bv.cpp @@ -1283,6 +1283,21 @@ namespace smt { theory::reset_eh(); } + bool theory_bv::include_func_interp(func_decl* f) { + SASSERT(f->get_family_id() == get_family_id()); + switch (f->get_decl_kind()) { + case OP_BSDIV0: + case OP_BUDIV0: + case OP_BSREM0: + case OP_BUREM0: + case OP_BSMOD0: + return true; + default: + return false; + } + return false; + } + theory_bv::theory_bv(ast_manager & m, theory_bv_params const & params, bit_blaster_params const & bb_params): theory(m.mk_family_id("bv")), m_params(params), diff --git a/src/smt/theory_bv.h b/src/smt/theory_bv.h index 0f74b3603..414474a89 100644 --- a/src/smt/theory_bv.h +++ b/src/smt/theory_bv.h @@ -236,6 +236,7 @@ namespace smt { virtual void pop_scope_eh(unsigned num_scopes); virtual final_check_status final_check_eh(); virtual void reset_eh(); + virtual bool include_func_interp(func_decl* f); svector m_merge_aux[2]; //!< auxiliary vector used in merge_zero_one_bits bool merge_zero_one_bits(theory_var r1, theory_var r2); From 77fec049a54395addf0dc69bd1a154422bba9e15 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 2 Nov 2015 10:27:44 -0800 Subject: [PATCH 06/21] Enable model construction and evaluation for theory functions that may be uninterpreted. To fix issue #237 Signed-off-by: Nikolaj Bjorner --- src/model/model_evaluator.cpp | 49 +++++++++++++++++++++-------------- 1 file changed, 29 insertions(+), 20 deletions(-) diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp index 245a09f5e..79b9209ab 100644 --- a/src/model/model_evaluator.cpp +++ b/src/model/model_evaluator.cpp @@ -118,13 +118,14 @@ struct evaluator_cfg : public default_rewriter_cfg { return BR_FAILED; } + br_status st = BR_FAILED; + if (fid == m_b_rw.get_fid()) { decl_kind k = f->get_decl_kind(); if (k == OP_EQ) { // theory dispatch for = SASSERT(num == 2); family_id s_fid = m().get_sort(args[0])->get_family_id(); - br_status st = BR_FAILED; if (s_fid == m_a_rw.get_fid()) st = m_a_rw.mk_eq_core(args[0], args[1], result); else if (s_fid == m_bv_rw.get_fid()) @@ -138,29 +139,37 @@ struct evaluator_cfg : public default_rewriter_cfg { } return m_b_rw.mk_app_core(f, num, args, result); } + if (fid == m_a_rw.get_fid()) - return m_a_rw.mk_app_core(f, num, args, result); - if (fid == m_bv_rw.get_fid()) - return m_bv_rw.mk_app_core(f, num, args, result); - if (fid == m_ar_rw.get_fid()) - return m_ar_rw.mk_app_core(f, num, args, result); - if (fid == m_dt_rw.get_fid()) - return m_dt_rw.mk_app_core(f, num, args, result); - if (fid == m_pb_rw.get_fid()) - return m_pb_rw.mk_app_core(f, num, args, result); - if (fid == m_f_rw.get_fid()) - return m_f_rw.mk_app_core(f, num, args, result); + st = m_a_rw.mk_app_core(f, num, args, result); + else if (fid == m_bv_rw.get_fid()) + st = m_bv_rw.mk_app_core(f, num, args, result); + else if (fid == m_ar_rw.get_fid()) + st = m_ar_rw.mk_app_core(f, num, args, result); + else if (fid == m_dt_rw.get_fid()) + st = m_dt_rw.mk_app_core(f, num, args, result); + else if (fid == m_pb_rw.get_fid()) + st = m_pb_rw.mk_app_core(f, num, args, result); + else if (fid == m_f_rw.get_fid()) + st = m_f_rw.mk_app_core(f, num, args, result); - func_interp * fi = m_model.get_func_interp(f); - if (fi != 0 && eval_fi(fi, num, args, result)) { - TRACE("model_evaluator", tout << "reduce_app " << f->get_name() << "\n"; - for (unsigned i = 0; i < num; i++) tout << mk_ismt2_pp(args[i], m()) << "\n"; - tout << "---->\n" << mk_ismt2_pp(result, m()) << "\n";); - return BR_DONE; + // allow for model evaluation to work on result of rewriting. + if (st == BR_DONE) { + return BR_REWRITE1; } - TRACE("model_evaluator", tout << f->get_name() << "\n";); - return BR_FAILED; + if (st == BR_FAILED) { + func_interp * fi = m_model.get_func_interp(f); + if (fi != 0 && eval_fi(fi, num, args, result)) { + TRACE("model_evaluator", tout << "reduce_app " << f->get_name() << "\n"; + for (unsigned i = 0; i < num; i++) tout << mk_ismt2_pp(args[i], m()) << "\n"; + tout << "---->\n" << mk_ismt2_pp(result, m()) << "\n";); + return BR_DONE; + } + TRACE("model_evaluator", tout << f->get_name() << "\n";); + } + + return st; } bool get_macro(func_decl * f, expr * & def, quantifier * & q, proof * & def_pr) { From ba70ab9ad24378c9ee67e7b23ffbaeaa9d42dfb9 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 2 Nov 2015 19:08:52 +0000 Subject: [PATCH 07/21] Bugfix for theory_fpa --- src/smt/theory_fpa.cpp | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp index 7c637309f..73cab556e 100644 --- a/src/smt/theory_fpa.cpp +++ b/src/smt/theory_fpa.cpp @@ -737,10 +737,11 @@ namespace smt { expr_ref converted(m); converted = m.mk_and(convert(e), mk_side_conditions()); - if (is_true) - assert_cnstr(m.mk_implies(e, converted)); - else - assert_cnstr(m.mk_implies(m.mk_not(e), m.mk_not(converted))); + + expr_ref cnstr(m); + cnstr = (is_true) ? m.mk_implies(e, converted) : m.mk_implies(m.mk_not(e), m.mk_not(converted)); + m_th_rw(cnstr); + assert_cnstr(cnstr); } void theory_fpa::relevant_eh(app * n) { From 14d2356a320c51579c0657e5f89253dcd82f037d Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 2 Nov 2015 19:25:11 +0000 Subject: [PATCH 08/21] Code simplification --- src/smt/theory_fpa.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp index 73cab556e..66a1a6321 100644 --- a/src/smt/theory_fpa.cpp +++ b/src/smt/theory_fpa.cpp @@ -739,7 +739,7 @@ namespace smt { converted = m.mk_and(convert(e), mk_side_conditions()); expr_ref cnstr(m); - cnstr = (is_true) ? m.mk_implies(e, converted) : m.mk_implies(m.mk_not(e), m.mk_not(converted)); + cnstr = (is_true) ? m.mk_implies(e, converted) : m.mk_implies(converted, e); m_th_rw(cnstr); assert_cnstr(cnstr); } From 92152b16ca30361e1df04fb007c37e204fd044a4 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 2 Nov 2015 19:25:44 +0000 Subject: [PATCH 09/21] Bugfixes for model verification of unspecified values of fp.min/fp.max --- src/ast/fpa/fpa2bv_converter.cpp | 56 +++++++++++------------ src/ast/fpa/fpa2bv_converter.h | 41 +++++++---------- src/ast/rewriter/fpa_rewriter.cpp | 4 +- src/tactic/fpa/fpa2bv_model_converter.cpp | 56 +++++++++++++++++------ src/tactic/fpa/fpa2bv_model_converter.h | 49 ++++++++++---------- src/tactic/fpa/fpa2bv_tactic.cpp | 38 +++++++-------- 6 files changed, 131 insertions(+), 113 deletions(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 6c4d2dc1d..4ee6366f0 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -36,10 +36,6 @@ fpa2bv_converter::fpa2bv_converter(ast_manager & m) : m_mpf_manager(m_util.fm()), m_mpz_manager(m_mpf_manager.mpz_manager()), m_hi_fp_unspecified(true), - m_min_pn_zeros(0, m), - m_min_np_zeros(0, m), - m_max_pn_zeros(0, m), - m_max_np_zeros(0, m), m_extra_assertions(m) { m_plugin = static_cast(m.get_plugin(m.mk_family_id("fpa"))); } @@ -1154,22 +1150,22 @@ expr_ref fpa2bv_converter::mk_min_unspecified(func_decl * f, expr * x, expr * y) // The hardware interpretation is -0.0. mk_nzero(f, res); else { - if (m_min_pn_zeros == 0) { - m_min_pn_zeros = m.mk_fresh_const(0, m_bv_util.mk_sort(1)); - m_decls_to_hide.insert_if_not_there(m_min_pn_zeros->get_decl()); - } - - if (m_min_np_zeros == 0) { - m_min_np_zeros = m.mk_fresh_const(0, m_bv_util.mk_sort(1)); - m_decls_to_hide.insert_if_not_there(m_min_np_zeros->get_decl()); + std::pair decls(0, 0); + if (!m_specials.find(f, decls)) { + decls.first = m.mk_fresh_const(0, m_bv_util.mk_sort(1)); + decls.second = m.mk_fresh_const(0, m_bv_util.mk_sort(1)); + m_specials.insert(f, decls); + m.inc_ref(f); + m.inc_ref(decls.first); + m.inc_ref(decls.second); } expr_ref pn(m), np(m); - mk_fp(m_min_pn_zeros, + mk_fp(decls.first, m_bv_util.mk_numeral(0, ebits), m_bv_util.mk_numeral(0, sbits - 1), pn); - mk_fp(m_min_np_zeros, + mk_fp(decls.second, m_bv_util.mk_numeral(0, ebits), m_bv_util.mk_numeral(0, sbits - 1), np); @@ -1243,22 +1239,22 @@ expr_ref fpa2bv_converter::mk_max_unspecified(func_decl * f, expr * x, expr * y) // The hardware interpretation is +0.0. mk_pzero(f, res); else { - if (m_max_pn_zeros == 0) { - m_max_pn_zeros = m.mk_fresh_const(0, m_bv_util.mk_sort(1)); - m_decls_to_hide.insert_if_not_there(m_max_pn_zeros->get_decl()); - } - - if (m_max_np_zeros == 0) { - m_max_np_zeros = m.mk_fresh_const(0, m_bv_util.mk_sort(1)); - m_decls_to_hide.insert_if_not_there(m_max_np_zeros->get_decl()); + std::pair decls(0, 0); + if (!m_specials.find(f, decls)) { + decls.first = m.mk_fresh_const(0, m_bv_util.mk_sort(1)); + decls.second = m.mk_fresh_const(0, m_bv_util.mk_sort(1)); + m_specials.insert(f, decls); + m.inc_ref(f); + m.inc_ref(decls.first); + m.inc_ref(decls.second); } expr_ref pn(m), np(m); - mk_fp(m_max_pn_zeros, + mk_fp(decls.first, m_bv_util.mk_numeral(0, ebits), m_bv_util.mk_numeral(0, sbits - 1), pn); - mk_fp(m_max_np_zeros, + mk_fp(decls.second, m_bv_util.mk_numeral(0, ebits), m_bv_util.mk_numeral(0, sbits - 1), np); @@ -3839,14 +3835,16 @@ void fpa2bv_converter::round(sort * s, expr_ref & bv_rm, expr_ref & sgn, expr_re TRACE("fpa2bv_round", tout << "ROUND = " << mk_ismt2_pp(result, m) << std::endl; ); } - void fpa2bv_converter::reset(void) { dec_ref_map_key_values(m, m_const2bv); dec_ref_map_key_values(m, m_rm_const2bv); dec_ref_map_key_values(m, m_uf2bvuf); - m_min_np_zeros = 0; - m_min_pn_zeros = 0; - m_max_np_zeros = 0; - m_max_pn_zeros = 0; + for (obj_map >::iterator it = m_specials.begin(); + it != m_specials.end(); + it++) { + m.dec_ref(it->m_key); + m.dec_ref(it->m_value.first); + m.dec_ref(it->m_value.second); + } m_extra_assertions.reset(); } diff --git a/src/ast/fpa/fpa2bv_converter.h b/src/ast/fpa/fpa2bv_converter.h index 95f2ca057..65d99d2c8 100644 --- a/src/ast/fpa/fpa2bv_converter.h +++ b/src/ast/fpa/fpa2bv_converter.h @@ -35,8 +35,8 @@ struct func_decl_triple { f_exp = exp; } func_decl * f_sgn; - func_decl * f_sig; - func_decl * f_exp; + func_decl * f_sig; + func_decl * f_exp; }; class fpa2bv_converter { @@ -47,22 +47,20 @@ protected: bv_util m_bv_util; arith_util m_arith_util; mpf_manager & m_mpf_manager; - unsynch_mpz_manager & m_mpz_manager; + unsynch_mpz_manager & m_mpz_manager; fpa_decl_plugin * m_plugin; bool m_hi_fp_unspecified; obj_map m_const2bv; obj_map m_rm_const2bv; obj_map m_uf2bvuf; - obj_hashtable m_decls_to_hide; - app_ref m_min_pn_zeros; - app_ref m_min_np_zeros; - app_ref m_max_pn_zeros; - app_ref m_max_np_zeros; - + obj_map > m_specials; + + friend class fpa2bv_model_converter; + public: - fpa2bv_converter(ast_manager & m); + fpa2bv_converter(ast_manager & m); ~fpa2bv_converter(); fpa_util & fu() { return m_util; } @@ -83,7 +81,7 @@ public: void split_fp(expr * e, expr * & sgn, expr * & exp, expr * & sig) const; void split_fp(expr * e, expr_ref & sgn, expr_ref & exp, expr_ref & sig) const; - void mk_eq(expr * a, expr * b, expr_ref & result); + void mk_eq(expr * a, expr * b, expr_ref & result); void mk_ite(expr * c, expr * t, expr * f, expr_ref & result); void mk_distinct(func_decl * f, unsigned num, expr * const * args, expr_ref & result); @@ -98,7 +96,7 @@ public: void mk_ninf(func_decl * f, expr_ref & result); void mk_nan(func_decl * f, expr_ref & result); void mk_nzero(func_decl *f, expr_ref & result); - void mk_pzero(func_decl *f, expr_ref & result); + void mk_pzero(func_decl *f, expr_ref & result); void mk_add(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_sub(func_decl * f, unsigned num, expr * const * args, expr_ref & result); @@ -106,7 +104,7 @@ public: void mk_mul(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_div(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_rem(func_decl * f, unsigned num, expr * const * args, expr_ref & result); - void mk_abs(func_decl * f, unsigned num, expr * const * args, expr_ref & result); + void mk_abs(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_fma(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_sqrt(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_round_to_integral(func_decl * f, unsigned num, expr * const * args, expr_ref & result); @@ -125,10 +123,10 @@ public: void mk_is_nan(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_is_inf(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_is_normal(func_decl * f, unsigned num, expr * const * args, expr_ref & result); - void mk_is_subnormal(func_decl * f, unsigned num, expr * const * args, expr_ref & result); + void mk_is_subnormal(func_decl * f, unsigned num, expr * const * args, expr_ref & result); - void mk_to_fp(func_decl * f, unsigned num, expr * const * args, expr_ref & result); - void mk_to_fp_float(func_decl * f, sort * s, expr * rm, expr * x, expr_ref & result); + void mk_to_fp(func_decl * f, unsigned num, expr * const * args, expr_ref & result); + void mk_to_fp_float(func_decl * f, sort * s, expr * rm, expr * x, expr_ref & result); void mk_to_fp_signed(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_to_fp_unsigned(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_to_ieee_bv(func_decl * f, unsigned num, expr * const * args, expr_ref & result); @@ -137,7 +135,7 @@ public: void mk_to_ubv(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_to_sbv(func_decl * f, unsigned num, expr * const * args, expr_ref & result); - void mk_to_real(func_decl * f, unsigned num, expr * const * args, expr_ref & result); + void mk_to_real(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void set_unspecified_fp_hi(bool v) { m_hi_fp_unspecified = v; } @@ -145,7 +143,7 @@ public: void mk_min_i(func_decl * f, unsigned num, expr * const * args, expr_ref & result); virtual expr_ref mk_min_unspecified(func_decl * f, expr * x, expr * y); - void mk_max(func_decl * f, unsigned num, expr * const * args, expr_ref & result); + void mk_max(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_max_i(func_decl * f, unsigned num, expr * const * args, expr_ref & result); virtual expr_ref mk_max_unspecified(func_decl * f, expr * x, expr * y); @@ -153,11 +151,6 @@ public: expr_ref mk_to_sbv_unspecified(unsigned width); expr_ref mk_to_real_unspecified(); - obj_map const & const2bv() const { return m_const2bv; } - obj_map const & rm_const2bv() const { return m_rm_const2bv; } - obj_map const & uf2bvuf() const { return m_uf2bvuf; } - obj_hashtable const & decls_to_hide() const { return m_decls_to_hide; } - void reset(void); void dbg_decouple(const char * prefix, expr_ref & e); @@ -191,7 +184,7 @@ protected: void mk_unbias(expr * e, expr_ref & result); void unpack(expr * e, expr_ref & sgn, expr_ref & sig, expr_ref & exp, expr_ref & lz, bool normalize); - void round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref & sig, expr_ref & exp, expr_ref & result); + void round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref & sig, expr_ref & exp, expr_ref & result); expr_ref mk_rounding_decision(expr * rm, expr * sgn, expr * last, expr * round, expr * sticky); void add_core(unsigned sbits, unsigned ebits, diff --git a/src/ast/rewriter/fpa_rewriter.cpp b/src/ast/rewriter/fpa_rewriter.cpp index cc3ba81a3..63af356c8 100644 --- a/src/ast/rewriter/fpa_rewriter.cpp +++ b/src/ast/rewriter/fpa_rewriter.cpp @@ -439,7 +439,7 @@ br_status fpa_rewriter::mk_min(expr * arg1, expr * arg2, expr_ref & result) { if (m_util.is_numeral(arg1, v1) && m_util.is_numeral(arg2, v2)) { if (m_fm.is_zero(v1) && m_fm.is_zero(v2) && m_fm.sgn(v1) != m_fm.sgn(v2)) { result = m().mk_app(get_fid(), OP_FPA_INTERNAL_MIN_UNSPECIFIED, arg1, arg2); - return BR_DONE; + return BR_REWRITE1; } else { scoped_mpf r(m_fm); @@ -474,7 +474,7 @@ br_status fpa_rewriter::mk_max(expr * arg1, expr * arg2, expr_ref & result) { if (m_util.is_numeral(arg1, v1) && m_util.is_numeral(arg2, v2)) { if (m_fm.is_zero(v1) && m_fm.is_zero(v2) && m_fm.sgn(v1) != m_fm.sgn(v2)) { result = m().mk_app(get_fid(), OP_FPA_INTERNAL_MAX_UNSPECIFIED, arg1, arg2); - return BR_DONE; + return BR_REWRITE1; } else { scoped_mpf r(m_fm); diff --git a/src/tactic/fpa/fpa2bv_model_converter.cpp b/src/tactic/fpa/fpa2bv_model_converter.cpp index 78c79dd11..90b2827b2 100644 --- a/src/tactic/fpa/fpa2bv_model_converter.cpp +++ b/src/tactic/fpa/fpa2bv_model_converter.cpp @@ -45,6 +45,15 @@ void fpa2bv_model_converter::display(std::ostream & out) { unsigned indent = n.size() + 4; out << mk_ismt2_pp(it->m_value, m, indent) << ")"; } + for (obj_map >::iterator it = m_specials.begin(); + it != m_specials.end(); + it++) { + const symbol & n = it->m_key->get_name(); + out << "\n (" << n << " "; + unsigned indent = n.size() + 4; + out << mk_ismt2_pp(it->m_value.first, m, indent) << "; " << + mk_ismt2_pp(it->m_value.second, m, indent) << ")"; + } out << ")" << std::endl; } @@ -79,12 +88,16 @@ model_converter * fpa2bv_model_converter::translate(ast_translation & translator translator.to().inc_ref(k); translator.to().inc_ref(v); } - for (obj_hashtable::iterator it = m_decls_to_hide.begin(); - it != m_decls_to_hide.end(); + for (obj_map >::iterator it = m_specials.begin(); + it != m_specials.end(); it++) { - func_decl * k = translator(*it); - res->m_decls_to_hide.insert(k); + func_decl * k = translator(it->m_key); + app * v1 = translator(it->m_value.first); + app * v2 = translator(it->m_value.second); + res->m_specials.insert(k, std::pair(v1, v2)); translator.to().inc_ref(k); + translator.to().inc_ref(v1); + translator.to().inc_ref(v2); } return res; } @@ -217,10 +230,29 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) { obj_hashtable seen; - for (obj_hashtable::iterator it = m_decls_to_hide.begin(); - it != m_decls_to_hide.end(); - it++) - seen.insert(*it); + for (obj_map >::iterator it = m_specials.begin(); + it != m_specials.end(); + it++) { + func_decl * f = it->m_key; + expr_ref pzero(m), nzero(m); + pzero = fu.mk_pzero(f->get_range()); + nzero = fu.mk_nzero(f->get_range()); + + expr_ref pn(m), np(m); + bv_mdl->eval(it->m_value.first, pn, true); + bv_mdl->eval(it->m_value.second, np, true); + seen.insert(it->m_value.first->get_decl()); + seen.insert(it->m_value.second->get_decl()); + + func_interp * flt_fi = alloc(func_interp, m, f->get_arity()); + expr * pn_args[2] = { pzero, nzero }; + if (pn != np) flt_fi->insert_new_entry(pn_args, (m.is_true(pn) ? nzero : pzero)); + flt_fi->set_else(m.is_true(np) ? nzero : pzero); + + float_mdl->register_decl(f, flt_fi); + TRACE("fpa2bv_mc", tout << "fp.min/fp.max special: " << std::endl << + mk_ismt2_pp(f, m) << " == " << mk_ismt2_pp(flt_fi->get_interp(), m) << std::endl;); + } for (obj_map::iterator it = m_const2bv.begin(); it != m_const2bv.end(); @@ -362,10 +394,6 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) { } } -model_converter * mk_fpa2bv_model_converter(ast_manager & m, - obj_map const & const2bv, - obj_map const & rm_const2bv, - obj_map const & uf2bvuf, - obj_hashtable const & decls_to_hide) { - return alloc(fpa2bv_model_converter, m, const2bv, rm_const2bv, uf2bvuf, decls_to_hide); +model_converter * mk_fpa2bv_model_converter(ast_manager & m, fpa2bv_converter const & conv) { + return alloc(fpa2bv_model_converter, m, conv); } diff --git a/src/tactic/fpa/fpa2bv_model_converter.h b/src/tactic/fpa/fpa2bv_model_converter.h index a864f753a..534fb6e1c 100644 --- a/src/tactic/fpa/fpa2bv_model_converter.h +++ b/src/tactic/fpa/fpa2bv_model_converter.h @@ -27,44 +27,41 @@ class fpa2bv_model_converter : public model_converter { obj_map m_const2bv; obj_map m_rm_const2bv; obj_map m_uf2bvuf; - obj_hashtable m_decls_to_hide; + obj_map > m_specials; public: - fpa2bv_model_converter(ast_manager & m, obj_map const & const2bv, - obj_map const & rm_const2bv, - obj_map const & uf2bvuf, - obj_hashtable const & decls_to_hide) : - m(m) { - for (obj_map::iterator it = const2bv.begin(); - it != const2bv.end(); + fpa2bv_model_converter(ast_manager & m, fpa2bv_converter const & conv) : m(m) { + for (obj_map::iterator it = conv.m_const2bv.begin(); + it != conv.m_const2bv.end(); it++) { m_const2bv.insert(it->m_key, it->m_value); m.inc_ref(it->m_key); m.inc_ref(it->m_value); } - for (obj_map::iterator it = rm_const2bv.begin(); - it != rm_const2bv.end(); + for (obj_map::iterator it = conv.m_rm_const2bv.begin(); + it != conv.m_rm_const2bv.end(); it++) { m_rm_const2bv.insert(it->m_key, it->m_value); m.inc_ref(it->m_key); m.inc_ref(it->m_value); } - for (obj_map::iterator it = uf2bvuf.begin(); - it != uf2bvuf.end(); + for (obj_map::iterator it = conv.m_uf2bvuf.begin(); + it != conv.m_uf2bvuf.end(); it++) { m_uf2bvuf.insert(it->m_key, it->m_value); m.inc_ref(it->m_key); m.inc_ref(it->m_value); } - for (obj_hashtable::iterator it = decls_to_hide.begin(); - it != decls_to_hide.end(); - it++) - { - m_decls_to_hide.insert(*it); - m.inc_ref(*it); + for (obj_map >::iterator it = conv.m_specials.begin(); + it != conv.m_specials.end(); + it++) { + m_specials.insert(it->m_key, it->m_value); + m.inc_ref(it->m_key); + m.inc_ref(it->m_value.first); + m.inc_ref(it->m_value.second); } } @@ -72,7 +69,13 @@ public: dec_ref_map_key_values(m, m_const2bv); dec_ref_map_key_values(m, m_rm_const2bv); dec_ref_map_key_values(m, m_uf2bvuf); - dec_ref_collection_values(m, m_decls_to_hide); + for (obj_map >::iterator it = m_specials.begin(); + it != m_specials.end(); + it++) { + m.dec_ref(it->m_key); + m.dec_ref(it->m_value.first); + m.dec_ref(it->m_value.second); + } } virtual void operator()(model_ref & md, unsigned goal_idx) { @@ -92,7 +95,7 @@ public: virtual model_converter * translate(ast_translation & translator); protected: - fpa2bv_model_converter(ast_manager & m) : m(m) { } + fpa2bv_model_converter(ast_manager & m) : m(m){ } void convert(model * bv_mdl, model * float_mdl); expr_ref convert_bv2fp(sort * s, expr * sgn, expr * exp, expr * sig) const; @@ -102,10 +105,6 @@ protected: }; -model_converter * mk_fpa2bv_model_converter(ast_manager & m, - obj_map const & const2bv, - obj_map const & rm_const2bv, - obj_map const & uf2bvuf, - obj_hashtable const & decls_to_hide); +model_converter * mk_fpa2bv_model_converter(ast_manager & m, fpa2bv_converter const & conv); #endif \ No newline at end of file diff --git a/src/tactic/fpa/fpa2bv_tactic.cpp b/src/tactic/fpa/fpa2bv_tactic.cpp index 472f6b30c..eb2aeaa0c 100644 --- a/src/tactic/fpa/fpa2bv_tactic.cpp +++ b/src/tactic/fpa/fpa2bv_tactic.cpp @@ -43,26 +43,26 @@ class fpa2bv_tactic : public tactic { } void updt_params(params_ref const & p) { - m_rw.cfg().updt_params(p); + m_rw.cfg().updt_params(p); } - + void set_cancel(bool f) { m_rw.set_cancel(f); } - virtual void operator()(goal_ref const & g, - goal_ref_buffer & result, - model_converter_ref & mc, + virtual void operator()(goal_ref const & g, + goal_ref_buffer & result, + model_converter_ref & mc, proof_converter_ref & pc, expr_dependency_ref & core) { SASSERT(g->is_well_sorted()); m_proofs_enabled = g->proofs_enabled(); m_produce_models = g->models_enabled(); m_produce_unsat_cores = g->unsat_core_enabled(); - + mc = 0; pc = 0; core = 0; result.reset(); tactic_report report("fpa2bv", *g); - m_rw.reset(); + m_rw.reset(); TRACE("fpa2bv", tout << "BEFORE: " << std::endl; g->display(tout);); @@ -70,7 +70,7 @@ class fpa2bv_tactic : public tactic { result.push_back(g.get()); return; } - + m_num_steps = 0; expr_ref new_curr(m); proof_ref new_pr(m); @@ -91,7 +91,7 @@ class fpa2bv_tactic : public tactic { const app * a = to_app(new_curr.get()); if (a->get_family_id() == m_conv.fu().get_family_id() && a->get_decl_kind() == OP_FPA_IS_NAN) { - // Inject auxiliary lemmas that fix e to the one and only NaN value, + // Inject auxiliary lemmas that fix e to the one and only NaN value, // that is (= e (fp #b0 #b1...1 #b0...01)), so that the value propagation // has a value to propagate. expr * sgn, *sig, *exp; @@ -104,8 +104,8 @@ class fpa2bv_tactic : public tactic { } } - if (g->models_enabled()) - mc = mk_fpa2bv_model_converter(m, m_conv.const2bv(), m_conv.rm_const2bv(), m_conv.uf2bvuf(), m_conv.decls_to_hide()); + if (g->models_enabled()) + mc = mk_fpa2bv_model_converter(m, m_conv); g->inc_depth(); result.push_back(g.get()); @@ -114,7 +114,7 @@ class fpa2bv_tactic : public tactic { result.back()->assert_expr(m_conv.m_extra_assertions[i].get()); SASSERT(g->is_well_sorted()); - TRACE("fpa2bv", tout << "AFTER: " << std::endl; g->display(tout); + TRACE("fpa2bv", tout << "AFTER: " << std::endl; g->display(tout); if (mc) mc->display(tout); tout << std::endl; ); } }; @@ -141,12 +141,12 @@ public: m_imp->updt_params(p); } - virtual void collect_param_descrs(param_descrs & r) { + virtual void collect_param_descrs(param_descrs & r) { } - virtual void operator()(goal_ref const & in, - goal_ref_buffer & result, - model_converter_ref & mc, + virtual void operator()(goal_ref const & in, + goal_ref_buffer & result, + model_converter_ref & mc, proof_converter_ref & pc, expr_dependency_ref & core) { try { @@ -156,8 +156,8 @@ public: throw tactic_exception(ex.msg()); } } - - virtual void cleanup() { + + virtual void cleanup() { imp * d = alloc(imp, m_imp->m, m_params); #pragma omp critical (tactic_cancel) { @@ -173,6 +173,6 @@ protected: } }; -tactic * mk_fpa2bv_tactic(ast_manager & m, params_ref const & p) { +tactic * mk_fpa2bv_tactic(ast_manager & m, params_ref const & p) { return clean(alloc(fpa2bv_tactic, m, p)); } From ec12368b548a91c21dc6f80e00ccea7d2322aae7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 2 Nov 2015 11:36:50 -0800 Subject: [PATCH 10/21] Enable model construction and evaluation for theory functions that may be uninterpreted. To fix issue #237 Signed-off-by: Nikolaj Bjorner --- src/model/model_evaluator.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp index 79b9209ab..67704719b 100644 --- a/src/model/model_evaluator.cpp +++ b/src/model/model_evaluator.cpp @@ -154,7 +154,7 @@ struct evaluator_cfg : public default_rewriter_cfg { st = m_f_rw.mk_app_core(f, num, args, result); // allow for model evaluation to work on result of rewriting. - if (st == BR_DONE) { + if (st == BR_DONE && is_app(result) && to_app(result)->get_num_args() > 0) { return BR_REWRITE1; } From 7ac64f1f964f4f7685a6deaa2eff838f6f4994b4 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 2 Nov 2015 19:55:25 +0000 Subject: [PATCH 11/21] Bugfix for FP model converter (fp.min/fp.max models) --- src/tactic/fpa/fpa2bv_model_converter.cpp | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/src/tactic/fpa/fpa2bv_model_converter.cpp b/src/tactic/fpa/fpa2bv_model_converter.cpp index 90b2827b2..62ad363fd 100644 --- a/src/tactic/fpa/fpa2bv_model_converter.cpp +++ b/src/tactic/fpa/fpa2bv_model_converter.cpp @@ -244,10 +244,15 @@ void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) { seen.insert(it->m_value.first->get_decl()); seen.insert(it->m_value.second->get_decl()); + rational pn_num, np_num; + unsigned bv_sz; + bu.is_numeral(pn, pn_num, bv_sz); + bu.is_numeral(np, np_num, bv_sz); + func_interp * flt_fi = alloc(func_interp, m, f->get_arity()); expr * pn_args[2] = { pzero, nzero }; - if (pn != np) flt_fi->insert_new_entry(pn_args, (m.is_true(pn) ? nzero : pzero)); - flt_fi->set_else(m.is_true(np) ? nzero : pzero); + if (pn != np) flt_fi->insert_new_entry(pn_args, (pn_num.is_one() ? nzero : pzero)); + flt_fi->set_else(np_num.is_one() ? nzero : pzero); float_mdl->register_decl(f, flt_fi); TRACE("fpa2bv_mc", tout << "fp.min/fp.max special: " << std::endl << From 2efd5bf9d18c805fcbe4cb5af2e54e0ab7316a0b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 2 Nov 2015 14:18:49 -0800 Subject: [PATCH 12/21] Fix bug exposed in #281 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_arith_aux.h | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h index 0622f03ff..581fbb4df 100644 --- a/src/smt/theory_arith_aux.h +++ b/src/smt/theory_arith_aux.h @@ -1346,7 +1346,7 @@ namespace smt { empty_column || (unbounded_gain(max_gain) == (x_i == null_theory_var))); - return !empty_column && safe_gain(min_gain, max_gain); + return safe_gain(min_gain, max_gain); } template @@ -1557,14 +1557,12 @@ namespace smt { // variable cannot be used for max/min. continue; } - bool picked_var = pick_var_to_leave(curr_x_j, curr_inc, curr_a_ij, + bool safe_to_leave = pick_var_to_leave(curr_x_j, curr_inc, curr_a_ij, curr_min_gain, curr_max_gain, has_shared, curr_x_i); - - SASSERT(!picked_var || safe_gain(curr_min_gain, curr_max_gain)); - if (!safe_gain(curr_min_gain, curr_max_gain)) { + if (!safe_to_leave) { TRACE("opt", tout << "no variable picked\n";); has_bound = true; best_efforts++; From 949ad4d2fc454d0665c5c00abc91af877cf8d377 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 3 Nov 2015 12:28:10 +0000 Subject: [PATCH 13/21] Trailing whitespace removed. --- src/cmd_context/cmd_context.cpp | 106 ++++++++++++++++---------------- src/shell/smtlib_frontend.cpp | 18 +++--- 2 files changed, 61 insertions(+), 63 deletions(-) diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 8648775ee..132418a11 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -131,11 +131,11 @@ bool func_decls::clash(func_decl * f) const { func_decl * g = *it; if (g == f) continue; - if (g->get_arity() != f->get_arity()) + if (g->get_arity() != f->get_arity()) continue; unsigned num = g->get_arity(); unsigned i; - for (i = 0; i < num; i++) + for (i = 0; i < num; i++) if (g->get_domain(i) != f->get_domain(i)) break; if (i == num) @@ -273,12 +273,12 @@ public: virtual array_util & get_arutil() { return m_arutil; } virtual fpa_util & get_futil() { return m_futil; } virtual datalog::dl_decl_util& get_dlutil() { return m_dlutil; } - virtual bool uses(symbol const & s) const { - return + virtual bool uses(symbol const & s) const { + return m_owner.m_builtin_decls.contains(s) || m_owner.m_func_decls.contains(s); } - virtual format_ns::format * pp_sort(sort * s) { + virtual format_ns::format * pp_sort(sort * s) { return m_owner.pp(s); } virtual format_ns::format * pp_fdecl(func_decl * f, unsigned & len) { @@ -309,7 +309,7 @@ cmd_context::cmd_context(bool main_ctx, ast_manager * m, symbol const & l): m_main_ctx(main_ctx), m_logic(l), m_interactive_mode(false), - m_global_decls(false), + m_global_decls(false), m_print_success(m_params.m_smtlib2_compliant), m_random_seed(0), m_produce_unsat_cores(false), @@ -318,7 +318,7 @@ cmd_context::cmd_context(bool main_ctx, ast_manager * m, symbol const & l): m_numeral_as_real(false), m_ignore_check(false), m_exit_on_error(false), - m_manager(m), + m_manager(m), m_own_manager(m == 0), m_manager_initialized(false), m_pmanager(0), @@ -331,7 +331,7 @@ cmd_context::cmd_context(bool main_ctx, ast_manager * m, symbol const & l): install_core_tactic_cmds(*this); install_interpolant_cmds(*this); SASSERT(m != 0 || !has_manager()); - if (m_main_ctx) { + if (m_main_ctx) { set_verbose_stream(diagnostic_stream()); } } @@ -343,7 +343,7 @@ cmd_context::~cmd_context() { finalize_cmds(); finalize_tactic_cmds(); finalize_probes(); - reset(true); + reset(true); m_solver = 0; m_check_sat_result = 0; } @@ -351,7 +351,7 @@ cmd_context::~cmd_context() { void cmd_context::set_cancel(bool f) { if (m_solver) { if (f) { - m_solver->cancel(); + m_solver->cancel(); } else { m_solver->reset_cancel(); @@ -412,20 +412,20 @@ void cmd_context::set_produce_interpolants(bool f) { // set_solver_factory(mk_smt_solver_factory()); } -bool cmd_context::produce_models() const { +bool cmd_context::produce_models() const { return m_params.m_model; } -bool cmd_context::produce_proofs() const { +bool cmd_context::produce_proofs() const { return m_params.m_proof; } -bool cmd_context::produce_interpolants() const { +bool cmd_context::produce_interpolants() const { // FIXME currently synonym for produce_proofs return m_params.m_proof; } -bool cmd_context::produce_unsat_cores() const { +bool cmd_context::produce_unsat_cores() const { return m_params.m_unsat_core; } @@ -497,7 +497,7 @@ void cmd_context::load_plugin(symbol const & name, bool install, svector::iterator it = fids.begin(); svector::iterator end = fids.end(); for (; it != end; ++it) { @@ -686,8 +686,8 @@ void cmd_context::init_external_manager() { } bool cmd_context::supported_logic(symbol const & s) const { - return s == "QF_UF" || s == "UF" || - logic_has_arith_core(s) || logic_has_bv_core(s) || + return s == "QF_UF" || s == "UF" || + logic_has_arith_core(s) || logic_has_bv_core(s) || logic_has_array_core(s) || logic_has_seq_core(s) || logic_has_horn(s) || logic_has_fpa_core(s); } @@ -695,11 +695,11 @@ bool cmd_context::supported_logic(symbol const & s) const { bool cmd_context::set_logic(symbol const & s) { if (has_logic()) throw cmd_exception("the logic has already been set"); - if (has_manager() && m_main_ctx) - throw cmd_exception("logic must be set before initialization"); + if (has_manager() && m_main_ctx) + throw cmd_exception("logic must be set before initialization"); if (!supported_logic(s)) { if (m_params.m_smtlib2_compliant) { - return false; + return false; } else { warning_msg("unknown logic, ignoring set-logic command"); @@ -719,10 +719,10 @@ bool cmd_context::set_logic(symbol const & s) { return true; } -std::string cmd_context::reason_unknown() const { +std::string cmd_context::reason_unknown() const { if (m_check_sat_result.get() == 0) throw cmd_exception("state of the most recent check-sat command is not unknown"); - return m_check_sat_result->reason_unknown(); + return m_check_sat_result->reason_unknown(); } bool cmd_context::is_func_decl(symbol const & s) const { @@ -865,7 +865,7 @@ static builtin_decl const & peek_builtin_decl(builtin_decl const & first, family return first; } -func_decl * cmd_context::find_func_decl(symbol const & s, unsigned num_indices, unsigned const * indices, +func_decl * cmd_context::find_func_decl(symbol const & s, unsigned num_indices, unsigned const * indices, unsigned arity, sort * const * domain, sort * range) const { builtin_decl d; if (m_builtin_decls.find(s, d)) { @@ -891,7 +891,7 @@ func_decl * cmd_context::find_func_decl(symbol const & s, unsigned num_indices, throw cmd_exception("invalid function declaration reference, invalid builtin reference ", s); return f; } - + if (m_macros.contains(s)) throw cmd_exception("invalid function declaration reference, named expressions (aka macros) cannot be referenced ", s); @@ -907,7 +907,7 @@ func_decl * cmd_context::find_func_decl(symbol const & s, unsigned num_indices, throw cmd_exception("invalid function declaration reference, unknown function ", s); return f; } - + psort_decl * cmd_context::find_psort_decl(symbol const & s) const { psort_decl * p = 0; m_psort_decls.find(s, p); @@ -1222,7 +1222,7 @@ void cmd_context::reset(bool finalize) { // reinit cmd_context if this is not a finalization step if (!finalize) init_external_manager(); - else + else m_manager_initialized = false; } } @@ -1272,14 +1272,14 @@ void cmd_context::push() { s.m_macros_stack_lim = m_macros_stack.size(); s.m_aux_pdecls_lim = m_aux_pdecls.size(); s.m_assertions_lim = m_assertions.size(); - if (m_solver) + if (m_solver) m_solver->push(); - if (m_opt) + if (m_opt) m_opt->push(); } void cmd_context::push(unsigned n) { - for (unsigned i = 0; i < n; i++) + for (unsigned i = 0; i < n; i++) push(); } @@ -1371,7 +1371,7 @@ void cmd_context::pop(unsigned n) { if (m_solver) { m_solver->pop(n); } - if (m_opt) + if (m_opt) m_opt->pop(n); unsigned new_lvl = lvl - n; scope & s = m_scopes[new_lvl]; @@ -1523,8 +1523,8 @@ void cmd_context::validate_check_sat_result(lbool r) { } } -void cmd_context::set_diagnostic_stream(char const * name) { - m_diagnostic.set(name); +void cmd_context::set_diagnostic_stream(char const * name) { + m_diagnostic.set(name); if (m_main_ctx) { set_warning_stream(&(*m_diagnostic)); set_verbose_stream(diagnostic_stream()); @@ -1536,15 +1536,15 @@ struct contains_array_op_proc { family_id m_array_fid; contains_array_op_proc(ast_manager & m):m_array_fid(m.mk_family_id("array")) {} void operator()(var * n) {} - void operator()(app * n) { + void operator()(app * n) { if (n->get_family_id() != m_array_fid) return; decl_kind k = n->get_decl_kind(); - if (k == OP_AS_ARRAY || - k == OP_STORE || - k == OP_ARRAY_MAP || + if (k == OP_AS_ARRAY || + k == OP_STORE || + k == OP_ARRAY_MAP || k == OP_CONST_ARRAY) - throw found(); + throw found(); } void operator()(quantifier * n) {} }; @@ -1553,7 +1553,7 @@ struct contains_array_op_proc { \brief Check if the current model satisfies the quantifier free formulas. */ void cmd_context::validate_model() { - if (!validate_model_enabled()) + if (!validate_model_enabled()) return; if (!is_model_available()) return; @@ -1562,8 +1562,8 @@ void cmd_context::validate_model() { SASSERT(md.get() != 0); params_ref p; p.set_uint("max_degree", UINT_MAX); // evaluate algebraic numbers of any degree. - p.set_uint("sort_store", true); - p.set_bool("completion", true); + p.set_uint("sort_store", true); + p.set_bool("completion", true); model_evaluator evaluator(*(md.get()), p); contains_array_op_proc contains_array(m()); { @@ -1612,8 +1612,6 @@ void cmd_context::mk_solver() { m_solver = (*m_solver_factory)(m(), p, proofs_enabled, models_enabled, unsat_core_enabled, m_logic); } - - void cmd_context::set_interpolating_solver_factory(solver_factory * f) { SASSERT(!has_manager()); m_interpolating_solver_factory = f; @@ -1718,7 +1716,7 @@ void cmd_context::pp(func_decl * f, format_ns::format_ref & r) const { void cmd_context::display(std::ostream & out, sort * s, unsigned indent) const { format_ns::format_ref f(format_ns::fm(m())); f = pp(s); - if (indent > 0) + if (indent > 0) f = format_ns::mk_indent(m(), indent, f); ::pp(out, f.get(), m()); } @@ -1726,7 +1724,7 @@ void cmd_context::display(std::ostream & out, sort * s, unsigned indent) const { void cmd_context::display(std::ostream & out, expr * n, unsigned indent, unsigned num_vars, char const * var_prefix, sbuffer & var_names) const { format_ns::format_ref f(format_ns::fm(m())); pp(n, num_vars, var_prefix, f, var_names); - if (indent > 0) + if (indent > 0) f = format_ns::mk_indent(m(), indent, f); ::pp(out, f.get(), m()); } @@ -1739,7 +1737,7 @@ void cmd_context::display(std::ostream & out, expr * n, unsigned indent) const { void cmd_context::display(std::ostream & out, func_decl * d, unsigned indent) const { format_ns::format_ref f(format_ns::fm(m())); pp(d, f); - if (indent > 0) + if (indent > 0) f = format_ns::mk_indent(m(), indent, f); ::pp(out, f.get(), m()); } @@ -1763,7 +1761,7 @@ void cmd_context::display_smt2_benchmark(std::ostream & out, unsigned num, expr } // TODO: display uninterpreted sort decls, and datatype decls. - + unsigned num_decls = decls.get_num_decls(); func_decl * const * fs = decls.get_func_decls(); for (unsigned i = 0; i < num_decls; i++) { @@ -1779,7 +1777,7 @@ void cmd_context::display_smt2_benchmark(std::ostream & out, unsigned num, expr out << "(check-sat)" << std::endl; } -void cmd_context::slow_progress_sample() { +void cmd_context::slow_progress_sample() { SASSERT(m_solver); statistics st; regular_stream() << "(progress\n"; diff --git a/src/shell/smtlib_frontend.cpp b/src/shell/smtlib_frontend.cpp index eb3b3587d..834fe4429 100644 --- a/src/shell/smtlib_frontend.cpp +++ b/src/shell/smtlib_frontend.cpp @@ -56,7 +56,7 @@ static void display_statistics() { } static void on_timeout() { - #pragma omp critical (g_display_stats) + #pragma omp critical (g_display_stats) { display_statistics(); exit(0); @@ -65,7 +65,7 @@ static void on_timeout() { static void on_ctrl_c(int) { signal (SIGINT, SIG_DFL); - #pragma omp critical (g_display_stats) + #pragma omp critical (g_display_stats) { display_statistics(); } @@ -78,9 +78,9 @@ unsigned read_smtlib_file(char const * benchmark_file) { signal(SIGINT, on_ctrl_c); smtlib::solver solver; g_solver = &solver; - + bool ok = true; - + ok = solver.solve_smt(benchmark_file); if (!ok) { if (benchmark_file) { @@ -90,8 +90,8 @@ unsigned read_smtlib_file(char const * benchmark_file) { std::cerr << "ERROR: solving input stream.\n"; } } - - #pragma omp critical (g_display_stats) + + #pragma omp critical (g_display_stats) { display_statistics(); register_on_timeout_proc(0); @@ -117,7 +117,7 @@ unsigned read_smtlib2_commands(char const * file_name) { g_cmd_context = &ctx; signal(SIGINT, on_ctrl_c); - + bool result = true; if (file_name) { std::ifstream in(file_name); @@ -130,9 +130,9 @@ unsigned read_smtlib2_commands(char const * file_name) { else { result = parse_smt2_commands(ctx, std::cin, true); } - - #pragma omp critical (g_display_stats) + + #pragma omp critical (g_display_stats) { display_statistics(); g_cmd_context = 0; From 20715bbf3b3953589f08142f000a5ffe4fb2ce48 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 3 Nov 2015 12:29:02 +0000 Subject: [PATCH 14/21] Fixed initialization of interpolation context so it is properly disabled when solving SMT v1 benchmarks. --- src/cmd_context/cmd_context.cpp | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 132418a11..7ed93ab37 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -1604,8 +1604,7 @@ void cmd_context::mk_solver() { bool proofs_enabled, models_enabled, unsat_core_enabled; params_ref p; m_params.get_solver_params(m(), p, proofs_enabled, models_enabled, unsat_core_enabled); - if(produce_interpolants()){ - SASSERT(m_interpolating_solver_factory); + if (produce_interpolants() && m_interpolating_solver_factory) { m_solver = (*m_interpolating_solver_factory)(m(), p, true /* must have proofs */, models_enabled, unsat_core_enabled, m_logic); } else From 27140c527ceae88e80b69364d37f0bb8e3624abb Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 3 Nov 2015 12:56:29 +0000 Subject: [PATCH 15/21] trailing whitespace --- src/ast/rewriter/arith_rewriter.cpp | 168 ++++++++++++++-------------- src/ast/rewriter/poly_rewriter.h | 10 +- 2 files changed, 89 insertions(+), 89 deletions(-) diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp index bea672265..d8a6f7e08 100644 --- a/src/ast/rewriter/arith_rewriter.cpp +++ b/src/ast/rewriter/arith_rewriter.cpp @@ -120,7 +120,7 @@ bool arith_rewriter::div_polynomial(expr * t, numeral const & g, const_treatment SASSERT(!g.is_one()); unsigned sz; expr * const * ms = get_monomials(t, sz); - expr_ref_buffer new_args(m()); + expr_ref_buffer new_args(m()); numeral a; for (unsigned i = 0; i < sz; i++) { expr * arg = ms[i]; @@ -357,21 +357,21 @@ br_status arith_rewriter::mk_le_ge_eq_core(expr * arg1, expr * arg2, op_kind kin if (m_anum_simp) { if (is_numeral(arg1, a1) && m_util.is_irrational_algebraic_numeral(arg2)) { - anum_manager & am = m_util.am(); + anum_manager & am = m_util.am(); scoped_anum v1(am); am.set(v1, a1.to_mpq()); anum const & v2 = m_util.to_irrational_algebraic_numeral(arg2); ANUM_LE_GE_EQ(); } if (m_util.is_irrational_algebraic_numeral(arg1) && is_numeral(arg2, a2)) { - anum_manager & am = m_util.am(); + anum_manager & am = m_util.am(); anum const & v1 = m_util.to_irrational_algebraic_numeral(arg1); scoped_anum v2(am); am.set(v2, a2.to_mpq()); ANUM_LE_GE_EQ(); } if (m_util.is_irrational_algebraic_numeral(arg1) && m_util.is_irrational_algebraic_numeral(arg2)) { - anum_manager & am = m_util.am(); + anum_manager & am = m_util.am(); anum const & v1 = m_util.to_irrational_algebraic_numeral(arg1); anum const & v2 = m_util.to_irrational_algebraic_numeral(arg2); ANUM_LE_GE_EQ(); @@ -384,7 +384,7 @@ br_status arith_rewriter::mk_le_ge_eq_core(expr * arg1, expr * arg2, op_kind kin bool is_int = m_util.is_int(arg1); if (is_int && m_gcd_rounding) { bool first = true; - numeral g; + numeral g; unsigned num_consts = 0; get_coeffs_gcd(arg1, g, first, num_consts); TRACE("arith_rewriter_gcd", tout << "[step1] g: " << g << ", num_consts: " << num_consts << "\n";); @@ -454,7 +454,7 @@ bool arith_rewriter::is_anum_simp_target(unsigned num_args, expr * const * args) if (num_irrat > 0) return true; } - if (m_util.is_irrational_algebraic_numeral(args[i]) && + if (m_util.is_irrational_algebraic_numeral(args[i]) && m_util.am().degree(m_util.to_irrational_algebraic_numeral(args[i])) <= m_max_degree) { num_irrat++; if (num_irrat > 1 || num_rat > 0) @@ -466,9 +466,9 @@ bool arith_rewriter::is_anum_simp_target(unsigned num_args, expr * const * args) br_status arith_rewriter::mk_add_core(unsigned num_args, expr * const * args, expr_ref & result) { if (is_anum_simp_target(num_args, args)) { - expr_ref_buffer new_args(m()); - anum_manager & am = m_util.am(); - scoped_anum r(am); + expr_ref_buffer new_args(m()); + anum_manager & am = m_util.am(); + scoped_anum r(am); scoped_anum arg(am); rational rarg; am.set(r, 0); @@ -478,13 +478,13 @@ br_status arith_rewriter::mk_add_core(unsigned num_args, expr * const * args, ex new_args.push_back(m_util.mk_numeral(r, false)); am.set(r, 0); } - + if (m_util.is_numeral(args[i], rarg)) { am.set(arg, rarg.to_mpq()); am.add(r, arg, r); continue; } - + if (m_util.is_irrational_algebraic_numeral(args[i])) { anum const & irarg = m_util.to_irrational_algebraic_numeral(args[i]); if (am.degree(irarg) <= m_max_degree) { @@ -516,9 +516,9 @@ br_status arith_rewriter::mk_add_core(unsigned num_args, expr * const * args, ex br_status arith_rewriter::mk_mul_core(unsigned num_args, expr * const * args, expr_ref & result) { if (is_anum_simp_target(num_args, args)) { - expr_ref_buffer new_args(m()); - anum_manager & am = m_util.am(); - scoped_anum r(am); + expr_ref_buffer new_args(m()); + anum_manager & am = m_util.am(); + scoped_anum r(am); scoped_anum arg(am); rational rarg; am.set(r, 1); @@ -537,7 +537,7 @@ br_status arith_rewriter::mk_mul_core(unsigned num_args, expr * const * args, ex if (m_util.is_irrational_algebraic_numeral(args[i])) { anum const & irarg = m_util.to_irrational_algebraic_numeral(args[i]); if (am.degree(irarg) <= m_max_degree) { - am.mul(r, irarg, r); + am.mul(r, irarg, r); continue; } } @@ -550,7 +550,7 @@ br_status arith_rewriter::mk_mul_core(unsigned num_args, expr * const * args, ex return BR_DONE; } new_args.push_back(m_util.mk_numeral(r, false)); - + br_status st = poly_rewriter::mk_mul_core(new_args.size(), new_args.c_ptr(), result); if (st == BR_FAILED) { result = m().mk_app(get_fid(), OP_MUL, new_args.size(), new_args.c_ptr()); @@ -563,55 +563,55 @@ br_status arith_rewriter::mk_mul_core(unsigned num_args, expr * const * args, ex } } -br_status arith_rewriter::mk_div_irrat_rat(expr * arg1, expr * arg2, expr_ref & result) { - SASSERT(m_util.is_real(arg1)); - SASSERT(m_util.is_irrational_algebraic_numeral(arg1)); - SASSERT(m_util.is_numeral(arg2)); - anum_manager & am = m_util.am(); - anum const & val1 = m_util.to_irrational_algebraic_numeral(arg1); - rational rval2; +br_status arith_rewriter::mk_div_irrat_rat(expr * arg1, expr * arg2, expr_ref & result) { + SASSERT(m_util.is_real(arg1)); + SASSERT(m_util.is_irrational_algebraic_numeral(arg1)); + SASSERT(m_util.is_numeral(arg2)); + anum_manager & am = m_util.am(); + anum const & val1 = m_util.to_irrational_algebraic_numeral(arg1); + rational rval2; VERIFY(m_util.is_numeral(arg2, rval2)); if (rval2.is_zero()) return BR_FAILED; - scoped_anum val2(am); - am.set(val2, rval2.to_mpq()); - scoped_anum r(am); - am.div(val1, val2, r); - result = m_util.mk_numeral(r, false); - return BR_DONE; -} - -br_status arith_rewriter::mk_div_rat_irrat(expr * arg1, expr * arg2, expr_ref & result) { - SASSERT(m_util.is_real(arg1)); - SASSERT(m_util.is_numeral(arg1)); - SASSERT(m_util.is_irrational_algebraic_numeral(arg2)); - anum_manager & am = m_util.am(); - rational rval1; - VERIFY(m_util.is_numeral(arg1, rval1)); - scoped_anum val1(am); - am.set(val1, rval1.to_mpq()); - anum const & val2 = m_util.to_irrational_algebraic_numeral(arg2); - scoped_anum r(am); - am.div(val1, val2, r); - result = m_util.mk_numeral(r, false); - return BR_DONE; -} - -br_status arith_rewriter::mk_div_irrat_irrat(expr * arg1, expr * arg2, expr_ref & result) { - SASSERT(m_util.is_real(arg1)); - SASSERT(m_util.is_irrational_algebraic_numeral(arg1)); - SASSERT(m_util.is_irrational_algebraic_numeral(arg2)); - anum_manager & am = m_util.am(); - anum const & val1 = m_util.to_irrational_algebraic_numeral(arg1); - if (am.degree(val1) > m_max_degree) - return BR_FAILED; - anum const & val2 = m_util.to_irrational_algebraic_numeral(arg2); - if (am.degree(val2) > m_max_degree) - return BR_FAILED; + scoped_anum val2(am); + am.set(val2, rval2.to_mpq()); scoped_anum r(am); am.div(val1, val2, r); result = m_util.mk_numeral(r, false); - return BR_DONE; + return BR_DONE; +} + +br_status arith_rewriter::mk_div_rat_irrat(expr * arg1, expr * arg2, expr_ref & result) { + SASSERT(m_util.is_real(arg1)); + SASSERT(m_util.is_numeral(arg1)); + SASSERT(m_util.is_irrational_algebraic_numeral(arg2)); + anum_manager & am = m_util.am(); + rational rval1; + VERIFY(m_util.is_numeral(arg1, rval1)); + scoped_anum val1(am); + am.set(val1, rval1.to_mpq()); + anum const & val2 = m_util.to_irrational_algebraic_numeral(arg2); + scoped_anum r(am); + am.div(val1, val2, r); + result = m_util.mk_numeral(r, false); + return BR_DONE; +} + +br_status arith_rewriter::mk_div_irrat_irrat(expr * arg1, expr * arg2, expr_ref & result) { + SASSERT(m_util.is_real(arg1)); + SASSERT(m_util.is_irrational_algebraic_numeral(arg1)); + SASSERT(m_util.is_irrational_algebraic_numeral(arg2)); + anum_manager & am = m_util.am(); + anum const & val1 = m_util.to_irrational_algebraic_numeral(arg1); + if (am.degree(val1) > m_max_degree) + return BR_FAILED; + anum const & val2 = m_util.to_irrational_algebraic_numeral(arg2); + if (am.degree(val2) > m_max_degree) + return BR_FAILED; + scoped_anum r(am); + am.div(val1, val2, r); + result = m_util.mk_numeral(r, false); + return BR_DONE; } br_status arith_rewriter::mk_div_core(expr * arg1, expr * arg2, expr_ref & result) { @@ -681,7 +681,7 @@ br_status arith_rewriter::mk_idiv_core(expr * arg1, expr * arg2, expr_ref & resu } return BR_FAILED; } - + br_status arith_rewriter::mk_mod_core(expr * arg1, expr * arg2, expr_ref & result) { set_curr_sort(m().get_sort(arg1)); numeral v1, v2; @@ -690,7 +690,7 @@ br_status arith_rewriter::mk_mod_core(expr * arg1, expr * arg2, expr_ref & resul result = m_util.mk_numeral(mod(v1, v2), is_int); return BR_DONE; } - + if (m_util.is_numeral(arg2, v2, is_int) && is_int && v2.is_one()) { result = m_util.mk_numeral(numeral(0), true); return BR_DONE; @@ -728,7 +728,7 @@ br_status arith_rewriter::mk_mod_core(expr * arg1, expr * arg2, expr_ref & resul TRACE("mod_bug", tout << "mk_mod result: " << mk_ismt2_pp(result, m()) << "\n";); return BR_REWRITE3; } - + return BR_FAILED; } @@ -782,8 +782,8 @@ br_status arith_rewriter::mk_power_core(expr * arg1, expr * arg2, expr_ref & res bool is_num_x = m_util.is_numeral(arg1, x); bool is_num_y = m_util.is_numeral(arg2, y); bool is_int_sort = m_util.is_int(arg1); - - if ((is_num_x && x.is_one()) || + + if ((is_num_x && x.is_one()) || (is_num_y && y.is_one())) { result = arg1; return BR_DONE; @@ -792,8 +792,8 @@ br_status arith_rewriter::mk_power_core(expr * arg1, expr * arg2, expr_ref & res if (is_num_x && is_num_y) { if (x.is_zero() && y.is_zero()) return BR_FAILED; - - if (y.is_zero()) { + + if (y.is_zero()) { result = m_util.mk_numeral(rational(1), m().get_sort(arg1)); return BR_DONE; } @@ -803,12 +803,12 @@ br_status arith_rewriter::mk_power_core(expr * arg1, expr * arg2, expr_ref & res return BR_DONE; } - if (y.is_unsigned() && y.get_unsigned() <= m_max_degree) { + if (y.is_unsigned() && y.get_unsigned() <= m_max_degree) { x = power(x, y.get_unsigned()); result = m_util.mk_numeral(x, m().get_sort(arg1)); return BR_DONE; } - + if (!is_int_sort && (-y).is_unsigned() && (-y).get_unsigned() <= m_max_degree) { x = power(rational(1)/x, (-y).get_unsigned()); result = m_util.mk_numeral(x, m().get_sort(arg1)); @@ -854,10 +854,10 @@ br_status arith_rewriter::mk_power_core(expr * arg1, expr * arg2, expr_ref & res return BR_FAILED; bool is_irrat_x = m_util.is_irrational_algebraic_numeral(arg1); - - if (!is_num_x && !is_irrat_x) + + if (!is_num_x && !is_irrat_x) return BR_FAILED; - + rational num_y = numerator(y); rational den_y = denominator(y); bool is_neg_y = false; @@ -867,7 +867,7 @@ br_status arith_rewriter::mk_power_core(expr * arg1, expr * arg2, expr_ref & res } SASSERT(num_y.is_pos()); SASSERT(den_y.is_pos()); - + if (is_neg_y && is_int_sort) return BR_FAILED; @@ -876,10 +876,10 @@ br_status arith_rewriter::mk_power_core(expr * arg1, expr * arg2, expr_ref & res unsigned u_num_y = num_y.get_unsigned(); unsigned u_den_y = den_y.get_unsigned(); - + if (u_num_y > m_max_degree || u_den_y > m_max_degree) return BR_FAILED; - + if (is_num_x) { rational xk, r; xk = power(x, u_num_y); @@ -984,7 +984,7 @@ br_status arith_rewriter::mk_to_real_core(expr * arg, expr_ref & result) { for (unsigned i = 0; i < num; i++) { new_args.push_back(m_util.mk_to_real(to_app(arg)->get_arg(i))); } - if (m_util.is_add(arg)) + if (m_util.is_add(arg)) result = m().mk_app(get_fid(), OP_ADD, new_args.size(), new_args.c_ptr()); else result = m().mk_app(get_fid(), OP_MUL, new_args.size(), new_args.c_ptr()); @@ -1052,9 +1052,9 @@ bool arith_rewriter::is_pi_offset(expr * t, rational & k, expr * & m) { bool arith_rewriter::is_2_pi_integer(expr * t) { expr * a, * m, * b, * c; rational k; - return - m_util.is_mul(t, a, m) && - m_util.is_numeral(a, k) && + return + m_util.is_mul(t, a, m) && + m_util.is_numeral(a, k) && k.is_int() && mod(k, rational(2)).is_zero() && m_util.is_mul(m, b, c) && @@ -1094,7 +1094,7 @@ bool arith_rewriter::is_pi_integer(expr * t) { TRACE("tan", tout << "is_pi_integer " << mk_ismt2_pp(t, m()) << "\n"; tout << "a: " << mk_ismt2_pp(a, m()) << "\n"; tout << "b: " << mk_ismt2_pp(b, m()) << "\n";); - return + return (m_util.is_pi(a) && m_util.is_to_real(b)) || (m_util.is_to_real(a) && m_util.is_pi(b)); } @@ -1130,7 +1130,7 @@ expr * arith_rewriter::mk_sin_value(rational const & k) { bool neg = false; if (k_prime >= rational(1)) { neg = true; - k_prime = k_prime - rational(1); + k_prime = k_prime - rational(1); } SASSERT(k_prime >= rational(0) && k_prime < rational(1)); if (k_prime.is_zero() || k_prime.is_one()) { @@ -1342,7 +1342,7 @@ br_status arith_rewriter::mk_tan_core(expr * arg, expr_ref & result) { } br_status arith_rewriter::mk_asin_core(expr * arg, expr_ref & result) { - // Remark: we assume that ForAll x : asin(-x) == asin(x). + // Remark: we assume that ForAll x : asin(-x) == asin(x). // Mathematica uses this as an axiom. Although asin is an underspecified function for x < -1 or x > 1. // Actually, in Mathematica, asin(x) is a total function that returns a complex number fo x < -1 or x > 1. rational k; @@ -1355,13 +1355,13 @@ br_status arith_rewriter::mk_asin_core(expr * arg, expr_ref & result) { // asin(-2) == -asin(2) // asin(-3) == -asin(3) k.neg(); - result = m_util.mk_uminus(m_util.mk_asin(m_util.mk_numeral(k, false))); + result = m_util.mk_uminus(m_util.mk_asin(m_util.mk_numeral(k, false))); return BR_REWRITE2; } if (k > rational(1)) return BR_FAILED; - + bool neg = false; if (k.is_neg()) { neg = true; @@ -1450,7 +1450,7 @@ br_status arith_rewriter::mk_atan_core(expr * arg, expr_ref & result) { // atan(-2) == -tan(2) // atan(-3) == -tan(3) k.neg(); - result = m_util.mk_uminus(m_util.mk_atan(m_util.mk_numeral(k, false))); + result = m_util.mk_uminus(m_util.mk_atan(m_util.mk_numeral(k, false))); return BR_REWRITE2; } return BR_FAILED; diff --git a/src/ast/rewriter/poly_rewriter.h b/src/ast/rewriter/poly_rewriter.h index 90a807874..ea0b9e85a 100644 --- a/src/ast/rewriter/poly_rewriter.h +++ b/src/ast/rewriter/poly_rewriter.h @@ -27,7 +27,7 @@ Notes: template class poly_rewriter : public Config { protected: - typedef typename Config::numeral numeral; + typedef typename Config::numeral numeral; sort * m_curr_sort; obj_map m_expr2pos; bool m_flat; @@ -36,7 +36,7 @@ protected: bool m_sort_sums; bool m_hoist_mul; bool m_hoist_cmul; - + bool is_numeral(expr * n) const { return Config::is_numeral(n); } bool is_numeral(expr * n, numeral & r) const { return Config::is_numeral(n, r); } bool is_zero(expr * n) const { return Config::is_zero(n); } @@ -85,10 +85,10 @@ protected: struct hoist_cmul_lt; bool is_mul(expr * t, numeral & c, expr * & pp); void hoist_cmul(expr_ref_buffer & args); - + public: poly_rewriter(ast_manager & m, params_ref const & p = params_ref()): - Config(m), + Config(m), m_curr_sort(0), m_sort_sums(false) { updt_params(p); @@ -154,7 +154,7 @@ public: // The result of the following functions is never BR_FAILED br_status mk_uminus(expr * arg, expr_ref & result); br_status mk_sub(unsigned num_args, expr * const * args, expr_ref & result); - + void mk_sub(expr* a1, expr* a2, expr_ref& result) { expr* args[2] = { a1, a2 }; mk_sub(2, args, result); From bd94b59a92b3370e9ceba2b2645e8f0afdd956d9 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 3 Nov 2015 13:00:10 +0000 Subject: [PATCH 16/21] Bugfix for arith rewriter to avoid rewriting loops. --- src/ast/rewriter/arith_rewriter.cpp | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp index d8a6f7e08..be088d2b5 100644 --- a/src/ast/rewriter/arith_rewriter.cpp +++ b/src/ast/rewriter/arith_rewriter.cpp @@ -318,6 +318,7 @@ br_status arith_rewriter::reduce_power(expr * arg1, expr * arg2, op_kind kind, e } br_status arith_rewriter::mk_le_ge_eq_core(expr * arg1, expr * arg2, op_kind kind, expr_ref & result) { + expr *orig_arg1 = arg1, *orig_arg2 = arg2; expr_ref new_arg1(m()); expr_ref new_arg2(m()); if ((is_zero(arg1) && is_reduce_power_target(arg2, kind == EQ)) || @@ -407,7 +408,11 @@ br_status arith_rewriter::mk_le_ge_eq_core(expr * arg1, expr * arg2, op_kind kin st = BR_DONE; } } - if (st != BR_FAILED) { + if (st == BR_DONE && arg1 == orig_arg1 && arg2 == orig_arg2) { + // Nothing new; return BR_FAILED to avoid rewriting loops. + return BR_FAILED; + } + else if (st != BR_FAILED) { switch (kind) { case LE: result = m_util.mk_le(arg1, arg2); return BR_DONE; case GE: result = m_util.mk_ge(arg1, arg2); return BR_DONE; From 2f216ee5c1952bafae36b9f5905310ca8069181e Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 3 Nov 2015 15:35:43 +0000 Subject: [PATCH 17/21] Fixed PREFIX for OSX installation. Fixes #124. --- scripts/mk_util.py | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index e53a90127..0baed2968 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -75,7 +75,7 @@ VER_MAJOR=None VER_MINOR=None VER_BUILD=None VER_REVISION=None -PREFIX=os.path.split(os.path.split(os.path.split(PYTHON_PACKAGE_DIR)[0])[0])[0] +PREFIX=sys.prefix GMP=False FOCI2=False FOCI2LIB='' @@ -531,6 +531,7 @@ if os.name == 'nt': elif os.name == 'posix': if os.uname()[0] == 'Darwin': IS_OSX=True + PREFIX="/usr/local" elif os.uname()[0] == 'Linux': IS_LINUX=True elif os.uname()[0] == 'FreeBSD': @@ -1984,6 +1985,7 @@ def mk_config(): print('Prefix: %s' % PREFIX) print('64-bit: %s' % is64()) print('FP math: %s' % FPMATH) + print("Python pkg dir: %s" % PYTHON_PACKAGE_DIR) if GPROF: print('gprof: enabled') print('Python version: %s' % distutils.sysconfig.get_python_version()) @@ -2074,8 +2076,6 @@ def mk_makefile(): # Finalize if VERBOSE: print("Makefile was successfully generated.") - if not IS_WINDOWS: - print(" python packages dir: %s" % PYTHON_PACKAGE_DIR) if DEBUG_MODE: print(" compilation mode: Debug") else: From d6cb778365decade923f4f8a8fef9f5ac7626177 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 3 Nov 2015 07:45:42 -0800 Subject: [PATCH 18/21] fix rewriter for model validation Signed-off-by: Nikolaj Bjorner --- src/model/model_evaluator.cpp | 27 ++++++++++++++------------- 1 file changed, 14 insertions(+), 13 deletions(-) diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp index 67704719b..8ee2fb9cc 100644 --- a/src/model/model_evaluator.cpp +++ b/src/model/model_evaluator.cpp @@ -73,6 +73,11 @@ struct evaluator_cfg : public default_rewriter_cfg { ast_manager & m() const { return m_model.get_manager(); } + bool evaluate(func_decl* f, unsigned num, expr * const * args, expr_ref & result) { + func_interp* fi = m_model.get_func_interp(f); + return (fi != 0) && eval_fi(fi, num, args, result); + } + // Try to use the entries to quickly evaluate the fi bool eval_fi(func_interp * fi, unsigned num, expr * const * args, expr_ref & result) { if (fi->num_entries() == 0) @@ -152,23 +157,19 @@ struct evaluator_cfg : public default_rewriter_cfg { st = m_pb_rw.mk_app_core(f, num, args, result); else if (fid == m_f_rw.get_fid()) st = m_f_rw.mk_app_core(f, num, args, result); - - // allow for model evaluation to work on result of rewriting. - if (st == BR_DONE && is_app(result) && to_app(result)->get_num_args() > 0) { - return BR_REWRITE1; + else if (evaluate(f, num, args, result)) { + TRACE("model_evaluator", tout << "reduce_app " << f->get_name() << "\n"; + for (unsigned i = 0; i < num; i++) tout << mk_ismt2_pp(args[i], m()) << "\n"; + tout << "---->\n" << mk_ismt2_pp(result, m()) << "\n";); + return BR_DONE; } - - if (st == BR_FAILED) { - func_interp * fi = m_model.get_func_interp(f); - if (fi != 0 && eval_fi(fi, num, args, result)) { - TRACE("model_evaluator", tout << "reduce_app " << f->get_name() << "\n"; - for (unsigned i = 0; i < num; i++) tout << mk_ismt2_pp(args[i], m()) << "\n"; - tout << "---->\n" << mk_ismt2_pp(result, m()) << "\n";); + if (st == BR_DONE && is_app(result)) { + app* a = to_app(result); + if (evaluate(a->get_decl(), a->get_num_args(), a->get_args(), result)) { return BR_DONE; } - TRACE("model_evaluator", tout << f->get_name() << "\n";); } - + TRACE("model_evaluator", tout << f->get_name() << "\n";); return st; } From 715050da0b73b83fe7dad16ff645924d724425d7 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 4 Nov 2015 13:34:50 +0000 Subject: [PATCH 19/21] Java API comments fix. --- src/api/java/Model.java | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/api/java/Model.java b/src/api/java/Model.java index e9922ac58..28934a1f3 100644 --- a/src/api/java/Model.java +++ b/src/api/java/Model.java @@ -56,7 +56,7 @@ public class Model extends Z3Object Native.getRange(getContext().nCtx(), f.getNativeObject())) == Z3_sort_kind.Z3_ARRAY_SORT .toInt()) throw new Z3Exception( - "Non-zero arity functions and arrays have FunctionInterpretations as a model. Use FuncInterp."); + "Non-zero arity functions and arrays have FunctionInterpretations as a model. Use getFuncInterp."); long n = Native.modelGetConstInterp(getContext().nCtx(), getNativeObject(), f.getNativeObject()); @@ -101,7 +101,7 @@ public class Model extends Z3Object } else { throw new Z3Exception( - "Constant functions do not have a function interpretation; use ConstInterp"); + "Constant functions do not have a function interpretation; use getConstInterp"); } } else { From ebbed7a92e19c43e680eb6514be5fc90f37c221a Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 4 Nov 2015 15:44:29 +0000 Subject: [PATCH 20/21] Added tactic comments for QF_AUFLIA, QF_AUFBV, QF_UF, and QF_UFBV default tactics. --- src/tactic/smtlogics/qfaufbv_tactic.h | 4 ++++ src/tactic/smtlogics/qfauflia_tactic.h | 4 ++++ src/tactic/smtlogics/qfidl_tactic.h | 4 ++++ src/tactic/smtlogics/qfuf_tactic.h | 4 ++++ src/tactic/smtlogics/qfufbv_tactic.h | 6 +++++- 5 files changed, 21 insertions(+), 1 deletion(-) diff --git a/src/tactic/smtlogics/qfaufbv_tactic.h b/src/tactic/smtlogics/qfaufbv_tactic.h index d4503a5de..1e4a7419f 100644 --- a/src/tactic/smtlogics/qfaufbv_tactic.h +++ b/src/tactic/smtlogics/qfaufbv_tactic.h @@ -25,4 +25,8 @@ class tactic; tactic * mk_qfaufbv_tactic(ast_manager & m, params_ref const & p = params_ref()); +/* + ADD_TACTIC("qfaufbv", "builtin strategy for solving QF_AUFBV problems.", "mk_qfaufbv_tactic(m, p)") +*/ + #endif diff --git a/src/tactic/smtlogics/qfauflia_tactic.h b/src/tactic/smtlogics/qfauflia_tactic.h index 10b790e70..fbf19fec0 100644 --- a/src/tactic/smtlogics/qfauflia_tactic.h +++ b/src/tactic/smtlogics/qfauflia_tactic.h @@ -25,4 +25,8 @@ class tactic; tactic * mk_qfauflia_tactic(ast_manager & m, params_ref const & p = params_ref()); +/* + ADD_TACTIC("qfauflia", "builtin strategy for solving QF_AUFLIA problems.", "mk_qfauflia_tactic(m, p)") +*/ + #endif diff --git a/src/tactic/smtlogics/qfidl_tactic.h b/src/tactic/smtlogics/qfidl_tactic.h index f502dbd89..f892bb8a5 100644 --- a/src/tactic/smtlogics/qfidl_tactic.h +++ b/src/tactic/smtlogics/qfidl_tactic.h @@ -25,4 +25,8 @@ class tactic; tactic * mk_qfidl_tactic(ast_manager & m, params_ref const & p = params_ref()); +/* + ADD_TACTIC("qfidl", "builtin strategy for solving QF_IDL problems.", "mk_qfidl_tactic(m, p)") +*/ + #endif diff --git a/src/tactic/smtlogics/qfuf_tactic.h b/src/tactic/smtlogics/qfuf_tactic.h index 732e1289f..0c81ad57b 100644 --- a/src/tactic/smtlogics/qfuf_tactic.h +++ b/src/tactic/smtlogics/qfuf_tactic.h @@ -26,4 +26,8 @@ class tactic; tactic * mk_qfuf_tactic(ast_manager & m, params_ref const & p); +/* + ADD_TACTIC("qfuf", "builtin strategy for solving QF_UF problems.", "mk_qfuf_tactic(m, p)") +*/ + #endif diff --git a/src/tactic/smtlogics/qfufbv_tactic.h b/src/tactic/smtlogics/qfufbv_tactic.h index e9ffe4dc3..ceb125517 100644 --- a/src/tactic/smtlogics/qfufbv_tactic.h +++ b/src/tactic/smtlogics/qfufbv_tactic.h @@ -7,7 +7,7 @@ Module Name: Abstract: - Tactic for QF_UFBV + Tactic for QF_UFBV Author: @@ -25,4 +25,8 @@ class tactic; tactic * mk_qfufbv_tactic(ast_manager & m, params_ref const & p = params_ref()); +/* + ADD_TACTIC("qfufbv", "builtin strategy for solving QF_UFBV problems.", "mk_qfufbv_tactic(m, p)") +*/ + #endif From d4242e16c5dfc74b66b0a0adcd1a24f2ef11315b Mon Sep 17 00:00:00 2001 From: Patrick Totzke Date: Thu, 5 Nov 2015 16:28:02 +0000 Subject: [PATCH 21/21] add __hash__ to AstRef AstRef objects needs to be hashable in order to be used as keys in python dictionaries --- src/api/python/z3.py | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/api/python/z3.py b/src/api/python/z3.py index 5763db916..84fd7b111 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -284,6 +284,9 @@ class AstRef(Z3PPObject): def __repr__(self): return obj_to_string(self) + def __hash__(self): + return self.hash() + def sexpr(self): """Return an string representing the AST node in s-expression notation.