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

src/muz/rel/karr_relation.cpp

@@ -111,8 +111,8 @@ namespace datalog {
 
         void filter_interpreted(app* cond) {
             rational one(1), mone(-1);
-            expr* e1, *e2, *en;
+            expr* e1 = 0, *e2 = 0, *en = 0;
-            var* v, *w;
+            var* v = 0, *w = 0;
             rational n1, n2;
             expr_ref_vector conjs(m);
             flatten_and(cond, conjs);

src/muz/transforms/dl_mk_interp_tail_simplifier.cpp

@@ -398,8 +398,8 @@ namespace datalog {
     }
 
     bool mk_interp_tail_simplifier::propagate_variable_equivalences(rule * r, rule_ref& res) {
-      if (!m_context.get_params ().xform_tail_simplifier_pve ())
+        if (!m_context.get_params ().xform_tail_simplifier_pve ())
-        return false;
+            return false;
         unsigned u_len = r->get_uninterpreted_tail_size();
         unsigned len = r->get_tail_size();
         if (u_len == len) {

src/smt/smt_implied_equalities.cpp

@@ -284,7 +284,7 @@ namespace smt {
         }
 
         lbool reduce_cond(model_ref& model, expr* e) {
-            expr* e1, *e2;
+            expr* e1 = 0, *e2 = 0;
             if (m.is_eq(e, e1, e2) && m_array_util.is_as_array(e1) && m_array_util.is_as_array(e2)) {
                 if (e1 == e2) {
                     return l_true;

src/smt/theory_lra.cpp

@@ -689,7 +689,7 @@ namespace smt {
             SASSERT(!ctx().b_internalized(atom));
             bool_var bv = ctx().mk_bool_var(atom);
             ctx().set_var_theory(bv, get_id());
-            expr* n1, *n2;
+            expr* n1 = 0, *n2 = 0;
             rational r;
             lra_lp::bound_kind k;
             theory_var v = null_theory_var;
@@ -721,7 +721,7 @@ namespace smt {
             SASSERT(!ctx().b_internalized(atom));
             bool_var bv = ctx().mk_bool_var(atom);
             ctx().set_var_theory(bv, get_id());
-            expr* n1, *n2;
+            expr* n1 = 0, *n2 = 0;
             rational r;
             lra_lp::bound_kind k;
             theory_var v = null_theory_var;
@@ -862,7 +862,7 @@ namespace smt {
 
         void relevant_eh(app* n) {
             TRACE("arith", tout << mk_pp(n, m) << "\n";);
-            expr* n1, *n2;
+            expr* n1 = 0, *n2 = 0;
             if (a.is_mod(n, n1, n2))
                 mk_idiv_mod_axioms(n1, n2);
             else if (a.is_rem(n, n1, n2))

src/tactic/core/CMakeLists.txt

@@ -7,6 +7,7 @@ z3_add_component(core_tactics
     ctx_simplify_tactic.cpp
     der_tactic.cpp
     distribute_forall_tactic.cpp
+    dom_simplify_tactic.cpp
     elim_term_ite_tactic.cpp
     elim_uncnstr_tactic.cpp
     injectivity_tactic.cpp
@@ -32,6 +33,7 @@ z3_add_component(core_tactics
     ctx_simplify_tactic.h
     der_tactic.h
     distribute_forall_tactic.h
+    dom_simplify_tactic.h
     elim_term_ite_tactic.h
     elim_uncnstr_tactic.h
     injectivity_tactic.h

src/tactic/core/dom_simplify_tactic.cpp

@@ -83,49 +83,59 @@ expr* expr_dominators::intersect(expr* x, expr * y) {
     return x;
 }
 
-void expr_dominators::compute_dominators() {
+bool expr_dominators::compute_dominators() {
     expr * e = m_root;
     SASSERT(m_doms.empty());
     m_doms.insert(e, e);
     bool change = true;
+    unsigned iterations = 1;
     while (change) {
         change = false;
-        SASSERT(m_post2expr.back() == e);
+        SASSERT(m_post2expr.empty() || m_post2expr.back() == e);
-        for (unsigned i = 0; i < m_post2expr.size() - 1; ++i) {
+        for (unsigned i = 0; i + 1 < m_post2expr.size(); ++i) {
             expr * child = m_post2expr[i];
             ptr_vector<expr> const& p = m_parents[child];
             SASSERT(!p.empty());
-            expr * new_idom = p[0], * idom2 = 0;
+            expr * new_idom = 0, *idom2 = 0;
-            for (unsigned j = 1; j < p.size(); ++j) {
+            for (unsigned j = 0; j < p.size(); ++j) {
-                if (m_doms.find(p[j], idom2)) {
+                if (!new_idom) {
+                    m_doms.find(p[j], new_idom);
+                }
+                else if (m_doms.find(p[j], idom2)) {
                     new_idom = intersect(new_idom, idom2);
                 }
             }
-            if (!m_doms.find(child, idom2) || idom2 != new_idom) {
+            if (new_idom && (!m_doms.find(child, idom2) || idom2 != new_idom)) {
                 m_doms.insert(child, new_idom);
                 change = true;
             }
         }
+        iterations *= 2;        
+        if (change && iterations > m_post2expr.size()) {
+            return false;
+        }
     }
+    return true;
 }
 
 void expr_dominators::extract_tree() {
     for (auto const& kv : m_doms) {
         add_edge(m_tree, kv.m_value, kv.m_key);
     }
-}    
+}
 
-void expr_dominators::compile(expr * e) {
+bool expr_dominators::compile(expr * e) {
     reset();
     m_root = e;
     compute_post_order();
-    compute_dominators();
+    if (!compute_dominators()) return false;
     extract_tree();
+    return true;
 }
 
-void expr_dominators::compile(unsigned sz, expr * const* es) {
+bool expr_dominators::compile(unsigned sz, expr * const* es) {
     expr_ref e(m.mk_and(sz, es), m);
-    compile(e);
+    return compile(e);
 }
 
 void expr_dominators::reset() {
@@ -147,9 +157,9 @@ tactic * dom_simplify_tactic::translate(ast_manager & m) {
 }
 
 void dom_simplify_tactic::operator()(
-    goal_ref const & in, 
+    goal_ref const & in,
-    goal_ref_buffer & result, 
+    goal_ref_buffer & result,
-    model_converter_ref & mc, 
+    model_converter_ref & mc,
     proof_converter_ref & pc,
     expr_dependency_ref & core) {
     mc = 0; pc = 0; core = 0;
@@ -162,33 +172,43 @@ void dom_simplify_tactic::operator()(
 }
 
 void dom_simplify_tactic::cleanup() {
-    m_trail.reset(); 
+    m_trail.reset();
-    m_args.reset(); 
+    m_args.reset();
-    m_args2.reset(); 
+    m_result.reset();
-    m_result.reset(); 
+    m_dominators.reset();
-    m_dominators.reset(); 
 }
 
 expr_ref dom_simplify_tactic::simplify_ite(app * ite) {
     expr_ref r(m);
-    expr * c = 0, * t = 0, * e = 0;
+    expr * c = 0, *t = 0, *e = 0;
     VERIFY(m.is_ite(ite, c, t, e));
     unsigned old_lvl = scope_level();
     expr_ref new_c = simplify(c);
     if (m.is_true(new_c)) {
         r = simplify(t);
-    }
+    } 
     else if (m.is_false(new_c) || !assert_expr(new_c, false)) {
         r = simplify(e);
-    }
+    } 
     else {
-        expr_ref new_t = simplify(t);
+        for (expr * child : tree(ite)) {
+            if (is_subexpr(child, t) && !is_subexpr(child, e)) {
+                simplify(child);
+            }
+        }
+
         pop(scope_level() - old_lvl);
+        expr_ref new_t = simplify(t);
         if (!assert_expr(new_c, true)) {
             return new_t;
         }
-        expr_ref new_e = simplify(e);
+        for (expr * child : tree(ite)) {
+            if (is_subexpr(child, e) && !is_subexpr(child, t)) {
+                simplify(child);
+            }
+        }
         pop(scope_level() - old_lvl);
+        expr_ref new_e = simplify(e);
         if (c == new_c && t == new_t && e == new_e) {
             r = ite;
         }
@@ -197,7 +217,7 @@ expr_ref dom_simplify_tactic::simplify_ite(app * ite) {
         }
         else {
             TRACE("tactic", tout << new_c << "\n" << new_t << "\n" << new_e << "\n";);
-            r = m.mk_ite(new_c, new_t, new_c);
+            r = m.mk_ite(new_c, new_t, new_e);
         }        
     }    
     return r;
@@ -224,11 +244,8 @@ expr_ref dom_simplify_tactic::simplify(expr * e0) {
         r = simplify_or(to_app(e));
     }
     else {
-        expr_dominators::tree_t const& t = m_dominators.get_tree();
+        for (expr * child : tree(e)) {
-        if (auto children = t.find_core(e)) {
+            simplify(child);
-            for (expr * child : children->get_data().m_value) {
-                simplify(child);
-            }
         }
         if (is_app(e)) {
             m_args.reset();
@@ -245,45 +262,52 @@ expr_ref dom_simplify_tactic::simplify(expr * e0) {
     cache(e0, r);
     TRACE("simplify", tout << "depth: " << m_depth << " " << mk_pp(e0, m) << " -> " << r << "\n";);
     --m_depth;
+    m_subexpr_cache.reset();
     return r;
 }
 
 expr_ref dom_simplify_tactic::simplify_and_or(bool is_and, app * e) {
     expr_ref r(m);
     unsigned old_lvl = scope_level();
-    m_args.reset();
+
+    auto is_subexpr_arg = [&](expr * child, expr * except) {
+        if (!is_subexpr(child, except))
+            return false;
+        for (expr * arg : *e) {
+            if (arg != except && is_subexpr(child, arg))
+                return false;
+        }
+        return true;
+    };
+
+    expr_ref_vector args(m);
     for (expr * arg : *e) {
-        r = simplify(arg);
+        for (expr * child : tree(arg)) {
-        if (!assert_expr(r, !is_and)) {
+            if (is_subexpr_arg(child, arg)) {
-            r = is_and ? m.mk_false() : m.mk_true();
+                simplify(child);
+            }
+        }
+        r = simplify(arg);
+        args.push_back(r);
+        if (!assert_expr(simplify(arg), !is_and)) {
+            r = is_and ? m.mk_false() : m.mk_true();
+            return r;
         }
-        m_args.push_back(r);
     }
     pop(scope_level() - old_lvl);
-    m_args.reverse();
+    r = is_and ? mk_and(args) : mk_or(args);
-    m_args2.reset();
-    for (expr * arg : m_args) {
-        r = simplify(arg);
-        if (!assert_expr(r, !is_and)) {
-            r = is_and ? m.mk_false() : m.mk_true();
-        }
-        m_args2.push_back(r);
-    }
-    pop(scope_level() - old_lvl);
-    m_args2.reverse();
-    r = is_and ? mk_and(m_args2) : mk_or(m_args2);
     return r;
 }
 
 
-void dom_simplify_tactic::init(goal& g) {
+bool dom_simplify_tactic::init(goal& g) {
     expr_ref_vector args(m);
     unsigned sz = g.size();
     for (unsigned i = 0; i < sz; ++i) args.push_back(g.form(i));
     expr_ref fml = mk_and(args);
     m_result.reset();
     m_trail.reset();
-    m_dominators.compile(fml);
+    return m_dominators.compile(fml);
 }
 
 void dom_simplify_tactic::simplify_goal(goal& g) {
@@ -295,7 +319,7 @@ void dom_simplify_tactic::simplify_goal(goal& g) {
         change = false;
 
         // go forwards
-        init(g);
+        if (!init(g)) return;
         unsigned sz = g.size();
         for (unsigned i = 0; !g.inconsistent() && i < sz; ++i) {
             expr_ref r = simplify(g.form(i));
@@ -312,7 +336,7 @@ void dom_simplify_tactic::simplify_goal(goal& g) {
         pop(scope_level());
         
         // go backwards
-        init(g);
+        if (!init(g)) return;
         sz = g.size();
         for (unsigned i = sz; !g.inconsistent() && i > 0; ) {
             --i;
@@ -332,11 +356,36 @@ void dom_simplify_tactic::simplify_goal(goal& g) {
     SASSERT(scope_level() == 0);
 }
 
+bool dom_simplify_tactic::is_subexpr(expr * a, expr * b) {
+    if (a == b)
+        return true;
+
+    bool r;
+    if (m_subexpr_cache.find(a, b, r))
+        return r;
+
+    for (expr * e : tree(b)) {
+        if (is_subexpr(a, e)) {
+            m_subexpr_cache.insert(a, b, true);
+            return true;
+        }
+    }
+    m_subexpr_cache.insert(a, b, false);   
+    return false;
+}
+
+ptr_vector<expr> const & dom_simplify_tactic::tree(expr * e) {
+    if (auto p = m_dominators.get_tree().find_core(e))
+        return p->get_data().get_value();
+    return m_empty;
+}
+
 
 // ----------------------
 // expr_substitution_simplifier
 
 bool expr_substitution_simplifier::assert_expr(expr * t, bool sign) {
+    m_scoped_substitution.push();
     expr* tt;    
     if (!sign) {
         update_substitution(t, 0);
@@ -388,6 +437,8 @@ void expr_substitution_simplifier::update_substitution(expr* n, proof* pr) {
     if (is_ground(n) && (m.is_eq(n, lhs, rhs) || m.is_iff(n, lhs, rhs))) {
         compute_depth(lhs);
         compute_depth(rhs);
+        m_trail.push_back(lhs);
+        m_trail.push_back(rhs);
         if (is_gt(lhs, rhs)) {
             TRACE("propagate_values", tout << "insert " << mk_pp(lhs, m) << " -> " << mk_pp(rhs, m) << "\n";);
             m_scoped_substitution.insert(lhs, rhs, pr);
@@ -439,3 +490,7 @@ void expr_substitution_simplifier::compute_depth(expr* e) {
         m_expr2depth.insert(e, d + 1);
     }
 }
+
+tactic * mk_dom_simplify_tactic(ast_manager & m, params_ref const & p) {
+    return clean(alloc(dom_simplify_tactic, m, alloc(expr_substitution_simplifier, m), p));
+}

src/tactic/core/dom_simplify_tactic.h

@@ -23,6 +23,8 @@ Notes:
 #include "ast/ast.h"
 #include "ast/expr_substitution.h"
 #include "tactic/tactic.h"
+#include "tactic/tactical.h"
+#include "util/obj_pair_hashtable.h"
 
 
 class expr_dominators {
@@ -43,52 +45,57 @@ private:
 
     void compute_post_order();
     expr* intersect(expr* x, expr * y);
-    void compute_dominators();
+    bool compute_dominators();
     void extract_tree();
 
 public:
     expr_dominators(ast_manager& m): m(m), m_root(m) {}
 
-    void compile(expr * e);
+    bool compile(expr * e);
-    void compile(unsigned sz, expr * const* es);
+    bool compile(unsigned sz, expr * const* es);
     tree_t const& get_tree() { return m_tree; }
     void reset();
     
 };
 
+class dom_simplifier {
+ public:
+    dom_simplifier() {}
+    
+    virtual ~dom_simplifier() {}
+    /**
+       \brief assert_expr performs an implicit push
+    */
+    virtual bool assert_expr(expr * t, bool sign) = 0;
+    
+    /**
+       \brief apply simplification.
+    */
+    virtual void operator()(expr_ref& r) = 0;
+    
+    /**
+       \brief pop scopes accumulated from assertions.
+    */
+    virtual void pop(unsigned num_scopes) = 0;
+    
+    virtual dom_simplifier * translate(ast_manager & m) = 0;
+    
+};
+
 class dom_simplify_tactic : public tactic {
 public:
-    class simplifier {
-    public:
-        virtual ~simplifier() {}
-        /**
-           \brief assert_expr performs an implicit push
-         */
-        virtual bool assert_expr(expr * t, bool sign) = 0;
-
-        /**
-           \brief apply simplification.
-        */
-        virtual void operator()(expr_ref& r) = 0;
-
-        /**
-           \brief pop scopes accumulated from assertions.
-         */
-        virtual void pop(unsigned num_scopes) = 0;
-
-        virtual simplifier * translate(ast_manager & m);
-
-    };
 private:
     ast_manager&         m;
-    simplifier*          m_simplifier;
+    dom_simplifier*      m_simplifier;
     params_ref           m_params;
-    expr_ref_vector      m_trail, m_args, m_args2;
+    expr_ref_vector      m_trail, m_args;
     obj_map<expr, expr*> m_result;
     expr_dominators      m_dominators;
     unsigned             m_scope_level;
     unsigned             m_depth;
     unsigned             m_max_depth;
+    ptr_vector<expr>     m_empty;
+    obj_pair_map<expr, expr, bool> m_subexpr_cache;
 
     expr_ref simplify(expr* t);
     expr_ref simplify_ite(app * ite);
@@ -97,19 +104,23 @@ private:
     expr_ref simplify_and_or(bool is_and, app * ite);
     void simplify_goal(goal& g);
 
-    expr_ref get_cached(expr* t) { expr* r = 0; if (!m_result.find(r, r)) r = t; return expr_ref(r, m); }
+    bool is_subexpr(expr * a, expr * b);
+
+    expr_ref get_cached(expr* t) { expr* r = 0; if (!m_result.find(t, r)) r = t; return expr_ref(r, m); }
     void cache(expr *t, expr* r) { m_result.insert(t, r); m_trail.push_back(r); }
 
+    ptr_vector<expr> const & tree(expr * e);
+
     unsigned scope_level() { return m_scope_level; }
     void pop(unsigned n) { SASSERT(n <= m_scope_level); m_scope_level -= n; m_simplifier->pop(n); }
     bool assert_expr(expr* f, bool sign) { m_scope_level++; return m_simplifier->assert_expr(f, sign); }
 
-    void init(goal& g);
+    bool init(goal& g);
 
 public:
-    dom_simplify_tactic(ast_manager & m, simplifier* s, params_ref const & p = params_ref()):
+    dom_simplify_tactic(ast_manager & m, dom_simplifier* s, params_ref const & p = params_ref()):
         m(m), m_simplifier(s), m_params(p), 
-        m_trail(m), m_args(m), m_args2(m), 
+        m_trail(m), m_args(m), 
         m_dominators(m), 
         m_scope_level(0), m_depth(0), m_max_depth(1024) {}
 
@@ -130,11 +141,12 @@ public:
     virtual void cleanup();
 };
 
-class expr_substitution_simplifier : public dom_simplify_tactic::simplifier {
+class expr_substitution_simplifier : public dom_simplifier {
     ast_manager&             m;
     expr_substitution        m_subst;
     scoped_expr_substitution m_scoped_substitution;
     obj_map<expr, unsigned>  m_expr2depth;
+    expr_ref_vector          m_trail;
 
     // move from asserted_formulas to here..
     void compute_depth(expr* e);
@@ -142,7 +154,7 @@ class expr_substitution_simplifier : public dom_simplify_tactic::simplifier {
     unsigned depth(expr* e) { return m_expr2depth[e]; }
 
 public:
-    expr_substitution_simplifier(ast_manager& m): m(m), m_subst(m), m_scoped_substitution(m_subst) {}
+    expr_substitution_simplifier(ast_manager& m): m(m), m_subst(m), m_scoped_substitution(m_subst), m_trail(m) {}
     virtual ~expr_substitution_simplifier() {}
     virtual bool assert_expr(expr * t, bool sign);
 
@@ -152,12 +164,17 @@ public:
     
     virtual void pop(unsigned num_scopes) { m_scoped_substitution.pop(num_scopes); }
     
-    virtual simplifier * translate(ast_manager & m) {
+    virtual dom_simplifier * translate(ast_manager & m) {
         SASSERT(m_subst.empty());
         return alloc(expr_substitution_simplifier, m);
     }
-
-    
 };
 
+
+tactic * mk_dom_simplify_tactic(ast_manager & m, params_ref const & p = params_ref());
+
+/*
+ADD_TACTIC("dom-simplify", "apply dominator simplification rules.", "mk_dom_simplify_tactic(m, p)")
+*/
+
 #endif

src/util/lp/lar_solver.h

@@ -417,6 +417,8 @@ public:
 
         for (unsigned i : m_rows_with_changed_bounds.m_index) {
             calculate_implied_bounds_for_row(i, bp);
+            if (settings().get_cancel_flag())
+                return;
         }
         m_rows_with_changed_bounds.clear();
         if (!use_tableau()) {

src/util/lp/lp_primal_core_solver_tableau.h

@@ -176,25 +176,34 @@ unsigned lp_primal_core_solver<T, X>::solve_with_tableau() {
         default:
             break; // do nothing
         }
-    } while (this->get_status() != FLOATING_POINT_ERROR
+	} while (this->get_status() != FLOATING_POINT_ERROR
-             &&
+		&&
-             this->get_status() != UNBOUNDED
+		this->get_status() != UNBOUNDED
-             &&
+		&&
-             this->get_status() != OPTIMAL
+		this->get_status() != OPTIMAL
-             &&
+		&&
-             this->get_status() != INFEASIBLE
+		this->get_status() != INFEASIBLE
-             &&
+		&&
-             this->iters_with_no_cost_growing() <= this->m_settings.max_number_of_iterations_with_no_improvements
+		this->iters_with_no_cost_growing() <= this->m_settings.max_number_of_iterations_with_no_improvements
-             &&
+		&&
-             this->total_iterations() <= this->m_settings.max_total_number_of_iterations
+		this->total_iterations() <= this->m_settings.max_total_number_of_iterations
-             &&
+		&&
-             !(this->current_x_is_feasible() && this->m_look_for_feasible_solution_only));
+		!(this->current_x_is_feasible() && this->m_look_for_feasible_solution_only)
+		&&
+		this->m_settings.get_cancel_flag() == false);
+	
+	if (this->m_settings.get_cancel_flag()) {
+            this->set_status(CANCELLED);
+	}
 
-    SASSERT(this->get_status() == FLOATING_POINT_ERROR
+	SASSERT(
-                ||
+            this->get_status() == FLOATING_POINT_ERROR
-                this->current_x_is_feasible() == false
+            ||
-                ||
+            this->get_status() == CANCELLED
-                this->calc_current_x_is_feasible_include_non_basis());
+            ||
+            this->current_x_is_feasible() == false
+            ||
+            this->calc_current_x_is_feasible_include_non_basis());
     return this->total_iterations();
 
 }

src/util/lp/lp_settings.h

@@ -61,7 +61,8 @@ enum lp_status {
     TIME_EXHAUSTED,
     ITERATIONS_EXHAUSTED,
     EMPTY,
-    UNSTABLE
+    UNSTABLE,
+    CANCELLED
 };
 
 // when the ratio of the vector lenth to domain size to is greater than the return value we switch to solve_By_for_T_indexed_only