From dd1ca8f6bd1e2bc8dada167eb0056cfd4abc3dd1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 29 Nov 2022 16:36:02 +0700 Subject: [PATCH] move qhead to attribute on the state instead of the simplifier, - add sat.smt option to enable the new incremental core (it is not ready for mainstream consumption as cloning and other features are not implemented and it hasn't been tested in any detail yet). - move "name" into attribute on simplifier so it can be reused for diagnostics by the seq-simplifier. --- src/ast/simplifiers/bit_blaster.cpp | 4 +-- src/ast/simplifiers/bit_blaster.h | 2 +- src/ast/simplifiers/bv_slice.cpp | 5 ++- src/ast/simplifiers/bv_slice.h | 2 +- src/ast/simplifiers/card2bv.cpp | 4 +-- src/ast/simplifiers/card2bv.h | 1 + src/ast/simplifiers/dependent_expr_state.h | 18 +++++++--- src/ast/simplifiers/elim_unconstrained.cpp | 7 ++-- src/ast/simplifiers/elim_unconstrained.h | 2 ++ src/ast/simplifiers/eliminate_predicates.cpp | 6 ++-- src/ast/simplifiers/eliminate_predicates.h | 2 ++ src/ast/simplifiers/euf_completion.cpp | 6 ++-- src/ast/simplifiers/euf_completion.h | 1 + src/ast/simplifiers/max_bv_sharing.cpp | 5 +-- src/ast/simplifiers/propagate_values.cpp | 7 ++-- src/ast/simplifiers/propagate_values.h | 1 + src/ast/simplifiers/rewriter_simplifier.h | 5 +-- src/ast/simplifiers/seq_simplifier.h | 36 +++++++++++++++++-- src/ast/simplifiers/solve_context_eqs.cpp | 2 +- src/ast/simplifiers/solve_eqs.cpp | 6 ++-- src/ast/simplifiers/solve_eqs.h | 2 ++ src/sat/sat_params.pyg | 9 ++--- src/sat/sat_solver/sat_smt_preprocess.cpp | 2 +- src/sat/sat_solver/sat_smt_solver.cpp | 30 ++++++++-------- src/sat/smt/q_mbi.cpp | 2 +- src/sat/tactic/goal2sat.cpp | 2 +- src/solver/solver.h | 2 +- src/tactic/arith/card2bv_tactic.h | 2 +- src/tactic/bv/bv_slice_tactic.cpp | 2 +- src/tactic/bv/max_bv_sharing_tactic.h | 2 +- src/tactic/core/elim_uncnstr2_tactic.h | 2 +- src/tactic/core/eliminate_predicates_tactic.h | 4 +-- src/tactic/core/euf_completion_tactic.cpp | 2 +- src/tactic/core/propagate_values2_tactic.h | 2 +- src/tactic/core/solve_eqs_tactic.h | 2 +- src/tactic/dependent_expr_state_tactic.h | 12 +++---- src/tactic/portfolio/smt_strategic_solver.cpp | 16 ++++++--- 37 files changed, 132 insertions(+), 85 deletions(-) diff --git a/src/ast/simplifiers/bit_blaster.cpp b/src/ast/simplifiers/bit_blaster.cpp index 218765d283b..dc086c62843 100644 --- a/src/ast/simplifiers/bit_blaster.cpp +++ b/src/ast/simplifiers/bit_blaster.cpp @@ -37,7 +37,7 @@ void bit_blaster::reduce() { expr_ref new_curr(m); proof_ref new_pr(m); bool change = false; - for (unsigned idx = m_qhead; idx < m_fmls.size(); idx++) { + for (unsigned idx = m_fmls.qhead(); idx < m_fmls.size(); idx++) { if (m_fmls.inconsistent()) break; auto [curr, d] = m_fmls[idx](); @@ -60,8 +60,6 @@ void bit_blaster::reduce() { m_fmls.model_trail().push(f, v, nullptr, {}); } m_rewriter.cleanup(); - - advance_qhead(); } diff --git a/src/ast/simplifiers/bit_blaster.h b/src/ast/simplifiers/bit_blaster.h index 70446918b4e..231a1ca68ed 100644 --- a/src/ast/simplifiers/bit_blaster.h +++ b/src/ast/simplifiers/bit_blaster.h @@ -33,7 +33,7 @@ class bit_blaster : public dependent_expr_simplifier { m_rewriter(m, p) { updt_params(p); } - + char const* name() const override { return "bit-blaster"; } void updt_params(params_ref const & p) override; void collect_param_descrs(param_descrs & r) override; void reduce() override; diff --git a/src/ast/simplifiers/bv_slice.cpp b/src/ast/simplifiers/bv_slice.cpp index 995231b3475..14d6edb99f0 100644 --- a/src/ast/simplifiers/bv_slice.cpp +++ b/src/ast/simplifiers/bv_slice.cpp @@ -24,11 +24,10 @@ namespace bv { void slice::reduce() { process_eqs(); apply_subst(); - advance_qhead(); } void slice::process_eqs() { - for (unsigned i = m_qhead; i < m_fmls.size(); ++i) { + for (unsigned i = m_fmls.qhead(); i < m_fmls.size(); ++i) { auto const [f, d] = m_fmls[i](); process_eq(f); } @@ -137,7 +136,7 @@ namespace bv { expr_ref_vector cache(m), pin(m); ptr_vector todo, args; expr* c; - for (unsigned i = m_qhead; i < m_fmls.size(); ++i) { + for (unsigned i = m_fmls.qhead(); i < m_fmls.size(); ++i) { auto const [f, d] = m_fmls[i](); todo.push_back(f); pin.push_back(f); diff --git a/src/ast/simplifiers/bv_slice.h b/src/ast/simplifiers/bv_slice.h index cc0f48cfcc6..3bf514ac394 100644 --- a/src/ast/simplifiers/bv_slice.h +++ b/src/ast/simplifiers/bv_slice.h @@ -47,7 +47,7 @@ namespace bv { public: slice(ast_manager& m, dependent_expr_state& fmls) : dependent_expr_simplifier(m, fmls), m_bv(m), m_rewriter(m) {} - + char const* name() const override { return "bv-slice"; } void push() override { dependent_expr_simplifier::push(); } void pop(unsigned n) override { dependent_expr_simplifier::pop(n); } void reduce() override; diff --git a/src/ast/simplifiers/card2bv.cpp b/src/ast/simplifiers/card2bv.cpp index 44bc8e589e8..3feb8647410 100644 --- a/src/ast/simplifiers/card2bv.cpp +++ b/src/ast/simplifiers/card2bv.cpp @@ -29,7 +29,7 @@ void card2bv::reduce() { expr_ref new_f1(m), new_f2(m); proof_ref new_pr(m); - for (unsigned idx = m_qhead; !m_fmls.inconsistent() && idx < m_fmls.size(); idx++) { + for (unsigned idx = m_fmls.qhead(); !m_fmls.inconsistent() && idx < m_fmls.size(); idx++) { auto [f, d] = m_fmls[idx](); rw1(f, new_f1); rw2(false, new_f1, new_f2, new_pr); @@ -48,8 +48,6 @@ void card2bv::reduce() { func_decl_ref_vector const& fns = rw2.fresh_constants(); for (func_decl* f : fns) m_fmls.model_trail().hide(f); - - advance_qhead(); } void card2bv::collect_statistics(statistics& st) const { diff --git a/src/ast/simplifiers/card2bv.h b/src/ast/simplifiers/card2bv.h index e089fa84c87..4c081c8cdf8 100644 --- a/src/ast/simplifiers/card2bv.h +++ b/src/ast/simplifiers/card2bv.h @@ -34,6 +34,7 @@ class card2bv : public dependent_expr_simplifier { public: card2bv(ast_manager& m, params_ref const& p, dependent_expr_state& fmls); + char const* name() const override { return "card2bv"; } void reduce() override; void collect_statistics(statistics& st) const override; void reset_statistics() override { m_stats.reset(); } diff --git a/src/ast/simplifiers/dependent_expr_state.h b/src/ast/simplifiers/dependent_expr_state.h index 90b95ab7d06..54ee5626b99 100644 --- a/src/ast/simplifiers/dependent_expr_state.h +++ b/src/ast/simplifiers/dependent_expr_state.h @@ -41,6 +41,7 @@ Module Name: abstract interface to state updated by simplifiers. */ class dependent_expr_state { + unsigned m_qhead = 0; public: virtual ~dependent_expr_state() {} virtual unsigned size() const = 0; @@ -53,8 +54,15 @@ class dependent_expr_state { trail_stack m_trail; void push() { m_trail.push_scope(); } void pop(unsigned n) { m_trail.pop_scope(n); } - - + unsigned qhead() const { return m_qhead; } + void advance_qhead() { m_qhead = size(); } + unsigned num_exprs() { + expr_fast_mark1 visited; + unsigned r = 0; + for (unsigned i = 0; i < size(); i++) + r += get_num_exprs((*this)[i].fml(), visited); + return r; + } }; /** @@ -65,14 +73,13 @@ class dependent_expr_simplifier { ast_manager& m; dependent_expr_state& m_fmls; trail_stack& m_trail; - unsigned m_qhead = 0; // pointer into last processed formula in m_fmls unsigned num_scopes() const { return m_trail.get_num_scopes(); } - void advance_qhead() { if (num_scopes() > 0) m_trail.push(value_trail(m_qhead)); m_qhead = m_fmls.size(); } 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() {} + virtual char const* name() const = 0; virtual void push() { } virtual void pop(unsigned n) { } virtual void reduce() = 0; @@ -80,7 +87,8 @@ class dependent_expr_simplifier { virtual void reset_statistics() {} virtual void updt_params(params_ref const& p) {} virtual void collect_param_descrs(param_descrs& r) {} - unsigned qhead() const { return m_qhead; } + ast_manager& get_manager() { return m; } + dependent_expr_state& get_fmls() { return m_fmls; } }; /** diff --git a/src/ast/simplifiers/elim_unconstrained.cpp b/src/ast/simplifiers/elim_unconstrained.cpp index ac5cc339d65..93a84dba644 100644 --- a/src/ast/simplifiers/elim_unconstrained.cpp +++ b/src/ast/simplifiers/elim_unconstrained.cpp @@ -138,7 +138,7 @@ void elim_unconstrained::init_nodes() { // freeze subterms before the already processed head terms.reset(); - for (unsigned i = 0; i < m_qhead; ++i) + for (unsigned i = 0; i < m_fmls.qhead(); ++i) terms.push_back(m_fmls[i].fml()); for (expr* e : subterms::all(terms)) m_frozen.mark(e, true); @@ -216,7 +216,7 @@ void elim_unconstrained::gc(expr* t) { */ void elim_unconstrained::reconstruct_terms() { expr_ref_vector terms(m); - for (unsigned i = m_qhead; i < m_fmls.size(); ++i) + for (unsigned i = m_fmls.qhead(); i < m_fmls.size(); ++i) terms.push_back(m_fmls[i].fml()); for (expr* e : subterms_postorder::all(terms)) { @@ -250,7 +250,7 @@ void elim_unconstrained::reconstruct_terms() { void elim_unconstrained::assert_normalized(vector& old_fmls) { unsigned sz = m_fmls.size(); - for (unsigned i = m_qhead; i < sz; ++i) { + for (unsigned i = m_fmls.qhead(); i < sz; ++i) { auto [f, d] = m_fmls[i](); node& n = get_node(f); expr* g = n.m_term; @@ -302,5 +302,4 @@ void elim_unconstrained::reduce() { vector old_fmls; assert_normalized(old_fmls); update_model_trail(*mc, old_fmls); - advance_qhead(); } diff --git a/src/ast/simplifiers/elim_unconstrained.h b/src/ast/simplifiers/elim_unconstrained.h index 89f28fe33e2..b66d0b72748 100644 --- a/src/ast/simplifiers/elim_unconstrained.h +++ b/src/ast/simplifiers/elim_unconstrained.h @@ -71,6 +71,8 @@ class elim_unconstrained : public dependent_expr_simplifier { elim_unconstrained(ast_manager& m, dependent_expr_state& fmls); + char const* name() const override { return "elim-unconstrained"; } + void reduce() override; void collect_statistics(statistics& st) const override { st.update("elim-unconstrained", m_stats.m_num_eliminated); } diff --git a/src/ast/simplifiers/eliminate_predicates.cpp b/src/ast/simplifiers/eliminate_predicates.cpp index 6d1288c5d70..fa615048f5b 100644 --- a/src/ast/simplifiers/eliminate_predicates.cpp +++ b/src/ast/simplifiers/eliminate_predicates.cpp @@ -501,7 +501,7 @@ void eliminate_predicates::reduce_definitions() { for (auto const& [k, v] : m_macros) macro_expander.insert(v->m_head, v->m_def, v->m_dep); - for (unsigned i = m_qhead; i < m_fmls.size(); ++i) { + for (unsigned i = m_fmls.qhead(); i < m_fmls.size(); ++i) { auto [f, d] = m_fmls[i](); expr_ref fml(f, m), new_fml(m); expr_dependency_ref dep(m); @@ -779,7 +779,7 @@ eliminate_predicates::clause* eliminate_predicates::init_clause(expr* f, expr_de * eliminations. */ void eliminate_predicates::init_clauses() { - for (unsigned i = 0; i < m_qhead; ++i) + for (unsigned i = 0; i < m_fmls.qhead(); ++i) m_to_exclude.push_back(m_fmls[i].fml()); recfun::util rec(m); if (rec.has_rec_defs()) @@ -788,7 +788,7 @@ void eliminate_predicates::init_clauses() { process_to_exclude(m_disable_macro); - for (unsigned i = m_qhead; i < m_fmls.size(); ++i) { + for (unsigned i = m_fmls.qhead(); i < m_fmls.size(); ++i) { clause* cl = init_clause(i); add_use_list(*cl); m_clauses.push_back(cl); diff --git a/src/ast/simplifiers/eliminate_predicates.h b/src/ast/simplifiers/eliminate_predicates.h index 6afd0886a8c..ca4110e99f2 100644 --- a/src/ast/simplifiers/eliminate_predicates.h +++ b/src/ast/simplifiers/eliminate_predicates.h @@ -129,6 +129,8 @@ class eliminate_predicates : public dependent_expr_simplifier { eliminate_predicates(ast_manager& m, dependent_expr_state& fmls); ~eliminate_predicates() override { reset(); } + + char const* name() const override { return "elim-predicates"; } void reduce() override; diff --git a/src/ast/simplifiers/euf_completion.cpp b/src/ast/simplifiers/euf_completion.cpp index 5056d818c2c..f077f19182d 100644 --- a/src/ast/simplifiers/euf_completion.cpp +++ b/src/ast/simplifiers/euf_completion.cpp @@ -80,7 +80,7 @@ namespace euf { m_nodes_to_canonize.push_back(ch); }; - for (unsigned i = m_qhead; i < sz; ++i) { + for (unsigned i = m_fmls.qhead(); i < sz; ++i) { expr* x, * y; auto [f, d] = m_fmls[i](); if (m.is_eq(f, x, y)) { @@ -114,7 +114,7 @@ namespace euf { } unsigned sz = m_fmls.size(); - for (unsigned i = m_qhead; i < sz; ++i) { + for (unsigned i = m_fmls.qhead(); i < sz; ++i) { auto [f, d] = m_fmls[i](); expr_dependency_ref dep(d, m); @@ -127,8 +127,6 @@ namespace euf { } CTRACE("euf_completion", g != f, tout << mk_bounded_pp(f, m) << " -> " << mk_bounded_pp(g, m) << "\n"); } - if (!m_has_new_eq) - advance_qhead(); } bool completion::is_new_eq(expr* a, expr* b) { diff --git a/src/ast/simplifiers/euf_completion.h b/src/ast/simplifiers/euf_completion.h index f02e3324569..da0fb7276f7 100644 --- a/src/ast/simplifiers/euf_completion.h +++ b/src/ast/simplifiers/euf_completion.h @@ -58,6 +58,7 @@ namespace euf { expr_dependency* explain_conflict(); public: completion(ast_manager& m, dependent_expr_state& fmls); + char const* name() const override { return "euf-reduce"; } void push() override { m_egraph.push(); dependent_expr_simplifier::push(); } void pop(unsigned n) override { dependent_expr_simplifier::pop(n); m_egraph.pop(n); } void reduce() override; diff --git a/src/ast/simplifiers/max_bv_sharing.cpp b/src/ast/simplifiers/max_bv_sharing.cpp index 3003a47a020..4744c473c5d 100644 --- a/src/ast/simplifiers/max_bv_sharing.cpp +++ b/src/ast/simplifiers/max_bv_sharing.cpp @@ -250,10 +250,12 @@ class max_bv_sharing : public dependent_expr_simplifier { "(default: 128) maximum number of arguments (per application) that will be considered by the greedy (quadratic) heuristic."); } + char const* name() const override { return "max-bv-sharing"; } + void reduce() override { expr_ref new_curr(m); proof_ref new_pr(m); - for (unsigned idx = m_qhead; idx < m_fmls.size() && !m_fmls.inconsistent(); idx++) { + for (unsigned idx = m_fmls.qhead(); idx < m_fmls.size() && !m_fmls.inconsistent(); idx++) { auto [curr, d] = m_fmls[idx](); m_rw(curr, new_curr, new_pr); // Proof reconstruction: new_pr = m.mk_modus_ponens(old_pr, new_pr); @@ -261,7 +263,6 @@ class max_bv_sharing : public dependent_expr_simplifier { m_fmls.update(idx, dependent_expr(m, new_curr, d)); } m_rw.cfg().cleanup(); - advance_qhead(); } }; diff --git a/src/ast/simplifiers/propagate_values.cpp b/src/ast/simplifiers/propagate_values.cpp index 6d6bc976f14..2572cc31002 100644 --- a/src/ast/simplifiers/propagate_values.cpp +++ b/src/ast/simplifiers/propagate_values.cpp @@ -78,7 +78,7 @@ void propagate_values::reduce() { subst.reset(); m_rewriter.reset(); m_rewriter.set_substitution(&subst); - for (unsigned i = 0; i < m_qhead; ++i) + for (unsigned i = 0; i < m_fmls.qhead(); ++i) add_sub(m_fmls[i]); }; @@ -86,10 +86,10 @@ void propagate_values::reduce() { for (unsigned r = 0; r < m_max_rounds && rw != m_stats.m_num_rewrites; ++r) { rw = m_stats.m_num_rewrites; init_sub(); - for (unsigned i = m_qhead; i < m_fmls.size() && !m_fmls.inconsistent(); ++i) + for (unsigned i = m_fmls.qhead(); i < m_fmls.size() && !m_fmls.inconsistent(); ++i) process_fml(i); init_sub(); - for (unsigned i = m_fmls.size(); i-- > m_qhead && !m_fmls.inconsistent();) + for (unsigned i = m_fmls.size(); i-- > m_fmls.qhead() && !m_fmls.inconsistent();) process_fml(i); if (subst.empty()) break; @@ -97,7 +97,6 @@ void propagate_values::reduce() { m_rewriter.set_substitution(nullptr); m_rewriter.reset(); - advance_qhead(); } void propagate_values::collect_statistics(statistics& st) const { diff --git a/src/ast/simplifiers/propagate_values.h b/src/ast/simplifiers/propagate_values.h index d263377b112..9ad59d1b34d 100644 --- a/src/ast/simplifiers/propagate_values.h +++ b/src/ast/simplifiers/propagate_values.h @@ -37,6 +37,7 @@ class propagate_values : public dependent_expr_simplifier { public: propagate_values(ast_manager& m, params_ref const& p, dependent_expr_state& fmls); + char const* name() const override { return "propagate-values2"; } void reduce() override; void collect_statistics(statistics& st) const override; void reset_statistics() override { m_stats.reset(); } diff --git a/src/ast/simplifiers/rewriter_simplifier.h b/src/ast/simplifiers/rewriter_simplifier.h index 23ebb4f84b4..f956ec80828 100644 --- a/src/ast/simplifiers/rewriter_simplifier.h +++ b/src/ast/simplifiers/rewriter_simplifier.h @@ -33,12 +33,14 @@ class rewriter_simplifier : public dependent_expr_simplifier { m_rewriter(m) { updt_params(p); } + + char const* name() const override { return "simplifier"; } void reduce() override { m_num_steps = 0; expr_ref new_curr(m); proof_ref new_pr(m); - for (unsigned idx = m_qhead; idx < m_fmls.size(); idx++) { + for (unsigned idx = m_fmls.qhead(); idx < m_fmls.size(); idx++) { if (m_fmls.inconsistent()) break; auto d = m_fmls[idx]; @@ -46,7 +48,6 @@ class rewriter_simplifier : public dependent_expr_simplifier { m_num_steps += m_rewriter.get_num_steps(); m_fmls.update(idx, dependent_expr(m, new_curr, d.dep())); } - advance_qhead(); } void collect_statistics(statistics& st) const override { st.update("simplifier", m_num_steps); } void reset_statistics() override { m_num_steps = 0; } diff --git a/src/ast/simplifiers/seq_simplifier.h b/src/ast/simplifiers/seq_simplifier.h index 0d5483b71aa..0fa5990ddc4 100644 --- a/src/ast/simplifiers/seq_simplifier.h +++ b/src/ast/simplifiers/seq_simplifier.h @@ -17,16 +17,46 @@ Module Name: #pragma once +#include "util/stopwatch.h" #include "ast/simplifiers/dependent_expr_state.h" class seq_simplifier : public dependent_expr_simplifier { scoped_ptr_vector m_simplifiers; + struct collect_stats { + stopwatch m_watch; + double m_start_memory = 0; + dependent_expr_simplifier& s; + collect_stats(dependent_expr_simplifier& s) : + m_start_memory(static_cast(memory::get_allocation_size()) / static_cast(1024 * 1024)), + s(s) { + m_watch.start(); + } + ~collect_stats() { + m_watch.stop(); + double end_memory = static_cast(memory::get_allocation_size()) / static_cast(1024 * 1024); + IF_VERBOSE(10, + statistics st; + verbose_stream() << "(" << s.name() + << " :num-exprs " << s.get_fmls().num_exprs() + << " :num-asts " << s.get_manager().get_num_asts() + << " :time " << std::fixed << std::setprecision(2) << m_watch.get_seconds() + << " :before-memory " << std::fixed << std::setprecision(2) << m_start_memory + << " :after-memory " << std::fixed << std::setprecision(2) << end_memory + << ")" << "\n"; + s.collect_statistics(st); + verbose_stream() << st); + } + }; + public: + seq_simplifier(ast_manager& m, params_ref const& p, dependent_expr_state& fmls): dependent_expr_simplifier(m, fmls) { } + + char const* name() const override { return "and-then"; } void add_simplifier(dependent_expr_simplifier* s) { m_simplifiers.push_back(s); @@ -36,9 +66,11 @@ class seq_simplifier : public dependent_expr_simplifier { for (auto* s : m_simplifiers) { if (m_fmls.inconsistent()) break; + if (!m.inc()) + break; + collect_stats _cs(*s); s->reduce(); - } - advance_qhead(); + } } void collect_statistics(statistics& st) const override { diff --git a/src/ast/simplifiers/solve_context_eqs.cpp b/src/ast/simplifiers/solve_context_eqs.cpp index ef52d009c52..7eaa8ad2fc9 100644 --- a/src/ast/simplifiers/solve_context_eqs.cpp +++ b/src/ast/simplifiers/solve_context_eqs.cpp @@ -148,7 +148,7 @@ namespace euf { void solve_context_eqs::collect_nested_equalities(dep_eq_vector& eqs) { expr_mark visited; unsigned sz = m_fmls.size(); - for (unsigned i = m_solve_eqs.m_qhead; i < sz; ++i) + for (unsigned i = m_fmls.qhead(); i < sz; ++i) collect_nested_equalities(m_fmls[i], visited, eqs); if (eqs.empty()) diff --git a/src/ast/simplifiers/solve_eqs.cpp b/src/ast/simplifiers/solve_eqs.cpp index 1bea283ac9e..f6055af50bb 100644 --- a/src/ast/simplifiers/solve_eqs.cpp +++ b/src/ast/simplifiers/solve_eqs.cpp @@ -34,7 +34,7 @@ namespace euf { void solve_eqs::get_eqs(dep_eq_vector& eqs) { for (extract_eq* ex : m_extract_plugins) - for (unsigned i = m_qhead; i < m_fmls.size(); ++i) + for (unsigned i = m_fmls.qhead(); i < m_fmls.size(); ++i) ex->get_eqs(m_fmls[i], eqs); } @@ -187,7 +187,7 @@ namespace euf { scoped_ptr rp = mk_default_expr_replacer(m, false); rp->set_substitution(m_subst.get()); - for (unsigned i = m_qhead; i < m_fmls.size() && !m_fmls.inconsistent(); ++i) { + for (unsigned i = m_fmls.qhead(); i < m_fmls.size() && !m_fmls.inconsistent(); ++i) { auto [f, d] = m_fmls[i](); auto [new_f, new_dep] = rp->replace_with_dep(f); m_rewriter(new_f); @@ -236,8 +236,6 @@ namespace euf { apply_subst(old_fmls); save_subst(old_fmls); } - - advance_qhead(); } void solve_eqs::save_subst(vector const& old_fmls) { diff --git a/src/ast/simplifiers/solve_eqs.h b/src/ast/simplifiers/solve_eqs.h index a2afd6e5892..4b2905b2a1c 100644 --- a/src/ast/simplifiers/solve_eqs.h +++ b/src/ast/simplifiers/solve_eqs.h @@ -68,6 +68,8 @@ namespace euf { solve_eqs(ast_manager& m, dependent_expr_state& fmls); + char const* name() const override { return "solve-eqs"; } + void reduce() override; void updt_params(params_ref const& p) override; diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg index 20a41544195..f9d7c643ac6 100644 --- a/src/sat/sat_params.pyg +++ b/src/sat/sat_params.pyg @@ -47,6 +47,7 @@ def_module_params('sat', ('threads', UINT, 1, 'number of parallel threads to use'), ('dimacs.core', BOOL, False, 'extract core from DIMACS benchmarks'), ('drat.disable', BOOL, False, 'override anything that enables DRAT'), + ('smt', BOOL, False, 'use the SAT solver based incremental SMT core'), ('smt.proof.check', BOOL, False, 'check SMT proof while it is created'), ('smt.proof.check_rup', BOOL, True, 'apply forward RUP proof checking'), ('drat.file', SYMBOL, '', 'file to dump DRAT proofs'), @@ -73,11 +74,11 @@ def_module_params('sat', ('local_search_mode', SYMBOL, 'wsat', 'local search algorithm, either default wsat or qsat'), ('local_search_dbg_flips', BOOL, False, 'write debug information for number of flips'), ('binspr', BOOL, False, 'enable SPR inferences of binary propagation redundant clauses. This inprocessing step eliminates models'), - ('anf', BOOL, False, 'enable ANF based simplification in-processing'), - ('anf.delay', UINT, 2, 'delay ANF simplification by in-processing round'), + ('anf', BOOL, False, 'enable ANF based simplification in-processing'), + ('anf.delay', UINT, 2, 'delay ANF simplification by in-processing round'), ('anf.exlin', BOOL, False, 'enable extended linear simplification'), - ('cut', BOOL, False, 'enable AIG based simplification in-processing'), - ('cut.delay', UINT, 2, 'delay cut simplification by in-processing round'), + ('cut', BOOL, False, 'enable AIG based simplification in-processing'), + ('cut.delay', UINT, 2, 'delay cut simplification by in-processing round'), ('cut.aig', BOOL, False, 'extract aigs (and ites) from cluases for cut simplification'), ('cut.lut', BOOL, False, 'extract luts from clauses for cut simplification'), ('cut.xor', BOOL, False, 'extract xors from clauses for cut simplification'), diff --git a/src/sat/sat_solver/sat_smt_preprocess.cpp b/src/sat/sat_solver/sat_smt_preprocess.cpp index 72c7c52323c..f05fc098ff6 100644 --- a/src/sat/sat_solver/sat_smt_preprocess.cpp +++ b/src/sat/sat_solver/sat_smt_preprocess.cpp @@ -44,7 +44,7 @@ void init_preprocess(ast_manager& m, params_ref const& p, seq_simplifier& s, dep simp2_p.set_bool("flat_and_or", false); sat_params sp(p); - if (sp.euf()) { + if (sp.euf() || sp.smt()) { s.add_simplifier(alloc(rewriter_simplifier, m, p, st)); s.add_simplifier(alloc(propagate_values, m, p, st)); // diff --git a/src/sat/sat_solver/sat_smt_solver.cpp b/src/sat/sat_solver/sat_smt_solver.cpp index 3ea0543ec49..2d95dab6922 100644 --- a/src/sat/sat_solver/sat_smt_solver.cpp +++ b/src/sat/sat_solver/sat_smt_solver.cpp @@ -130,7 +130,7 @@ class sat_smt_solver : public solver { trail_stack& m_trail; dependency2assumptions m_dep; goal2sat m_goal2sat; - expr_ref_vector m_assumptions, m_core, m_ors, m_aux_fmls; + expr_ref_vector m_assumptions, m_core, m_ors, m_aux_fmls, m_internalized_fmls; atom2bool_var m_map; generic_model_converter_ref m_mc; unsigned m_mc_size = 0; @@ -140,9 +140,8 @@ class sat_smt_solver : public solver { // access formulas after they have been pre-processed and handled by the sat solver. // this allows to access the internal state of the SAT solver and carry on partial results. bool m_internalized_converted = false; // have internalized formulas been converted back - expr_ref_vector m_internalized_fmls; // formulas in internalized format - bool is_internalized() const { return m_preprocess.qhead() == m_fmls.size(); } + bool is_internalized() const { return m_preprocess_state.qhead() == m_fmls.size(); } public: sat_smt_solver(ast_manager& m, params_ref const& p): @@ -152,16 +151,12 @@ class sat_smt_solver : public solver { m_trail(m_preprocess_state.m_trail), m_dep(m, m_trail), m_solver(p, m.limit()), - m_assumptions(m), - m_core(m), - m_ors(m), - m_aux_fmls(m), + m_assumptions(m), m_core(m), m_ors(m), m_aux_fmls(m), m_internalized_fmls(m), m_map(m), - m_internalized_fmls(m) { + m_mc(alloc(generic_model_converter, m, "sat-smt-solver")) { updt_params(p); init_preprocess(); m_solver.set_incremental(true); - m_mc = alloc(generic_model_converter, m, "sat-smt-solver"); } solver* translate(ast_manager& dst_m, params_ref const& p) override { @@ -214,7 +209,7 @@ class sat_smt_solver : public solver { expr_ref_vector assumptions(m); for (unsigned i = 0; i < sz; ++i) assumptions.push_back(ensure_literal(_assumptions[i])); - TRACE("sat", tout << _assumptions << "\n";); + TRACE("sat", tout << assumptions << "\n";); lbool r = internalize_formulas(); if (r != l_true) return r; @@ -267,8 +262,7 @@ class sat_smt_solver : public solver { } void pop(unsigned n) override { - if (n > m_trail.get_num_scopes()) // allow inc_sat_solver to - n = m_trail.get_num_scopes(); // take over for another solver. + n = std::min(n, m_trail.get_num_scopes()); // allow sat_smt_solver to take over for another solver. m_preprocess.pop(n); m_preprocess_state.pop(n); @@ -357,7 +351,7 @@ class sat_smt_solver : public solver { m_solver.updt_params(m_params); m_solver.set_incremental(true); m_preprocess.updt_params(m_params); - if (sp.euf()) + if (sp.smt()) ensure_euf(); } @@ -537,7 +531,7 @@ class sat_smt_solver : public solver { void convert_internalized() { m_solver.pop_to_base_level(); - if (!is_internalized() && m_preprocess.qhead() > 0) + if (!is_internalized() && m_preprocess_state.qhead() > 0) internalize_formulas(); if (!is_internalized() || m_internalized_converted) return; @@ -623,15 +617,19 @@ class sat_smt_solver : public solver { if (is_internalized()) return l_true; - unsigned qhead = m_preprocess.qhead(); + unsigned qhead = m_preprocess_state.qhead(); m_trail.push(restore_vector(m_assumptions)); m_trail.push(restore_vector(m_fmls)); m_trail.push(value_trail(m_mc_size)); + TRACE("sat", tout << "qhead " << qhead << "\n"); m_internalized_converted = false; m_preprocess_state.replay(qhead); m_preprocess.reduce(); + if (!m.inc()) + return l_undef; + m_preprocess_state.advance_qhead(); m_preprocess_state.append(*m_mc); m_solver.pop_to_base_level(); m_aux_fmls.reset(); @@ -695,7 +693,7 @@ class sat_smt_solver : public solver { mdl = nullptr; if (!m_solver.model_is_current()) return; - if (m_fmls.size() > m_preprocess.qhead()) + if (m_fmls.size() > m_preprocess_state.qhead()) return; TRACE("sat", m_solver.display_model(tout);); CTRACE("sat", m_sat_mc, m_sat_mc->display(tout);); diff --git a/src/sat/smt/q_mbi.cpp b/src/sat/smt/q_mbi.cpp index 2c9b87c13a5..6f2db37e1a2 100644 --- a/src/sat/smt/q_mbi.cpp +++ b/src/sat/smt/q_mbi.cpp @@ -629,7 +629,7 @@ namespace q { void mbqi::init_solver() { if (!m_solver) - m_solver = mk_smt2_solver(m, m_no_drat_params); + m_solver = mk_smt2_solver(m, m_no_drat_params, symbol::null); } void mbqi::init_search() { diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index 0f23527dd1a..865c5f15d72 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -99,7 +99,7 @@ struct goal2sat::imp : public sat::sat_internalizer { sat_params sp(p); m_ite_extra = p.get_bool("ite_extra", true); m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX)); - m_euf = sp.euf(); + m_euf = sp.euf() || sp.smt(); } void throw_op_not_handled(std::string const& s) { diff --git a/src/solver/solver.h b/src/solver/solver.h index 4ffdd509269..957cb7c8edc 100644 --- a/src/solver/solver.h +++ b/src/solver/solver.h @@ -35,7 +35,7 @@ class solver_factory { solver_factory * mk_smt_strategic_solver_factory(symbol const & logic = symbol::null); -solver* mk_smt2_solver(ast_manager& m, params_ref const& p); +solver* mk_smt2_solver(ast_manager& m, params_ref const& p, symbol const& logic = symbol::null); /** \brief Abstract interface for making solvers available in the Z3 diff --git a/src/tactic/arith/card2bv_tactic.h b/src/tactic/arith/card2bv_tactic.h index 95282d93cce..63cb021d706 100644 --- a/src/tactic/arith/card2bv_tactic.h +++ b/src/tactic/arith/card2bv_tactic.h @@ -30,7 +30,7 @@ class card2bv_tactic_factory : public dependent_expr_simplifier_factory { }; inline tactic* mk_card2bv_tactic(ast_manager& m, params_ref const& p = params_ref()) { - return alloc(dependent_expr_state_tactic, m, p, alloc(card2bv_tactic_factory), "card2bv"); + return alloc(dependent_expr_state_tactic, m, p, alloc(card2bv_tactic_factory)); } /* diff --git a/src/tactic/bv/bv_slice_tactic.cpp b/src/tactic/bv/bv_slice_tactic.cpp index 040068e3941..17d69c7b147 100644 --- a/src/tactic/bv/bv_slice_tactic.cpp +++ b/src/tactic/bv/bv_slice_tactic.cpp @@ -29,5 +29,5 @@ class bv_slice_factory : public dependent_expr_simplifier_factory { }; tactic* mk_bv_slice_tactic(ast_manager& m, params_ref const& p) { - return alloc(dependent_expr_state_tactic, m, p, alloc(bv_slice_factory), "bv-slice"); + return alloc(dependent_expr_state_tactic, m, p, alloc(bv_slice_factory)); } diff --git a/src/tactic/bv/max_bv_sharing_tactic.h b/src/tactic/bv/max_bv_sharing_tactic.h index ebd050aa514..3521b4a041e 100644 --- a/src/tactic/bv/max_bv_sharing_tactic.h +++ b/src/tactic/bv/max_bv_sharing_tactic.h @@ -32,7 +32,7 @@ class max_bv_sharing_tactic_factory : public dependent_expr_simplifier_factory { }; inline tactic* mk_max_bv_sharing_tactic(ast_manager& m, params_ref const& p = params_ref()) { - return alloc(dependent_expr_state_tactic, m, p, alloc(max_bv_sharing_tactic_factory), "max-bv-sharing"); + return alloc(dependent_expr_state_tactic, m, p, alloc(max_bv_sharing_tactic_factory)); } /* diff --git a/src/tactic/core/elim_uncnstr2_tactic.h b/src/tactic/core/elim_uncnstr2_tactic.h index d9f6196f2f7..e7226a8f0af 100644 --- a/src/tactic/core/elim_uncnstr2_tactic.h +++ b/src/tactic/core/elim_uncnstr2_tactic.h @@ -29,7 +29,7 @@ class elim_uncnstr2_tactic_factory : public dependent_expr_simplifier_factory { }; inline tactic * mk_elim_uncnstr2_tactic(ast_manager & m, params_ref const & p = params_ref()) { - return alloc(dependent_expr_state_tactic, m, p, alloc(elim_uncnstr2_tactic_factory), "elim-uncnstr2"); + return alloc(dependent_expr_state_tactic, m, p, alloc(elim_uncnstr2_tactic_factory)); } diff --git a/src/tactic/core/eliminate_predicates_tactic.h b/src/tactic/core/eliminate_predicates_tactic.h index 3daffb1f32d..de2291260b7 100644 --- a/src/tactic/core/eliminate_predicates_tactic.h +++ b/src/tactic/core/eliminate_predicates_tactic.h @@ -17,9 +17,9 @@ Module Name: #pragma once #include "util/params.h" +#include "ast/simplifiers/eliminate_predicates.h" #include "tactic/tactic.h" #include "tactic/dependent_expr_state_tactic.h" -#include "ast/simplifiers/eliminate_predicates.h" class eliminate_predicates_tactic_factory : public dependent_expr_simplifier_factory { @@ -30,7 +30,7 @@ class eliminate_predicates_tactic_factory : public dependent_expr_simplifier_fac }; inline tactic * mk_eliminate_predicates_tactic(ast_manager& m, params_ref const& p = params_ref()) { - return alloc(dependent_expr_state_tactic, m, p, alloc(eliminate_predicates_tactic_factory), "elim-predicates"); + return alloc(dependent_expr_state_tactic, m, p, alloc(eliminate_predicates_tactic_factory)); } /* diff --git a/src/tactic/core/euf_completion_tactic.cpp b/src/tactic/core/euf_completion_tactic.cpp index bdd940f175f..d229df62f74 100644 --- a/src/tactic/core/euf_completion_tactic.cpp +++ b/src/tactic/core/euf_completion_tactic.cpp @@ -28,5 +28,5 @@ class euf_completion_tactic_factory : public dependent_expr_simplifier_factory { }; tactic * mk_euf_completion_tactic(ast_manager& m, params_ref const& p) { - return alloc(dependent_expr_state_tactic, m, p, alloc(euf_completion_tactic_factory), "euf-completion"); + return alloc(dependent_expr_state_tactic, m, p, alloc(euf_completion_tactic_factory)); } diff --git a/src/tactic/core/propagate_values2_tactic.h b/src/tactic/core/propagate_values2_tactic.h index 58e263e8021..834e8bebd48 100644 --- a/src/tactic/core/propagate_values2_tactic.h +++ b/src/tactic/core/propagate_values2_tactic.h @@ -31,7 +31,7 @@ class propagate_values2_tactic_factory : public dependent_expr_simplifier_factor }; inline tactic * mk_propagate_values2_tactic(ast_manager & m, params_ref const & p = params_ref()) { - return alloc(dependent_expr_state_tactic, m, p, alloc(propagate_values2_tactic_factory), "propagate-values2"); + return alloc(dependent_expr_state_tactic, m, p, alloc(propagate_values2_tactic_factory)); } diff --git a/src/tactic/core/solve_eqs_tactic.h b/src/tactic/core/solve_eqs_tactic.h index 5d6da2e9a1e..76a73866004 100644 --- a/src/tactic/core/solve_eqs_tactic.h +++ b/src/tactic/core/solve_eqs_tactic.h @@ -30,7 +30,7 @@ class solve_eqs_tactic_factory : public dependent_expr_simplifier_factory { }; inline tactic * mk_solve_eqs_tactic(ast_manager& m, params_ref const& p = params_ref()) { - return alloc(dependent_expr_state_tactic, m, p, alloc(solve_eqs_tactic_factory), "solve-eqs"); + return alloc(dependent_expr_state_tactic, m, p, alloc(solve_eqs_tactic_factory)); } /* diff --git a/src/tactic/dependent_expr_state_tactic.h b/src/tactic/dependent_expr_state_tactic.h index f16bb0ff3d1..dda114c24dc 100644 --- a/src/tactic/dependent_expr_state_tactic.h +++ b/src/tactic/dependent_expr_state_tactic.h @@ -22,7 +22,6 @@ Module Name: class dependent_expr_state_tactic : public tactic, public dependent_expr_state { ast_manager& m; params_ref m_params; - std::string m_name; trail_stack m_trail; goal_ref m_goal; dependent_expr m_dep; @@ -42,10 +41,9 @@ class dependent_expr_state_tactic : public tactic, public dependent_expr_state { public: - dependent_expr_state_tactic(ast_manager& m, params_ref const& p, dependent_expr_simplifier_factory* f, char const* name): + dependent_expr_state_tactic(ast_manager& m, params_ref const& p, dependent_expr_simplifier_factory* f): m(m), m_params(p), - m_name(name), m_factory(f), m_simp(nullptr), m_dep(m, m.mk_true(), nullptr) @@ -79,7 +77,7 @@ class dependent_expr_state_tactic : public tactic, public dependent_expr_state { return *m_model_trail; } - char const* name() const override { return m_name.c_str(); } + char const* name() const override { return m_simp?m_simp->name():"null"; } void updt_params(params_ref const & p) override { m_params.append(p); @@ -93,7 +91,7 @@ class dependent_expr_state_tactic : public tactic, public dependent_expr_state { } tactic * translate(ast_manager & m) override { - return alloc(dependent_expr_state_tactic, m, m_params, m_factory.get(), name()); + return alloc(dependent_expr_state_tactic, m, m_params, m_factory.get()); } void operator()(goal_ref const & in, @@ -105,10 +103,12 @@ class dependent_expr_state_tactic : public tactic, public dependent_expr_state { try { if (!in->proofs_enabled()) m_simp->reduce(); + if (m.inc()) + advance_qhead(); } catch (rewriter_exception& ex) { throw tactic_exception(ex.msg()); - } + } m_goal->elim_true(); m_goal->elim_redundancies(); m_goal->inc_depth(); diff --git a/src/tactic/portfolio/smt_strategic_solver.cpp b/src/tactic/portfolio/smt_strategic_solver.cpp index 1a9fc0f56ca..8acfbe40d63 100644 --- a/src/tactic/portfolio/smt_strategic_solver.cpp +++ b/src/tactic/portfolio/smt_strategic_solver.cpp @@ -47,6 +47,7 @@ Module Name: #include "solver/parallel_params.hpp" #include "params/tactic_params.hpp" #include "parsers/smt2/smt2parser.h" +#include "sat/sat_params.hpp" @@ -114,6 +115,15 @@ static solver* mk_special_solver_for_logic(ast_manager & m, params_ref const & p return nullptr; } +solver* mk_smt2_solver(ast_manager& m, params_ref const& p, symbol const& logic) { + sat_params sp(p); + if (sp.smt()) + return mk_sat_smt_solver(m, p); + if (sp.euf()) + return mk_inc_sat_solver(m, p); + return mk_smt_solver(m, p, logic); +} + static solver* mk_solver_for_logic(ast_manager & m, params_ref const & p, symbol const& logic) { bv_rewriter rw(m); solver* s = mk_special_solver_for_logic(m, p, logic); @@ -123,7 +133,7 @@ static solver* mk_solver_for_logic(ast_manager & m, params_ref const & p, symbol if (!s && tp.default_tactic() == "sat") s = mk_inc_sat_solver(m, p); if (!s) - s = mk_smt_solver(m, p, logic); + s = mk_smt2_solver(m, p, logic); return s; } @@ -170,6 +180,4 @@ solver_factory * mk_smt_strategic_solver_factory(symbol const & logic) { return alloc(smt_strategic_solver_factory, logic); } -solver* mk_smt2_solver(ast_manager& m, params_ref const& p) { - return mk_inc_sat_solver(m, p); -} +