From fae66671d8b7edf22e1508796f063caf3d0b9497 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 10 Sep 2018 08:57:35 -0700 Subject: [PATCH] fix #1817 Signed-off-by: Nikolaj Bjorner --- src/smt/smt_internalizer.cpp | 41 +++++++++++++++++------------------- src/smt/theory_arith_core.h | 1 - src/smt/theory_lra.cpp | 8 +++---- 3 files changed, 22 insertions(+), 28 deletions(-) diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp index 1414cb522..618450f9d 100644 --- a/src/smt/smt_internalizer.cpp +++ b/src/smt/smt_internalizer.cpp @@ -216,13 +216,17 @@ namespace smt { SASSERT(m_manager.is_bool(n)); if (is_gate(m_manager, n)) { switch(to_app(n)->get_decl_kind()) { - case OP_AND: - UNREACHABLE(); + case OP_AND: { + for (expr * arg : *to_app(n)) { + internalize(arg, true); + literal lit = get_literal(arg); + mk_root_clause(1, &lit, pr); + } + break; + } case OP_OR: { literal_buffer lits; - unsigned num = to_app(n)->get_num_args(); - for (unsigned i = 0; i < num; i++) { - expr * arg = to_app(n)->get_arg(i); + for (expr * arg : *to_app(n)) { internalize(arg, true); lits.push_back(get_literal(arg)); } @@ -294,8 +298,7 @@ namespace smt { sort * s = m_manager.get_sort(n->get_arg(0)); sort_ref u(m_manager.mk_fresh_sort("distinct-elems"), m_manager); func_decl_ref f(m_manager.mk_fresh_func_decl("distinct-aux-f", "", 1, &s, u), m_manager); - for (unsigned i = 0; i < num_args; i++) { - expr * arg = n->get_arg(i); + for (expr * arg : *n) { app_ref fapp(m_manager.mk_app(f, arg), m_manager); app_ref val(m_manager.mk_fresh_const("unique-value", u), m_manager); enode * e = mk_enode(val, false, false, true); @@ -826,9 +829,7 @@ namespace smt { void context::internalize_uninterpreted(app * n) { SASSERT(!e_internalized(n)); // process args - unsigned num = n->get_num_args(); - for (unsigned i = 0; i < num; i++) { - expr * arg = n->get_arg(i); + for (expr * arg : *n) { internalize(arg, false); SASSERT(e_internalized(arg)); } @@ -1542,10 +1543,9 @@ namespace smt { void context::add_and_rel_watches(app * n) { if (relevancy()) { relevancy_eh * eh = m_relevancy_propagator->mk_and_relevancy_eh(n); - unsigned num = n->get_num_args(); - for (unsigned i = 0; i < num; i++) { + for (expr * arg : *n) { // if one child is assigned to false, the and-parent must be notified - literal l = get_literal(n->get_arg(i)); + literal l = get_literal(arg); add_rel_watch(~l, eh); } } @@ -1554,10 +1554,9 @@ namespace smt { void context::add_or_rel_watches(app * n) { if (relevancy()) { relevancy_eh * eh = m_relevancy_propagator->mk_or_relevancy_eh(n); - unsigned num = n->get_num_args(); - for (unsigned i = 0; i < num; i++) { + for (expr * arg : *n) { // if one child is assigned to true, the or-parent must be notified - literal l = get_literal(n->get_arg(i)); + literal l = get_literal(arg); add_rel_watch(l, eh); } } @@ -1588,9 +1587,8 @@ namespace smt { TRACE("mk_and_cnstr", tout << "l: "; display_literal(tout, l); tout << "\n";); literal_buffer buffer; buffer.push_back(l); - unsigned num_args = n->get_num_args(); - for (unsigned i = 0; i < num_args; i++) { - literal l_arg = get_literal(n->get_arg(i)); + for (expr * arg : *n) { + literal l_arg = get_literal(arg); TRACE("mk_and_cnstr", tout << "l_arg: "; display_literal(tout, l_arg); tout << "\n";); mk_gate_clause(~l, l_arg); buffer.push_back(~l_arg); @@ -1602,9 +1600,8 @@ namespace smt { literal l = get_literal(n); literal_buffer buffer; buffer.push_back(~l); - unsigned num_args = n->get_num_args(); - for (unsigned i = 0; i < num_args; i++) { - literal l_arg = get_literal(n->get_arg(i)); + for (expr * arg : *n) { + literal l_arg = get_literal(arg); mk_gate_clause(l, ~l_arg); buffer.push_back(l_arg); } diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index f96b6228b..67271ad4f 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -484,7 +484,6 @@ namespace smt { void theory_arith::mk_idiv_mod_axioms(expr * dividend, expr * divisor) { if (!m_util.is_zero(divisor)) { ast_manager & m = get_manager(); - bool is_numeral = m_util.is_numeral(divisor); // if divisor is zero, then idiv and mod are uninterpreted functions. expr_ref div(m), mod(m), zero(m), abs_divisor(m), one(m); expr_ref eqz(m), eq(m), lower(m), upper(m); diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 267412da6..b7f8549fb 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -692,9 +692,7 @@ class theory_lra::imp { ++m_stats.m_add_rows; } - void internalize_eq(theory_var v1, theory_var v2) { - enode* n1 = get_enode(v1); - enode* n2 = get_enode(v2); + void internalize_eq(theory_var v1, theory_var v2) { app_ref term(m.mk_fresh_const("eq", a.mk_real()), m); scoped_internalize_state st(*this); st.vars().push_back(v1); @@ -707,8 +705,8 @@ class theory_lra::imp { add_def_constraint(m_solver->add_var_bound(vi, lp::GE, rational::zero())); TRACE("arith", { - expr* o1 = n1->get_owner(); - expr* o2 = n2->get_owner(); + expr* o1 = get_enode(v1)->get_owner(); + expr* o2 = get_enode(v2)->get_owner(); tout << "v" << v1 << " = " << "v" << v2 << ": " << mk_pp(o1, m) << " = " << mk_pp(o2, m) << "\n"; });