Merge branch 'opt' of https://git01.codeplex.com/z3 into opt

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);
         }
     }
 

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();
     };
 }

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_vars.push_back(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)));
         }
           
+        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();
+        smt::theory_opt& opt = s->get_optimizer();
-        return l_undef;
+        
+        if (typeid(smt::theory_inf_arith) != typeid(opt)) {
+            return l_true;
+        }
+        smt::theory_inf_arith& th = dynamic_cast<smt::theory_inf_arith&>(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<inf_eps>& values) {
         s = &solver;
-        lbool result = basic_opt(objectives);
+        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 result;
+        }
+        return is_sat;
     }
 
 }

src/opt/optimize_objectives.h

@@ -33,6 +33,7 @@ namespace opt {
         volatile bool m_cancel;
         vector<inf_eps> m_lower;
         vector<inf_eps> m_upper;
+        svector<smt::theory_var> m_vars;
     public:
         optimize_objectives(ast_manager& m): m(m), s(0), m_cancel(false) {}
 

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;
             }
         }

src/smt/network_flow.h

@@ -42,8 +42,9 @@ namespace smt {
     template<typename Ext>
     class network_flow : private Ext {
         enum edge_state {
-            NON_BASIS = 0,
+            LOWER = 1,
-            BASIS = 1
+            BASIS = 0,
+            UPPER = -1
         };
         typedef dl_var node;
         typedef dl_edge<Ext> edge;
@@ -66,14 +67,15 @@ namespace smt {
         
         svector<edge_state> 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<bool> m_upwards;
 
         // Store the parent of a node i in the spanning tree
         svector<node> m_pred;
         // Store the number of edge on the path from node i to the root
         svector<int> 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<node> m_thread;
         // Reverse orders of m_thread
         svector<node> 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<numeral> 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<fin_numeral> const & balances);        

src/smt/network_flow_def.h

@@ -45,8 +45,20 @@ namespace smt {
 
     template<typename Ext>
     network_flow<Ext>::network_flow(graph & g, vector<fin_numeral> 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<edge> 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<typename Ext>
@@ -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<typename Ext>
     void network_flow<Ext>::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<Ext>::choose_entering_edge() {
         TRACE("network_flow", tout << "choose_entering_edge...\n";);
         vector<edge> const & es = m_graph.get_all_edges();
-        for (unsigned int i = 0; i < es.size(); ++i) {
+        for (unsigned i = 0; i < es.size(); ++i) {
-            edge const & e = es[i];
+            node src = m_graph.get_source(i);
-            edge_id e_id;
+            node tgt = m_graph.get_target(i);
-            node source = e.get_source();
+            if (m_states[i] != BASIS) {
-            node target = e.get_target();
+                numeral change = fin_numeral(m_states[i]) * (m_graph.get_weight(i) + m_potentials[src] - m_potentials[tgt]);
-            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];
                 // Choose the first negative-cost edge to be the violating edge
                 // TODO: add multiple pivoting strategies
-                if (cost.is_neg()) {
+                if (change.is_neg()) {
-                    m_entering_edge = e_id;
+                    m_entering_edge = i;
                     TRACE("network_flow", {
-                        tout << "Found entering edge " << e_id << " between node ";
+                        tout << "Found entering edge " << i << " between node ";
-                        tout << source << " and node " << target << "...\n";
+                        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])
@@ -208,33 +225,31 @@ 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
+        m_delta.set_invalid();
-        numeral infty = numeral(INT_MAX);
-        m_delta = infty; 
         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 (m_upwards[u] && (!m_delta || m_flows[e_id] < *m_delta)) {
-            if (d < m_delta) {
+                m_delta = m_flows[e_id];
-                m_delta = d;
                 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 (!m_upwards[u] && (!m_delta || m_flows[e_id] <= *m_delta)) {
-            if (d <= m_delta) {
+                m_delta = m_flows[e_id];
-                m_delta = d;
                 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;
@@ -252,6 +267,18 @@ namespace smt {
         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,12 +292,12 @@ 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;
+        node prev = p;
-        while (n != last) {
+        while (n != last && n != -1) {
             node next = m_pred[n];  
-            m_pred[n] = parent;
+            m_pred[n] = prev;          
-            m_upwards[n] = !m_upwards[n];
+            m_upwards[n] = !m_upwards[prev];
-            parent = n;
+            prev = n;
             n = next;
         }     
 
@@ -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];
+            node n = v;
-            m_thread[m_final[q]] = n;
+            last = q;            
-            last = v;            
             node alpha1, alpha2;
-            unsigned count = 0;
+            node prev = q;
-            while (n != last) {
+            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;
                 }
@@ -339,18 +366,22 @@ namespace smt {
                 }                
                 m_thread[n] = alpha1;
                 m_thread[m_final[alpha1]] = alpha2;                                
+                m_thread[m_final[alpha2]] = prev;
+                prev = n;
                 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[q]] = prev;
         }
-            m_thread[m_final[alpha2]] = v;
+
+        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,7 +407,6 @@ namespace smt {
         vector<edge> 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";
@@ -385,7 +415,6 @@ namespace smt {
                 oss << "[label=\"" << m_flows[i] << "/" << e.get_weight() << "\"];\n";
             }
         }
-        }
         oss << std::endl;
         return oss.str();
     }
@@ -396,16 +425,20 @@ namespace smt {
     bool network_flow<Ext>::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";);
         return true;
@@ -418,7 +451,7 @@ namespace smt {
         vector<edge> 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<int>& roots, unsigned x) {
+        unsigned old_x = x;
+        while (roots[x] >= 0) {
+            x = roots[x];
+        }
+        roots[old_x] = x;
+        return x;
+    }
+
+    static void merge(svector<int>& 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<typename Ext>
+    bool network_flow<Ext>::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<int> 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

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<atom_kind>(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<inf_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

src/smt/theory_arith_aux.h

@@ -367,7 +367,7 @@ namespace smt {
     // -----------------------------------
 
     template<typename Ext>
-    theory_arith<Ext>::atom::atom(bool_var bv, theory_var v, numeral const & k, atom_kind kind):
+    theory_arith<Ext>::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<typename Ext>
+    expr* theory_arith<Ext>::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<typename Ext>
     inf_eps_rational<inf_rational> theory_arith<Ext>::get_objective_value(theory_var v) {
         return m_objective_value; 
@@ -1117,15 +1133,6 @@ namespace smt {
                   );
             pivot<true>(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);

src/smt/theory_arith_core.h

@@ -801,7 +801,7 @@ namespace smt {
     void theory_arith<Ext>::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

src/smt/theory_arith_pp.h

@@ -428,7 +428,7 @@ namespace smt {
     template<typename Ext>
     void theory_arith<Ext>::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()) 

src/smt/theory_opt.h

@@ -27,14 +27,16 @@ Notes:
 namespace smt {
     class theory_opt {
     public:
+        typedef inf_eps_rational<inf_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<inf_rational> get_objective_value(theory_var v) { 
+        virtual inf_eps get_objective_value(theory_var v) { 
             UNREACHABLE(); 
-            inf_eps_rational<inf_rational> r(rational(1), inf_rational(0)); 
+            return inf_eps(rational(1), inf_rational(0));
-            return r; 
         }
         virtual expr* block_lower_bound(theory_var v, inf_rational const& val) { return 0; }
+
+
     };
 }