enable more simplification in case inequality triggers a change.

src/ast/simplifiers/dependent_expr_state.h

@@ -74,6 +74,8 @@ class dependent_expr_state {
     virtual bool inconsistent() = 0;
     virtual model_reconstruction_trail& model_trail() = 0;
     virtual void flatten_suffix() {}
+    virtual bool updated() = 0;
+    virtual void reset_updated() = 0;
 
     trail_stack    m_trail;
     void push() {
@@ -109,6 +111,9 @@ class default_dependent_expr_state : public dependent_expr_state {
     virtual void add(dependent_expr const& j) { throw default_exception("unexpected addition"); }
     virtual bool inconsistent() { return false; }
     virtual model_reconstruction_trail& model_trail() { throw default_exception("unexpected access to model reconstruction"); }
+    virtual bool updated() { return false; }
+    virtual void reset_updated() {}
+
 };
 
 inline std::ostream& operator<<(std::ostream& out, dependent_expr_state& st) {
@@ -147,7 +152,7 @@ class dependent_expr_simplifier {
     index_set indices() { return index_set(*this); }
 
     proof* mp(proof* a, proof* b) { return (a && b) ? m.mk_modus_ponens(a, b) : nullptr;  }
-
+    proof* tr(proof* a, proof* b) { return m.mk_transitivity(a, b); }
 public:
     dependent_expr_simplifier(ast_manager& m, dependent_expr_state& s) : m(m), m_fmls(s), m_trail(s.m_trail) {}
     virtual ~dependent_expr_simplifier() {}

src/ast/simplifiers/then_simplifier.h

@@ -51,6 +51,10 @@ class then_simplifier : public dependent_expr_simplifier {
         }
     };
 
+protected:
+
+    bool m_bail_on_no_change = false;
+
 public:
 
     then_simplifier(ast_manager& m, params_ref const& p, dependent_expr_state& fmls):
@@ -72,9 +76,17 @@ class then_simplifier : public dependent_expr_simplifier {
                 break;
             s->reset_statistics();
             collect_stats _cs(*s);
-            s->reduce();
-            m_fmls.flatten_suffix();
+            m_fmls.reset_updated();
+            try {
+                s->reduce();
+                m_fmls.flatten_suffix();
+            }
+            catch (rewriter_exception &) {
+                break;
+            }
             TRACE("simplifier", tout << s->name() << "\n" << m_fmls);
+            if (m_bail_on_no_change && !m_fmls.updated())
+                break;
         }      
     }
 
@@ -108,3 +120,14 @@ class then_simplifier : public dependent_expr_simplifier {
             s->pop(n);     
     }
 };
+
+class if_change_simplifier : public then_simplifier {
+public:
+    if_change_simplifier(ast_manager& m, params_ref const& p, dependent_expr_state& fmls):
+        then_simplifier(m, p, fmls) {
+        m_bail_on_no_change = true;
+    }
+
+    char const* name() const override { return "if-change-then"; }
+
+};

src/solver/simplifier_solver.cpp

@@ -36,17 +36,21 @@ class simplifier_solver : public solver {
     struct dep_expr_state : public dependent_expr_state {
         simplifier_solver& s;
         model_reconstruction_trail m_reconstruction_trail;
+        bool m_updated = false;
         dep_expr_state(simplifier_solver& s) :dependent_expr_state(s.m), s(s), m_reconstruction_trail(s.m, m_trail) {}
         ~dep_expr_state() override {}
         virtual unsigned qtail() const override { return s.m_fmls.size(); }
         dependent_expr const& operator[](unsigned i) override { return s.m_fmls[i]; }
         void update(unsigned i, dependent_expr const& j) override { 
             SASSERT(j.fml());  
             check_false(j.fml());
-            s.m_fmls[i] = j; 
+            s.m_fmls[i] = j;
+            m_updated = true;
         }
-        void add(dependent_expr const& j) override { check_false(j.fml()); s.m_fmls.push_back(j); }
+        void add(dependent_expr const& j) override { m_updated = true; check_false(j.fml()); s.m_fmls.push_back(j); }
         bool inconsistent() override { return s.m_inconsistent; }
+        bool updated() override { return m_updated; }
+        void reset_updated() override { m_updated = false; }
         model_reconstruction_trail& model_trail() override { return m_reconstruction_trail; }
         std::ostream& display(std::ostream& out) const override {
             unsigned i = 0;
@@ -77,7 +81,7 @@ class simplifier_solver : public solver {
             expr_mark seen;
             unsigned j = qhead();
             for (unsigned i = qhead(); i < qtail(); ++i) {
-                expr* f = s.m_fmls[i].fml();
+                expr* f = s.m_fmls[i].fml(), *g = nullptr;
                 if (seen.is_marked(f))
                     continue;
                 seen.mark(f, true);
@@ -89,6 +93,12 @@ class simplifier_solver : public solver {
                         add(dependent_expr(s.m, arg, nullptr, d));
                     continue;
                 }
+                if (s.m.is_not(f, g) && s.m.is_or(g)) {
+                    auto* d = s.m_fmls[i].dep();
+                    for (expr* arg : *to_app(g))
+                        add(dependent_expr(s.m, mk_not(s.m, arg), nullptr, d));
+                    continue;
+                }
                 if (i != j)
                     s.m_fmls[j] = s.m_fmls[i];
                 ++j;

src/solver/solver_preprocess.cpp

@@ -47,6 +47,17 @@ Module Name:
 
 void init_preprocess(ast_manager& m, params_ref const& p, then_simplifier& s, dependent_expr_state& st) {
 
+    auto mk_bound_simplifier = [&]() {
+        auto* s1 = alloc(bound_simplifier, m, p, st);
+        auto* s2 = alloc(then_simplifier, m, p, st);
+        s2->add_simplifier(alloc(rewriter_simplifier, m, p, st));
+        s2->add_simplifier(alloc(propagate_values, m, p, st));
+        s2->add_simplifier(alloc(euf::solve_eqs, m, st));
+        auto* r = alloc(if_change_simplifier, m, p, st);
+        r->add_simplifier(s1);
+        r->add_simplifier(s2);
+        return r;
+    };
     smt_params smtp(p);
     s.add_simplifier(alloc(rewriter_simplifier, m, p, st));
     if (smtp.m_propagate_values) s.add_simplifier(alloc(propagate_values, m, p, st));
@@ -60,7 +71,7 @@ void init_preprocess(ast_manager& m, params_ref const& p, then_simplifier& s, de
     if (smtp.m_refine_inj_axiom) s.add_simplifier(alloc(refine_inj_axiom_simplifier, m, p, st));
     if (smtp.m_bv_size_reduce) s.add_simplifier(alloc(bv::slice, m, st));
     if (smtp.m_distribute_forall) s.add_simplifier(alloc(distribute_forall_simplifier, m, p, st));
-    if (smtp.m_bound_simplifier) s.add_simplifier(alloc(bound_simplifier, m, p, st));
+    if (smtp.m_bound_simplifier) s.add_simplifier(mk_bound_simplifier());
     if (smtp.m_eliminate_bounds) s.add_simplifier(alloc(elim_bounds_simplifier, m, p, st));
     if (smtp.m_simplify_bit2int) s.add_simplifier(alloc(bit2int_simplifier, m, p, st));
     if (smtp.m_bb_quantifiers) s.add_simplifier(alloc(bv::elim_simplifier, m, p, st));

src/tactic/dependent_expr_state_tactic.h

@@ -33,6 +33,7 @@ class dependent_expr_state_tactic : public tactic, public dependent_expr_state {
     expr_ref_vector m_frozen;
     scoped_ptr<dependent_expr_simplifier>   m_simp;
     scoped_ptr<model_reconstruction_trail>  m_model_trail;
+    bool m_updated = false;
 
     void init() {
         if (!m_simp) {
@@ -75,13 +76,15 @@ class dependent_expr_state_tactic : public tactic, public dependent_expr_state {
     void update(unsigned i, dependent_expr const& j) override {
         if (inconsistent())
             return;
+        m_updated = true;
         auto [f, p, d] = j();
         m_goal->update(i, f, p, d);
     }
 
     void add(dependent_expr const& j) override {
         if (inconsistent())
             return;
+        m_updated = true;
         auto [f, p, d] = j();
         m_goal->assert_expr(f, p, d);
     }
@@ -96,6 +99,10 @@ class dependent_expr_state_tactic : public tactic, public dependent_expr_state {
 
     char const* name() const override { return m_simp ? m_simp->name() : "null"; }
 
+    bool updated() override { return m_updated; }
+
+    void reset_updated() override { m_updated = false; }
+
     void updt_params(params_ref const& p) override {
         m_params.append(p);
         init();