add more simplifiers, fix model reconstruction order for elim_unconst…

…rained

- enable sat.smt in smt_tactic that
is invoked by default on first goals
add flatten-clauses
add push-ite
have tptp5 front-end pretty print SMT2 formulas a little nicer.

examples/tptp/tptp5.cpp

@@ -2305,20 +2305,33 @@ static void display_smt2(std::ostream& out) {
         return;
     }
 
+    z3::expr_vector asms(ctx);
     size_t num_assumptions = fmls.m_formulas.size();
+    for (size_t i = 0; i < num_assumptions; ++i) 
+        asms.push_back(fmls.m_formulas[i]);
 
-    Z3_ast* assumptions = new Z3_ast[num_assumptions];
-    for (size_t i = 0; i < num_assumptions; ++i) {
-        assumptions[i] = fmls.m_formulas[i];
+    for (size_t i = 0; i < asms.size(); ++i) {
+        z3::expr fml = asms[i];
+        if (fml.is_and()) {
+            asms.set(i, fml.arg(0));
+            for (unsigned j = 1; j < fml.num_args(); ++j)
+                asms.push_back(fml.arg(j));
+            --i;
+        }
     }
+
+    Z3_ast* assumptions = new Z3_ast[asms.size()];
+    for (size_t i = 0; i < asms.size(); ++i) 
+        assumptions[i] = asms[i];        
+    Z3_set_ast_print_mode(ctx, Z3_PRINT_SMTLIB_FULL);
     Z3_string s = 
         Z3_benchmark_to_smtlib_string(
             ctx, 
             "Benchmark generated from TPTP", // comment
             0,         // no logic is set
             "unknown", // no status annotation
             "",        // attributes
-            static_cast<unsigned>(num_assumptions), 
+            static_cast<unsigned>(asms.size()), 
             assumptions, 
             ctx.bool_val(true));
 

src/ast/simplifiers/elim_term_ite.h

@@ -15,19 +15,21 @@ Module Name:
 #pragma once
 
 #include "ast/simplifiers/dependent_expr_state.h"
-#include "ast/rewriter/elim_term_ite.h"
+#include "ast/normal_forms/elim_term_ite.h""
 
 
 class elim_term_ite_simplifier : public dependent_expr_simplifier {
-    elim_term_ite m_elim;
-
+    defined_names    m_df;
+    elim_term_ite_rw m_rewriter;
+
 public:
     elim_term_ite_simplifier(ast_manager& m, params_ref const& p, dependent_expr_state& fmls):
         dependent_expr_simplifier(m, fmls),
-        m_elim_term_ite(m) {
+        m_df(m),
+        m_rewriter(m, m_df) {
     }
 
-    char const* name() const override { return "distribute-forall"; }
+    char const* name() const override { return "elim-term-ite"; }
         
     void reduce() override {
         if (!m_fmls.has_quantifiers())
@@ -42,8 +44,8 @@ class elim_term_ite_simplifier : public dependent_expr_simplifier {
         }
     }
 
-    void push() override { dependent_expr_simplifier::push(); m_rewriter.push(); }
+    void push() override { dependent_expr_simplifier::push(); m_df.push(); m_rewriter.push(); }
     
-    void pop(unsigned n) override { dependent_expr_simplifier::pop(n); m_rewriter.pop(n); } 
+    void pop(unsigned n) override { m_rewriter.pop(n); m_df.pop(n); dependent_expr_simplifier::pop(n); }
 };
 

src/ast/simplifiers/elim_unconstrained.cpp

@@ -249,32 +249,32 @@ void elim_unconstrained::assert_normalized(vector<dependent_expr>& old_fmls) {
 
 void elim_unconstrained::update_model_trail(generic_model_converter& mc, vector<dependent_expr> const& old_fmls) {
     auto& trail = m_fmls.model_trail();
-    scoped_ptr<expr_replacer> rp = mk_default_expr_replacer(m, false);
-    scoped_ptr<expr_substitution> sub = alloc(expr_substitution, m, true, false);
-    rp->set_substitution(sub.get());
-    expr_ref new_def(m);
+
     for (auto const& entry : mc.entries()) {
         switch (entry.m_instruction) {
         case generic_model_converter::instruction::HIDE:
+            trail.hide(entry.m_f);
             break;
         case generic_model_converter::instruction::ADD:
-            new_def = entry.m_def;
-            (*rp)(new_def);           
-            sub->insert(m.mk_const(entry.m_f), new_def, nullptr, nullptr);
             break;
         }
     }
-    trail.push(sub.detach(), old_fmls);
-
+    scoped_ptr<expr_replacer> rp = mk_default_expr_replacer(m, false);
+    scoped_ptr<expr_substitution> sub = alloc(expr_substitution, m, true, false);
+    rp->set_substitution(sub.get());
+    expr_ref new_def(m);
     for (auto const& entry : mc.entries()) {
         switch (entry.m_instruction) {
         case generic_model_converter::instruction::HIDE:
-            trail.hide(entry.m_f);
             break;
         case generic_model_converter::instruction::ADD:
+            new_def = entry.m_def;
+            (*rp)(new_def);           
+            sub->insert(m.mk_const(entry.m_f), new_def, nullptr, nullptr);
             break;
         }
     }
+    trail.push(sub.detach(), old_fmls);
 }
 
 void elim_unconstrained::reduce() {

src/ast/simplifiers/flatten_clauses.h

@@ -0,0 +1,95 @@
+/*++
+Copyright (c) 2022 Microsoft Corporation
+
+Module Name:
+
+    flatten_clauses.h
+
+Abstract:
+
+    flatten clauses
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2022-11-24
+
+--*/
+
+#pragma once
+
+#include "ast/simplifiers/dependent_expr_state.h"
+#include "ast/rewriter/th_rewriter.h"
+#include "ast/ast_util.h"
+
+
+class flatten_clauses : public dependent_expr_simplifier {
+
+    unsigned m_num_flat = 0;
+
+    bool is_literal(expr* a) {
+        m.is_not(a, a);
+        return !is_app(a) || to_app(a)->get_num_args() == 0;        
+    }
+
+    bool is_reducible(expr* a, expr* b) {
+        return b->get_ref_count() == 1 || is_literal(a);
+    }
+
+public:
+    flatten_clauses(ast_manager& m, params_ref const& p, dependent_expr_state& fmls):
+        dependent_expr_simplifier(m, fmls) {
+    }
+
+    char const* name() const override { return "flatten-clauses"; }
+
+    void reset_statistics() override { m_num_flat = 0; }
+
+    void collect_statistics(statistics& st) const override {
+        st.update("flatten-clauses-rewrites", m_num_flat);
+    }
+
+    void reduce() override {
+        bool change = true;
+
+        while (change) {
+            change = false;
+            for (unsigned idx : indices()) {
+                auto de = m_fmls[idx];
+                expr* f = de.fml(), *a, *b, *c;
+                bool decomposed = false;
+                if (m.is_or(f, a, b) && m.is_not(b, b) && m.is_or(b) && is_reducible(a, b)) 
+                    decomposed = true;
+                else if (m.is_or(f, b, a) && m.is_not(b, b) && m.is_or(b) && is_reducible(a, b))
+                    decomposed = true;
+                if (decomposed) {
+                    for (expr* arg : *to_app(b)) 
+                        m_fmls.add(dependent_expr(m, m.mk_or(a, mk_not(m, arg)), de.dep()));
+                    m_fmls.update(idx, dependent_expr(m, m.mk_true(), nullptr));
+                    change = true;
+                    ++m_num_flat;
+                    continue;
+                }
+                if (m.is_or(f, a, b) && m.is_and(b) && is_reducible(a, b))
+                    decomposed = true;
+                else if (m.is_or(f, b, a) && m.is_and(b) && is_reducible(a, b))
+                    decomposed = true;
+                if (decomposed) {
+                    for (expr * arg : *to_app(b))
+                        m_fmls.add(dependent_expr(m, m.mk_or(a, arg), de.dep()));
+                    m_fmls.update(idx, dependent_expr(m, m.mk_true(), nullptr));
+                    change = true;
+                    ++m_num_flat;
+                    continue;
+                }
+                if (m.is_ite(f, a, b, c)) {
+                    m_fmls.add(dependent_expr(m, m.mk_or(mk_not(m, a), b), de.dep()));
+                    m_fmls.add(dependent_expr(m, m.mk_or(a, c), de.dep()));
+                    m_fmls.update(idx, dependent_expr(m, m.mk_true(), nullptr));
+                    change = true;
+                    ++m_num_flat;
+                    continue;
+                }
+            }
+        }
+    }
+};

src/ast/simplifiers/model_reconstruction_trail.cpp

@@ -151,8 +151,10 @@ std::ostream& model_reconstruction_trail::display(std::ostream& out) const {
             out << t->m_decl->get_name() << " <- " << mk_pp(t->m_def, m) << "\n";
         else {
             for (auto const& [v, def] : t->m_subst->sub())
-                out << mk_pp(v, m) << " <- " << mk_pp(def, m) << "\n";
+                out << mk_pp(v, m) << " <- " << mk_pp(def, m) << "\n";            
         }
+        for (auto const& d : t->m_removed)
+            out << "rm: " << d << "\n";
     }
     return out;
-}
+}

src/ast/simplifiers/push_ite.h

@@ -0,0 +1,66 @@
+
+/*++
+Copyright (c) 2022 Microsoft Corporation
+
+Module Name:
+
+    push_ite.h
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2022-11-24
+
+--*/
+
+#pragma once
+
+#include "ast/simplifiers/dependent_expr_state.h"
+#include "ast/rewriter/push_app_ite.h"
+
+
+class push_ite_simplifier : public dependent_expr_simplifier {
+    push_app_ite_rw m_push;
+
+public:
+    push_ite_simplifier(ast_manager& m, params_ref const& p, dependent_expr_state& fmls, bool c):
+        dependent_expr_simplifier(m, fmls),
+        m_push(m) {
+        m_push.set_conservative(c);
+    }
+
+    char const* name() const override { return "push-app-ite"; }
+
+    void reduce() override {
+        expr_ref r(m);
+        for (unsigned idx : indices()) {
+            auto const& d = m_fmls[idx];
+            m_push(d.fml(), r);
+            m_fmls.update(idx, dependent_expr(m, r, d.dep()));
+        }
+    }
+
+};
+
+
+class ng_push_ite_simplifier : public dependent_expr_simplifier {
+    ng_push_app_ite_rw m_push;
+
+public:
+    ng_push_ite_simplifier(ast_manager& m, params_ref const& p, dependent_expr_state& fmls, bool c):
+        dependent_expr_simplifier(m, fmls),
+        m_push(m) {
+        m_push.set_conservative(c);
+    }
+
+    char const* name() const override { return "ng-push-app-ite"; }
+
+    void reduce() override {
+        expr_ref r(m);
+        for (unsigned idx : indices()) {
+            auto const& d = m_fmls[idx];
+            m_push(d.fml(), r);
+            m_fmls.update(idx, dependent_expr(m, r, d.dep()));
+        }
+    }
+};
+

src/ast/simplifiers/seq_simplifier.h

@@ -64,7 +64,7 @@ class seq_simplifier : public dependent_expr_simplifier {
     }
 
     void reduce() override {
-        TRACE("simplifier", tout << m_fmls << "\n");
+        TRACE("simplifier", tout << m_fmls);
         for (auto* s : m_simplifiers) {
             if (m_fmls.inconsistent())
                 break;
@@ -74,7 +74,7 @@ class seq_simplifier : public dependent_expr_simplifier {
             collect_stats _cs(*s);
             s->reduce();
             m_fmls.flatten_suffix();
-            TRACE("simplifier", tout << s->name() << "\n" << m_fmls << "\n");
+            TRACE("simplifier", tout << s->name() << "\n" << m_fmls);
         }      
     }
 

src/math/simplex/model_based_opt.cpp

@@ -1014,12 +1014,14 @@ namespace opt {
         return dst;
     }
 
+    // -x + lo <= 0
     void model_based_opt::add_lower_bound(unsigned x, rational const& lo) {
         vector<var> coeffs;
         coeffs.push_back(var(x, rational::minus_one()));
         add_constraint(coeffs, lo, t_le);
     }
 
+    // x - hi <= 0
     void model_based_opt::add_upper_bound(unsigned x, rational const& hi) {
         vector<var> coeffs;
         coeffs.push_back(var(x, rational::one()));
@@ -1442,33 +1444,62 @@ namespace opt {
         for (unsigned ri : mod_rows) {
             rational a = get_coefficient(ri, x);
             replace_var(ri, x, rational::zero());
+            rational rMod = m_rows[ri].m_mod;
 
-            // add w = b mod K
+            // add w = b mod rMod
             vector<var> coeffs = m_rows[ri].m_vars;
             rational coeff = m_rows[ri].m_coeff;
             unsigned v = m_rows[ri].m_id;
             rational v_value = m_var2value[v];
 
             unsigned w = UINT_MAX;
             rational offset(0);
-            if (coeffs.empty() || K == 1)
-                offset = mod(coeff, K);
+            if (coeffs.empty() || rMod == 1)
+                offset = mod(coeff, rMod);
             else
-                w = add_mod(coeffs, coeff, K);
+                w = add_mod(coeffs, coeff, rMod);
 
 
             rational w_value = w == UINT_MAX ? offset : m_var2value[w];
 
-            // add v = a*z + w - V, for k = (a*z_value + w_value) div K
-            // claim: (= (mod x K) (- x (* K (div x K)))))) is a theorem for every x, K != 0
+#if 1
+            // V := (a * z_value - w_value) div rMod
+            // V*rMod <= a*z + w < (V+1)*rMod
+            // v = a*z + w - V*rMod
+            SASSERT(a * z_value - w_value >= 0);
+            rational V = div(a * z_value + w_value, rMod);
+            vector<var> mod_coeffs;
+            SASSERT(V >= 0);
+            SASSERT(a * z_value + w_value >= V*rMod);
+            SASSERT((V+1)*rMod > a*z_value + w_value);
+            // -a*z - w + V*rMod <= 0
+            mod_coeffs.push_back(var(z, -a));
+            if (w != UINT_MAX) mod_coeffs.push_back(var(w, -rational::one()));
+            add_constraint(mod_coeffs, V*rMod - offset, t_le);
+            mod_coeffs.reset();
+            // a*z + w - (V+1)*rMod + 1 <= 0
+            mod_coeffs.push_back(var(z, a));
+            if (w != UINT_MAX) mod_coeffs.push_back(var(w, rational::one()));
+            add_constraint(mod_coeffs, -(V+1)*rMod + offset + 1, t_le); 
+            mod_coeffs.reset();
+            // -v + a*z + w - V*rMod = 0
+            mod_coeffs.push_back(var(v, rational::minus_one()));
+            mod_coeffs.push_back(var(z, a));
+            if (w != UINT_MAX) mod_coeffs.push_back(var(w, rational::one()));
+            add_constraint(mod_coeffs, offset - V*rMod, t_eq);
+
+#else
+            // add v = a*z + w - V, for V = v_value - a * z_value - w_value
+            // claim: (= (mod x rMod) (- x (* rMod (div x rMod)))))) is a theorem for every x, rMod != 0
             rational V = v_value - a * z_value - w_value;
             vector<var> mod_coeffs;
             mod_coeffs.push_back(var(v, rational::minus_one()));
             mod_coeffs.push_back(var(z, a));
             if (w != UINT_MAX) mod_coeffs.push_back(var(w, rational::one()));
             add_constraint(mod_coeffs, V + offset, t_eq);
             add_lower_bound(v, rational::zero());
-            add_upper_bound(v, K - 1);
+            add_upper_bound(v, rMod - 1);
+#endif
 
             retire_row(ri);
             vs.push_back(v);