Merge branch 'master' of https://github.com/Z3Prover/z3

src/math/simplex/model_based_opt.cpp

@@ -34,8 +34,7 @@ std::ostream& operator<<(std::ostream& out, opt::ineq_type ie) {
 namespace opt {
     
 
-    model_based_opt::model_based_opt():
+    model_based_opt::model_based_opt()
-        m_objective_id(0)
     {
         m_rows.push_back(row());
     }
@@ -448,5 +447,132 @@ namespace opt {
         set_row(m_objective_id, coeffs, c, t_le);
     }
 
+    void model_based_opt::get_live_rows(vector<row>& rows) {
+        for (unsigned i = 0; i < m_rows.size(); ++i) {
+            if (m_rows[i].m_alive) {
+                rows.push_back(m_rows[i]);
+            }
+        }
+    }
+
+    //
+    // pick glb and lub representative.
+    // The representative is picked such that it 
+    // represents the fewest inequalities. 
+    // The constraints that enforce a glb or lub are not forced.
+    // The constraints that separate the glb from ub or the lub from lb
+    // are not forced.
+    // In other words, suppose there are 
+    // . N inequalities of the form t <= x
+    // . M inequalities of the form s >= x
+    // . t0 is glb among N under valuation.
+    // . s0 is lub among M under valuation.
+    // If N < M
+    //    create the inequalities:
+    //       t <= t0 for each t other than t0 (N-1 inequalities).
+    //       t0 <= s for each s (M inequalities).
+    // If N >= M the construction is symmetric.
+    // 
+    void model_based_opt::project(unsigned x) {
+        unsigned_vector& lub_rows = m_lub;
+        unsigned_vector& glb_rows = m_glb;        
+        unsigned lub_index = UINT_MAX, glb_index = UINT_MAX;
+        bool     lub_strict = false, glb_strict = false;
+        rational lub_val, glb_val;
+        rational const& x_val = m_var2value[x];
+        unsigned_vector const& row_ids = m_var2row_ids[x];
+        uint_set visited;
+        lub_rows.reset();
+        glb_rows.reset();
+        // select the lub and glb.
+        for (unsigned i = 0; i < row_ids.size(); ++i) {
+            unsigned row_id = row_ids[i];
+            if (visited.contains(row_id)) {
+                continue;
+            }
+            visited.insert(row_id);
+            row& r = m_rows[row_id];
+            if (!r.m_alive) {
+                continue;
+            }
+            rational a = get_coefficient(row_id, x);
+            if (a.is_zero()) {
+                continue;
+            }
+            if (r.m_type == t_eq) {
+                solve_for(row_id, x);
+                return;
+            }
+            if (a.is_pos()) {
+                rational lub_value = x_val - (r.m_value/a);
+                if (lub_rows.empty() || 
+                    lub_value < lub_val ||
+                    (lub_value == lub_val && r.m_type == t_lt && !lub_strict)) {
+                    lub_val = lub_value;
+                    lub_index = row_id;
+                    lub_strict = r.m_type == t_lt;                    
+                }
+                lub_rows.push_back(row_id);
+            }
+            else {
+                SASSERT(a.is_neg());
+                rational glb_value = x_val - (r.m_value/a);
+                if (glb_rows.empty() || 
+                    glb_value > glb_val ||
+                    (glb_value == glb_val && r.m_type == t_lt && !glb_strict)) {
+                    glb_val = glb_value;
+                    glb_index = row_id;
+                    glb_strict = r.m_type == t_lt;                    
+                }
+                glb_rows.push_back(row_id);
+            }
+        }
+        unsigned row_index = (lub_rows.size() <= glb_rows.size())? lub_index : glb_index;
+        glb_rows.append(lub_rows);            
+        if (row_index == UINT_MAX) {
+            for (unsigned i = 0; i < glb_rows.size(); ++i) {
+                unsigned row_id = glb_rows[i];
+                SASSERT(m_rows[row_id].m_alive);
+                SASSERT(!get_coefficient(row_id, x).is_zero());
+                m_rows[row_id].m_alive = false;
+            }
+        }
+        else {
+            rational coeff = get_coefficient(row_index, x);
+            for (unsigned i = 0; i < glb_rows.size(); ++i) {
+                unsigned row_id = glb_rows[i];
+                if (row_id != row_index) {
+                    resolve(row_index, coeff, row_id, x);
+                }
+            }
+            m_rows[row_index].m_alive = false;
+        }
+    }
+
+    void model_based_opt::solve_for(unsigned row_id1, unsigned x) {
+        rational a = get_coefficient(row_id1, x);
+        row& r1 = m_rows[row_id1];
+        SASSERT(!a.is_zero());
+        SASSERT(r1.m_type == t_eq);
+        SASSERT(r1.m_alive);
+        unsigned_vector const& row_ids = m_var2row_ids[x];
+        uint_set visited;
+        visited.insert(row_id1);
+        for (unsigned i = 0; i < row_ids.size(); ++i) {
+            unsigned row_id2 = row_ids[i];
+            if (!visited.contains(row_id2)) {                
+                visited.insert(row_id2);
+                resolve(row_id1, a, row_id2, x);            
+            }
+        }
+        r1.m_alive = false;
+    }
+
+    void model_based_opt::project(unsigned num_vars, unsigned const* vars) {
+        for (unsigned i = 0; i < num_vars; ++i) {
+            project(vars[i]);
+        }
+    }
+
 }
 

src/math/simplex/model_based_opt.h

@@ -48,7 +48,6 @@ namespace opt {
                 }
             };
         };
-    private:
         struct row {
             row(): m_type(t_le), m_value(0), m_alive(false) {}
             vector<var> m_vars;         // variables with coefficients
@@ -58,11 +57,14 @@ namespace opt {
             bool        m_alive;        // rows can be marked dead if they have been processed.
         };
 
+    private:
+
         vector<row>             m_rows;
-        unsigned                m_objective_id;
+        static const unsigned   m_objective_id = 0;
         vector<unsigned_vector> m_var2row_ids;
         vector<rational>        m_var2value;
         vector<var>             m_new_vars;
+        unsigned_vector         m_lub, m_glb;
         
         bool invariant();
         bool invariant(unsigned index, row const& r);
@@ -81,6 +83,10 @@ namespace opt {
         
         void update_values(unsigned_vector const& bound_vars, unsigned_vector const& bound_trail);
 
+        void project(unsigned var);
+
+        void solve_for(unsigned row_id, unsigned x);
+
     public:
 
         model_based_opt();
@@ -106,6 +112,17 @@ namespace opt {
         //
         inf_eps maximize();
 
+
+        // 
+        // Project set of variables from inequalities.
+        //
+        void project(unsigned num_vars, unsigned const* vars);
+
+        //
+        // Extract current rows (after projection).
+        // 
+        void get_live_rows(vector<row>& rows);
+
         void display(std::ostream& out) const;
         void display(std::ostream& out, row const& r) const;
 

src/qe/qe_arith.cpp

@@ -29,6 +29,7 @@ Revision History:
 #include "expr_functors.h"
 #include "expr_safe_replace.h"
 #include "model_based_opt.h"
+#include "model_evaluator.h"
 
 namespace qe {
 
@@ -658,6 +659,9 @@ namespace qe {
             bool new_max = true;
             rational max_r, r;
             expr_ref val(m);
+            model_evaluator eval(mdl);
+            eval.set_model_completion(true);
+            
             bool is_int = a.is_int(m_var->x());
             for (unsigned i = 0; i < num_ineqs(); ++i) {
                 rational const& ac = m_ineq_coeffs[i];
@@ -669,7 +673,7 @@ namespace qe {
                 // ac < 0: x + t/ac > 0 <=> x > max { - t/ac | ac < 0 } = max { t/|ac| | ac < 0 } 
                 //
                 if (ac.is_pos() == do_pos) {
-                    VERIFY(mdl.eval(ineq_term(i), val));
+                    eval(ineq_term(i), val);
                     VERIFY(a.is_numeral(val, r));
                     r /= abs(ac);
                     new_max =

src/qe/qe_mbp.cpp

@@ -28,10 +28,15 @@ Revision History:
 #include "th_rewriter.h"
 #include "model_v2_pp.h"
 #include "expr_functors.h"
+#include "for_each_expr.h"
 
 
 using namespace qe;
 
+struct noop_op_proc {
+    void operator()(expr*) {}
+};
+
 
 /**
    \brief return two terms that are equal in the model.
@@ -106,6 +111,7 @@ void project_plugin::push_back(expr_ref_vector& lits, expr* e) {
 
 class mbp::impl {
     ast_manager& m;
+    th_rewriter m_rw;
     ptr_vector<project_plugin> m_plugins;
     expr_mark m_visited;
 
@@ -130,7 +136,6 @@ class mbp::impl {
             is_var.mark(vars[i].get());
         }
         expr_ref tmp(m), t(m), v(m);            
-        th_rewriter rw(m);
         for (unsigned i = 0; i < lits.size(); ++i) {
             expr* e = lits[i].get(), *l, *r;
             if (m.is_eq(e, l, r) && reduce_eq(is_var, l, r, v, t)) {
@@ -141,7 +146,7 @@ class mbp::impl {
                 is_rem.mark(v);
                 for (unsigned j = 0; j < lits.size(); ++j) {
                     sub(lits[j].get(), tmp);
-                    rw(tmp);
+                    m_rw(tmp);
                     lits[j] = tmp;
                 }
             }
@@ -177,6 +182,29 @@ class mbp::impl {
     }
 
 
+    void filter_variables(model& model, app_ref_vector& vars, expr_ref_vector& lits, expr_ref_vector& unused_lits) {
+        ast_manager& m = vars.get_manager();
+        expr_mark lit_visited;
+        for_each_expr_proc<noop_op_proc> fe;
+        for (unsigned i = 0; i < lits.size(); ++i) {
+            for_each_expr(fe, lit_visited, lits[i].get());
+        }
+        unsigned j = 0;
+        for (unsigned i = 0; i < vars.size(); ++i) {
+            app* var = vars[i].get();
+            if (lit_visited.is_marked(var)) {
+                if (i != j) {
+                    vars[j] = vars[i].get();
+                }
+                ++j;
+            }
+        }
+        if (vars.size() != j) {
+            vars.resize(j);
+        }
+    }
+
+
     void extract_bools(model& model, expr_ref_vector& fmls, expr* fml) {
         TRACE("qe", tout << "extract bools: " << mk_pp(fml, m) << "\n";);
         ptr_vector<expr> todo;
@@ -210,6 +238,42 @@ class mbp::impl {
         }
     }
 
+    void project_bools(model& model, app_ref_vector& vars, expr_ref_vector& fmls) {
+        expr_safe_replace sub(m);
+        expr_ref val(m);
+        unsigned j = 0;
+        for (unsigned i = 0; i < vars.size(); ++i) {
+            app* var = vars[i].get();
+            if (m.is_bool(var)) {
+                VERIFY(model.eval(var, val));
+                sub.insert(var, val);
+            }
+            else {
+                if (j != i) {
+                    vars[j] = vars[i].get();
+                }
+                ++j;
+            }
+        }
+        if (j != vars.size()) {
+            vars.resize(j);
+            j = 0;
+            for (unsigned i = 0; i < fmls.size(); ++i) {
+                sub(fmls[i].get(), val);
+                m_rw(val);
+                if (!m.is_true(val)) {
+                    if (j != i) {
+                        fmls[j] = fmls[i].get();
+                    }
+                    ++j;
+                }
+            }
+            if (j != fmls.size()) {
+                fmls.resize(j);
+            }
+        }
+    }
+
 public:
 
 
@@ -333,7 +397,7 @@ public:
         m_visited.reset();
     }
 
-    impl(ast_manager& m):m(m) {
+    impl(ast_manager& m):m(m), m_rw(m) {
         add_plugin(alloc(arith_project_plugin, m));
         add_plugin(alloc(datatype_project_plugin, m));
         add_plugin(alloc(array_project_plugin, m));
@@ -359,14 +423,16 @@ public:
     void operator()(bool force_elim, app_ref_vector& vars, model& model, expr_ref_vector& fmls) {
         expr_ref val(m), tmp(m);
         app_ref var(m);
-        th_rewriter rw(m);
+        expr_ref_vector unused_fmls(m);
         bool progress = true;
         TRACE("qe", tout << vars << " " << fmls << "\n";);
-        while (progress && !vars.empty()) {
         preprocess_solve(model, vars, fmls);
+        filter_variables(model, vars, fmls, unused_fmls);
+        project_bools(model, vars, fmls);
+        while (progress && !vars.empty() && !fmls.empty()) {
             app_ref_vector new_vars(m);
             progress = false;
-            while (!vars.empty()) {
+            while (!vars.empty() && !fmls.empty()) {
                 var = vars.back();
                 vars.pop_back();
                 project_plugin* p = get_plugin(var);
@@ -377,7 +443,7 @@ public:
                     new_vars.push_back(var);
                 }
             }
-            if (!progress && !new_vars.empty() && force_elim) {
+            if (!progress && !new_vars.empty() && !fmls.empty() && force_elim) {
                 var = new_vars.back();
                 new_vars.pop_back();
                 expr_safe_replace sub(m);
@@ -385,7 +451,7 @@ public:
                 sub.insert(var, val);
                 for (unsigned i = 0; i < fmls.size(); ++i) {
                     sub(fmls[i].get(), tmp);
-                    rw(tmp);
+                    m_rw(tmp);
                     if (m.is_true(tmp)) {
                         project_plugin::erase(fmls, i);
                     }
@@ -396,9 +462,17 @@ public:
                 progress = true;
             }
             vars.append(new_vars);
+            if (progress) {
+                preprocess_solve(model, vars, fmls);
             }
+        }
+        if (fmls.empty()) {
+            vars.reset();
+        }
+        fmls.append(unused_fmls);
         TRACE("qe", tout << vars << " " << fmls << "\n";);
     }
+    
 };
     
 mbp::mbp(ast_manager& m) {

src/qe/qe_mbp.h

@@ -37,6 +37,7 @@ namespace qe {
         virtual bool operator()(model& model, app* var, app_ref_vector& vars, expr_ref_vector& lits) = 0;
         virtual bool solve(model& model, app_ref_vector& vars, expr_ref_vector& lits) = 0;
         virtual family_id get_family_id() = 0;
+        virtual bool operator()(model& model, app_ref_vector& vars, expr_ref_vector& lits) { return false; };
 
         static expr_ref pick_equality(ast_manager& m, model& model, expr* t);
         static void partition_values(model& model, expr_ref_vector const& vals, expr_ref_vector& lits);

src/qe/qsat.cpp

@@ -575,6 +575,7 @@ namespace qe {
         lbool check_sat() {        
             while (true) {
                 ++m_stats.m_num_rounds;
+                IF_VERBOSE(3, verbose_stream() << "(check-qsat level: " << m_level << " round: " << m_stats.m_num_rounds << ")\n";);
                 check_cancel();
                 expr_ref_vector asms(m_asms);
                 m_pred_abs.get_assumptions(m_model.get(), asms);
@@ -1191,7 +1192,7 @@ namespace qe {
 
         lbool maximize(expr_ref_vector const& fmls, app* t, model_ref& mdl, opt::inf_eps& value) {
             expr_ref_vector defs(m);
-            expr_ref fml = negate_core(fmls);
+            expr_ref fml = mk_and(fmls);
             hoist(fml);
             m_objective = t;
             m_value = opt::inf_eps();

src/smt/theory_pb.cpp

@@ -1063,7 +1063,7 @@ namespace smt {
         }
 #endif
         else {
-            IF_VERBOSE(3, display(verbose_stream() << "no propagation ", c, true););
+            IF_VERBOSE(14, display(verbose_stream() << "no propagation ", c, true););
         }
     }
 
@@ -1637,7 +1637,7 @@ namespace smt {
                 // same order as the assignment stack.
                 // It is not a correctness bug but causes to miss lemmas.
                 //
-                IF_VERBOSE(2, display_resolved_lemma(verbose_stream()););
+                IF_VERBOSE(12, display_resolved_lemma(verbose_stream()););
                 TRACE("pb", display_resolved_lemma(tout););
                 return false;
             }
@@ -1735,12 +1735,12 @@ namespace smt {
         // 3x + 3y + z + u >= 4
         // ~x /\ ~y => z + u >= 
 
-        IF_VERBOSE(4, display(verbose_stream() << "lemma1: ", m_lemma););
+        IF_VERBOSE(14, display(verbose_stream() << "lemma1: ", m_lemma););
         hoist_maximal_values();
         lbool is_true = m_lemma.normalize(false);
         m_lemma.prune(false);
 
-        IF_VERBOSE(4, display(verbose_stream() << "lemma2: ", m_lemma););
+        IF_VERBOSE(14, display(verbose_stream() << "lemma2: ", m_lemma););
         //unsigned l_size = m_ineq_literals.size() + ((is_true==l_false)?0:m_lemma.size());
         //if (s_min_l_size >= l_size) {
         //    verbose_stream() << "(pb.conflict min size: " << l_size << ")\n";

src/test/model_based_opt.cpp

@@ -216,6 +216,77 @@ static void test4() {
     std::cout << "u: " << mbo.get_value(u) << "\n";
 }
 
+static void test5() {
+    opt::model_based_opt mbo;
+    unsigned x = mbo.add_var(rational(2));
+    unsigned y = mbo.add_var(rational(3));
+    unsigned z = mbo.add_var(rational(4));
+    unsigned u = mbo.add_var(rational(5));
+
+    add_ineq(mbo, x, 1, y, -1, 0, opt::t_le);
+    add_ineq(mbo, x, 1, z, -1, 0, opt::t_le);
+    add_ineq(mbo, y, 1, u, -1, 0, opt::t_le);
+    add_ineq(mbo, z, 1, u, -1, 1, opt::t_le);
+
+    unsigned vars[2] = { y, z };
+    mbo.project(1, vars);    
+    mbo.display(std::cout);
+
+    mbo.project(1, vars);    
+    mbo.display(std::cout);
+
+    mbo.project(1, vars+1);
+    mbo.display(std::cout);
+
+    vector<opt::model_based_opt::row> rows;
+    mbo.get_live_rows(rows);
+}
+
+
+static void test6() {
+    opt::model_based_opt mbo;
+    unsigned x0 = mbo.add_var(rational(1));
+    unsigned x = mbo.add_var(rational(2));
+    unsigned y = mbo.add_var(rational(3));
+    unsigned z = mbo.add_var(rational(4));
+    unsigned u = mbo.add_var(rational(5));
+    unsigned v = mbo.add_var(rational(6));
+    unsigned w = mbo.add_var(rational(6));
+
+    add_ineq(mbo, x0, 1, y, -1, 0, opt::t_le);
+    add_ineq(mbo, x, 1, y, -1, 0, opt::t_le);
+    add_ineq(mbo, y, 1, u, -1, 0, opt::t_le);
+    add_ineq(mbo, y, 1, z, -1, 1, opt::t_le);
+    add_ineq(mbo, y, 1, v, -1, 1, opt::t_le);
+    add_ineq(mbo, y, 1, w, -1, 1, opt::t_le);
+
+    mbo.display(std::cout);
+    mbo.project(1, &y);
+    mbo.display(std::cout);
+}
+
+static void test7() {
+    opt::model_based_opt mbo;
+    unsigned x0 = mbo.add_var(rational(2));
+    unsigned x = mbo.add_var(rational(1));
+    unsigned y = mbo.add_var(rational(3));
+    unsigned z = mbo.add_var(rational(4));
+    unsigned u = mbo.add_var(rational(5));
+    unsigned v = mbo.add_var(rational(6));
+    unsigned w = mbo.add_var(rational(6));
+
+    add_ineq(mbo, x0, 1, y, -1, 0, opt::t_le);
+    add_ineq(mbo, x, 1, y, -1, 0, opt::t_lt);
+    add_ineq(mbo, y, 1, u, -1, 0, opt::t_le);
+    add_ineq(mbo, y, 1, z, -1, 1, opt::t_le);
+    add_ineq(mbo, y, 1, v, -1, 1, opt::t_le);
+    add_ineq(mbo, y, 1, w, -1, 1, opt::t_lt);
+
+    mbo.display(std::cout);
+    mbo.project(1, &y);
+    mbo.display(std::cout);
+}
+
 // test with mix of upper and lower bounds
 
 void tst_model_based_opt() {
@@ -224,4 +295,8 @@ void tst_model_based_opt() {
     test2();
     test3();
     test4();
+    test5();
+    test6();
+    test7();
+
 }