From cfc8e19baf676102214ed97c71bb721ddc930a34 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 1 Dec 2022 02:35:43 +0900 Subject: [PATCH] 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 | 21 +++- src/ast/simplifiers/elim_term_ite.h | 16 ++-- src/ast/simplifiers/elim_unconstrained.cpp | 20 ++-- src/ast/simplifiers/flatten_clauses.h | 95 +++++++++++++++++++ .../model_reconstruction_trail.cpp | 6 +- src/ast/simplifiers/push_ite.h | 66 +++++++++++++ src/ast/simplifiers/seq_simplifier.h | 4 +- src/math/simplex/model_based_opt.cpp | 45 +++++++-- src/sat/sat_solver/sat_smt_preprocess.cpp | 44 +++++---- src/tactic/smtlogics/smt_tactic.cpp | 8 +- 10 files changed, 271 insertions(+), 54 deletions(-) create mode 100644 src/ast/simplifiers/flatten_clauses.h create mode 100644 src/ast/simplifiers/push_ite.h diff --git a/examples/tptp/tptp5.cpp b/examples/tptp/tptp5.cpp index 4f1d25aa9ea..04b225caf90 100644 --- a/examples/tptp/tptp5.cpp +++ b/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(num_assumptions), + static_cast(asms.size()), assumptions, ctx.bool_val(true)); diff --git a/src/ast/simplifiers/elim_term_ite.h b/src/ast/simplifiers/elim_term_ite.h index e34b0b45753..6455db321e8 100644 --- a/src/ast/simplifiers/elim_term_ite.h +++ b/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); } }; diff --git a/src/ast/simplifiers/elim_unconstrained.cpp b/src/ast/simplifiers/elim_unconstrained.cpp index 9d40a5f2115..d9fe5d48003 100644 --- a/src/ast/simplifiers/elim_unconstrained.cpp +++ b/src/ast/simplifiers/elim_unconstrained.cpp @@ -249,32 +249,32 @@ void elim_unconstrained::assert_normalized(vector& old_fmls) { void elim_unconstrained::update_model_trail(generic_model_converter& mc, vector const& old_fmls) { auto& trail = m_fmls.model_trail(); - scoped_ptr rp = mk_default_expr_replacer(m, false); - scoped_ptr 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 rp = mk_default_expr_replacer(m, false); + scoped_ptr 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() { diff --git a/src/ast/simplifiers/flatten_clauses.h b/src/ast/simplifiers/flatten_clauses.h new file mode 100644 index 00000000000..02444f0930c --- /dev/null +++ b/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; + } + } + } + } +}; diff --git a/src/ast/simplifiers/model_reconstruction_trail.cpp b/src/ast/simplifiers/model_reconstruction_trail.cpp index 0436822d136..7e8d3e2f1c3 100644 --- a/src/ast/simplifiers/model_reconstruction_trail.cpp +++ b/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; -} \ No newline at end of file +} diff --git a/src/ast/simplifiers/push_ite.h b/src/ast/simplifiers/push_ite.h new file mode 100644 index 00000000000..e2acdbdb063 --- /dev/null +++ b/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())); + } + } +}; + diff --git a/src/ast/simplifiers/seq_simplifier.h b/src/ast/simplifiers/seq_simplifier.h index 0e93f62f924..a5ef91d7c8a 100644 --- a/src/ast/simplifiers/seq_simplifier.h +++ b/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); } } diff --git a/src/math/simplex/model_based_opt.cpp b/src/math/simplex/model_based_opt.cpp index 9e7ac75ce72..919e07b163b 100644 --- a/src/math/simplex/model_based_opt.cpp +++ b/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 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 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 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 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 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); diff --git a/src/sat/sat_solver/sat_smt_preprocess.cpp b/src/sat/sat_solver/sat_smt_preprocess.cpp index dfacf3fbaee..e3d6b3edba2 100644 --- a/src/sat/sat_solver/sat_smt_preprocess.cpp +++ b/src/sat/sat_solver/sat_smt_preprocess.cpp @@ -31,27 +31,15 @@ Module Name: #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)); diff --git a/src/tactic/smtlogics/smt_tactic.cpp b/src/tactic/smtlogics/smt_tactic.cpp index 0b78761ca8d..d47650c3460 100644 --- a/src/tactic/smtlogics/smt_tactic.cpp +++ b/src/tactic/smtlogics/smt_tactic.cpp @@ -18,10 +18,16 @@ Module Name: #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) {