diff --git a/src/smt/params/smt_params.cpp b/src/smt/params/smt_params.cpp index 3c63e2fff..ef617f724 100644 --- a/src/smt/params/smt_params.cpp +++ b/src/smt/params/smt_params.cpp @@ -51,6 +51,7 @@ void smt_params::updt_local_params(params_ref const & _p) { m_core_validate = p.core_validate(); m_logic = _p.get_sym("logic", m_logic); m_string_solver = p.string_solver(); + m_up_persist_clauses = p.up_persist_clauses(); validate_string_solver(m_string_solver); if (_p.get_bool("arith.greatest_error_pivot", false)) m_arith_pivot_strategy = arith_pivot_strategy::ARITH_PIVOT_GREATEST_ERROR; @@ -145,6 +146,7 @@ void smt_params::display(std::ostream & out) const { DISPLAY_PARAM(m_agility_factor); DISPLAY_PARAM(m_restart_agility_threshold); + DISPLAY_PARAM(m_up_persist_clauses); DISPLAY_PARAM(m_lemma_gc_strategy); DISPLAY_PARAM(m_lemma_gc_half); DISPLAY_PARAM(m_recent_lemmas_size); diff --git a/src/smt/params/smt_params.h b/src/smt/params/smt_params.h index 07b6b6095..c678b7536 100644 --- a/src/smt/params/smt_params.h +++ b/src/smt/params/smt_params.h @@ -170,6 +170,14 @@ struct smt_params : public preprocessor_params, unsigned m_old_clause_relevancy = 6; //!< Max. number of unassigned literals to be considered relevant. double m_inv_clause_decay = 1; //!< clause activity decay + // ----------------------------------- + // + // User propagator configuration + // + // ----------------------------------- + + bool m_up_persist_clauses = false; + // ----------------------------------- // // SMT-LIB (debug) pretty printer diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index c4660d1ea..708fa87d8 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -102,6 +102,7 @@ def_module_params(module_name='smt', ('arith.print_ext_var_names', BOOL, False, 'print external variable names'), ('pb.conflict_frequency', UINT, 1000, 'conflict frequency for Pseudo-Boolean theory'), ('pb.learn_complements', BOOL, True, 'learn complement literals for Pseudo-Boolean theory'), + ('up.persist_clauses', BOOL, True, 'replay propagated clauses below the levels they are asserted'), ('array.weak', BOOL, False, 'weak array theory'), ('array.extensional', BOOL, True, 'extensional array theory'), ('clause_proof', BOOL, False, 'record a clausal proof'), diff --git a/src/smt/theory_user_propagator.cpp b/src/smt/theory_user_propagator.cpp index 84a6799fb..395be3e68 100644 --- a/src/smt/theory_user_propagator.cpp +++ b/src/smt/theory_user_propagator.cpp @@ -293,7 +293,7 @@ void theory_user_propagator::pop_scope_eh(unsigned num_scopes) { } bool theory_user_propagator::can_propagate() { - return m_qhead < m_prop.size() || m_to_add_qhead < m_to_add.size(); + return m_qhead < m_prop.size() || m_to_add_qhead < m_to_add.size() || m_replay_qhead < m_clauses_to_replay.size(); } void theory_user_propagator::propagate_consequence(prop_info const& prop) { @@ -321,12 +321,10 @@ void theory_user_propagator::propagate_consequence(prop_info const& prop) { ctx.set_conflict(js); } else { -#if 1 for (auto& lit : m_lits) lit.neg(); for (auto const& [a,b] : m_eqs) m_lits.push_back(~mk_eq(a->get_expr(), b->get_expr(), false)); -#endif literal lit; if (has_quantifiers(prop.m_conseq)) { @@ -340,19 +338,17 @@ void theory_user_propagator::propagate_consequence(prop_info const& prop) { lit = mk_literal(prop.m_conseq); ctx.mark_as_relevant(lit); -#if 0 - justification* js = - ctx.mk_justification( - ext_theory_propagation_justification( - get_id(), ctx, m_lits.size(), m_lits.data(), m_eqs.size(), m_eqs.data(), lit)); - - ctx.assign(lit, js); -#endif - -#if 1 m_lits.push_back(lit); - ctx.mk_th_lemma(get_id(), m_lits); -#endif + if (ctx.get_fparams().m_up_persist_clauses) { + ctx.mk_th_axiom(get_id(), m_lits); + expr_ref_vector clause(m); + for (auto lit : m_lits) + clause.push_back(ctx.literal2expr(lit)); + m_clauses_to_replay.push_back(clause); + } + else { + ctx.mk_th_lemma(get_id(), m_lits); + } TRACE("user_propagate", ctx.display(tout);); } } @@ -363,12 +359,20 @@ void theory_user_propagator::propagate_new_fixed(prop_info const& prop) { void theory_user_propagator::propagate() { - if (m_qhead == m_prop.size() && m_to_add_qhead == m_to_add.size()) + if (m_qhead == m_prop.size() && m_to_add_qhead == m_to_add.size() && m_replay_qhead == m_clauses_to_replay.size()) return; TRACE("user_propagate", tout << "propagating queue head: " << m_qhead << " prop queue: " << m_prop.size() << "\n"); force_push(); - unsigned qhead = m_to_add_qhead; + unsigned qhead = m_replay_qhead; + if (qhead < m_clauses_to_replay.size()) { + for (; qhead < m_clauses_to_replay.size() && !ctx.inconsistent(); ++qhead) + replay_clause(m_clauses_to_replay.get(qhead)); + ctx.push_trail(value_trail(m_replay_qhead)); + m_replay_qhead = qhead; + } + + qhead = m_to_add_qhead; if (qhead < m_to_add.size()) { for (; qhead < m_to_add.size(); ++qhead) add_expr(m_to_add.get(qhead), true); @@ -391,6 +395,13 @@ void theory_user_propagator::propagate() { } +void theory_user_propagator::replay_clause(expr_ref_vector const& clause) { + m_lits.reset(); + for (expr* e : clause) + m_lits.push_back(mk_literal(e)); + ctx.mk_th_axiom(get_id(), m_lits); +} + bool theory_user_propagator::internalize_atom(app* atom, bool gate_ctx) { return internalize_term(atom); } diff --git a/src/smt/theory_user_propagator.h b/src/smt/theory_user_propagator.h index 4b365ef7a..5dbae59ed 100644 --- a/src/smt/theory_user_propagator.h +++ b/src/smt/theory_user_propagator.h @@ -86,6 +86,8 @@ namespace smt { expr* m_next_split_var = nullptr; unsigned m_next_split_idx = 0; lbool m_next_split_phase = l_undef; + vector m_clauses_to_replay; + unsigned m_replay_qhead = 0; expr* var2expr(theory_var v) { return m_var2expr.get(v); } theory_var expr2var(expr* e) { check_defined(e); return m_expr2var[e->get_id()]; } @@ -101,6 +103,8 @@ namespace smt { bool_var enode_to_bool(enode* n, unsigned bit); + void replay_clause(expr_ref_vector const& clause); + public: theory_user_propagator(context& ctx);