diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp index 9b28af631..515edcbff 100644 --- a/src/opt/opt_solver.cpp +++ b/src/opt/opt_solver.cpp @@ -175,7 +175,8 @@ namespace opt { return expr_ref(m.mk_true(), m); } else { - return expr_ref(get_optimizer().block_lower_bound(m_objective_vars[var], val.get_numeral()), m); + inf_rational n = val.get_numeral(); + return expr_ref(get_optimizer().block_lower_bound(m_objective_vars[var], n), m); } } diff --git a/src/opt/opt_solver.h b/src/opt/opt_solver.h index 3c149aefd..4afa65f31 100644 --- a/src/opt/opt_solver.h +++ b/src/opt/opt_solver.h @@ -91,7 +91,6 @@ namespace opt { smt::context& get_context() { return m_context.get_context(); } // used by weighted maxsat. - private: smt::theory_opt& get_optimizer(); }; } diff --git a/src/opt/optimize_objectives.cpp b/src/opt/optimize_objectives.cpp index 8e111953e..086c52bf4 100644 --- a/src/opt/optimize_objectives.cpp +++ b/src/opt/optimize_objectives.cpp @@ -66,24 +66,16 @@ namespace opt { */ lbool optimize_objectives::basic_opt(app_ref_vector& objectives) { arith_util autil(m); - s->reset_objectives(); - m_lower.reset(); - m_upper.reset(); - // First check_sat call to initialize theories - lbool is_sat = s->check_sat(0, 0); - if (is_sat != l_true) { - return is_sat; - } opt_solver::scoped_push _push(*s); opt_solver::toggle_objective _t(*s, true); for (unsigned i = 0; i < objectives.size(); ++i) { - s->add_objective(objectives[i].get()); - m_lower.push_back(inf_eps(rational(-1),inf_rational(0))); - m_upper.push_back(inf_eps(rational(1), inf_rational(0))); + m_vars.push_back(s->add_objective(objectives[i].get())); } - + + lbool is_sat = l_true; + // ready to test: is_sat = update_upper(); while (is_sat == l_true && !m_cancel) { is_sat = update_lower(); } @@ -117,8 +109,31 @@ namespace opt { } lbool optimize_objectives::update_upper() { - NOT_IMPLEMENTED_YET(); - return l_undef; + smt::theory_opt& opt = s->get_optimizer(); + + if (typeid(smt::theory_inf_arith) != typeid(opt)) { + return l_true; + } + smt::theory_inf_arith& th = dynamic_cast(opt); + + expr_ref bound(m); + lbool is_sat = l_true; + + for (unsigned i = 0; i < m_lower.size(); ++i) { + if (m_lower[i] < m_upper[i]) { + opt_solver::scoped_push _push(*s); + smt::theory_var v = m_vars[i]; + bound = th.block_upper_bound(v, m_upper[i]); + expr* bounds[1] = { bound }; + is_sat = s->check_sat(1, bounds); + if (is_sat) { + IF_VERBOSE(1, verbose_stream() << "Setting lower bound for " << v << " to " << m_upper[i] << "\n";); + m_lower[i] = m_upper[i]; + } + // else: TBD extract Farkas coefficients. + } + } + return l_true; } /** @@ -127,10 +142,22 @@ namespace opt { */ lbool optimize_objectives::operator()(opt_solver& solver, app_ref_vector& objectives, vector& values) { s = &solver; - lbool result = basic_opt(objectives); - values.reset(); - values.append(m_lower); - return result; + s->reset_objectives(); + m_lower.reset(); + m_upper.reset(); + for (unsigned i = 0; i < objectives.size(); ++i) { + m_lower.push_back(inf_eps(rational(-1),inf_rational(0))); + m_upper.push_back(inf_eps(rational(1), inf_rational(0))); + } + + // First check_sat call to initialize theories + lbool is_sat = s->check_sat(0, 0); + if (is_sat == l_true) { + is_sat = basic_opt(objectives); + values.reset(); + values.append(m_lower); + } + return is_sat; } } diff --git a/src/opt/optimize_objectives.h b/src/opt/optimize_objectives.h index cb3176d0d..227cd8f00 100644 --- a/src/opt/optimize_objectives.h +++ b/src/opt/optimize_objectives.h @@ -33,6 +33,7 @@ namespace opt { volatile bool m_cancel; vector m_lower; vector m_upper; + svector m_vars; public: optimize_objectives(ast_manager& m): m(m), s(0), m_cancel(false) {} diff --git a/src/smt/diff_logic.h b/src/smt/diff_logic.h index b96a038eb..cf0d5f5a6 100644 --- a/src/smt/diff_logic.h +++ b/src/smt/diff_logic.h @@ -933,7 +933,7 @@ public: return found; } - // Return true if there is an edge source --> target. + // Return true if there is an edge source --> target (also counting disabled edges). // If there is such edge, return its edge_id in parameter id. bool get_edge_id(dl_var source, dl_var target, edge_id & id) { edge_id_vector & edges = m_out_edges[source]; @@ -942,7 +942,7 @@ public: for (; it != end; ++it) { id = *it; edge & e = m_edges[id]; - if (e.is_enabled() && e.get_target() == target) { + if (e.get_target() == target) { return true; } } diff --git a/src/smt/network_flow.h b/src/smt/network_flow.h index 865ac9791..a19cae0a2 100644 --- a/src/smt/network_flow.h +++ b/src/smt/network_flow.h @@ -42,8 +42,9 @@ namespace smt { template class network_flow : private Ext { enum edge_state { - NON_BASIS = 0, - BASIS = 1 + LOWER = 1, + BASIS = 0, + UPPER = -1 }; typedef dl_var node; typedef dl_edge edge; @@ -66,14 +67,15 @@ namespace smt { svector m_states; - // An element is true if the corresponding edge points upwards (compared to the root node) + // m_upwards[i] is true if the corresponding edge + // (i, m_pred[i]) points upwards (pointing toward the root node) svector m_upwards; // Store the parent of a node i in the spanning tree svector m_pred; // Store the number of edge on the path from node i to the root svector m_depth; - // Store the pointer from node i to the next node in depth first search ordering + // Store the pointer from node i to the next node in depth-first search order svector m_thread; // Reverse orders of m_thread svector m_rev_thread; @@ -83,7 +85,8 @@ namespace smt { edge_id m_entering_edge; edge_id m_leaving_edge; node m_join_node; - numeral m_delta; + optional m_delta; + bool m_in_edge_dir; unsigned m_step; @@ -109,6 +112,8 @@ namespace smt { std::string display_spanning_tree(); + bool check_well_formed(); + public: network_flow(graph & g, vector const & balances); diff --git a/src/smt/network_flow_def.h b/src/smt/network_flow_def.h index 02dd60e59..5d7f5018b 100644 --- a/src/smt/network_flow_def.h +++ b/src/smt/network_flow_def.h @@ -45,8 +45,20 @@ namespace smt { template network_flow::network_flow(graph & g, vector const & balances) : - m_graph(g), m_balances(balances) { + // Network flow graph has the edges in the reversed order compared to constraint graph + // We only take enabled edges from the original graph + for (unsigned i = 0; i < g.get_num_nodes(); ++i) { + m_graph.init_var(i); + } + vector const & es = g.get_all_edges(); + for (unsigned i = 0; i < es.size(); ++i) { + edge const & e = es[i]; + if (e.is_enabled()) { + m_graph.add_edge(e.get_target(), e.get_source(), e.get_weight(), explanation()); + } + } + unsigned num_nodes = m_graph.get_num_nodes() + 1; unsigned num_edges = m_graph.get_num_edges(); @@ -87,9 +99,9 @@ namespace smt { m_flows.resize(num_nodes + num_edges); m_states.resize(num_nodes + num_edges); - m_states.fill(NON_BASIS); + m_states.fill(LOWER); - // Create artificial edges and initialize the spanning tree + // Create artificial edges from/to root node to/from other nodes and initialize the spanning tree for (unsigned i = 0; i < num_nodes; ++i) { m_upwards[i] = !m_balances[i].is_neg(); m_pred[i] = root; @@ -101,12 +113,13 @@ namespace smt { node src = m_upwards[i] ? i : root; node tgt = m_upwards[i] ? root : i; m_flows[num_edges + i] = m_upwards[i] ? m_balances[i] : -m_balances[i]; - m_graph.enable_edge(m_graph.add_edge(src, tgt, numeral::one(), explanation())); + m_graph.add_edge(src, tgt, numeral::one(), explanation()); } // Compute initial potentials node u = m_thread[root]; while (u != root) { + bool direction = m_upwards[u]; node v = m_pred[u]; edge_id e_id = get_edge_id(u, v); m_potentials[u] = m_potentials[v] + (m_upwards[u] ? - m_graph.get_weight(e_id) : m_graph.get_weight(e_id)); @@ -120,6 +133,7 @@ namespace smt { tout << pp_vector("Potentials", m_potentials) << pp_vector("Flows", m_flows); }); TRACE("network_flow", tout << "Spanning tree:\n" << display_spanning_tree();); + SASSERT(check_well_formed()); } template @@ -136,7 +150,7 @@ namespace smt { node src = m_graph.get_source(m_entering_edge); node tgt = m_graph.get_target(m_entering_edge); numeral cost = m_graph.get_weight(m_entering_edge); - numeral change = m_upwards[src] ? (-cost + m_potentials[src] - m_potentials[tgt]) : (cost - m_potentials[src] + m_potentials[tgt]); + numeral change = m_upwards[src] ? (-cost - m_potentials[src] + m_potentials[tgt]) : (cost + m_potentials[src] - m_potentials[tgt]); node last = m_thread[m_final[src]]; for (node u = src; u != last; u = m_thread[u]) { m_potentials[u] += change; @@ -147,7 +161,7 @@ namespace smt { template void network_flow::update_flows() { TRACE("network_flow", tout << "update_flows...\n";); - numeral val = m_states[m_entering_edge] == BASIS ? numeral::zero() : m_delta; + numeral val = fin_numeral(m_states[m_entering_edge]) * (*m_delta); m_flows[m_entering_edge] += val; node source = m_graph.get_source(m_entering_edge); for (unsigned u = source; u != m_join_node; u = m_pred[u]) { @@ -166,20 +180,18 @@ namespace smt { bool network_flow::choose_entering_edge() { TRACE("network_flow", tout << "choose_entering_edge...\n";); vector const & es = m_graph.get_all_edges(); - for (unsigned int i = 0; i < es.size(); ++i) { - edge const & e = es[i]; - edge_id e_id; - node source = e.get_source(); - node target = e.get_target(); - if (e.is_enabled() && m_graph.get_edge_id(source, target, e_id) && m_states[e_id] == NON_BASIS) { - numeral cost = e.get_weight() - m_potentials[source] + m_potentials[target]; + for (unsigned i = 0; i < es.size(); ++i) { + node src = m_graph.get_source(i); + node tgt = m_graph.get_target(i); + if (m_states[i] != BASIS) { + numeral change = fin_numeral(m_states[i]) * (m_graph.get_weight(i) + m_potentials[src] - m_potentials[tgt]); // Choose the first negative-cost edge to be the violating edge // TODO: add multiple pivoting strategies - if (cost.is_neg()) { - m_entering_edge = e_id; + if (change.is_neg()) { + m_entering_edge = i; TRACE("network_flow", { - tout << "Found entering edge " << e_id << " between node "; - tout << source << " and node " << target << "...\n"; + tout << "Found entering edge " << i << " between node "; + tout << src << " and node " << tgt << "...\n"; }); return true; } @@ -194,6 +206,11 @@ namespace smt { TRACE("network_flow", tout << "choose_leaving_edge...\n";); node source = m_graph.get_source(m_entering_edge); node target = m_graph.get_target(m_entering_edge); + if (m_states[m_entering_edge] == UPPER) { + node temp = source; + source = target; + target = temp; + } node u = source, v = target; while (u != v) { if (m_depth[u] > m_depth[v]) @@ -207,34 +224,32 @@ namespace smt { } // Found first common ancestor of source and target m_join_node = u; - TRACE("network_flow", tout << "Found join node " << m_join_node << std::endl;); - // FIXME: need to get truly infinite value - numeral infty = numeral(INT_MAX); - m_delta = infty; + TRACE("network_flow", tout << "Found join node " << m_join_node << std::endl;); + m_delta.set_invalid(); node src, tgt; // Send flows along the path from source to the ancestor for (unsigned u = source; u != m_join_node; u = m_pred[u]) { - edge_id e_id = get_edge_id(u, m_pred[u]); - numeral d = m_upwards[u] ? infty : m_flows[e_id]; - if (d < m_delta) { - m_delta = d; + edge_id e_id = get_edge_id(u, m_pred[u]); + if (m_upwards[u] && (!m_delta || m_flows[e_id] < *m_delta)) { + m_delta = m_flows[e_id]; src = u; tgt = m_pred[u]; + m_in_edge_dir = true; } } // Send flows along the path from target to the ancestor for (unsigned u = target; u != m_join_node; u = m_pred[u]) { edge_id e_id = get_edge_id(u, m_pred[u]); - numeral d = m_upwards[u] ? m_flows[e_id] : infty; - if (d <= m_delta) { - m_delta = d; + if (!m_upwards[u] && (!m_delta || m_flows[e_id] <= *m_delta)) { + m_delta = m_flows[e_id]; src = u; tgt = m_pred[u]; + m_in_edge_dir = false; } } - if (m_delta < infty) { + if (m_delta) { m_leaving_edge = get_edge_id(src, tgt); TRACE("network_flow", { tout << "Found leaving edge " << m_leaving_edge; @@ -249,9 +264,21 @@ namespace smt { template void network_flow::update_spanning_tree() { node p = m_graph.get_source(m_entering_edge); - node q = m_graph.get_target(m_entering_edge); + node q = m_graph.get_target(m_entering_edge); node u = m_graph.get_source(m_leaving_edge); node v = m_graph.get_target(m_leaving_edge); + // v is parent of u so T_u does not contain root node + if (m_pred[u] == v) { + node temp = u; + u = v; + v = temp; + } + if ((m_states[m_entering_edge] == UPPER) == m_in_edge_dir) { + // q should be in T_v so swap p and q + node temp = p; + p = q; + q = temp; + } TRACE("network_flow", { tout << "update_spanning_tree: (" << p << ", " << q << ") enters, ("; @@ -265,14 +292,14 @@ namespace smt { // Update m_pred (for nodes in the stem from q to v) node n = q; node last = m_pred[v]; - node parent = p; - while (n != last) { + node prev = p; + while (n != last && n != -1) { node next = m_pred[n]; - m_pred[n] = parent; - m_upwards[n] = !m_upwards[n]; - parent = n; + m_pred[n] = prev; + m_upwards[n] = !m_upwards[prev]; + prev = n; n = next; - } + } TRACE("network_flow", tout << "Graft T_q and T_r'\n";); @@ -289,7 +316,7 @@ namespace smt { node gamma = m_thread[m_final[p]]; n = p; last = m_pred[gamma]; - while (n != last) { + while (n != last && n != -1) { m_final[n] = z; n = m_pred[n]; } @@ -299,33 +326,33 @@ namespace smt { // Update T_r' node phi = m_rev_thread[v]; node theta = m_thread[m_final[v]]; - m_thread[phi] = theta; - + gamma = m_thread[m_final[v]]; - // REVIEW: check f(n) is not in T_v + // Check that f(u) is not in T_v node delta = m_final[u] != m_final[v] ? m_final[u] : phi; n = u; last = m_pred[gamma]; - while (n != last) { + while (n != last && n != -1) { m_final[n] = delta; n = m_pred[n]; } + m_thread[phi] = theta; + // Reroot T_v at q - if (u != q) { + if (v != q) { TRACE("network_flow", tout << "Reroot T_v at q\n";); - node n = m_pred[q]; - m_thread[m_final[q]] = n; - last = v; + node n = v; + last = q; node alpha1, alpha2; - unsigned count = 0; - while (n != last) { + node prev = q; + while (n != last && n != -1) { // Find all immediate successors of n node t1 = m_thread[n]; node t2 = m_thread[m_final[t1]]; node t3 = m_thread[m_final[t2]]; - if (t1 = m_pred[n]) { + if (t1 == m_pred[n]) { alpha1 = t2; alpha2 = t3; } @@ -338,19 +365,23 @@ namespace smt { alpha2 = t2; } m_thread[n] = alpha1; - m_thread[m_final[alpha1]] = alpha2; - n = m_pred[n]; - m_thread[m_final[alpha2]] = n; - // Decrease depth of all children in the subtree - ++count; - int d = m_depth[n] - count; - for (node m = m_thread[n]; m != m_final[n]; m = m_thread[m]) { - m_depth[m] -= d; - } + m_thread[m_final[alpha1]] = alpha2; + m_thread[m_final[alpha2]] = prev; + prev = n; + n = m_pred[n]; } - m_thread[m_final[alpha2]] = v; + m_thread[m_final[q]] = prev; } + for (node n = m_thread[v]; m_pred[n] != -1; n = m_pred[n]) { + m_depth[n] = m_depth[m_pred[n]] + 1; + } + + for (unsigned i = 0; i < m_thread.size(); ++i) { + m_rev_thread[m_thread[i]] = i; + } + SASSERT(check_well_formed()); + TRACE("network_flow", { tout << pp_vector("Predecessors", m_pred, true) << pp_vector("Threads", m_thread); tout << pp_vector("Reverse Threads", m_rev_thread) << pp_vector("Last Successors", m_final); @@ -376,14 +407,12 @@ namespace smt { vector const & es = m_graph.get_all_edges(); for (unsigned i = 0; i < es.size(); ++i) { edge const & e = es[i]; - if (e.is_enabled()) { - oss << prefix << e.get_source() << " -> " << prefix << e.get_target(); - if (m_states[i] == BASIS) { - oss << "[color=red,penwidth=3.0,label=\"" << m_flows[i] << "/" << e.get_weight() << "\"];\n"; - } - else { - oss << "[label=\"" << m_flows[i] << "/" << e.get_weight() << "\"];\n"; - } + oss << prefix << e.get_source() << " -> " << prefix << e.get_target(); + if (m_states[i] == BASIS) { + oss << "[color=red,penwidth=3.0,label=\"" << m_flows[i] << "/" << e.get_weight() << "\"];\n"; + } + else { + oss << "[label=\"" << m_flows[i] << "/" << e.get_weight() << "\"];\n"; } } oss << std::endl; @@ -396,15 +425,19 @@ namespace smt { bool network_flow::min_cost() { initialize(); while (choose_entering_edge()) { + SASSERT(check_well_formed()); bool bounded = choose_leaving_edge(); if (!bounded) return false; update_flows(); if (m_entering_edge != m_leaving_edge) { m_states[m_entering_edge] = BASIS; - m_states[m_leaving_edge] = NON_BASIS; + m_states[m_leaving_edge] = (m_flows[m_leaving_edge].is_zero()) ? LOWER : UPPER; update_spanning_tree(); update_potentials(); TRACE("network_flow", tout << "Spanning tree:\n" << display_spanning_tree();); + } + else { + m_states[m_leaving_edge] = m_states[m_leaving_edge] == LOWER ? UPPER : LOWER; } } TRACE("network_flow", tout << "Found optimal solution.\n";); @@ -418,7 +451,7 @@ namespace smt { vector const & es = m_graph.get_all_edges(); for (unsigned i = 0; i < es.size(); ++i) { edge const & e = es[i]; - if (e.is_enabled() && m_states[i] == BASIS) { + if (m_states[i] == BASIS) { m_objective_value += e.get_weight().get_rational() * m_flows[i]; } } @@ -431,6 +464,70 @@ namespace smt { } return m_objective_value; } + + static unsigned find(svector& roots, unsigned x) { + unsigned old_x = x; + while (roots[x] >= 0) { + x = roots[x]; + } + roots[old_x] = x; + return x; + } + + static void merge(svector& roots, unsigned x, unsigned y) { + x = find(roots, x); + y = find(roots, y); + SASSERT(roots[x] < 0 && roots[y] < 0); + if (x == y) { + return; + } + if (roots[x] > roots[y]) { + std::swap(x, y); + } + SASSERT(roots[x] <= roots[y]); + roots[y] = x; + roots[x] += roots[y]; + } + + template + bool network_flow::check_well_formed() { + // m_thread is depth-first stack + // m_pred is predecessor link + // m_depth depth counting from a root note. + // m_graph + + node root = m_pred.size()-1; + for (unsigned i = 0; i < m_upwards.size(); ++i) { + if (m_upwards[i]) { + node p = m_pred[i]; + edge_id e = get_edge_id(i, p); + // we are either the root or the predecessor points up. + SASSERT(p == root || m_upwards[p]); + } + } + + // m_thread forms a spanning tree over [0..root] + // union-find structure: + svector roots(root+1, -1); + +#if 0 + for (unsigned i = 0; i < m_thread.size(); ++i) { + if (m_states[i] == BASIS) { + node x = m_thread[i]; + node y = i; + // we are now going to check the edge between x and y: + SASSERT(find(roots, x) != find(roots, y)); + merge(roots, x, y); + } + else { + // ? LOWER, UPPER + } + } +#endif + + return true; + } + } #endif diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h index 75a0f9ff3..56c361a93 100644 --- a/src/smt/theory_arith.h +++ b/src/smt/theory_arith.h @@ -273,14 +273,14 @@ namespace smt { class atom : public bound { protected: bool_var m_bvar; - numeral m_k; + inf_numeral m_k; unsigned m_atom_kind:2; // atom kind unsigned m_is_true:1; // cache: true if the atom was assigned to true. public: - atom(bool_var bv, theory_var v, numeral const & k, atom_kind kind); + atom(bool_var bv, theory_var v, inf_numeral const & k, atom_kind kind); atom_kind get_atom_kind() const { return static_cast(m_atom_kind); } virtual ~atom() {} - numeral const & get_k() const { return m_k; } + inf_numeral const & get_k() const { return m_k; } bool_var get_bool_var() const { return m_bvar; } bool is_true() const { return m_is_true; } void assign_eh(bool is_true, inf_numeral const & epsilon); @@ -999,7 +999,7 @@ namespace smt { virtual theory_var add_objective(app* term); virtual inf_eps_rational get_objective_value(theory_var v); virtual expr* block_lower_bound(theory_var v, inf_rational const& val); - + virtual expr* block_upper_bound(theory_var v, inf_numeral const& val); // ----------------------------------- // // Pretty Printing diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h index a1fff392f..a84a9ebf9 100644 --- a/src/smt/theory_arith_aux.h +++ b/src/smt/theory_arith_aux.h @@ -367,7 +367,7 @@ namespace smt { // ----------------------------------- template - theory_arith::atom::atom(bool_var bv, theory_var v, numeral const & k, atom_kind kind): + theory_arith::atom::atom(bool_var bv, theory_var v, inf_numeral const & k, atom_kind kind): bound(v, inf_numeral::zero(), B_LOWER, true), m_bvar(bv), m_k(k), @@ -997,6 +997,22 @@ namespace smt { } } + template + expr* theory_arith::block_upper_bound(theory_var v, inf_numeral const& val) { + ast_manager& m = get_manager(); + context& ctx = get_context(); + std::ostringstream strm; + strm << val << " <= " << v; + expr* b = m.mk_fresh_const(strm.str().c_str(), m.mk_bool_sort()); + bool_var bv = ctx.mk_bool_var(b); + atom* a = alloc(atom, bv, v, val, A_LOWER); + m_unassigned_atoms[v]++; + m_var_occs[v].push_back(a); + m_atoms.push_back(a); + insert_bv2a(bv, a); + return b; + } + template inf_eps_rational theory_arith::get_objective_value(theory_var v) { return m_objective_value; @@ -1117,15 +1133,6 @@ namespace smt { ); pivot(x_i, x_j, a_ij, false); - TRACE("maximize", tout << "max: " << max << ", x_i: v" << x_i << ", x_j: v" << x_j << ", a_ij: " << a_ij << ", coeff: " << coeff << "\n"; - if (upper(x_i)) tout << "upper x_i: " << upper_bound(x_i) << " "; - if (lower(x_i)) tout << "lower x_i: " << lower_bound(x_i) << " "; - tout << "value x_i: " << get_value(x_i) << "\n"; - if (upper(x_j)) tout << "upper x_j: " << upper_bound(x_j) << " "; - if (lower(x_j)) tout << "lower x_j: " << lower_bound(x_j) << " "; - tout << "value x_j: " << get_value(x_j) << "\n"; - - ); SASSERT(is_non_base(x_i)); SASSERT(is_base(x_j)); @@ -1137,15 +1144,6 @@ namespace smt { move_xi_to_lower = a_ij.is_neg(); move_to_bound(x_i, move_xi_to_lower); - TRACE("maximize", tout << "max: " << max << ", x_i: v" << x_i << ", x_j: v" << x_j << ", a_ij: " << a_ij << ", coeff: " << coeff << "\n"; - if (upper(x_i)) tout << "upper x_i: " << upper_bound(x_i) << " "; - if (lower(x_i)) tout << "lower x_i: " << lower_bound(x_i) << " "; - tout << "value x_i: " << get_value(x_i) << "\n"; - if (upper(x_j)) tout << "upper x_j: " << upper_bound(x_j) << " "; - if (lower(x_j)) tout << "lower x_j: " << lower_bound(x_j) << " "; - tout << "value x_j: " << get_value(x_j) << "\n"; - ); - row & r2 = m_rows[get_var_row(x_j)]; coeff.neg(); add_tmp_row(r, coeff, r2); diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index 195d78e25..11484c779 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -801,7 +801,7 @@ namespace smt { void theory_arith::mk_bound_axioms(atom * a1) { theory_var v = a1->get_var(); literal l1(a1->get_bool_var()); - numeral const & k1(a1->get_k()); + inf_numeral const & k1(a1->get_k()); atom_kind kind1 = a1->get_atom_kind(); TRACE("mk_bound_axioms", tout << "making bound axioms for v" << v << " " << kind1 << " " << k1 << "\n";); atoms & occs = m_var_occs[v]; @@ -810,7 +810,7 @@ namespace smt { for (; it != end; ++it) { atom * a2 = *it; literal l2(a2->get_bool_var()); - numeral const & k2 = a2->get_k(); + inf_numeral const & k2 = a2->get_k(); atom_kind kind2 = a2->get_atom_kind(); SASSERT(k1 != k2 || kind1 != kind2); SASSERT(a2->get_var() == v); @@ -880,7 +880,7 @@ namespace smt { ctx.set_var_theory(bv, get_id()); rational _k; m_util.is_numeral(rhs, _k); - numeral k(_k); + inf_numeral k(_k); atom * a = alloc(atom, bv, v, k, kind); mk_bound_axioms(a); m_unassigned_atoms[v]++; @@ -2475,7 +2475,7 @@ namespace smt { bool_var bv = a->get_bool_var(); literal l(bv); if (get_context().get_assignment(bv) == l_undef) { - numeral const & k2 = a->get_k(); + inf_numeral const & k2 = a->get_k(); delta.reset(); if (a->get_atom_kind() == A_LOWER) { // v >= k k >= k2 |- v >= k2 diff --git a/src/smt/theory_arith_pp.h b/src/smt/theory_arith_pp.h index 274cd5499..4eeb6a189 100644 --- a/src/smt/theory_arith_pp.h +++ b/src/smt/theory_arith_pp.h @@ -428,7 +428,7 @@ namespace smt { template void theory_arith::display_atom(std::ostream & out, atom * a, bool show_sign) const { theory_var v = a->get_var(); - numeral const & k = a->get_k(); + inf_numeral const & k = a->get_k(); enode * e = get_enode(v); if (show_sign) { if (!a->is_true()) diff --git a/src/smt/theory_opt.h b/src/smt/theory_opt.h index f1c6c242d..d57875712 100644 --- a/src/smt/theory_opt.h +++ b/src/smt/theory_opt.h @@ -27,14 +27,16 @@ Notes: namespace smt { class theory_opt { public: + typedef inf_eps_rational inf_eps; virtual bool maximize(theory_var v) { UNREACHABLE(); return false; }; virtual theory_var add_objective(app* term) { UNREACHABLE(); return null_theory_var; } - virtual inf_eps_rational get_objective_value(theory_var v) { + virtual inf_eps get_objective_value(theory_var v) { UNREACHABLE(); - inf_eps_rational r(rational(1), inf_rational(0)); - return r; + return inf_eps(rational(1), inf_rational(0)); } virtual expr* block_lower_bound(theory_var v, inf_rational const& val) { return 0; } + + }; }