mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-04-02 09:58:59 +00:00
Code Activity

Properly extract justifications from subsolver

Browse source
This commit is contained in:
CEisenhofer 2026-04-01 16:58:26 +02:00
parent e25e93503b
commit 36b01a51f1
6 changed files with 74 additions and 38 deletions
Download patch file Download diff file Expand all files Collapse all files

20
src/smt/nseq_context_solver.h
View file

@ -32,7 +32,7 @@ namespace smt {
*/
class context_solver : public seq::simple_solver {
smt_params m_params; // must be declared before m_kernel
smt::kernel m_kernel;
kernel m_kernel;
arith_value m_arith_value;
static smt_params make_seq_len_params() {
@ -55,6 +55,10 @@ namespace smt {
// std::cout << "\t" << mk_pp(m_kernel.get_formula(i), m_kernel.m()) << std::endl;
// }
// std::cout << std::endl;
// std::cout << "Checking" << std::endl;
// for (unsigned i = 0; i < m_kernel.size(); i++) {
// std::cout << mk_pp(m_kernel.get_formula(i), m_kernel.m()) << std::endl;
// }
return m_kernel.check();
}
@ -84,14 +88,20 @@ namespace smt {
return m_arith_value.get_up(e, hi, is_strict) && !is_strict && hi.is_int();
}
virtual expr_ref_vector get_unsat_core() {
lbool check_with_assumptions(expr_ref_vector& assumptions, expr_ref_vector& core) override {
// TODO: Not ideal
// Replay with assumptions
// std::cout << "Assuming" << std::endl;
// for (unsigned i = 0; i < assumptions.size(); i++) {
// std::cout << mk_pp(assumptions[i].get(), m_kernel.m()) << std::endl;
// }
lbool r = m_kernel.check(assumptions.size(), assumptions.data());
unsigned cnt = m_kernel.get_unsat_core_size();
expr_ref_vector core(m_kernel.m());
core.reserve(cnt);
core.resize(cnt);
for (unsigned i = 0; i < cnt; i++) {
core[i] = m_kernel.get_unsat_core_expr(i);
}
return core;
return r;
}
void reset() override {

28
src/smt/seq/seq_nielsen.cpp
View file

@ -243,6 +243,12 @@ namespace seq {
}
void nielsen_node::add_constraint(constraint const &c) {
if (graph().get_manager().is_and(c.fml)) {
// this is important, as the subsolver might decompose for returned unsat cores
for (unsigned i = 0; i < to_app(c.fml)->get_num_args(); ++i) {
add_constraint(constraint(to_app(c.fml)->get_arg(i), c.dep, graph().get_manager()));
}
}
m_constraints.push_back(c);
if (m_graph.m_literal_if_false) {
auto lit = m_graph.m_literal_if_false(c.fml);
@ -386,11 +392,12 @@ namespace seq {
// nielsen_graph
// -----------------------------------------------
nielsen_graph::nielsen_graph(euf::sgraph &sg, simple_solver &solver):
nielsen_graph::nielsen_graph(euf::sgraph &sg, simple_solver &solver, simple_solver &core_solver):
m(sg.get_manager()),
m_seq(sg.get_seq_util()),
m_sg(sg),
m_solver(solver),
m_core_solver(core_solver),
m_parikh(alloc(seq_parikh, sg)),
m_seq_regex(alloc(seq::seq_regex, sg)),
m_len_vars(sg.get_manager()),
@ -495,6 +502,7 @@ namespace seq {
m_gpower_vars.reset();
m_dep_mgr.reset();
m_solver.reset();
m_core_solver.reset();
}
// -----------------------------------------------------------------------
@ -1268,7 +1276,7 @@ namespace seq {
vector<length_constraint> constraints;
generate_length_constraints(constraints);
for (auto const& lc : constraints) {
m_solver.assert_expr(lc.m_expr);
m_root->add_constraint(lc.to_constraint());
}
}
@ -3916,15 +3924,20 @@ namespace seq {
}
dep_tracker nielsen_graph::get_subsolver_dependency(nielsen_node* n) {
auto core = m_solver.get_unsat_core();
SASSERT(!core.empty());
u_map<dep_tracker> expr_to_dep;
for (unsigned i = 0; i < n->m_parent_ic_count; i++) {
expr_ref_vector assumptions(m);
assumptions.resize(n->constraints().size());
for (unsigned i = 0; i < assumptions.size(); i++) {
auto& c = n->constraints()[i];
expr_to_dep.insert_if_not_there(c.fml->get_id(), c.dep);
assumptions[i] = c.fml;
}
expr_ref_vector core(m);
lbool res = m_core_solver.check_with_assumptions(assumptions, core);
VERIFY(res == l_false);
dep_tracker dep = dep_mgr().mk_empty();
for (const expr * const e : core) {
for (expr* e : core) {
dep = dep_mgr().mk_join(dep, expr_to_dep[e->get_id()]);
}
return dep;
@ -3996,8 +4009,9 @@ namespace seq {
IF_VERBOSE(1, verbose_stream() << "solve_sat_path_ints: sat_path length=" << m_sat_path.size() << "\n";);
m_solver.push();
for (nielsen_edge* e : m_sat_path) {
for (auto const& ic : e->side_constraints())
for (auto const& ic : e->side_constraints()) {
m_solver.assert_expr(ic.fml);
}
}
if (m_sat_node) {
for (auto const& ic : m_sat_node->constraints())

56
src/smt/seq/seq_nielsen.h
View file

@ -273,12 +273,12 @@ namespace seq {
class simple_solver {
public:
virtual ~simple_solver() {}
virtual lbool check() = 0;
virtual void assert_expr(expr* e) = 0;
virtual void push() = 0;
virtual void pop(unsigned num_scopes) = 0;
virtual void get_model(model_ref& mdl) { mdl = nullptr; }
virtual expr_ref_vector get_unsat_core() { throw z3_exception(); }
virtual lbool check() = 0;
virtual void assert_expr(expr* e) = 0;
virtual void push() = 0;
virtual void pop(unsigned num_scopes) = 0;
virtual void get_model(model_ref& mdl) { mdl = nullptr; }
virtual lbool check_with_assumptions(expr_ref_vector& assumptions, expr_ref_vector& core) { return l_undef; }
// Optional bound queries on arithmetic expressions (non-strict integer bounds).
// Default implementation reports "unsupported".
virtual bool lower_bound(expr* e, rational& lo) const { return false; }
@ -439,24 +439,6 @@ namespace seq {
}
};
// kind of length constraint determines propagation strategy
enum class length_kind {
nonneg, // len(x) >= 0: unconditional axiom
eq, // len(lhs) = len(rhs): conditional on string equality
bound // Parikh bound: conditional on regex membership
};
// arithmetic length constraint derived from string equations
struct length_constraint {
expr_ref m_expr; // arithmetic expression (e.g., len(x) + len(y) = len(a) + 1)
dep_tracker m_dep; // tracks which input constraints contributed
length_kind m_kind; // determines propagation strategy
length_constraint(ast_manager& m): m_expr(m), m_dep(nullptr), m_kind(length_kind::nonneg) {}
length_constraint(expr* e, dep_tracker const& dep, length_kind kind, ast_manager& m):
m_expr(e, m), m_dep(dep), m_kind(kind) {}
};
// -----------------------------------------------
// integer constraint: equality or inequality over length expressions
// mirrors ZIPT's IntEq and IntLe
@ -476,6 +458,29 @@ namespace seq {
std::ostream& display(std::ostream& out) const;
};
// kind of length constraint determines propagation strategy
enum class length_kind {
nonneg, // len(x) >= 0: unconditional axiom
eq, // len(lhs) = len(rhs): conditional on string equality
bound // Parikh bound: conditional on regex membership
};
// arithmetic length constraint derived from string equations
struct length_constraint {
expr_ref m_expr; // arithmetic expression (e.g., len(x) + len(y) = len(a) + 1)
dep_tracker m_dep; // tracks which input constraints contributed
length_kind m_kind; // determines propagation strategy
length_constraint(ast_manager& m): m_expr(m), m_dep(nullptr), m_kind(length_kind::nonneg) {}
length_constraint(expr* e, dep_tracker const& dep, length_kind kind, ast_manager& m):
m_expr(e, m), m_dep(dep), m_kind(kind) {}
constraint to_constraint() const {
return constraint(m_expr, m_dep, m_expr.get_manager());
}
};
// edge in the Nielsen graph connecting two nodes
// mirrors ZIPT's NielsenEdge
class nielsen_edge {
@ -763,6 +768,7 @@ namespace seq {
// and optimistically assumes feasibility.
// -----------------------------------------------
simple_solver& m_solver;
simple_solver& m_core_solver;
// Constraint.Shared: guards re-assertion of root-level constraints.
// Set to true after assert_root_constraints_to_solver() is first called.
@ -820,7 +826,7 @@ namespace seq {
public:
// Construct with a caller-supplied solver. Ownership is NOT transferred;
// the caller is responsible for keeping the solver alive.
nielsen_graph(euf::sgraph& sg, simple_solver& solver);
nielsen_graph(euf::sgraph& sg, simple_solver& solver, simple_solver &core_solver);
~nielsen_graph();
void set_literal_if_false(std::function<sat::literal(expr* e)> const& lif) {

4
src/smt/smt_kernel.cpp
View file

@ -93,6 +93,10 @@ namespace smt {
return m_imp->m_kernel.get_num_asserted_formulas();
}
void kernel::get_formulas(ptr_vector<expr>& r) const {
return m_imp->m_kernel.get_asserted_formulas(r);
}
expr* kernel::get_formula(unsigned i) const {
return m_imp->m_kernel.get_asserted_formula(i);
}

3
src/smt/theory_nseq.cpp
View file

@ -34,7 +34,8 @@ namespace smt {
m_egraph(m),
m_sgraph(m, m_egraph),
m_context_solver(m),
m_nielsen(m_sgraph, m_context_solver),
m_core_solver(m),
m_nielsen(m_sgraph, m_context_solver, m_core_solver),
m_axioms(m_th_rewriter),
m_regex(m_sgraph),
m_model(m, m_seq, m_rewriter, m_sgraph),

1
src/smt/theory_nseq.h
View file

@ -46,6 +46,7 @@ namespace smt {
// m_context_solver must be declared before m_nielsen: its address is passed
// to the m_nielsen constructor and must remain stable for the object's lifetime.
context_solver m_context_solver;
context_solver m_core_solver;
seq::nielsen_graph m_nielsen;
seq::axioms m_axioms;
seq::seq_regex m_regex; // regex membership pre-processing