Merge branch 'opt' of https://git01.codeplex.com/z3 into opt

src/api/python/z3.py

@@ -6314,8 +6314,24 @@ class Fixedpoint(Z3PPObject):
 #########################################
 
 class OptimizeObjective:
-    def __init__(self, value):
+    def __init__(self, opt, value, is_max):
-	self.value = value	
+	self._opt = opt
+	self._value = value
+	self._is_max = is_max
+
+    def lower(self):
+	opt = self._opt
+	return _to_expr_ref(Z3_optimize_get_lower(opt.ctx.ref(), opt.optimize, self._value), opt.ctx)
+    
+    def upper(self):
+	opt = self._opt
+	return _to_expr_ref(Z3_optimize_get_upper(opt.ctx.ref(), opt.optimize, self._value), opt.ctx)
+
+    def value(self):
+	if self._is_max:
+	    return self.upper()
+	else:
+	    return self.lower()
 
 class Optimize(Z3PPObject):
     """Optimize API provides methods for solving using objective functions and weighted soft constraints"""
@@ -6372,15 +6388,15 @@ class Optimize(Z3PPObject):
 	    id = ""
 	id = to_symbol(id, self.ctx)
 	v = Z3_optimize_assert_soft(self.ctx.ref(), self.optimize, arg.as_ast(), weight, id)
-	return OptimizeObjective(v)
+	return OptimizeObjective(self, v, False)
 
     def maximize(self, arg):
 	"""Add objective function to maximize."""
-	return OptimizeObjective(Z3_optimize_maximize(self.ctx.ref(), self.optimize, arg.as_ast()))
+	return OptimizeObjective(self, Z3_optimize_maximize(self.ctx.ref(), self.optimize, arg.as_ast()), True)
 
     def minimize(self, arg):
 	"""Add objective function to minimize."""
-	return OptimizeObjective(Z3_optimize_minimize(self.ctx.ref(), self.optimize, arg.as_ast()))
+	return OptimizeObjective(self, Z3_optimize_minimize(self.ctx.ref(), self.optimize, arg.as_ast()), False)
 
     def push(self):
         """create a backtracking point for added rules, facts and assertions"""
@@ -6404,12 +6420,12 @@ class Optimize(Z3PPObject):
     def lower(self, obj):
 	if not isinstance(obj, OptimizeObjective):
 	    raise Z3Exception("Expecting objective handle returned by maximize/minimize")
-	return _to_expr_ref(Z3_optimize_get_lower(self.ctx.ref(), self.optimize, obj.value), self.ctx)
+	return obj.lower()
 
     def upper(self, obj):
 	if not isinstance(obj, OptimizeObjective):
 	    raise Z3Exception("Expecting objective handle returned by maximize/minimize")
-	return _to_expr_ref(Z3_optimize_get_upper(self.ctx.ref(), self.optimize, obj.value), self.ctx)    
+	return obj.upper()
     
     def __repr__(self):
         """Return a formatted string with all added rules and constraints."""

src/ast/ast_smt2_pp.cpp

@@ -1140,6 +1140,17 @@ std::ostream& operator<<(std::ostream& out, app_ref const&  e) {
     return out << mk_ismt2_pp(e.get(), e.get_manager());
 }
 
+std::ostream& operator<<(std::ostream& out, expr_ref_vector const&  e) {
+    for (unsigned i = 0; i < e.size(); ++i) 
+        out << mk_ismt2_pp(e[i], e.get_manager()) << "\n";
+    return out;
+}
+
+std::ostream& operator<<(std::ostream& out, app_ref_vector const&  e) {
+    for (unsigned i = 0; i < e.size(); ++i) 
+        out << mk_ismt2_pp(e[i], e.get_manager()) << "\n";
+    return out;
+}
 
 #ifdef Z3DEBUG
 void pp(expr const * n, ast_manager & m) {

src/ast/ast_smt2_pp.h

@@ -113,4 +113,7 @@ std::ostream& operator<<(std::ostream& out, mk_ismt2_pp const & p);
 std::ostream& operator<<(std::ostream& out, expr_ref const& e);
 std::ostream& operator<<(std::ostream& out, app_ref const& e);
 
+std::ostream& operator<<(std::ostream& out, expr_ref_vector const& e);
+std::ostream& operator<<(std::ostream& out, app_ref_vector const& e);
+
 #endif

src/opt/maxres.cpp

@@ -78,6 +78,7 @@ public:
 private:
     expr_ref_vector  m_B;
     expr_ref_vector  m_asms;    
+    expr_ref_vector  m_defs;
     obj_map<expr, rational> m_asm2weight;
     ptr_vector<expr> m_new_core;
     mus              m_mus;
@@ -102,7 +103,7 @@ public:
            weights_t& ws, expr_ref_vector const& soft, 
            strategy_t st):
         maxsmt_solver_base(c, ws, soft),
-        m_B(m), m_asms(m),
+        m_B(m), m_asms(m), m_defs(m),
         m_mus(c.get_solver(), m),
         m_mss(c.get_solver(), m),
         m_trail(m),
@@ -377,15 +378,19 @@ public:
             for (unsigned i = 0; i < m_asms.size(); ++i) {
                 SASSERT(is_true(m_asms[i].get()));
             });
+        rational upper(0);
         for (unsigned i = 0; i < m_soft.size(); ++i) {
             m_assignment[i] = is_true(m_soft[i]);
+            if (!m_assignment[i]) upper += m_weights[i];
         }
+        SASSERT(upper == m_lower);
         m_upper = m_lower;
         m_found_feasible_optimum = true;
     }
 
 
     virtual lbool operator()() {
+        m_defs.reset();
         switch(m_st) {
         case s_mus:
             return mus_solver();
@@ -635,7 +640,6 @@ public:
         app_ref cls(m), d(m), dd(m);
         m_B.reset();
         m_B.append(core.size(), core.c_ptr());
-        d = m.mk_true();
         //
         // d_0 := true
         // d_i := b_{i-1} and d_{i-1}    for i = 1...sz-1
@@ -651,23 +655,29 @@ public:
         for (unsigned i = 1; i < core.size(); ++i) {
             expr* b_i = m_B[i-1].get();
             expr* b_i1 = m_B[i].get();
-            if (i > 2) {
+            if (i == 1) {
+                d = to_app(b_i);
+            }
+            else if (i == 2) {
+                d = m.mk_and(b_i, d);
+                m_trail.push_back(d);
+            }
+            else {
                 dd = mk_fresh_bool("d");
                 fml = m.mk_implies(dd, d);
                 s().assert_expr(fml);
+                m_defs.push_back(fml);
                 fml = m.mk_implies(dd, b_i);
                 s().assert_expr(fml);
+                m_defs.push_back(fml);
                 d = dd;
             }
-            else {
-                d = m.mk_and(b_i, d);
-                m_trail.push_back(d);
-            }
             asum = mk_fresh_bool("a");
             cls = m.mk_or(b_i1, d);
             fml = m.mk_implies(asum, cls);
             new_assumption(asum, w);
             s().assert_expr(fml);
+            m_defs.push_back(fml);
         }
     }
 
@@ -698,6 +708,7 @@ public:
                 d = mk_fresh_bool("d");
                 fml = m.mk_implies(d, cls);
                 s().assert_expr(fml);
+                m_defs.push_back(fml);
             }
             else {
                 d = cls;
@@ -705,8 +716,10 @@ public:
             asum = mk_fresh_bool("a");
             fml = m.mk_implies(asum, b_i1);
             s().assert_expr(fml);
+            m_defs.push_back(fml);
             fml = m.mk_implies(asum, cls);
             s().assert_expr(fml);
+            m_defs.push_back(fml);
             new_assumption(asum, w);
         }
         fml = m.mk_or(m_B.size(), m_B.c_ptr());
@@ -872,7 +885,13 @@ public:
 
     virtual void commit_assignment() {
         if (m_found_feasible_optimum) {
-            TRACE("opt", tout << "Committing feasible solution\n";);
+            TRACE("opt", tout << "Committing feasible solution\n";
+                  tout << m_defs;
+                  tout << m_asms;
+                  );
+            for (unsigned i = 0; i < m_defs.size(); ++i) {
+                s().assert_expr(m_defs[i].get());
+            }
             for (unsigned i = 0; i < m_asms.size(); ++i) {
                 s().assert_expr(m_asms[i].get());
             }
@@ -884,41 +903,24 @@ public:
 
     void verify_core(exprs const& core) {
         IF_VERBOSE(3, verbose_stream() << "verify core\n";);                
-        ref<solver> sat_solver = mk_inc_sat_solver(m, m_params);
+        ref<solver> smt_solver = mk_smt_solver(m, m_params, symbol());
-
         for (unsigned i = 0; i < s().get_num_assertions(); ++i) {
-            sat_solver->assert_expr(s().get_assertion(i));
+            smt_solver->assert_expr(s().get_assertion(i));
-        }
-        expr_ref n(m);        
-        for (unsigned i = 0; i < core.size(); ++i) {
-            IF_VERBOSE(1, verbose_stream() << mk_pp(core[i],m) << " ";);
-            sat_solver->assert_expr(core[i]);
-        }
-        IF_VERBOSE(1, verbose_stream() << "\n";);
-        lbool is_sat = sat_solver->check_sat(0, 0);
-        if (is_sat != l_false) {
-            IF_VERBOSE(0, verbose_stream() << "!!!not a core\n";);
-        }        
-
-        sat_solver = mk_smt_solver(m, m_params, symbol());
-        for (unsigned i = 0; i < s().get_num_assertions(); ++i) {
-            sat_solver->assert_expr(s().get_assertion(i));
         }
         for (unsigned i = 0; i < core.size(); ++i) {
-            sat_solver->assert_expr(core[i]);
+            smt_solver->assert_expr(core[i]);
         }
-        is_sat = sat_solver->check_sat(0, 0);
+        lbool is_sat = smt_solver->check_sat(0, 0);
         if (is_sat == l_true) {
             IF_VERBOSE(0, verbose_stream() << "not a core\n";);
         }        
-        
     }
 
     void verify_assignment() {
         IF_VERBOSE(0, verbose_stream() << "verify assignment\n";);        
-        ref<solver> sat_solver = mk_inc_sat_solver(m, m_params);
+        ref<solver> smt_solver = mk_smt_solver(m, m_params, symbol());
         for (unsigned i = 0; i < s().get_num_assertions(); ++i) {
-            sat_solver->assert_expr(s().get_assertion(i));
+            smt_solver->assert_expr(s().get_assertion(i));
         }
         expr_ref n(m);
         for (unsigned i = 0; i < m_soft.size(); ++i) {
@@ -926,9 +928,9 @@ public:
             if (!m_assignment[i]) {
                 n = mk_not(m, n);
             }
-            sat_solver->assert_expr(n);
+            smt_solver->assert_expr(n);
         }
-        lbool is_sat = sat_solver->check_sat(0, 0);
+        lbool is_sat = smt_solver->check_sat(0, 0);
         if (is_sat == l_false) {
             IF_VERBOSE(0, verbose_stream() << "assignment is infeasible\n";);
         }

src/opt/maxsmt.cpp

@@ -66,6 +66,7 @@ namespace opt {
         }       
         pb_util pb(m);
         tmp = pb.mk_ge(m_weights.size(), m_weights.c_ptr(), m_soft.c_ptr(), k);
+        TRACE("opt", tout << tmp << "\n";);
         s().assert_expr(tmp);
     }
 
@@ -205,18 +206,13 @@ namespace opt {
             }
         }
 
-        // Infrastructure for displaying and storing solution is TBD.
         IF_VERBOSE(1, verbose_stream() << "is-sat: " << is_sat << "\n";
                    if (is_sat == l_true) {
                        verbose_stream() << "Satisfying soft constraints\n";
                        display_answer(verbose_stream());
                    });
 
-        DEBUG_CODE(if (is_sat == l_true) {
+        DEBUG_CODE(if (is_sat == l_true) verify_assignment(););
-                       verify_assignment();
-                   });
-
-        // TBD: check that all extensions are unsat too
         
         return is_sat;
     }

src/opt/opt_context.cpp

@@ -1203,10 +1203,15 @@ namespace opt {
             }
             case O_MAXSMT: {
                 maxsmt& ms = *m_maxsmts.find(obj.m_id);
+                rational value(0);
                 for (unsigned i = 0; i < obj.m_terms.size(); ++i) {
                     VERIFY(m_model->eval(obj.m_terms[i], val));
+                    if (!m.is_true(val)) {
+                        value += obj.m_weights[i];
+                    }
                     // TBD: check that optimal was not changed.
                 }
+                TRACE("opt", tout << "value " << value << "\n";);
                 break;
             }
             }       

src/shell/opt_frontend.cpp

@@ -313,12 +313,17 @@ static unsigned parse_opt(std::istream& in, bool is_wcnf) {
         opb opb(opt, _in);
         opb.parse();
     }
+    try {
         lbool r = opt.optimize();
         switch (r) {
         case l_true:  std::cout << "sat\n"; break;
         case l_false: std::cout << "unsat\n"; break;
         case l_undef: std::cout << "unknown\n"; break;
         }
+    }
+    catch (z3_exception & ex) {
+        std::cerr << ex.msg() << "\n";
+    }
     #pragma omp critical (g_display_stats) 
     {
         display_statistics();
@@ -329,6 +334,7 @@ static unsigned parse_opt(std::istream& in, bool is_wcnf) {
 }
 
 unsigned parse_opt(char const* file_name, bool is_wcnf) {
+    g_first_interrupt = true;
     g_start_time = static_cast<double>(clock());
     register_on_timeout_proc(on_timeout);
     signal(SIGINT, on_ctrl_c);