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

src/opt/opt_context.cpp

@@ -1166,7 +1166,13 @@ namespace opt {
        out << mk_pp(term, m);
        app* q = m.mk_fresh_const(out.str().c_str(), m.get_sort(term));
        if (!fm) fm = alloc(generic_model_converter, m, "opt");
-       m_hard_constraints.push_back(m.mk_eq(q, term));
+       if (m_arith.is_int_real(term)) {
+           m_hard_constraints.push_back(m_arith.mk_ge(q, term));
+           m_hard_constraints.push_back(m_arith.mk_le(q, term));
+       }
+       else {
+           m_hard_constraints.push_back(m.mk_eq(q, term));
+       }
        fm->hide(q);
        return q;
     }

src/opt/opt_context.h

@@ -186,6 +186,7 @@ namespace opt {
         void add_hard_constraint(expr* f, expr* t);
         
         void get_hard_constraints(expr_ref_vector& hard);
+        expr_ref_vector get_hard_constraints() { expr_ref_vector hard(m); get_hard_constraints(hard); return hard; }
         expr_ref get_objective(unsigned i);
 
         void push() override;

src/qe/qe_mbi.cpp

@@ -38,6 +38,7 @@ Notes:
 #include "qe/qe_mbi.h"
 #include "qe/qe_term_graph.h"
 #include "qe/qe_arith.h"
+#include "opt/opt_context.h"
 
 
 namespace qe {
@@ -139,6 +140,10 @@ namespace qe {
 
             if (m_arith.is_int_real(a)) {
                 m_avars.push_back(a);
+                if (!m_seen.contains(a)) {
+                    m_proxies.push_back(a);
+                    m_seen.insert(a);
+                }
             }
             for (expr* arg : *a) {
                 if (is_app(arg) && !m_seen.contains(arg) && m_arith.is_int_real(arg)) {
@@ -259,27 +264,31 @@ namespace qe {
         TRACE("qe", tout << m_solver->get_assertions() << "\n";);
 
 
-        // 1. arithmetical variables - atomic and in purified positions
+        // . arithmetical variables - atomic and in purified positions
         app_ref_vector proxies(m);
         app_ref_vector avars = get_arith_vars(mdl, lits, proxies);
         TRACE("qe", tout << "vars: " << avars << "\nproxies: " << proxies << "\nlits: " << lits << "\n";);
 
-        // 2. project private non-arithmetical variables from lits
+        // . project private non-arithmetical variables from lits
         project_euf(mdl, lits, avars);
 
-        // 3. Order arithmetical variables and purified positions
+        // . Minimzie span between smallest and largest proxy variable.
+        minimize_span(mdl, avars, proxies);
+
+        // . Order arithmetical variables and purified positions
         order_avars(mdl, lits, avars, proxies);
         TRACE("qe", tout << "ordered: " << lits << "\n";);
 
-        // 4. Perform arithmetical projection
+        // . Perform arithmetical projection
         arith_project_plugin ap(m);
         ap.set_check_purified(false);
         auto defs = ap.project(*mdl.get(), avars, lits);
         TRACE("qe", tout << "aproject: " << lits << "\n";);
 
-        // 5. Substitute solution into lits
+        // . Substitute solution into lits
         substitute(defs, lits);
         TRACE("qe", tout << "substitute: " << lits << "\n";);
+        IF_VERBOSE(1, verbose_stream() << lits << "\n");
     }
 
     /**
@@ -307,12 +316,7 @@ namespace qe {
         TRACE("qe", tout << "project: " << lits << "\n";);                
     }
 
-    /**
+    vector<std::pair<rational, app*>> euf_arith_mbi_plugin::sort_proxies(model_ref& mdl, app_ref_vector const& proxies) {
-     * \brief Order arithmetical variables:
-     * 1. add literals that order the proxies according to the model.
-     * 2. sort arithmetical terms, such that deepest terms are first.
-     */
-    void euf_arith_mbi_plugin::order_avars(model_ref& mdl, expr_ref_vector& lits, app_ref_vector& avars, app_ref_vector const& proxies) {
         arith_util a(m);
         model_evaluator mev(*mdl.get());
         vector<std::pair<rational, app*>> vals;
@@ -328,15 +332,61 @@ namespace qe {
                 return x.first < y.first;
             }
         };
-        // add linear order between proxies
+        // add offset ordering between proxies
         compare_first cmp;
         std::sort(vals.begin(), vals.end(), cmp);
+        return vals;
+    }
+
+    void euf_arith_mbi_plugin::minimize_span(model_ref& mdl, app_ref_vector& avars, app_ref_vector const& proxies) {
+        arith_util a(m);
+        opt::context opt(m);        
+        expr_ref_vector fmls(m);
+        m_solver->get_assertions(fmls);
+        for (expr* l : fmls) opt.add_hard_constraint(l);
+        vector<std::pair<rational, app*>> vals = sort_proxies(mdl, proxies);
+        app_ref t(m);
         for (unsigned i = 1; i < vals.size(); ++i) {
-            if (vals[i-1].first == vals[i].first) {
+            rational offset = vals[i].first - vals[i-1].first;
-                lits.push_back(m.mk_eq(vals[i-1].second, vals[i].second));
+            expr* t1 = vals[i-1].second;
+            expr* t2 = vals[i].second;
+            if (offset.is_zero()) {
+                t = m.mk_eq(t1, t2);
             }
             else {
-                lits.push_back(a.mk_lt(vals[i-1].second, vals[i].second));
+                SASSERT(offset.is_pos());
+                t = a.mk_lt(t1, t2);
+            }
+            opt.add_hard_constraint(t);
+        }
+        t = a.mk_sub(vals[0].second, vals.back().second);
+        opt.add_objective(t, true);
+        expr_ref_vector asms(m);
+        VERIFY(l_true == opt.optimize(asms));
+        opt.get_model(mdl);
+        model_evaluator mev(*mdl.get());
+        std::cout << mev(t) << "\n";
+    }
+
+    /**
+     * \brief Order arithmetical variables:
+     * 1. add literals that order the proxies according to the model.
+     * 2. sort arithmetical terms, such that deepest terms are first.
+     */
+    void euf_arith_mbi_plugin::order_avars(model_ref& mdl, expr_ref_vector& lits, app_ref_vector& avars, app_ref_vector const& proxies) {
+        arith_util a(m);
+        model_evaluator mev(*mdl.get());
+        vector<std::pair<rational, app*>> vals = sort_proxies(mdl, proxies);
+        for (unsigned i = 1; i < vals.size(); ++i) {
+            rational offset = vals[i].first - vals[i-1].first;
+            expr* t1 = vals[i-1].second;
+            expr* t2 = vals[i].second;
+            if (offset.is_zero()) {
+                lits.push_back(m.mk_eq(t1, t2));
+            }
+            else {
+                expr_ref t(a.mk_add(t1, a.mk_numeral(offset, true)), m);
+                lits.push_back(a.mk_le(t, t2));
             }
         }
 
@@ -355,9 +405,11 @@ namespace qe {
     }
 
     void euf_arith_mbi_plugin::block(expr_ref_vector const& lits) {
-        collect_atoms(lits);
+        // want to rely only on atoms from original literals: collect_atoms(lits);
-        m_fmls.push_back(mk_not(mk_and(lits)));
+        expr_ref conj(mk_not(mk_and(lits)), m);
-        m_solver->assert_expr(m_fmls.back());
+        //m_fmls.push_back(conj);
+        TRACE("qe", tout << "block " << lits << "\n";);
+        m_solver->assert_expr(conj);
     }
 
 

src/qe/qe_mbi.h

@@ -107,6 +107,8 @@ namespace qe {
         bool get_literals(model_ref& mdl, expr_ref_vector& lits);
         void collect_atoms(expr_ref_vector const& fmls);
         void project_euf(model_ref& mdl, expr_ref_vector& lits, app_ref_vector& avars);
+        vector<std::pair<rational, app*>> sort_proxies(model_ref& mdl, app_ref_vector const& proxies);
+        void minimize_span(model_ref& mdl, app_ref_vector& avars, app_ref_vector const& proxies);
         void order_avars(model_ref& mdl, expr_ref_vector& lits, app_ref_vector& avars, app_ref_vector const& proxies);
         void substitute(vector<def> const& defs, expr_ref_vector& lits);
         void filter_private_arith(app_ref_vector& avars);

src/smt/smt_setup.cpp

@@ -753,6 +753,7 @@ namespace smt {
     }
 
     void setup::setup_lra_arith() {
+        // m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params));
         m_context.register_plugin(alloc(smt::theory_lra, m_manager, m_params));
     }
 

src/smt/theory_lra.cpp

@@ -3149,20 +3149,22 @@ public:
 
     theory_lra::inf_eps value(theory_var v) {
         lp::impq ival = get_ivalue(v);
-        return inf_eps(0, inf_rational(ival.x, ival.y));
+        return inf_eps(rational(0), inf_rational(ival.x, ival.y));
     }
 
     theory_lra::inf_eps maximize(theory_var v, expr_ref& blocker, bool& has_shared) {
         lp::impq term_max;
         lp::lp_status st;
+        lp::var_index vi = 0;
         if (!can_get_bound(v)) {
+            TRACE("arith", tout << "cannot get bound for v" << v << "\n";);
             st = lp::lp_status::UNBOUNDED;
         }
         else {
-            lp::var_index vi = m_theory_var2var_index[v];
+            vi = m_theory_var2var_index[v];
             st = m_solver->maximize_term(vi, term_max);
         }
-        TRACE("arith", display(tout << st << " v" << v << "\n"););
+        TRACE("arith", display(tout << st << " v" << v << " vi: " << vi << "\n"););
         switch (st) {
         case lp::lp_status::OPTIMAL: {
             init_variable_values();