From e29adbf304fc137703c8747f383eca4237b1d8f7 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 30 Apr 2016 11:18:34 -0700
Subject: [PATCH] fix issues #581: nested timeouts canceled each-other

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/cmd_context/cmd_context.h        |  2 -
 src/math/simplex/model_based_opt.cpp | 86 +++++++++++-----------------
 src/math/simplex/model_based_opt.h   |  8 +--
 src/opt/opt_context.cpp              |  7 ++-
 src/parsers/smt2/smt2parser.cpp      |  2 +-
 src/qe/qe_arith.cpp                  | 11 ++--
 src/qe/qsat.cpp                      |  7 ++-
 src/qe/qsat.h                        |  2 +-
 src/solver/combined_solver.cpp       | 10 ++--
 src/util/cancel_eh.h                 |  8 ++-
 src/util/rlimit.cpp                  | 31 +++++++---
 src/util/rlimit.h                    |  9 ++-
 12 files changed, 96 insertions(+), 87 deletions(-)

diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h
index be3a1f4f8..976fe946a 100644
--- a/src/cmd_context/cmd_context.h
+++ b/src/cmd_context/cmd_context.h
@@ -272,8 +272,6 @@ public:
     cmd_context(bool main_ctx = true, ast_manager * m = 0, symbol const & l = symbol::null);
     ~cmd_context(); 
     void set_cancel(bool f);
-    void cancel() { set_cancel(true); }
-    void reset_cancel() { set_cancel(false); }
     context_params  & params() { return m_params; }
     solver_factory &get_solver_factory() { return *m_solver_factory; }
     solver_factory &get_interpolating_solver_factory() { return *m_interpolating_solver_factory; }
diff --git a/src/math/simplex/model_based_opt.cpp b/src/math/simplex/model_based_opt.cpp
index 989db2cad..77e552da9 100644
--- a/src/math/simplex/model_based_opt.cpp
+++ b/src/math/simplex/model_based_opt.cpp
@@ -20,14 +20,6 @@ Revision History:
 
 #include "model_based_opt.h"
 
-std::ostream& operator<<(std::ostream& out, opt::bound_type bt) {
-    switch (bt) {
-    case opt::unbounded: return out << "unbounded";
-    case opt::strict: return out << "strict";
-    case opt::non_strict: return out << "non-strict";
-    }
-    return out;
-}
 
 std::ostream& operator<<(std::ostream& out, opt::ineq_type ie) {
     switch (ie) {
@@ -128,8 +120,10 @@ namespace opt {
                 return inf_eps::infinity();
             }
         }
+
         //
         // update the evaluation of variables to satisfy the bound.
+        //
 
         update_values(bound_vars, bound_trail);
 
@@ -164,10 +158,10 @@ namespace opt {
             SASSERT(!x_coeff.is_zero());
             val /= -x_coeff;
             // Adjust epsilon to be s
-            if (eps.is_zero() || (!val.is_zero() && eps > abs(val))) {
+            if (!val.is_zero() && (eps.is_zero() || eps > abs(val))) {
                 eps = abs(val)/rational(2);
             }
-            if (eps.is_zero() || (!r.m_value.is_zero() && eps > abs(r.m_value))) {
+            if (!r.m_value.is_zero() && (eps.is_zero() || eps > abs(r.m_value))) {
                 eps = abs(r.m_value)/rational(2);
             }
             //
@@ -186,10 +180,6 @@ namespace opt {
             // <=> x > t/a
             // <=> x := t/a + epsilon
             //
-
-            if (x_coeff.is_pos() && r.m_type == t_lt) {
-                val -= eps;
-            }
             else if (x_coeff.is_neg() && r.m_type == t_lt) {
                 val += eps;
             }
@@ -265,48 +255,36 @@ namespace opt {
         }
     }
 
-    // v0 - v1 <= 0
-    // v0 - v2 <= 0
-    // v2 >= v1
-    // -> v1 - v2 <= 0
     // 
-    // t1 + a1*x <= 0
-    // t2 + a2*x <= 0
-    // (t2 + a2*x) <= (t1 + a1*x)*a2/a1 
-    // => t2*a1/a2 - t1 <= 0
-    // => t2 - t1*a2/a1 <= 0
+    // Let
+    //   row1: t1 + a1*x <= 0
+    //   row2: t2 + a2*x <= 0
+    //
+    // assume a1, a2 have the same signs:
+    //       (t2 + a2*x) <= (t1 + a1*x)*a2/a1 
+    //   <=> t2*a1/a2 - t1 <= 0
+    //   <=> t2 - t1*a2/a1 <= 0
+    //
+    // assume a1 > 0, -a2 < 0:
+    //       t1 + a1*x <= 0,  t2 - a2*x <= 0
+    //       t2/a2 <= -t1/a1
+    //       t2 + t1*a2/a1 <= 0
+    // assume -a1 < 0, a2 > 0:
+    //       t1 - a1*x <= 0,  t2 + a2*x <= 0
+    //       t1/a1 <= -t2/a2
+    //       t2 + t1*a2/a1 <= 0
+    // 
+    // the resolvent is the same in all cases (simpler proof should exist)
+    // 
 
-    bool model_based_opt::resolve(unsigned row_id1, rational const& a1, unsigned row_id2, unsigned x) {
+    void model_based_opt::resolve(unsigned row_src, rational const& a1, unsigned row_dst, unsigned x) {
 
-        SASSERT(a1 == get_coefficient(row_id1, x));
+        SASSERT(a1 == get_coefficient(row_src, 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.
-        // if a1 is positive, then val(t1*a2/a1) <= val(t2*a1/a2)
-        //   replace row2 with the new inequality of the form:
-        //   t1 - a1*t2/a2 <~~ 0
-        //   where <~~ is strict if either <~1 or <~2 is strict.
-        // if a1 is negative, then ....
-        //
    
-        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() || row2.m_type == t_eq) {
-            mul_add(row_id2, -a2/a1, row_id1);
-            return true;
-        }
-        else {
-            row2.m_alive = false;
-            return false;
+        if (m_rows[row_dst].m_alive) {
+            rational a2 = get_coefficient(row_dst, x);
+            mul_add(row_dst, -a2/a1, row_src);            
         }
     }
     
@@ -314,6 +292,9 @@ namespace opt {
     // set row1 <- row1 + c*row2
     //
     void model_based_opt::mul_add(unsigned row_id1, rational const& c, unsigned row_id2) {
+        if (c.is_zero()) {
+            return;
+        }
         m_new_vars.reset();
         row& r1 = m_rows[row_id1];
         row const& r2 = m_rows[row_id2];
@@ -364,6 +345,9 @@ namespace opt {
         if (r2.m_type == t_lt) {
             r1.m_type = t_lt;
         }
+        else if (r2.m_type == t_le && r1.m_type == t_eq) {
+            r1.m_type = t_le;
+        }
         SASSERT(invariant(row_id1, r1));
     }
     
diff --git a/src/math/simplex/model_based_opt.h b/src/math/simplex/model_based_opt.h
index 8a1694059..4efcf8f8f 100644
--- a/src/math/simplex/model_based_opt.h
+++ b/src/math/simplex/model_based_opt.h
@@ -33,11 +33,6 @@ namespace opt {
         t_le
     };
 
-    enum bound_type {
-        unbounded,
-        strict,
-        non_strict
-    };
 
     typedef inf_eps_rational<inf_rational> inf_eps;
     
@@ -78,7 +73,7 @@ namespace opt {
         
         rational get_coefficient(unsigned row_id, unsigned var_id);
 
-        bool resolve(unsigned row_id1, rational const& a1, unsigned row_id2, unsigned x);
+        void resolve(unsigned row_src, rational const& a1, unsigned row_dst, unsigned x);
 
         void mul_add(unsigned row_id1, rational const& c, unsigned row_id2);
 
@@ -118,7 +113,6 @@ namespace opt {
 
 }
 
-std::ostream& operator<<(std::ostream& out, opt::bound_type bt);
 std::ostream& operator<<(std::ostream& out, opt::ineq_type ie);
 
 
diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index c96ba563a..4d65b9a25 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -238,6 +238,11 @@ namespace opt {
         import_scoped_state(); 
         normalize();
         internalize();
+#if 0
+        if (is_qsat_opt()) {
+            return run_qsat_opt();
+        }
+#endif
         update_solver();
         solver& s = get_solver();
         s.assert_expr(m_hard_constraints);
@@ -1465,7 +1470,7 @@ namespace opt {
             term = m_arith.mk_uminus(term);
         }
         inf_eps value;
-        lbool result = qe::maximize(m_hard_constraints, term, value, m_params);
+        lbool result = qe::maximize(m_hard_constraints, term, value, m_model, m_params);
         if (result != l_undef && obj.m_type == O_MINIMIZE) {
             value.neg();
         }
diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp
index 71ef2a06e..2e98a4072 100644
--- a/src/parsers/smt2/smt2parser.cpp
+++ b/src/parsers/smt2/smt2parser.cpp
@@ -403,7 +403,7 @@ namespace smt2 {
         void check_float(char const * msg) { if (!curr_is_float()) throw parser_exception(msg); }
 
         void error(unsigned line, unsigned pos, char const * msg) {
-            m_ctx.reset_cancel();
+            m_ctx.set_cancel(false);
             if (use_vs_format()) {
                 m_ctx.diagnostic_stream() << "Z3(" << line << ", " << pos << "): ERROR: " << msg;
                 if (msg[strlen(msg)-1] != '\n')
diff --git a/src/qe/qe_arith.cpp b/src/qe/qe_arith.cpp
index 243b3dce6..60111a473 100644
--- a/src/qe/qe_arith.cpp
+++ b/src/qe/qe_arith.cpp
@@ -968,32 +968,34 @@ namespace qe {
         
 
         opt::inf_eps maximize(expr_ref_vector const& fmls, model& mdl, app* t, expr_ref& bound) {
+            SASSERT(a.is_real(t));
             opt::model_based_opt mbo;
             opt::inf_eps value;
             obj_map<expr, rational> ts;
             obj_map<expr, unsigned> tids;
+
+            // extract objective function.
             vars coeffs;
             rational c(0), mul(1);
             linearize(mdl, mul, t, c, ts);
             extract_coefficients(ts, tids, coeffs);
             mbo.set_objective(coeffs, c);
 
+            // extract linear constraints
             for (unsigned i = 0; i < fmls.size(); ++i) {
                 linearize(mdl, mbo, fmls[i], tids);
             }
             
-
+            // 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
+            // update model to use new values that satisfy optimality
             ptr_vector<expr> vars;
             obj_map<expr, unsigned>::iterator it = tids.begin(), end = tids.end();
             for (; it != end; ++it) {
@@ -1009,6 +1011,7 @@ namespace qe {
                 }
             }
 
+            // update the predicate 'bound' which forces larger values.
             if (value.get_infinitesimal().is_neg()) {
                 bound = a.mk_le(val, t);
             }
diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp
index 03d8987cf..74b1101fe 100644
--- a/src/qe/qsat.cpp
+++ b/src/qe/qsat.cpp
@@ -1285,7 +1285,7 @@ namespace qe {
         opt::inf_eps     m_value;
         bool             m_was_sat;
 
-        lbool maximize(expr_ref_vector const& fmls, app* t, opt::inf_eps& value) {
+        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);
             hoist(fml);
@@ -1299,6 +1299,7 @@ namespace qe {
             m_ex.assert_expr(fml);
             m_fa.assert_expr(m.mk_not(fml));
             lbool is_sat = check_sat();
+            mdl = m_model.get();
             switch (is_sat) {
             case l_false:
                 if (!m_was_sat) {
@@ -1329,10 +1330,10 @@ namespace qe {
 
     };
 
-    lbool maximize(expr_ref_vector const& fmls, app* t, opt::inf_eps& value, params_ref const& p) {
+    lbool maximize(expr_ref_vector const& fmls, app* t, opt::inf_eps& value, model_ref& mdl, params_ref const& p) {
         ast_manager& m = fmls.get_manager();
         qsat qs(m, p, qsat_maximize);
-        return qs.maximize(fmls, t, value);
+        return qs.maximize(fmls, t, mdl, value);
     }    
 };
 
diff --git a/src/qe/qsat.h b/src/qe/qsat.h
index 08a2cbd53..456711c4f 100644
--- a/src/qe/qsat.h
+++ b/src/qe/qsat.h
@@ -114,7 +114,7 @@ namespace qe {
         void collect_statistics(statistics& st) const;
     };
 
-    lbool maximize(expr_ref_vector const& fmls, app* t, opt::inf_eps& value, params_ref const& p);
+    lbool maximize(expr_ref_vector const& fmls, app* t, opt::inf_eps& value, model_ref& mdl, params_ref const& p);
 
 }
 
diff --git a/src/solver/combined_solver.cpp b/src/solver/combined_solver.cpp
index e19d7a1e3..4e645116c 100644
--- a/src/solver/combined_solver.cpp
+++ b/src/solver/combined_solver.cpp
@@ -83,9 +83,14 @@ private:
         solver *        m_solver;
         volatile bool   m_canceled;
         aux_timeout_eh(solver * s):m_solver(s), m_canceled(false) {}
+        ~aux_timeout_eh() {
+            if (m_canceled) {                
+                m_solver->get_manager().limit().dec_cancel();
+            }
+        }
         virtual void operator()() {
-            m_solver->get_manager().limit().cancel();
             m_canceled = true;
+            m_solver->get_manager().limit().inc_cancel();
         }
     };
 
@@ -225,9 +230,6 @@ public:
                 if ((r != l_undef || !use_solver1_when_undef()) && !eh.m_canceled) {
                     return r;
                 }
-                if (eh.m_canceled) {
-                    m_solver1->get_manager().limit().reset_cancel();
-                }
             }
             IF_VERBOSE(PS_VB_LVL, verbose_stream() << "(combined-solver \"solver 2 failed, trying solver1\")\n";);
         }
diff --git a/src/util/cancel_eh.h b/src/util/cancel_eh.h
index 6b8fc8351..d23e5f544 100644
--- a/src/util/cancel_eh.h
+++ b/src/util/cancel_eh.h
@@ -26,12 +26,14 @@ Revision History:
 */
 template<typename T>
 class cancel_eh : public event_handler {
+    bool m_canceled;
     T & m_obj;
 public:
-    cancel_eh(T & o):m_obj(o) {}
-    ~cancel_eh() { m_obj.reset_cancel(); }
+    cancel_eh(T & o): m_canceled(false), m_obj(o) {}
+    ~cancel_eh() { if (m_canceled) m_obj.dec_cancel(); }
     virtual void operator()() { 
-        m_obj.cancel(); 
+        m_canceled = true;
+        m_obj.inc_cancel(); 
     }
 };
 
diff --git a/src/util/rlimit.cpp b/src/util/rlimit.cpp
index fa34a9555..b3f055955 100644
--- a/src/util/rlimit.cpp
+++ b/src/util/rlimit.cpp
@@ -31,7 +31,7 @@ uint64 reslimit::count() const {
 
 bool reslimit::inc() {
     ++m_count;
-    return !m_cancel && (m_limit == 0 || m_count <= m_limit);
+    return m_cancel == 0 && (m_limit == 0 || m_count <= m_limit);
 }
 
 bool reslimit::inc(unsigned offset) {
@@ -46,7 +46,7 @@ void reslimit::push(unsigned delta_limit) {
     }
     m_limits.push_back(m_limit);
     m_limit = m_limit==0?new_limit:std::min(new_limit, m_limit);
-    m_cancel = false;
+    m_cancel = 0;
 }
 
 void reslimit::pop() {
@@ -55,11 +55,11 @@ void reslimit::pop() {
     }
     m_limit = m_limits.back();
     m_limits.pop_back();
-    m_cancel = false;
+    m_cancel = 0;
 }
 
 char const* reslimit::get_cancel_msg() const {
-    if (m_cancel) {
+    if (m_cancel > 0) {
         return Z3_CANCELED_MSG;
     }
     else {
@@ -84,7 +84,7 @@ void reslimit::pop_child() {
 void reslimit::cancel() {
     #pragma omp critical (reslimit_cancel)
     {
-        set_cancel(true);
+        set_cancel(m_cancel+1);
     }
 }
 
@@ -92,11 +92,28 @@ void reslimit::cancel() {
 void reslimit::reset_cancel() {
     #pragma omp critical (reslimit_cancel)
     {
-        set_cancel(false);
+        set_cancel(0);
     }
 }
 
-void reslimit::set_cancel(bool f) { 
+void reslimit::inc_cancel() {
+    #pragma omp critical (reslimit_cancel)
+    {        
+        set_cancel(m_cancel+1);
+    }
+}
+
+
+void reslimit::dec_cancel() {
+    #pragma omp critical (reslimit_cancel)
+    {
+        if (m_cancel > 0) {
+            set_cancel(m_cancel-1);
+        }
+    }
+}
+
+void reslimit::set_cancel(unsigned f) { 
     m_cancel = f; 
     for (unsigned i = 0; i < m_children.size(); ++i) {
         m_children[i]->set_cancel(f);
diff --git a/src/util/rlimit.h b/src/util/rlimit.h
index c16a8d49b..ac5db6136 100644
--- a/src/util/rlimit.h
+++ b/src/util/rlimit.h
@@ -22,13 +22,13 @@ Revision History:
 #include "vector.h"
 
 class reslimit {
-    volatile bool   m_cancel;
+    volatile unsigned   m_cancel;
     uint64          m_count;
     uint64          m_limit;
     svector<uint64> m_limits;
     ptr_vector<reslimit> m_children;
 
-    void set_cancel(bool f);
+    void set_cancel(unsigned f);
     
 public:    
     reslimit();
@@ -42,10 +42,13 @@ public:
     uint64 count() const; 
 
 
-    bool get_cancel_flag() const { return m_cancel; }
+    bool get_cancel_flag() const { return m_cancel > 0; }
     char const* get_cancel_msg() const;
     void cancel();
     void reset_cancel();
+
+    void inc_cancel();
+    void dec_cancel();
 };
 
 class scoped_rlimit {