mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-17 07:29:28 +00:00
Code Activity

add initial scaffolding for using assumption literals

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-04-25 08:09:25 -07:00
parent abbe36561d
commit b28f83e2e0
2 changed files with 49 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

46
src/smt/theory_nseq.cpp
View file

@ -831,7 +831,9 @@ namespace smt {
ctx.push_trail(value_trail(m_should_internalize));
m_should_internalize = true;
break;
}
}
// use assumptions to bound search
// "propagate(m_assumption_lit, lit)"; // to force the phase of lit to be true or force a conflict
}
return all_sat;
}
@ -1574,6 +1576,48 @@ namespace smt {
return true;
}
// -----------------------------------------------------------------------
// Use theory assumptions to bound search depth and force literal assignments
// m_assumption_lit gets added as an assumption to the set of existing assumptions.
// If it is part of a core, a the epoch of the assumption literal is increased
// such that the current core can be unblocked in the next round of search.
//
// Suppose we would like to force a literal lit_i
// We would assert:
// m_assumption_lit => lit_i
// If there is an infeasible subset containing m_assumption_lit, one
// or more of the forced literals is conflicting and have to be relaxed.
//
// A base level scheme for using forced literals can be as follows:
// We can keep track of the set of forced literals lit_i that were implied by m_assumption_lit
// in a given round. Then we can selectively force each of these to learn exactly which are
// part of a core.
// Say they are lit_1, lit_2, lit_3.
// Let us mark lit_1 as tabu.
// Literals that are marked as tabu will not be forced in subsequent rounds of final_check_eh.
//
// -----------------------------------------------------------------------
bool theory_nseq::should_research(expr_ref_vector& core) {
for (auto c : core)
if (m_axioms.sk().is_max_unfolding(c)) {
// one or more of the "m_nielsen_literals" cannot be forced.
ctx.push_trail(value_trail(m_max_unfolding_depth));
++m_max_unfolding_depth;
return true;
}
return false;
}
void theory_nseq::add_theory_assumptions(expr_ref_vector& assumptions) {
if (m_seq.has_seq()) {
expr_ref dlimit = m_axioms.sk().mk_max_unfolding_depth(m_max_unfolding_depth);
ctx.push_trail(value_trail(m_assumption_lit));
m_assumption_lit = mk_literal(dlimit);
assumptions.push_back(std::move(dlimit));
}
}
}

4
src/smt/theory_nseq.h
View file

@ -66,6 +66,8 @@ namespace smt {
expr_ref_vector m_relevant_lengths; // track variables whose lengths are relevant
obj_map<expr, unsigned> m_gradient_cache;
sat::literal_vector m_nielsen_literals; // literals created by a Nilsen check
sat::literal m_assumption_lit; // literal used as assumption to bound search to selected literal assignments
unsigned m_max_unfolding_depth = 0;
// statistics
unsigned m_num_conflicts = 0;
@ -110,6 +112,8 @@ namespace smt {
void finalize_model(model_generator& mg) override;
void validate_model(proto_model& mdl) override;
void collect_statistics(::statistics& st) const override;
bool should_research(expr_ref_vector &) override;
void add_theory_assumptions(expr_ref_vector &assumptions) override;
char const* get_name() const override { return "nseq"; }