add more simplifiers, fix model reconstruction order for elim_unconstrained

- 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,12 +2305,25 @@ 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, 
@@ -2318,7 +2331,7 @@ static void display_smt2(std::ostream& out) {
             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 @@ Author:
 #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 @@ public:
         }
     }
 
-    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,6 +249,16 @@ 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();
+
+    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:
+            break;
+        }
+    }
     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());
@@ -265,16 +275,6 @@ void elim_unconstrained::update_model_trail(generic_model_converter& mc, vector<
         }
     }
     trail.push(sub.detach(), old_fmls);
-
-    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:
-            break;
-        }
-    }
 }
 
 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 @@ public:
     }
         
     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 @@ public:
             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,8 +1444,9 @@ 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;
@@ -1451,16 +1454,43 @@ namespace opt {
 
             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()));
@@ -1468,7 +1498,8 @@ namespace opt {
             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);

src/sat/sat_solver/sat_smt_preprocess.cpp

@@ -31,27 +31,15 @@ Author:
 #include "ast/simplifiers/elim_bounds.h"
 #include "ast/simplifiers/bit2int.h"
 #include "ast/simplifiers/bv_elim.h"
+#include "ast/simplifiers/push_ite.h"
+#include "ast/simplifiers/elim_term_ite.h"
+#include "ast/simplifiers/flatten_clauses.h"
 #include "sat/sat_params.hpp"
 #include "smt/params/smt_params.h"
 #include "sat/sat_solver/sat_smt_preprocess.h"
 #include "qe/lite/qe_lite.h"
 
 void init_preprocess(ast_manager& m, params_ref const& p, seq_simplifier& s, dependent_expr_state& st) {
-    params_ref simp1_p = p;
-    simp1_p.set_bool("som", true);
-    simp1_p.set_bool("pull_cheap_ite", true);
-    simp1_p.set_bool("push_ite_bv", false);
-    simp1_p.set_bool("local_ctx", true);
-    simp1_p.set_uint("local_ctx_limit", 10000000);
-    simp1_p.set_bool("flat", true); // required by som
-    simp1_p.set_bool("hoist_mul", false); // required by som
-    simp1_p.set_bool("elim_and", true);
-    simp1_p.set_bool("blast_distinct", true);
-    simp1_p.set_bool("flat_and_or", false);
-    
-    params_ref simp2_p = p;
-    simp2_p.set_bool("flat", false);
-    simp2_p.set_bool("flat_and_or", false);
     
     sat_params sp(p);
     smt_params smtp(p);
@@ -70,6 +58,10 @@ void init_preprocess(ast_manager& m, params_ref const& p, seq_simplifier& s, dep
         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));
+        if (smtp.m_eliminate_term_ite && smtp.m_lift_ite != lift_ite_kind::LI_FULL) s.add_simplifier(alloc(elim_term_ite_simplifier, m, p, st));        
+        if (smtp.m_lift_ite != lift_ite_kind::LI_NONE) s.add_simplifier(alloc(push_ite_simplifier, m, p, st, smtp.m_lift_ite == lift_ite_kind::LI_CONSERVATIVE));
+        if (smtp.m_ng_lift_ite != lift_ite_kind::LI_NONE) s.add_simplifier(alloc(ng_push_ite_simplifier, m, p, st, smtp.m_ng_lift_ite == lift_ite_kind::LI_CONSERVATIVE));
+        s.add_simplifier(alloc(flatten_clauses, m, p, st));
         //
         // add: 
         // euf_completion?
@@ -77,17 +69,27 @@ void init_preprocess(ast_manager& m, params_ref const& p, seq_simplifier& s, dep
         // add: make it externally programmable
         // 
 #if 0
-    ?? if (!invoke(m_lift_ite)) return;
-    m_lift_ite.m_functor.set_conservative(m_smt_params.m_lift_ite == lift_ite_kind::LI_CONSERVATIVE);
-    m_ng_lift_ite.m_functor.set_conservative(m_smt_params.m_ng_lift_ite == lift_ite_kind::LI_CONSERVATIVE);
-    ?? if (!invoke(m_ng_lift_ite)) return;
-    if (!invoke(m_elim_term_ite)) return;
     if (!invoke(m_apply_quasi_macros)) return;
-    if (!invoke(m_flatten_clauses)) return;
 #endif
 
     }
     else {
+        params_ref simp1_p = p;
+        simp1_p.set_bool("som", true);
+        simp1_p.set_bool("pull_cheap_ite", true);
+        simp1_p.set_bool("push_ite_bv", false);
+        simp1_p.set_bool("local_ctx", true);
+        simp1_p.set_uint("local_ctx_limit", 10000000);
+        simp1_p.set_bool("flat", true); // required by som
+        simp1_p.set_bool("hoist_mul", false); // required by som
+        simp1_p.set_bool("elim_and", true);
+        simp1_p.set_bool("blast_distinct", true);
+        simp1_p.set_bool("flat_and_or", false);
+
+        params_ref simp2_p = p;
+        simp2_p.set_bool("flat", false);
+        simp2_p.set_bool("flat_and_or", false);
+
         s.add_simplifier(alloc(rewriter_simplifier, m, p, st));
         s.add_simplifier(alloc(propagate_values, m, p, st));
         s.add_simplifier(alloc(card2bv, m, p, st));

src/tactic/smtlogics/smt_tactic.cpp

@@ -18,10 +18,16 @@ Author:
 #include "smt/tactic/smt_tactic_core.h"
 #include "sat/tactic/sat_tactic.h"
 #include "sat/sat_params.hpp"
+#include "solver/solver2tactic.h"
+#include "solver/solver.h"
 
 tactic * mk_smt_tactic(ast_manager & m, params_ref const & p) {
     sat_params sp(p);
-    return sp.euf() ? mk_sat_tactic(m, p) : mk_smt_tactic_core(m, p);
+        if (sp.smt())
+        return mk_solver2tactic(mk_smt2_solver(m, p));
+    if (sp.euf())
+        return mk_sat_tactic(m, p);
+    return mk_smt_tactic_core(m, p);
 }
 
 tactic * mk_smt_tactic_using(ast_manager& m, bool auto_config, params_ref const& p) {