diff --git a/src/muz/base/rule_properties.cpp b/src/muz/base/rule_properties.cpp index 7f019c74e..f5cac29e5 100644 --- a/src/muz/base/rule_properties.cpp +++ b/src/muz/base/rule_properties.cpp @@ -26,7 +26,7 @@ Notes: using namespace datalog; rule_properties::rule_properties(ast_manager & m, rule_manager& rm, context& ctx, i_expr_pred& p): - m(m), rm(rm), m_ctx(ctx), m_is_predicate(p), m_dt(m), m_generate_proof(false) {} + m(m), rm(rm), m_ctx(ctx), m_is_predicate(p), m_dt(m), m_dl(m), m_generate_proof(false) {} rule_properties::~rule_properties() {} @@ -168,7 +168,7 @@ void rule_properties::operator()(app* n) { if (m_is_predicate(n)) { insert(m_interp_pred, m_rule); } - else if (is_uninterp(n)) { + else if (is_uninterp(n) && !m_dl.is_rule_sort(n->get_decl()->get_range())) { m_uninterp_funs.insert(n->get_decl(), m_rule); } else if (m_dt.is_accessor(n)) { diff --git a/src/muz/base/rule_properties.h b/src/muz/base/rule_properties.h index bfff8cbe4..a16f63507 100644 --- a/src/muz/base/rule_properties.h +++ b/src/muz/base/rule_properties.h @@ -32,6 +32,7 @@ namespace datalog { context& m_ctx; i_expr_pred& m_is_predicate; datatype_util m_dt; + dl_decl_util m_dl; bool m_generate_proof; rule* m_rule; obj_map m_quantifiers; diff --git a/src/muz/rel/dl_mk_explanations.cpp b/src/muz/rel/dl_mk_explanations.cpp index 60a10190a..e650b6e6b 100644 --- a/src/muz/rel/dl_mk_explanations.cpp +++ b/src/muz/rel/dl_mk_explanations.cpp @@ -434,6 +434,7 @@ namespace datalog { relation_union_fn * explanation_relation_plugin::mk_union_fn(const relation_base & tgt, const relation_base & src, const relation_base * delta) { + std::cout << "check kind: " << check_kind(tgt) << "\n"; if (!check_kind(tgt) || (delta && !check_kind(*delta))) { return 0; } @@ -854,7 +855,10 @@ namespace datalog { scoped_ptr product_fun = rmgr.mk_join_fn(orig_rel, *m_e_fact_relation, 0, 0, 0); SASSERT(product_fun); scoped_rel aux_extended_rel = (*product_fun)(orig_rel, *m_e_fact_relation); + TRACE("dl", tout << aux_extended_rel << " " << aux_extended_rel->get_plugin().get_name() << "\n"; + tout << e_rel.get_plugin().get_name() << "\n";); scoped_ptr union_fun = rmgr.mk_union_fn(e_rel, *aux_extended_rel); + TRACE("dl", tout << union_fun << "\n";); SASSERT(union_fun); (*union_fun)(e_rel, *aux_extended_rel); } diff --git a/src/muz/rel/karr_relation.h b/src/muz/rel/karr_relation.h index 00a92748a..72448f026 100644 --- a/src/muz/rel/karr_relation.h +++ b/src/muz/rel/karr_relation.h @@ -45,7 +45,7 @@ namespace datalog { {} virtual bool can_handle_signature(const relation_signature & sig) { - return true; + return get_manager().get_context().karr(); } static symbol get_name() { return symbol("karr_relation"); } diff --git a/src/muz/rel/rel_context.cpp b/src/muz/rel/rel_context.cpp index c5c4d6d95..0d07b7c81 100644 --- a/src/muz/rel/rel_context.cpp +++ b/src/muz/rel/rel_context.cpp @@ -115,7 +115,7 @@ namespace datalog { rm.register_plugin(alloc(bound_relation_plugin, rm)); rm.register_plugin(alloc(interval_relation_plugin, rm)); - rm.register_plugin(alloc(karr_relation_plugin, rm)); + if (m_context.karr()) rm.register_plugin(alloc(karr_relation_plugin, rm)); rm.register_plugin(alloc(product_set_plugin, rm)); rm.register_plugin(alloc(udoc_plugin, rm)); rm.register_plugin(alloc(check_relation_plugin, rm)); diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h index 15d1edee9..30c92feea 100644 --- a/src/smt/theory_arith_aux.h +++ b/src/smt/theory_arith_aux.h @@ -1377,11 +1377,11 @@ namespace smt { SASSERT(satisfy_bounds()); result = skipped_row?BEST_EFFORT:OPTIMIZED; break; - } + } if (x_i == null_theory_var) { // can increase/decrease x_j as much as we want. - if (inc && upper(x_j)) { + if (inc && upper(x_j) && !skipped_row) { update_value(x_j, upper_bound(x_j) - get_value(x_j)); TRACE("opt", tout << "moved v" << x_j << " to upper bound\n";); SASSERT(valid_row_assignment()); @@ -1389,7 +1389,7 @@ namespace smt { SASSERT(satisfy_integrality()); continue; } - if (!inc && lower(x_j)) { + if (!inc && lower(x_j) && !skipped_row) { update_value(x_j, lower_bound(x_j) - get_value(x_j)); TRACE("opt", tout << "moved v" << x_j << " to lower bound\n";); SASSERT(valid_row_assignment()); @@ -1463,6 +1463,7 @@ namespace smt { template bool theory_arith::move_to_bound(theory_var x_i, bool move_to_lower) { inf_numeral delta, delta_abs; + numeral lc(1); if (move_to_lower) { delta = lower_bound(x_i) - get_value(x_i); @@ -1475,7 +1476,7 @@ namespace smt { TRACE("opt", tout << "Original delta: " << delta << "\n";); - delta_abs = abs(delta); + delta_abs = abs(delta); // // Decrease absolute value of delta according to bounds on rows where x_i is used. // @@ -1483,28 +1484,31 @@ namespace smt { typename svector::iterator it = c.begin_entries(); typename svector::iterator end = c.end_entries(); for (; it != end && delta_abs.is_pos(); ++it) { - if (!it->is_dead()) { - row & r = m_rows[it->m_row_id]; - theory_var s = r.get_base_var(); - if (s != null_theory_var && !is_quasi_base(s)) { - numeral const & coeff = r[it->m_row_idx].m_coeff; - SASSERT(!coeff.is_zero()); - bool inc_s = coeff.is_pos() ? move_to_lower : !move_to_lower; // NSB: review this.. - bound * b = get_bound(s, inc_s); - if (b) { - inf_numeral delta2 = abs((get_value(s) - b->get_value())/coeff); - if (delta2 < delta_abs) { - delta_abs = delta2; - } + if (it->is_dead()) continue; + row & r = m_rows[it->m_row_id]; + theory_var s = r.get_base_var(); + if (s != null_theory_var && !is_quasi_base(s)) { + numeral const & coeff = r[it->m_row_idx].m_coeff; + SASSERT(!coeff.is_zero()); + bool inc_s = coeff.is_pos() ? move_to_lower : !move_to_lower; // NSB: review this.. + bound * b = get_bound(s, inc_s); + if (b) { + inf_numeral delta2 = abs((get_value(s) - b->get_value())/coeff); + if (delta2 < delta_abs) { + delta_abs = delta2; } } + if (is_int(x_i)) { + lc = lcm(lc, denominator(abs(coeff))); + } } } bool truncated = false; if (is_int(x_i)) { - truncated = !delta_abs.is_int(); - delta_abs = floor(delta_abs); + inf_numeral tmp = delta_abs/lc; + truncated = !tmp.is_int(); + delta_abs = lc*floor(tmp); } if (move_to_lower) {