mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

relevancy level is queried during smt_setup, so it has to update the local parameter that tracks the min

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-11-25 09:53:00 -08:00
parent 17fb07875d
commit 055cf6c7b9
3 changed files with 10 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/smt/smt_context.cpp
View file

@ -148,6 +148,10 @@ namespace smt {
m_asserted_formulas.updt_params(p);
}
unsigned context::relevancy_lvl() const {
return std::min(m_relevancy_lvl, m_fparams.m_relevancy_lvl);
}
void context::copy(context& src_ctx, context& dst_ctx) {
ast_manager& dst_m = dst_ctx.get_manager();
ast_manager& src_m = src_ctx.get_manager();
@ -322,7 +326,7 @@ namespace smt {
TRACE("relevancy",
tout << "is_atom: " << d.is_atom() << " is relevant: " << is_relevant_core(l) << "\n";);
if (d.is_atom() && (m_relevancy_lvl == 0 || (m_relevancy_lvl == 1 && !d.is_quantifier()) || is_relevant_core(l)))
if (d.is_atom() && (relevancy_lvl() == 0 || (relevancy_lvl() == 1 && !d.is_quantifier()) || is_relevant_core(l)))
m_atom_propagation_queue.push_back(l);
if (m.has_trace_stream())
@ -1582,8 +1586,8 @@ namespace smt {
bool_var_data & d = get_bdata(v);
SASSERT(relevancy());
// Quantifiers are only asserted when marked as relevant.
// Other atoms are only asserted when marked as relevant if m_relevancy_lvl >= 2
if (d.is_atom() && (d.is_quantifier() || m_relevancy_lvl >= 2)) {
// Other atoms are only asserted when marked as relevant if relevancy_lvl >= 2
if (d.is_atom() && (d.is_quantifier() || relevancy_lvl() >= 2)) {
lbool val = get_assignment(v);
if (val != l_undef)
m_atom_propagation_queue.push_back(literal(v, val == l_false));

4
src/smt/smt_context.h
View file

@ -281,10 +281,10 @@ namespace smt {
}
bool relevancy() const {
return m_relevancy_lvl > 0;
return relevancy_lvl() > 0;
}
unsigned relevancy_lvl() const { return m_relevancy_lvl; }
unsigned relevancy_lvl() const;
enode * get_enode(expr const * n) const {
SASSERT(e_internalized(n));

2
src/smt/smt_internalizer.cpp
View file

@ -1195,7 +1195,7 @@ namespace smt {
// Reason: when a learned clause becomes unit, it should mark the
// unit literal as relevant. When binary_clause_opt is used,
// it is not possible to distinguish between learned and non-learned clauses.
if (lemma && m_relevancy_lvl >= 2)
if (lemma && relevancy_lvl() >= 2)
return false;
if (m_base_lvl > 0)
return false;