qsat-opt

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

src/math/simplex/model_based_opt.cpp

@@ -105,13 +105,10 @@ namespace opt {
             var v = objective().m_vars.back();
             unsigned x = v.m_id;
             rational const& coeff = v.m_coeff;
-            rational const& x_val = m_var2value[x];
-            unsigned_vector const& row_ids = m_var2row_ids[x];
             unsigned bound_row_index;
             rational bound_coeff;
             other.reset();
             if (find_bound(x, bound_row_index, bound_coeff, other, coeff.is_pos())) {
-                row& r = m_rows[bound_row_index];
                 SASSERT(!bound_coeff.is_zero());
                 for (unsigned i = 0; i < other.size(); ++i) {
                     resolve(bound_row_index, bound_coeff, other[i], x);
@@ -150,7 +147,7 @@ namespace opt {
                 if (a.is_zero()) {
                     // skip
                 }
-                else if (a.is_pos() == is_pos) {
+                else if (a.is_pos() == is_pos || r.m_type == t_eq) {
                     rational value = x_val - (r.m_value/a);
                     if (bound_row_index == UINT_MAX) {
                         lub_val = value;
@@ -221,6 +218,7 @@ namespace opt {
         SASSERT(a1 == get_coefficient(row_id1, x));
         SASSERT(!a1.is_zero());
 
+        //
         // row1 is of the form a1*x + t1 <~ 0
         // row2 is of the form a2*x + t2 <~ 0
         // assume that a1, a2 have the same sign.
@@ -229,20 +227,22 @@ namespace opt {
         //   t1 - a1*t2/a2 <~~ 0
         //   where <~~ is strict if either <~1 or <~2 is strict.
         // if a1 is negative, then ....
-        //   
-        if (!m_rows[row_id2].m_alive) {
+        //
+   
+        row& row2 = m_rows[row_id2];
+        if (!row2.m_alive) {
             return false;
         }
         rational a2 = get_coefficient(row_id2, x);
         if (a2.is_zero()) {
             return false;
         }
-        if (a1.is_pos() == a2.is_pos()) {
+        if (a1.is_pos() == a2.is_pos() || row2.m_type == t_eq) {
             mul_add(row_id2, -a2/a1, row_id1);
             return true;
         }
         else {
-            m_rows[row_id2].m_alive = false;
+            row2.m_alive = false;
             return false;
         }
     }

src/opt/opt_context.cpp

@@ -42,6 +42,7 @@ Notes:
 #include "filter_model_converter.h"
 #include "ast_pp_util.h"
 #include "inc_sat_solver.h"
+#include "qsat.h"
 
 namespace opt {
 
@@ -1439,4 +1440,42 @@ namespace opt {
             }       
         } 
     }
+
+    bool context::is_qsat_opt() {
+        if (m_objectives.size() != 1) {
+            return false;
+        }
+        if (m_objectives[0].m_type != O_MAXIMIZE && 
+            m_objectives[0].m_type != O_MINIMIZE) {
+            return false;
+        }
+        for (unsigned i = 0; i < m_hard_constraints.size(); ++i) {
+            if (has_quantifiers(m_hard_constraints[i].get())) {
+                return true;
+            }
+        }
+        return false;
+    }
+
+    lbool context::run_qsat_opt() {
+        SASSERT(is_qsat_opt());
+        app_ref objective(m);
+        opt::bound_type bound;
+        expr_ref value(m);
+        lbool result = qe::maximize(m_hard_constraints, objective, value, bound, m_params);
+        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;
+    }
 }

src/opt/opt_context.h

@@ -289,12 +289,15 @@ namespace opt {
 
         void display_benchmark();
 
-
         // pareto
         void yield();
         expr_ref mk_ge(expr* t, expr* s);
         expr_ref mk_cmp(bool is_ge, model_ref& mdl, objective const& obj);
 
+
+        // quantifiers
+        bool is_qsat_opt();
+        lbool run_qsat_opt();
     };
 
 }

src/qe/qe_arith.cpp

@@ -28,6 +28,7 @@ Revision History:
 #include "expr_functors.h"
 #include "model_v2_pp.h"
 #include "expr_safe_replace.h"
+#include "model_based_opt.h"
 
 namespace qe {
 
@@ -98,6 +99,55 @@ namespace qe {
             }
         }
 
+        void linearize(model& model, opt::model_based_opt& mbo, expr* lit, obj_map<expr, unsigned>& tids) {
+            obj_map<expr, rational> ts;
+            rational c(0), mul(1);
+            expr_ref t(m);
+            opt::ineq_type ty = opt::t_le;
+            expr* e1, *e2;
+            bool is_not = m.is_not(lit, lit);
+            if (is_not) {
+                mul.neg();
+            }
+            SASSERT(!m.is_not(lit));
+            if (a.is_le(lit, e1, e2) || a.is_ge(lit, e2, e1)) {
+                if (is_not) mul.neg();
+                linearize(model, mul, e1, c, ts);
+                linearize(model, -mul, e2, c, ts);
+                ty = is_not ? opt::t_lt : opt::t_le;
+            }
+            else if (a.is_lt(lit, e1, e2) || a.is_gt(lit, e2, e1)) {
+                if (is_not) mul.neg();
+                linearize(model,  mul, e1, c, ts);
+                linearize(model, -mul, e2, c, ts);
+                ty = is_not ? opt::t_le: opt::t_lt;
+            }
+            else if (m.is_eq(lit, e1, e2) && !is_not && is_arith(e1)) {
+                linearize(model,  mul, e1, c, ts);
+                linearize(model, -mul, e2, c, ts);
+                ty = opt::t_eq;
+            }  
+            else if (m.is_distinct(lit) && !is_not && is_arith(to_app(lit)->get_arg(0))) {
+                UNREACHABLE();
+            }
+            else if (m.is_distinct(lit) && is_not && is_arith(to_app(lit)->get_arg(0))) {
+                UNREACHABLE();
+            }
+            else if (m.is_eq(lit, e1, e2) && is_not && is_arith(e1)) {
+                UNREACHABLE();
+            }            
+            else {
+                return;
+            }
+            if (ty == opt::t_lt && is_int()) {
+                c += rational(1);
+                ty = opt::t_le;
+            }            
+            vars coeffs;
+            extract_coefficients(ts, tids, coeffs);
+            mbo.add_constraint(coeffs, c, ty);
+        }
+
         void linearize(model& model, rational const& mul, expr* t, rational& c, obj_map<expr, rational>& ts) {
             expr* t1, *t2, *t3;
             rational mul1;
@@ -913,18 +963,54 @@ namespace qe {
             return true;
         }
 
+        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::model_based_opt mbo;
+
             obj_map<expr, rational> ts;
+            obj_map<expr, unsigned> tids;
+            vars coeffs;
             rational c(0), mul(1);
             linearize(mdl, mul, t, c, ts);              
-                
-            // TBD: 
-            // pick variables one by one from ts.
-            // m_var = alloc(contains_app, m, v);
-            // perform upper or lower projection depending on sign of v.
-            // 
-            return opt::unbounded;
+            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;
+            opt::bound_type result = mbo.maximize(val);
+            value = a.mk_numeral(val, false);
+            switch (result) {
+            case opt::unbounded:
+                bound = m.mk_false();
+                break;
+            case opt::strict:
+                bound = a.mk_le(value, t);
+                break;
+            case opt::non_strict:
+                bound = a.mk_lt(value, t);
+                break;
+            }            
+            return result;
         }
+
+        void extract_coefficients(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();
+            for (; it != end; ++it) {
+                unsigned id;
+                if (!tids.find(it->m_key, id)) {
+                    id = tids.size();
+                    tids.insert(it->m_key, id);
+                }
+                coeffs.push_back(var(id, it->m_value));                
+            }
+        }
+
     };
 
     arith_project_plugin::arith_project_plugin(ast_manager& m) {

src/qe/qsat.cpp

@@ -1326,25 +1326,9 @@ namespace qe {
         void maximize(expr_ref_vector const& core, model& mdl) {
             TRACE("qe", tout << "maximize: " << core << "\n";);
             m_was_sat |= !core.empty();
-            if (core.empty()) {
-                m_ex.assert_expr(m.mk_false());
-                m_fa.assert_expr(m.mk_false());
-                return;
-            }
             expr_ref bound(m);
             m_bound = m_mbp.maximize(core, mdl, m_objective, m_value, bound);
-            switch (m_bound) {
-            case opt::unbounded:
-                m_ex.assert_expr(m.mk_false());
-                m_fa.assert_expr(m.mk_false());
-                break;
-            case opt::strict:
-                m_ex.assert_expr(bound);
-                break;
-            case opt::non_strict:
-                m_ex.assert_expr(bound);
-                break;
-            }
+            m_ex.assert_expr(bound);            
         }
 
     };