fix mb maximization logic, so far not accessible

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

src/math/simplex/model_based_opt.cpp

@@ -41,7 +41,6 @@ namespace opt {
 
         
     bool model_based_opt::invariant() {
-        // variables in each row are sorted.
         for (unsigned i = 0; i < m_rows.size(); ++i) {
             if (!invariant(i, m_rows[i])) {
                 return false;
@@ -50,19 +49,21 @@ namespace opt {
         return true;
     }
 
+#define PASSERT(_e_) if (!(_e_)) { TRACE("opt", display(tout, r);); SASSERT(_e_); }
+
     bool model_based_opt::invariant(unsigned index, row const& r) {
-        rational val = r.m_coeff;
         vector<var> const& vars = r.m_vars;
         for (unsigned i = 0; i < vars.size(); ++i) {
-            var const& v = vars[i];
+            // variables in each row are sorted and have non-zero coefficients
-            SASSERT(i + 1 == vars.size() || v.m_id < vars[i+1].m_id);
+            SASSERT(i + 1 == vars.size() || vars[i].m_id < vars[i+1].m_id);
-            SASSERT(!v.m_coeff.is_zero());
+            SASSERT(!vars[i].m_coeff.is_zero());
-            val += v.m_coeff * m_var2value[v.m_id];
         }
-        SASSERT(val == r.m_value);
+        
-        SASSERT(r.m_type != t_eq ||  val.is_zero());
+        PASSERT(r.m_value == get_row_value(r));
-        SASSERT(index == 0 || r.m_type != t_lt ||  val.is_neg());
+        PASSERT(r.m_type != t_eq ||  r.m_value.is_zero());
-        SASSERT(index == 0 || r.m_type != t_le || !val.is_pos());        
+        // values satisfy constraints
+        PASSERT(index == 0 || r.m_type != t_lt ||  r.m_value.is_neg());
+        PASSERT(index == 0 || r.m_type != t_le || !r.m_value.is_pos());        
         return true;
     }
         
@@ -90,20 +91,25 @@ namespace opt {
     // 
     inf_eps model_based_opt::maximize() {
         SASSERT(invariant());
-        unsigned_vector other;
         unsigned_vector bound_trail, bound_vars;
+        TRACE("opt", display(tout << "tableau\n"););
         while (!objective().m_vars.empty()) {
-            TRACE("opt", display(tout << "tableau\n"););
             var v = objective().m_vars.back();
             unsigned x = v.m_id;
             rational const& coeff = v.m_coeff;
             unsigned bound_row_index;
             rational bound_coeff;
-            other.reset();
+            if (find_bound(x, bound_row_index, bound_coeff, coeff.is_pos())) {
-            if (find_bound(x, bound_row_index, bound_coeff, other, coeff.is_pos())) {
                 SASSERT(!bound_coeff.is_zero());
-                for (unsigned i = 0; i < other.size(); ++i) {
+                TRACE("opt", display(tout << "update: " << v << " ", objective());
-                    resolve(bound_row_index, bound_coeff, other[i], x);
+                      for (unsigned i = 0; i < m_above.size(); ++i) {
+                          display(tout << "resolve: ", m_rows[m_above[i]]);
+                      });
+                for (unsigned i = 0; i < m_above.size(); ++i) {
+                    resolve(bound_row_index, bound_coeff, m_above[i], x);
+                }
+                for (unsigned i = 0; i < m_below.size(); ++i) {
+                    resolve(bound_row_index, bound_coeff, m_below[i], x);
                 }
                 // coeff*x + objective <= ub
                 // a2*x + t2 <= 0
@@ -116,6 +122,8 @@ namespace opt {
                 bound_vars.push_back(x);
             }
             else {
+                TRACE("opt", display(tout << "unbound: " << v << " ", objective()););
+                update_values(bound_vars, bound_trail);
                 return inf_eps::infinity();
             }
         }
@@ -136,15 +144,33 @@ namespace opt {
     }
 
 
+    void model_based_opt::update_value(unsigned x, rational const& val) {
+        rational old_val = m_var2value[x];
+        m_var2value[x] = val;
+        unsigned_vector const& row_ids = m_var2row_ids[x];
+        for (unsigned i = 0; i < row_ids.size(); ++i) {            
+            unsigned row_id = row_ids[i];
+            rational coeff = get_coefficient(row_id, x);
+            if (coeff.is_zero()) {
+                continue;
+            }
+            row & r = m_rows[row_id];
+            rational delta = coeff * (val - old_val);            
+            r.m_value += delta;
+            SASSERT(invariant(row_id, r));
+        }
+    }
+
+
     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& r = m_rows[bound_trail[i]];
             rational val = r.m_coeff;
-            rational x_val;
+            rational old_x_val = m_var2value[x];
-            rational x_coeff;
+            rational new_x_val;
+            rational x_coeff, eps(0);
             vector<var> const& vars = r.m_vars;
             for (unsigned j = 0; j < vars.size(); ++j) {
                 var const& v = vars[j];
@@ -155,28 +181,21 @@ namespace opt {
                     val += m_var2value[v.m_id]*v.m_coeff;
                 }
             }
-            TRACE("opt", display(tout << "v" << x << " val: " << val 
-                                 << " coeff_x: " << x_coeff << " val_x: " << m_var2value[x] << " ", r); );
             SASSERT(!x_coeff.is_zero());
-            x_val = -val/x_coeff;
+            new_x_val = -val/x_coeff;
-            //
-            //
-            //     ax + t < 0
-            // <=> x < -t/a
-            // <=> x := -t/a - epsilon
-            // 
-            if (r.m_type == t_lt) {
-                // Adjust epsilon to be 
-                if (!x_val.is_zero() && (eps.is_zero() || eps >= abs(x_val))) {
-                    eps = abs(x_val)/rational(2);
-                }
-                if (!r.m_value.is_zero() && (eps.is_zero() || eps >= abs(r.m_value))) {
-                    eps = abs(r.m_value)/rational(2);
-                }
 
+            if (r.m_type == t_lt) {
+                eps = abs(old_x_val - new_x_val)/rational(2);
+                eps = std::min(rational::one(), eps);
                 SASSERT(!eps.is_zero());
+
+                //
+                //     ax + t < 0
+                // <=> x < -t/a
+                // <=> x := -t/a - epsilon
+                // 
                 if (x_coeff.is_pos()) {
-                    x_val -= eps;
+                    new_x_val -= eps;
                 }
                 //
                 //     -ax + t < 0 
@@ -185,27 +204,47 @@ namespace opt {
                 // <=> x > t/a
                 // <=> x := t/a + epsilon
                 //
-                else if (x_coeff.is_neg()) {
+                else {
-                    x_val += eps;
+                    new_x_val += eps;
                 }
             }
-            m_var2value[x] = x_val;
+            TRACE("opt", display(tout << "v" << x 
-            r.m_value = (x_val * x_coeff) + val;
+                                 << " coeff_x: " << x_coeff 
+                                 << " old_x_val: " << old_x_val
+                                 << " new_x_val: " << new_x_val
+                                 << " eps: " << eps << " ", r); );
+            m_var2value[x] = new_x_val;
             
-            TRACE("opt", display(tout << "v" << x << " val: " << val << " coeff_x: " 
+            r.m_value = get_row_value(r);
-                                 << x_coeff << " val_x: " << m_var2value[x] << " ", r); );
             SASSERT(invariant(bound_trail[i], r));
         }        
+        
+        // update and check bounds for all other affected rows.
+        for (unsigned i = bound_trail.size(); i > 0; ) {
+            --i;
+            unsigned x = bound_vars[i];
+            unsigned_vector const& row_ids = m_var2row_ids[x];
+            for (unsigned j = 0; j < row_ids.size(); ++j) {            
+                unsigned row_id = row_ids[j];
+                row & r = m_rows[row_id];
+                r.m_value = get_row_value(r);
+                SASSERT(invariant(row_id, r));
+            }            
+        }
+        SASSERT(invariant());
     }
 
-    bool model_based_opt::find_bound(unsigned x, unsigned& bound_row_index, rational& bound_coeff, unsigned_vector& other, bool is_pos) {
+    bool model_based_opt::find_bound(unsigned x, unsigned& bound_row_index, rational& bound_coeff, bool is_pos) {
         bound_row_index = UINT_MAX;
         rational lub_val;
         rational const& x_val = m_var2value[x];
         unsigned_vector const& row_ids = m_var2row_ids[x];
         uint_set visited;
+        m_above.reset();
+        m_below.reset();
         for (unsigned i = 0; i < row_ids.size(); ++i) {
             unsigned row_id = row_ids[i];
+            SASSERT(row_id != m_objective_id);
             if (visited.contains(row_id)) {
                 continue;
             }
@@ -226,24 +265,34 @@ namespace opt {
                     else if ((value == lub_val && r.m_type == opt::t_lt) ||
                              (is_pos && value < lub_val) || 
                              (!is_pos && value > lub_val)) {
-                        other.push_back(bound_row_index);
+                        m_above.push_back(bound_row_index);
                         lub_val = value;
                         bound_row_index = row_id;                          
                         bound_coeff = a;
                     }
                     else {
-                        other.push_back(row_id);
+                        m_above.push_back(row_id);
                     }
                 }
                 else {
-                    r.m_alive = false;
+                    m_below.push_back(row_id);
                 }
             }
         }
         return bound_row_index != UINT_MAX;
     }
        
-    rational model_based_opt::get_coefficient(unsigned row_id, unsigned var_id) {
+    rational model_based_opt::get_row_value(row const& r) const {
+        vector<var> const& vars = r.m_vars;
+        rational val = r.m_coeff;
+        for (unsigned i = 0; i < vars.size(); ++i) {
+            var const& v = vars[i];
+            val += v.m_coeff * m_var2value[v.m_id];
+        }
+        return val;
+    }    
+ 
+    rational model_based_opt::get_coefficient(unsigned row_id, unsigned var_id) const {
         row const& r = m_rows[row_id];
         if (r.m_vars.empty()) {
             return rational::zero();

src/math/simplex/model_based_opt.h

@@ -65,15 +65,18 @@ namespace opt {
         vector<rational>        m_var2value;
         vector<var>             m_new_vars;
         unsigned_vector         m_lub, m_glb;
+        unsigned_vector         m_above, m_below;
         
         bool invariant();
         bool invariant(unsigned index, row const& r);
 
         row& objective() { return m_rows[0]; }        
 
-        bool find_bound(unsigned x, unsigned& bound_index, rational& bound_coeff, unsigned_vector& other, bool is_pos);
+        bool find_bound(unsigned x, unsigned& bound_index, rational& bound_coeff, bool is_pos);
         
-        rational get_coefficient(unsigned row_id, unsigned var_id);
+        rational get_coefficient(unsigned row_id, unsigned var_id) const;
+
+        rational get_row_value(row const& r) const;
 
         void resolve(unsigned row_src, rational const& a1, unsigned row_dst, unsigned x);
 
@@ -83,6 +86,8 @@ namespace opt {
 
         void update_values(unsigned_vector const& bound_vars, unsigned_vector const& bound_trail);
 
+        void update_value(unsigned x, rational const& val);
+
         void project(unsigned var);
 
         void solve_for(unsigned row_id, unsigned x);
@@ -132,5 +137,6 @@ namespace opt {
 
 std::ostream& operator<<(std::ostream& out, opt::ineq_type ie);
 
+inline std::ostream& operator<<(std::ostream& out, opt::model_based_opt::var const v) { return out << "v" << v.m_id; }
 
 #endif 

src/opt/opt_context.cpp

@@ -225,7 +225,7 @@ namespace opt {
         normalize();
         internalize();
         update_solver();
-#if 1
+#if 0
         if (is_qsat_opt()) {
             return run_qsat_opt();
         }
@@ -367,6 +367,7 @@ namespace opt {
 
     lbool context::execute_box() {
         if (m_box_index < m_objectives.size()) {
+            SASSERT(m_box_index < m_box_models.size());            
             m_model = m_box_models[m_box_index];
             ++m_box_index;           
             return l_true;
@@ -383,7 +384,9 @@ namespace opt {
             if (obj.m_type == O_MAXSMT) {
                 solver::scoped_push _sp(get_solver());
                 r = execute(obj, false, false);
-                if (r == l_true) m_box_models.push_back(m_model.get());
+                if (r == l_true) {
+                    m_box_models.push_back(m_model.get());
+                }
             }
             else {
                 m_box_models.push_back(m_optsmt.get_model(j));
@@ -391,6 +394,7 @@ namespace opt {
             }
         }
         if (r == l_true && m_objectives.size() > 0) {
+            SASSERT(!m_box_models.empty());
             m_model = m_box_models[0];
         }
         return r;

src/opt/opt_params.pyg

@@ -1,8 +1,7 @@
 def_module_params('opt', 
                   description='optimization parameters',
                   export=True,
-                  params=(('timeout', UINT, UINT_MAX, 'set timeout'),
+                  params=(('optsmt_engine', SYMBOL, 'basic', "select optimization engine: 'basic', 'farkas', 'symba'"),
-                          ('optsmt_engine', SYMBOL, 'basic', "select optimization engine: 'basic', 'farkas', 'symba'"),
 	                  ('maxsat_engine', SYMBOL, 'maxres', "select engine for maxsat: 'fu_malik', 'core_maxsat', 'wmax', 'pbmax', 'maxres', 'pd-maxres', 'bcd2', 'wpm2', 'sls', 'maxhs'"),
                           ('priority', SYMBOL, 'lex', "select how to priortize objectives: 'lex' (lexicographic), 'pareto', or 'box'"),
                           ('dump_benchmarks', BOOL, False, 'dump benchmarks for profiling'),

src/qe/qe_arith.cpp

@@ -105,7 +105,10 @@ namespace qe {
             expr_ref t(m);
             opt::ineq_type ty = opt::t_le;
             expr* e1, *e2;
-            DEBUG_CODE(expr_ref val(m); VERIFY(model.eval(lit, val) && m.is_true(val)););
+            DEBUG_CODE(expr_ref val(m); 
+                       VERIFY(model.eval(lit, val)); 
+                       CTRACE("qe", !m.is_true(val), tout << mk_pp(lit, m) << " := " << val << "\n";);
+                       SASSERT(m.is_true(val)););
 
             bool is_not = m.is_not(lit, lit);
             if (is_not) {
@@ -942,7 +945,7 @@ namespace qe {
             SASSERT(m_u < m_delta && rational(0) <= m_u);
             for (unsigned i = 0; i < n; ++i) {
                 add_lit(model, lits, mk_divides(div_divisor(i), 
-                                         mk_add(mk_num(div_coeff(i) * m_u), div_term(i))));
+                                                mk_add(mk_num(div_coeff(i) * m_u), div_term(i))));
             }
             reset_divs();
             //
@@ -1070,7 +1073,7 @@ namespace qe {
             
             for (unsigned i = 0; i < rows.size(); ++i) {
                 expr_ref_vector ts(m);
-                expr_ref t(m), s(m);
+                expr_ref t(m), s(m), val(m);
                 row const& r = rows[i];
                 if (r.m_vars.size() == 0) {
                     continue;
@@ -1088,6 +1091,8 @@ namespace qe {
                     case opt::t_eq: t = a.mk_eq(t, s); break;
                     }
                     fmls.push_back(t);
+                    VERIFY(model.eval(t, val));
+                    CTRACE("qe", !m.is_true(val), tout << "Evaluated unit " << t << " to " << val << "\n";);
                     continue;
                 }
                 for (j = 0; j < r.m_vars.size(); ++j) {
@@ -1111,10 +1116,16 @@ namespace qe {
                 case opt::t_eq: t = a.mk_eq(t, s); break;
                 }
                 fmls.push_back(t);
+                
+                
+                VERIFY(model.eval(t, val));
+                CTRACE("qe", !m.is_true(val), tout << "Evaluated " << t << " to " << val << "\n";);
+
             }
         }        
 
-        opt::inf_eps maximize(expr_ref_vector const& fmls0, model& mdl, app* t, expr_ref& bound) {
+        opt::inf_eps maximize(expr_ref_vector const& fmls0, model& mdl, app* t, expr_ref& ge, expr_ref& gt) {
+            validate_model(mdl, fmls0);
             m_trail.reset();
             SASSERT(a.is_real(t));
             expr_ref_vector fmls(fmls0);
@@ -1139,11 +1150,6 @@ namespace qe {
             // find optimal value
             value = mbo.maximize();
 
-            expr_ref val(a.mk_numeral(value.get_rational(), false), m);
-            if (!value.is_finite()) {
-                bound = m.mk_false();
-                return value;
-            }
 
             // update model to use new values that satisfy optimality
             ptr_vector<expr> vars;
@@ -1160,17 +1166,42 @@ namespace qe {
                     TRACE("qe", tout << "omitting model update for non-uninterpreted constant " << mk_pp(e, m) << "\n";);
                 }
             }
+            expr_ref val(a.mk_numeral(value.get_rational(), false), m);
+            expr_ref tval(m);
+            VERIFY (mdl.eval(t, tval));
 
-            // update the predicate 'bound' which forces larger values.
+            // update the predicate 'bound' which forces larger values when 'strict' is true.
-            if (value.get_infinitesimal().is_neg()) {
+            // strict:  bound := valuue < t
-                bound = a.mk_le(val, t);
+            // !strict: bound := value <= t
+            if (!value.is_finite()) {
+                ge = a.mk_ge(t, tval);
+                gt = m.mk_false();
+            }
+            else if (value.get_infinitesimal().is_neg()) {
+                ge = a.mk_ge(t, tval);
+                gt = a.mk_ge(t, val);
             }
             else {
-                bound = a.mk_lt(val, t);
+                ge = a.mk_ge(t, val);
+                gt = a.mk_gt(t, val);
             }
+            validate_model(mdl, fmls0);
             return value;
         }
 
+        bool validate_model(model& mdl, expr_ref_vector const& fmls) {
+            bool valid = true;
+            for (unsigned i = 0; i < fmls.size(); ++i) {
+                expr_ref val(m);
+                VERIFY(mdl.eval(fmls[i], val));
+                if (!m.is_true(val)) {
+                    valid = false;
+                    TRACE("qe", tout << mk_pp(fmls[i], m) << " := " << val << "\n";);
+                }
+            }
+            return valid;
+        }
+
         void extract_coefficients(opt::model_based_opt& mbo, model& model, obj_map<expr, rational> const& ts, obj_map<expr, unsigned>& tids, vars& coeffs) {
             coeffs.reset();
             obj_map<expr, rational>::iterator it = ts.begin(), end = ts.end();
@@ -1219,8 +1250,8 @@ namespace qe {
         return m_imp->a.get_family_id();
     }
 
-    opt::inf_eps arith_project_plugin::maximize(expr_ref_vector const& fmls, model& mdl, app* t, expr_ref& bound) {
+    opt::inf_eps arith_project_plugin::maximize(expr_ref_vector const& fmls, model& mdl, app* t, expr_ref& ge, expr_ref& gt) {
-        return m_imp->maximize(fmls, mdl, t, bound);
+        return m_imp->maximize(fmls, mdl, t, ge, gt);
     }
 
     bool arith_project(model& model, app* var, expr_ref_vector& lits) {

src/qe/qe_arith.h

@@ -32,7 +32,7 @@ namespace qe {
         virtual void operator()(model& model, app_ref_vector& vars, expr_ref_vector& lits);
 
 
-        opt::inf_eps maximize(expr_ref_vector const& fmls, model& mdl, app* t, expr_ref& bound);
+        opt::inf_eps maximize(expr_ref_vector const& fmls, model& mdl, app* t, expr_ref& ge, expr_ref& gt);
     };
 
     bool arith_project(model& model, app* var, expr_ref_vector& lits);

src/qe/qe_mbp.cpp

@@ -285,9 +285,9 @@ class mbp::impl {
 public:
 
 
-    opt::inf_eps maximize(expr_ref_vector const& fmls, model& mdl, app* t, expr_ref& bound) {
+    opt::inf_eps maximize(expr_ref_vector const& fmls, model& mdl, app* t, expr_ref& ge, expr_ref& gt) {
         arith_project_plugin arith(m);
-        return arith.maximize(fmls, mdl, t, bound);
+        return arith.maximize(fmls, mdl, t, ge, gt);
     }
 
     void extract_literals(model& model, expr_ref_vector& fmls) {
@@ -428,7 +428,16 @@ public:
         }        
     }
 
+    bool validate_model(model& model, expr_ref_vector const& fmls) {
+        expr_ref val(m);
+        for (unsigned i = 0; i < fmls.size(); ++i) { 
+            VERIFY(model.eval(fmls[i], val) && m.is_true(val)); 
+        }
+        return true;
+    }
+
     void operator()(bool force_elim, app_ref_vector& vars, model& model, expr_ref_vector& fmls) {
+        SASSERT(validate_model(model, fmls));
         expr_ref val(m), tmp(m);
         app_ref var(m);
         expr_ref_vector unused_fmls(m);
@@ -446,6 +455,7 @@ public:
                 }
             }
             while (!vars.empty() && !fmls.empty()) {
+                std::cout << "mbp: " << var << "\n";
                 var = vars.back();
                 vars.pop_back();
                 project_plugin* p = get_plugin(var);
@@ -483,6 +493,7 @@ public:
             vars.reset();
         }
         fmls.append(unused_fmls);
+        SASSERT(validate_model(model, fmls));
         TRACE("qe", tout << vars << " " << fmls << "\n";);
     }
     
@@ -508,6 +519,6 @@ void mbp::extract_literals(model& model, expr_ref_vector& lits) {
     m_impl->extract_literals(model, lits);
 }
 
-opt::inf_eps mbp::maximize(expr_ref_vector const& fmls, model& mdl, app* t, expr_ref& bound) {
+opt::inf_eps mbp::maximize(expr_ref_vector const& fmls, model& mdl, app* t, expr_ref& ge, expr_ref& gt) {
-    return m_impl->maximize(fmls, mdl, t, bound);
+    return m_impl->maximize(fmls, mdl, t, ge, gt);
 }

src/qe/qe_mbp.h

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

src/qe/qsat.cpp

@@ -507,6 +507,26 @@ namespace qe {
         }
     }
 
+    bool pred_abs::validate_defs(model& model) const {
+        bool valid = true;
+        obj_map<expr, expr*>::iterator it = m_pred2lit.begin(), end = m_pred2lit.end();
+        for (; it != end; ++it) {
+            expr_ref val_a(m), val_b(m);
+            expr* a = it->m_key;
+            expr* b = it->m_value;
+            VERIFY(model.eval(a, val_a));
+            VERIFY(model.eval(b, val_b));
+            if (val_a != val_b) {
+                TRACE("qe", 
+                      tout << mk_pp(a, m) << " := " << val_a << "\n";
+                      tout << mk_pp(b, m) << " := " << val_b << "\n";
+                      tout << m_elevel.find(a) << "\n";);
+                valid = false;
+            }
+        }
+        return valid;
+    }
+
     class kernel {
         ast_manager& m;
         params_ref   m_params;
@@ -575,6 +595,9 @@ namespace qe {
         app*                       m_objective;
         opt::inf_eps*              m_value;
         bool                       m_was_sat;
+        model_ref                  m_model_save;
+        expr_ref                   m_gt;
+        opt::inf_eps               m_value_save;
 
         
         /**
@@ -588,15 +611,23 @@ namespace qe {
                 check_cancel();
                 expr_ref_vector asms(m_asms);
                 m_pred_abs.get_assumptions(m_model.get(), asms);
+                if (m_model.get()) {
+                    validate_assumptions(*m_model.get(), asms);
+                }
                 TRACE("qe", tout << asms << "\n";);
                 solver& s = get_kernel(m_level).s();
                 lbool res = s.check_sat(asms);
                 switch (res) {
                 case l_true:
                     s.get_model(m_model);
+                    SASSERT(validate_defs("check_sat"));
+                    SASSERT(validate_assumptions(*m_model.get(), asms));
                     SASSERT(validate_model(asms));
                     TRACE("qe", s.display(tout); display(tout << "\n", *m_model.get()); display(tout, asms); );
                     push();
+                    if (m_level == 1 && m_mode == qsat_maximize) {
+                        maximize_model();
+                    }
                     break;
                 case l_false:
                     switch (m_level) {
@@ -607,6 +638,7 @@ namespace qe {
                             return l_true; 
                         }
                         if (m_model.get()) {
+                            SASSERT(validate_assumptions(*m_model.get(), asms));
                             if (!project_qe(asms)) return l_undef;
                         }
                         else {
@@ -734,7 +766,28 @@ namespace qe {
             }
         }
         
+        bool validate_defs(char const* msg) {
+            if (m_model.get() && !m_pred_abs.validate_defs(*m_model.get())) {
+                TRACE("qe", 
+                      tout << msg << "\n";
+                      display(tout);
+                      if (m_level > 0) {
+                          get_kernel(m_level-1).s().display(tout);
+                      }
+                      expr_ref_vector asms(m);
+                      m_pred_abs.get_assumptions(m_model.get(), asms);
+                      tout << asms << "\n";
+                      m_pred_abs.pred2lit(asms);
+                      tout << asms << "\n";);
+                return false;
+            }
+            else {
+                return true;
+            }
+        }
+
         bool get_core(expr_ref_vector& core, unsigned level) {
+            SASSERT(validate_defs("get_core"));
             get_kernel(level).get_core(core);
             m_pred_abs.pred2lit(core);
             return true;
@@ -814,33 +867,33 @@ namespace qe {
             if (!get_core(core, m_level)) {
                 return false;
             }
-            SASSERT(validate_core(core));
+            SASSERT(validate_core(mdl, core));
             get_vars(m_level);
+            SASSERT(validate_assumptions(mdl, core));
             m_mbp(force_elim(), m_avars, mdl, core);
+            SASSERT(validate_defs("project_qe"));
             if (m_mode == qsat_maximize) {
-                maximize(core, mdl);
+                maximize_core(core, mdl);
-                pop(1);
             }
             else {
                 fml = negate_core(core);
                 add_assumption(fml);
                 m_answer.push_back(fml);
                 m_free_vars.append(m_avars);
-                pop(1);
             }
+            pop(1);
             return true;
         }
                 
         bool project(expr_ref_vector& core) {
             if (!get_core(core, m_level)) return false;
             TRACE("qe", display(tout); display(tout << "core\n", core););
-            SASSERT(validate_core(core));
             SASSERT(m_level >= 2);
             expr_ref fml(m); 
             expr_ref_vector defs(m), core_save(m);
             max_level level;
             model& mdl = *m_model.get();
-            
+            SASSERT(validate_core(mdl, core));
             get_vars(m_level-1);
             SASSERT(validate_project(mdl, core));
             m_mbp(force_elim(), m_avars, mdl, core);
@@ -875,6 +928,7 @@ namespace qe {
                 fml = m_pred_abs.mk_abstract(fml);
                 get_kernel(m_level).assert_expr(fml);
             }
+            SASSERT(!m_model.get());
             return true;
         }
         
@@ -1005,7 +1059,19 @@ namespace qe {
             }
         }
 
-        bool validate_core(expr_ref_vector const& core) {
+        bool validate_assumptions(model& mdl, expr_ref_vector const& core) {
+            for (unsigned i = 0; i < core.size(); ++i) {
+                expr_ref val(m);
+                VERIFY(mdl.eval(core[i], val));
+                if (!m.is_true(val)) {
+                    TRACE("qe", tout << "component of core is not true: " << mk_pp(core[i], m) << "\n";);
+                    return false;
+                }
+            }
+            return true;
+        }
+
+        bool validate_core(model& mdl, expr_ref_vector const& core) {
             return true;
 #if 0
             TRACE("qe", tout << "Validate core\n";);
@@ -1130,7 +1196,8 @@ namespace qe {
             m_free_vars(m),
             m_objective(0),
             m_value(0),
-            m_was_sat(false)
+            m_was_sat(false),
+            m_gt(m)
         {
             reset();
         }
@@ -1258,6 +1325,7 @@ namespace qe {
             m_objective = t;
             m_value = &value;
             m_was_sat = false;
+            m_model_save.reset();
             m_pred_abs.abstract_atoms(fml, defs);
             fml = m_pred_abs.mk_abstract(fml);
             m_ex.assert_expr(mk_and(defs));
@@ -1271,6 +1339,7 @@ namespace qe {
                 if (!m_was_sat) {
                     return l_false;
                 }
+                mdl = m_model_save;
                 break;
             case l_true:
                 UNREACHABLE();
@@ -1286,15 +1355,49 @@ namespace qe {
             return l_true;
         }
 
-        void maximize(expr_ref_vector const& core, model& mdl) {
+        void maximize_core(expr_ref_vector const& core, model& mdl) {
             SASSERT(m_value);
             SASSERT(m_objective);
             TRACE("qe", tout << "maximize: " << core << "\n";);
             m_was_sat |= !core.empty();
             expr_ref bound(m);
-            *m_value = m_mbp.maximize(core, mdl, m_objective, bound);
+            *m_value = m_value_save;
-            IF_VERBOSE(0, verbose_stream() << "(maximize " << *m_value << " bound: " << bound << ")\n";);
+            IF_VERBOSE(3, verbose_stream() << "(maximize " << *m_value << ")\n";);
-            m_ex.assert_expr(bound);            
+            m_ex.assert_expr(m_gt);            
+            m_fa.assert_expr(m_gt);            
+        }
+
+        void maximize_model() {
+            SASSERT(m_level == 1 && m_mode == qsat_maximize);
+            SASSERT(m_objective);
+            expr_ref ge(m);
+            expr_ref_vector asms(m), defs(m);
+            m_pred_abs.get_assumptions(m_model.get(), asms);
+            m_pred_abs.pred2lit(asms);
+
+            SASSERT(validate_defs("maximize_model1"));
+
+            m_value_save = m_mbp.maximize(asms, *m_model.get(), m_objective, ge, m_gt);
+
+            SASSERT(validate_defs("maximize_model2"));
+            
+            // bound := val <= m_objective
+            
+            IF_VERBOSE(3, verbose_stream() << "(qsat-maximize-bound: " << m_value_save << ")\n";);
+
+            max_level level;
+            m_pred_abs.abstract_atoms(ge, level, defs);
+            m_ex.assert_expr(mk_and(defs));
+            m_fa.assert_expr(mk_and(defs));
+
+            ge = m_pred_abs.mk_abstract(ge);
+
+            SASSERT(is_uninterp_const(ge));
+            // update model with evaluation for bound.
+            if (is_uninterp_const(ge)) {
+                m_model->register_decl(to_app(ge)->get_decl(), m.mk_true());
+            }
+            SASSERT(validate_defs("maximize_model3"));
         }
 
     };

src/qe/qsat.h

@@ -112,6 +112,8 @@ namespace qe {
         void display(std::ostream& out) const;
         void display(std::ostream& out, expr_ref_vector const& asms) const;
         void collect_statistics(statistics& st) const;
+
+        bool validate_defs(model& model) const;
     };
 
     class qmax {

src/smt/smt_context.h

@@ -1406,10 +1406,8 @@ namespace smt {
 
         void internalize_instance(expr * body, proof * pr, unsigned generation) {
             internalize_assertion(body, pr, generation);
-#ifndef SMTCOMP
             if (relevancy())
                 m_case_split_queue->internalize_instance_eh(body, generation);
-#endif
         }
 
         bool already_internalized() const { return m_e_internalized_stack.size() > 2 || m_b_internalized_stack.size() > 1; }

src/smt/smt_model_checker.cpp

@@ -138,8 +138,10 @@ namespace smt {
     }
 
     bool model_checker::add_instance(quantifier * q, model * cex, expr_ref_vector & sks, bool use_inv) {
-        if (cex == 0)
+        if (cex == 0) {
-            return false; // no model available.
+            TRACE("model_checker", tout << "no model is available\n";);
+            return false; 
+        }
         unsigned num_decls = q->get_num_decls();
         // Remark: sks were created for the flat version of q.
         SASSERT(sks.size() >= num_decls);
@@ -153,8 +155,10 @@ namespace smt {
             sk_value  = cex->get_const_interp(sk_d);
             if (sk_value == 0) {
                 sk_value = cex->get_some_value(sk_d->get_range());
-                if (sk_value == 0)
+                if (sk_value == 0) {
+                    TRACE("model_checker", tout << "Could not get value for " << sk_d->get_name() << "\n";);
                     return false; // get_some_value failed... giving up
+                }
             }
             if (use_inv) {
                 unsigned sk_term_gen;
@@ -166,6 +170,7 @@ namespace smt {
                     sk_value = sk_term;
                 }
                 else {
+                    TRACE("model_checker", tout << "no inverse value for " << sk_value << "\n";);
                     return false;
                 }
             }
@@ -175,8 +180,10 @@ namespace smt {
                     sk_value = sk_term;
                 }
             }
-            if (contains_model_value(sk_value))
+            if (contains_model_value(sk_value)) {
+                TRACE("model_checker", tout << "value is private to model: " << sk_value << "\n";);
                 return false;
+            }
             bindings.set(num_decls - i - 1, sk_value);
         }
         
@@ -286,18 +293,15 @@ namespace smt {
                 break; 
             model_ref cex;
             m_aux_context->get_model(cex);
-            if (add_instance(q, cex.get(), sks, true)) {
+            if (!add_instance(q, cex.get(), sks, true)) {
-                num_new_instances++;
-                if (num_new_instances < m_max_cexs) {
-                    if (!add_blocking_clause(cex.get(), sks))
-                        break; // add_blocking_clause failed... stop the search for new counter-examples...
-                }
-            }
-            else {
                 break;
             }
-            if (num_new_instances >= m_max_cexs)
+            num_new_instances++;
+            if (num_new_instances >= m_max_cexs || !add_blocking_clause(cex.get(), sks)) {
+                TRACE("model_checker", tout << "Add blocking clause failed\n";);
+                // add_blocking_clause failed... stop the search for new counter-examples...
                 break; 
+            }
         }
 
         if (num_new_instances == 0) {
@@ -368,8 +372,10 @@ namespace smt {
         if (it == end)
             return true;
 
-        if (m_iteration_idx >= m_params.m_mbqi_max_iterations)
+        if (m_iteration_idx >= m_params.m_mbqi_max_iterations) {
+            IF_VERBOSE(10, verbose_stream() << "(smt.mbqi \"max instantiations reached \")" << m_iteration_idx << "\n";);
             return false;
+        }
 
         m_curr_model = md;
         m_value2expr.reset();