add model correction

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/math/simplex/model_based_opt.cpp

@@ -97,9 +97,10 @@ namespace opt {
     // e.g. t2/a2 >= t3/a3
     // then replace a3*x + t3 by t3/a3 - t2/a2 <= 0
     // 
-    bound_type model_based_opt::maximize(rational& value) {
+    inf_eps model_based_opt::maximize() {
         SASSERT(invariant());
         unsigned_vector other;
+        unsigned_vector bound_trail, bound_vars;
         while (!objective().m_vars.empty()) {
             TRACE("opt", tout << "tableau\n";);
             var v = objective().m_vars.back();
@@ -120,17 +121,79 @@ namespace opt {
 
                 mul_add(m_objective_id, - coeff/bound_coeff, bound_row_index);
                 m_rows[bound_row_index].m_alive = false;
+                bound_trail.push_back(bound_row_index);
+                bound_vars.push_back(x);
             }
             else {
-                return unbounded;
+                return inf_eps::infinity();
             }
         }
-        value = objective().m_value;
+        //
-        if (objective().m_type == t_lt) {
+        // update the evaluation of variables to satisfy the bound.
-            return strict;
+
+        update_values(bound_vars, bound_trail);
+
+        rational value = objective().m_value;
+        if (objective().m_type == t_lt) {            
+            return inf_eps(inf_rational(value, rational(-1)));
         }
         else {
-            return non_strict;
+            return inf_eps(inf_rational(value));
+        }
+    }
+
+
+    void model_based_opt::update_values(unsigned_vector const& bound_vars, unsigned_vector const& bound_trail) {
+        rational eps(0);
+        for (unsigned i = bound_trail.size(); i > 0; ) {
+            --i;
+            unsigned x = bound_vars[i];
+            row const& r = m_rows[bound_trail[i]];
+            rational val = r.m_coeff;
+            rational x_coeff;
+            vector<var> const& vars = r.m_vars;
+            for (unsigned j = 0; j < vars.size(); ++j) {
+                var const& v = vars[j];
+                if (x = v.m_id) {
+                    x_coeff = v.m_coeff;
+                }
+                else {
+                    val += m_var2value[v.m_id]*v.m_coeff;
+                }
+            }
+            SASSERT(!x_coeff.is_zero());
+            val /= -x_coeff;
+            // Adjust epsilon to be s
+            if (eps.is_zero() || (!val.is_zero() && eps > abs(val))) {
+                eps = abs(val)/rational(2);
+            }
+            if (eps.is_zero() || (!r.m_value.is_zero() && eps > abs(r.m_value))) {
+                eps = abs(r.m_value)/rational(2);
+            }
+            //
+            //
+            //     ax + t < 0
+            // <=> x < -t/a
+            // <=> x := -t/a - epsilon
+            // 
+            if (x_coeff.is_pos() && r.m_type == t_lt) {
+                val -= eps;
+            }
+            //
+            //     -ax + t < 0 
+            // <=> -ax < -t
+            // <=> -x < -t/a
+            // <=> x > t/a
+            // <=> x := t/a + epsilon
+            //
+
+            if (x_coeff.is_pos() && r.m_type == t_lt) {
+                val -= eps;
+            }
+            else if (x_coeff.is_neg() && r.m_type == t_lt) {
+                val += eps;
+            }
+            m_var2value[x] = val;
         }
     }
 
@@ -343,6 +406,10 @@ namespace opt {
         return v;
     }
 
+    rational model_based_opt::get_value(unsigned var) {
+        return m_var2value[var];
+    }
+
     void model_based_opt::set_row(unsigned row_id, vector<var> const& coeffs, rational const& c, ineq_type rel) {
         row& r = m_rows[row_id];
         rational val(c);

src/math/simplex/model_based_opt.h

@@ -23,6 +23,7 @@ Revision History:
 
 #include "util.h"
 #include "rational.h"
+#include"inf_eps_rational.h"
 
 namespace opt {
    
@@ -38,7 +39,7 @@ namespace opt {
         non_strict
     };
 
-
+    typedef inf_eps_rational<inf_rational> inf_eps;
     
     class model_based_opt {
     public:
@@ -71,8 +72,7 @@ namespace opt {
         bool invariant();
         bool invariant(unsigned index, row const& r);
 
-        row& objective() { return m_rows[0]; }
+        row& objective() { return m_rows[0]; }        
-        
 
         bool find_bound(unsigned x, unsigned& bound_index, rational& bound_coeff, unsigned_vector& other, bool is_pos);
         
@@ -83,6 +83,8 @@ namespace opt {
         void mul_add(unsigned row_id1, rational const& c, unsigned row_id2);
 
         void set_row(unsigned row_id, vector<var> const& coeffs, rational const& c, ineq_type rel);
+        
+        void update_values(unsigned_vector const& bound_vars, unsigned_vector const& bound_trail);
 
     public:
 
@@ -91,6 +93,9 @@ namespace opt {
         // add a fresh variable with value 'value'.
         unsigned add_var(rational const& value);
 
+        // retrieve updated value of variable.
+        rational get_value(unsigned var_id);
+
         // add a constraint. We assume that the constraint is 
         // satisfied under the values provided to the variables.
         void add_constraint(vector<var> const& coeffs, rational const& c, ineq_type r);
@@ -98,12 +103,13 @@ namespace opt {
         // Set the objective function (linear).
         void set_objective(vector<var> const& coeffs, rational const& c);
 
+        //
         // find a maximal value for the objective function over the current values.
         // in other words, the returned maximal value may not be globally optimal,
         // but the current evaluation of variables are used to select a local
         // optimal.
-        bound_type maximize(rational& value);
+        //
-
+        inf_eps maximize();
 
         void display(std::ostream& out) const;
         void display(std::ostream& out, row const& r) const;

src/opt/opt_context.cpp

@@ -1459,23 +1459,20 @@ namespace opt {
 
     lbool context::run_qsat_opt() {
         SASSERT(is_qsat_opt());
-        app_ref objective(m);
+        objective const& obj = m_objectives[0];
-        opt::bound_type bound;
+        app_ref term(obj.m_term);
-        expr_ref value(m);
+        if (obj.m_type == O_MINIMIZE) {
-        lbool result = qe::maximize(m_hard_constraints, objective, value, bound, m_params);
+            term = m_arith.mk_uminus(term);
-        if (result != l_undef) {
-            switch (bound) {
-            case opt::unbounded:
-            case opt::strict:
-            case opt::non_strict:
-                // set_max
-                break;
-                // TBD:
-                
-            default:
-                break;
-            }
         }
-        return l_undef;
+        inf_eps value;
+        lbool result = qe::maximize(m_hard_constraints, term, value, m_params);
+        if (result != l_undef && obj.m_type == O_MINIMIZE) {
+            value.neg();
+        }
+        if (result != l_undef) {
+            m_optsmt.update_lower(obj.m_index, value);
+            m_optsmt.update_upper(obj.m_index, value);
+        }
+        return result;
     }
 }

src/opt/optsmt.h

@@ -61,7 +61,9 @@ namespace opt {
         void    get_model(model_ref& mdl, svector<symbol>& labels);
         model*  get_model(unsigned index) const { return m_models[index]; }
 
+
         void update_lower(unsigned idx, inf_eps const& r);
+
         void update_upper(unsigned idx, inf_eps const& r);
 
         void reset();
@@ -82,6 +84,7 @@ namespace opt {
 
         lbool update_upper();
 
+
     };
 
 };

src/qe/qe_arith.cpp

@@ -965,37 +965,57 @@ namespace qe {
 
         typedef opt::model_based_opt::var var;
         typedef vector<var> vars;
+        
 
-        opt::bound_type maximize(expr_ref_vector const& fmls, model& mdl, app* t, expr_ref& value, expr_ref& bound) {
+        opt::inf_eps maximize(expr_ref_vector const& fmls, model& mdl, app* t, expr_ref& bound) {
             opt::model_based_opt mbo;
-
+            opt::inf_eps value;
             obj_map<expr, rational> ts;
             obj_map<expr, unsigned> tids;
             vars coeffs;
             rational c(0), mul(1);
-            linearize(mdl, mul, t, c, ts);              
+            linearize(mdl, mul, t, c, ts);
             extract_coefficients(ts, tids, coeffs);
             mbo.set_objective(coeffs, c);
 
             for (unsigned i = 0; i < fmls.size(); ++i) {
                 linearize(mdl, mbo, fmls[i], tids);
             }
+            
 
-            rational val;
+            value = mbo.maximize();
-            opt::bound_type result = mbo.maximize(val);
+
-            value = a.mk_numeral(val, false);
+
-            switch (result) {
+
-            case opt::unbounded:
+            expr_ref val(a.mk_numeral(value.get_rational(), false), m);
+            if (!value.is_finite()) {
                 bound = m.mk_false();
-                break;
+                return value;
-            case opt::strict:
+            }
-                bound = a.mk_le(value, t);
+
-                break;
+            // update model
-            case opt::non_strict:
+            ptr_vector<expr> vars;
-                bound = a.mk_lt(value, t);
+            obj_map<expr, unsigned>::iterator it = tids.begin(), end = tids.end();
-                break;
+            for (; it != end; ++it) {
+                expr* e = it->m_key;
+                if (is_uninterp_const(e)) {
+                    unsigned id = it->m_value;
+                    func_decl* f = to_app(e)->get_decl();
+                    expr_ref val(a.mk_numeral(mbo.get_value(id), false), m);
+                    mdl.register_decl(f, val);
+                }
+                else {
+                    TRACE("qe", tout << "omitting model update for non-uninterpreted constant " << mk_pp(e, m) << "\n";);
+                }
+            }
+
+            if (value.get_infinitesimal().is_neg()) {
+                bound = a.mk_le(val, t);
+            }
+            else {
+                bound = a.mk_lt(val, t);
             }            
-            return result;
+            return value;
         }
 
         void extract_coefficients(obj_map<expr, rational> const& ts, obj_map<expr, unsigned>& tids, vars& coeffs) {
@@ -1033,8 +1053,8 @@ namespace qe {
         return m_imp->a.get_family_id();
     }
 
-    opt::bound_type arith_project_plugin::maximize(expr_ref_vector const& fmls, model& mdl, app* t, expr_ref& value, expr_ref& bound) {
+    opt::inf_eps arith_project_plugin::maximize(expr_ref_vector const& fmls, model& mdl, app* t, expr_ref& bound) {
-        return m_imp->maximize(fmls, mdl, t, value, bound);
+        return m_imp->maximize(fmls, mdl, t, bound);
     }
 
     bool arith_project(model& model, app* var, expr_ref_vector& lits) {

src/qe/qe_arith.h

@@ -22,14 +22,15 @@ namespace qe {
 
     class arith_project_plugin : public project_plugin {
         struct imp;
-        imp* m_imp;
+        imp* m_imp;        
     public:
         arith_project_plugin(ast_manager& m);
         virtual ~arith_project_plugin();
         virtual bool operator()(model& model, app* var, app_ref_vector& vars, expr_ref_vector& lits);
         virtual bool solve(model& model, app_ref_vector& vars, expr_ref_vector& lits);
         virtual family_id get_family_id();
-        opt::bound_type maximize(expr_ref_vector const& fmls, model& mdl, app* t, expr_ref& value, expr_ref& bound);
+
+        opt::inf_eps maximize(expr_ref_vector const& fmls, model& mdl, app* t, expr_ref& bound);
     };
 
     bool arith_project(model& model, app* var, expr_ref_vector& lits);

src/qe/qe_mbp.cpp

@@ -213,9 +213,9 @@ class mbp::impl {
 public:
 
 
-    opt::bound_type maximize(expr_ref_vector const& fmls, model& mdl, app* t, expr_ref& value, expr_ref& bound) {
+    opt::inf_eps maximize(expr_ref_vector const& fmls, model& mdl, app* t, expr_ref& bound) {
         arith_project_plugin arith(m);
-        return arith.maximize(fmls, mdl, t, value, bound);
+        return arith.maximize(fmls, mdl, t, bound);
     }
 
     void extract_literals(model& model, expr_ref_vector& fmls) {
@@ -421,6 +421,6 @@ void mbp::extract_literals(model& model, expr_ref_vector& lits) {
     m_impl->extract_literals(model, lits);
 }
 
-opt::bound_type mbp::maximize(expr_ref_vector const& fmls, model& mdl, app* t, expr_ref& value, expr_ref& bound) {
+opt::inf_eps mbp::maximize(expr_ref_vector const& fmls, model& mdl, app* t, expr_ref& bound) {
-    return m_impl->maximize(fmls, mdl, t, value, bound);
+    return m_impl->maximize(fmls, mdl, t, bound);
 }

src/qe/qe_mbp.h

@@ -76,7 +76,7 @@ namespace qe {
            \brief 
            Maximize objective t under current model for constraints in fmls.
          */
-        opt::bound_type maximize(expr_ref_vector const& fmls, model& mdl, app* t, expr_ref& value, expr_ref& bound);
+        opt::inf_eps maximize(expr_ref_vector const& fmls, model& mdl, app* t, expr_ref& bound);
     };
 }
 

src/qe/qsat.cpp

@@ -1162,8 +1162,7 @@ namespace qe {
             m_level(0),
             m_mode(mode),
             m_avars(m),
-            m_free_vars(m),
+            m_free_vars(m)
-            m_value(m)
         {
             reset();
         }
@@ -1283,17 +1282,15 @@ namespace qe {
         }        
 
         app*             m_objective;
-        expr_ref         m_value;
+        opt::inf_eps     m_value;
-        opt::bound_type  m_bound;
         bool             m_was_sat;
 
-        lbool maximize(expr_ref_vector const& fmls, app* t, expr_ref& value, opt::bound_type& bound) {
+        lbool maximize(expr_ref_vector const& fmls, app* t, opt::inf_eps& value) {
             expr_ref_vector defs(m);
             expr_ref fml = negate_core(fmls);
             hoist(fml);
             m_objective = t;
-            m_value = 0;
+            m_value = opt::inf_eps();
-            m_bound = opt::unbounded;
             m_was_sat = false;
             m_pred_abs.abstract_atoms(fml, defs);
             fml = m_pred_abs.mk_abstract(fml);
@@ -1319,7 +1316,6 @@ namespace qe {
                 throw tactic_exception(s.c_str()); 
             }        
             value = m_value;
-            bound = m_bound;
             return l_true;
         }
 
@@ -1327,16 +1323,16 @@ namespace qe {
             TRACE("qe", tout << "maximize: " << core << "\n";);
             m_was_sat |= !core.empty();
             expr_ref bound(m);
-            m_bound = m_mbp.maximize(core, mdl, m_objective, m_value, bound);
+            m_value = m_mbp.maximize(core, mdl, m_objective, bound);
             m_ex.assert_expr(bound);            
         }
 
     };
 
-    lbool maximize(expr_ref_vector const& fmls, app* t, expr_ref& value, opt::bound_type& bound, params_ref const& p) {
+    lbool maximize(expr_ref_vector const& fmls, app* t, opt::inf_eps& value, params_ref const& p) {
         ast_manager& m = fmls.get_manager();
         qsat qs(m, p, qsat_maximize);
-        return qs.maximize(fmls, t, value, bound);
+        return qs.maximize(fmls, t, value);
     }    
 };
 

src/qe/qsat.h

@@ -114,7 +114,7 @@ namespace qe {
         void collect_statistics(statistics& st) const;
     };
 
-    lbool maximize(expr_ref_vector const& fmls, app* t, expr_ref& value, opt::bound_type& bound, params_ref const& p);
+    lbool maximize(expr_ref_vector const& fmls, app* t, opt::inf_eps& value, params_ref const& p);
 
 }
 

src/util/inf_eps_rational.h

@@ -23,6 +23,7 @@ Revision History:
 #include"debug.h"
 #include"vector.h"
 #include"rational.h"
+#include"inf_rational.h"
 
 template<typename Numeral>
 class inf_eps_rational {