mirror of
https://github.com/Z3Prover/z3
synced 2026-05-16 15:15:35 +00:00
Using only one solver
This commit is contained in:
CEisenhofer
parent
712cd68e8c
commit
f7f2ee8f74
8 changed files with 154 additions and 108 deletions
|
|
@ -11,6 +11,12 @@ Abstract:
|
|||
that delegates arithmetic feasibility checks to an smt::kernel
|
||||
configured with seq.solver = "seq_len".
|
||||
|
||||
Each call to assert_expr(e, dep) with a non-null dep creates a fresh
|
||||
Boolean assumption literal `a` and asserts `a => e` into the kernel.
|
||||
The literal-to-dep mapping is maintained across push/pop scopes.
|
||||
After check() returns l_false, core() returns the joined dep_tracker
|
||||
for all assumption literals that appear in the kernel's UNSAT core.
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2026-03-10
|
||||
|
|
@ -22,6 +28,7 @@ Author:
|
|||
#include "smt/smt_kernel.h"
|
||||
#include "smt/smt_arith_value.h"
|
||||
#include "params/smt_params.h"
|
||||
#include "util/map.h"
|
||||
|
||||
namespace smt {
|
||||
|
||||
|
|
@ -29,11 +36,30 @@ namespace smt {
|
|||
* Concrete simple_solver that wraps smt::kernel.
|
||||
* Initializes the kernel with seq.solver = "seq_len" so that
|
||||
* sequence length constraints are handled by theory_seq_len.
|
||||
*
|
||||
* Assertions with a non-null dep_tracker are converted to assumption-
|
||||
* literal form: a fresh bool `a` is introduced, `(or (not a) e)` is
|
||||
* asserted, and the mapping a.id -> dep is tracked per push/pop scope.
|
||||
* After an UNSAT check(), core() returns the union of the deps for the
|
||||
* literals that appear in the kernel's UNSAT core.
|
||||
*
|
||||
* Assertions with dep == nullptr are asserted directly (always active).
|
||||
*/
|
||||
class context_solver : public seq::simple_solver {
|
||||
smt_params m_params; // must be declared before m_kernel
|
||||
kernel m_kernel;
|
||||
arith_value m_arith_value;
|
||||
smt_params m_params; // must be declared before m_kernel
|
||||
kernel m_kernel;
|
||||
arith_value m_arith_value;
|
||||
|
||||
// Tracked assumption literals.
|
||||
// m_assump_lits[i] and m_frame_bounds together encode a stack of
|
||||
// frames, one frame per push(). pop(n) removes the top n frames.
|
||||
expr_ref_vector m_assump_lits; // live assumption exprs
|
||||
svector<unsigned> m_frame_bounds; // m_assump_lits.size() at each push()
|
||||
u_map<seq::dep_tracker> m_lid_to_dep; // literal expr-id -> dep
|
||||
|
||||
// Scratch dep_manager for joining core deps; reset before each check().
|
||||
seq::dep_manager m_core_dep_mgr;
|
||||
seq::dep_tracker m_last_core = nullptr;
|
||||
|
||||
static smt_params make_seq_len_params() {
|
||||
smt_params p;
|
||||
|
|
@ -45,39 +71,67 @@ namespace smt {
|
|||
context_solver(ast_manager& m) :
|
||||
m_params(make_seq_len_params()),
|
||||
m_kernel(m, m_params),
|
||||
m_arith_value(m) {
|
||||
m_arith_value(m),
|
||||
m_assump_lits(m) {
|
||||
m_arith_value.init(&m_kernel.get_context());
|
||||
}
|
||||
|
||||
lbool check() override {
|
||||
// std::cout << "Checking:\n";
|
||||
// for (int i = 0; i < m_kernel.size(); i++) {
|
||||
// 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();
|
||||
m_core_dep_mgr.reset();
|
||||
m_last_core = nullptr;
|
||||
lbool r;
|
||||
if (m_assump_lits.empty()) {
|
||||
r = m_kernel.check();
|
||||
} else {
|
||||
r = m_kernel.check(m_assump_lits.size(), m_assump_lits.data());
|
||||
if (r == l_false) {
|
||||
unsigned cnt = m_kernel.get_unsat_core_size();
|
||||
for (unsigned i = 0; i < cnt; ++i) {
|
||||
expr* ce = m_kernel.get_unsat_core_expr(i);
|
||||
seq::dep_tracker d = nullptr;
|
||||
if (m_lid_to_dep.find(ce->get_id(), d))
|
||||
m_last_core = m_core_dep_mgr.mk_join(m_last_core, d);
|
||||
}
|
||||
}
|
||||
}
|
||||
return r;
|
||||
}
|
||||
|
||||
void assert_expr(expr* e) override {
|
||||
m_kernel.assert_expr(e);
|
||||
void assert_expr(expr* e, seq::dep_tracker dep) override {
|
||||
if (!dep) {
|
||||
m_kernel.assert_expr(e);
|
||||
return;
|
||||
}
|
||||
ast_manager& m = m_kernel.m();
|
||||
expr_ref lit(m.mk_fresh_const("_a", m.mk_bool_sort()), m);
|
||||
m_kernel.assert_expr(m.mk_or(m.mk_not(lit), e));
|
||||
m_lid_to_dep.insert_if_not_there(lit->get_id(), dep);
|
||||
m_assump_lits.push_back(lit);
|
||||
}
|
||||
|
||||
void push() override {
|
||||
m_kernel.push();
|
||||
m_frame_bounds.push_back((unsigned)m_assump_lits.size());
|
||||
}
|
||||
|
||||
void pop(unsigned num_scopes) override {
|
||||
m_kernel.pop(num_scopes);
|
||||
void pop(unsigned n) override {
|
||||
SASSERT(n <= m_frame_bounds.size());
|
||||
unsigned target = m_frame_bounds[m_frame_bounds.size() - n];
|
||||
while ((unsigned)m_assump_lits.size() > target) {
|
||||
m_lid_to_dep.erase(m_assump_lits.back()->get_id());
|
||||
m_assump_lits.pop_back();
|
||||
}
|
||||
for (unsigned i = 0; i < n; ++i)
|
||||
m_frame_bounds.pop_back();
|
||||
m_kernel.pop(n);
|
||||
}
|
||||
|
||||
void get_model(model_ref& mdl) override {
|
||||
m_kernel.get_model(mdl);
|
||||
}
|
||||
|
||||
seq::dep_tracker core() override { return m_last_core; }
|
||||
|
||||
bool lower_bound(expr* e, rational& lo) const override {
|
||||
bool is_strict = true;
|
||||
return m_arith_value.get_lo(e, lo, is_strict) && !is_strict && lo.is_int();
|
||||
|
|
@ -89,28 +143,17 @@ namespace smt {
|
|||
}
|
||||
|
||||
bool current_value(expr* e, rational& v) const override {
|
||||
return m_arith_value.get_value(e, v) && v.is_int();
|
||||
}
|
||||
|
||||
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();
|
||||
core.resize(cnt);
|
||||
for (unsigned i = 0; i < cnt; i++) {
|
||||
core[i] = m_kernel.get_unsat_core_expr(i);
|
||||
}
|
||||
return r;
|
||||
}
|
||||
return m_arith_value.get_value(e, v) && v.is_int();
|
||||
}
|
||||
|
||||
void reset() override {
|
||||
m_kernel.reset();
|
||||
m_arith_value.init(&m_kernel.get_context());
|
||||
m_assump_lits.reset();
|
||||
m_frame_bounds.reset();
|
||||
m_lid_to_dep.reset();
|
||||
m_core_dep_mgr.reset();
|
||||
m_last_core = nullptr;
|
||||
}
|
||||
};
|
||||
|
||||
|
|
|
|||
|
|
@ -414,13 +414,12 @@ namespace seq {
|
|||
// nielsen_graph
|
||||
// -----------------------------------------------
|
||||
|
||||
nielsen_graph::nielsen_graph(euf::sgraph &sg, simple_solver &solver, simple_solver &core_solver):
|
||||
nielsen_graph::nielsen_graph(euf::sgraph &sg, simple_solver &solver):
|
||||
m(sg.get_manager()),
|
||||
a(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)) {}
|
||||
|
||||
|
|
@ -534,7 +533,6 @@ namespace seq {
|
|||
m_length_info.reset();
|
||||
m_dep_mgr.reset();
|
||||
m_solver.reset();
|
||||
m_core_solver.reset();
|
||||
SASSERT(m_nodes.empty());
|
||||
SASSERT(m_edges.empty());
|
||||
SASSERT(m_root == nullptr);
|
||||
|
|
@ -4438,7 +4436,7 @@ namespace seq {
|
|||
SASSERT(m_literal_if_false);
|
||||
for (unsigned i = node->m_parent_ic_count; i < node->constraints().size(); ++i) {
|
||||
auto& c = node->constraints()[i];
|
||||
m_solver.assert_expr(c.fml);
|
||||
m_solver.assert_expr(c.fml, c.dep);
|
||||
auto lit = m_literal_if_false(c.fml);
|
||||
// std::cout << "Internalizing literal " << mk_pp(c.fml, m) << " [" << (lit == sat::null_literal) << "]" << std::endl;
|
||||
if (lit != sat::null_literal)
|
||||
|
|
@ -4505,32 +4503,10 @@ namespace seq {
|
|||
return m_solver.check() != l_false;
|
||||
}
|
||||
|
||||
dep_tracker nielsen_graph::get_subsolver_dependency(nielsen_node* n) {
|
||||
u_map<dep_tracker> expr_to_dep;
|
||||
expr_ref_vector assumptions(m);
|
||||
assumptions.resize(n->constraints().size());
|
||||
unsigned j = 0;
|
||||
for (auto const &c : n->constraints()) {
|
||||
if (expr_to_dep.contains(c.fml->get_id()))
|
||||
continue;
|
||||
expr_to_dep.insert_if_not_there(c.fml->get_id(), c.dep);
|
||||
assumptions[j++] = c.fml;
|
||||
}
|
||||
assumptions.shrink(j);
|
||||
expr_ref_vector core(m);
|
||||
lbool res = m_core_solver.check_with_assumptions(assumptions, core);
|
||||
CTRACE(seq, res != l_false,
|
||||
tout << "Unexpected satisfiable/unknown result from core solver "
|
||||
<< res << " " << core
|
||||
<< "\nassumptions\n"
|
||||
<< assumptions << "\n");
|
||||
VERIFY(res == l_false);
|
||||
|
||||
dep_tracker dep = dep_mgr().mk_empty();
|
||||
for (expr* e : core) {
|
||||
dep = dep_mgr().mk_join(dep, expr_to_dep[e->get_id()]);
|
||||
}
|
||||
return dep;
|
||||
dep_tracker nielsen_graph::get_subsolver_dependency(nielsen_node* /*n*/) {
|
||||
// check_int_feasibility() already called m_solver.check() which computed
|
||||
// the UNSAT core in terms of tracked assumption literals and their deps.
|
||||
return m_solver.core();
|
||||
}
|
||||
|
||||
bool nielsen_graph::check_lp_le(expr* lhs, expr* rhs, nielsen_node* n, dep_tracker& dep) {
|
||||
|
|
|
|||
|
|
@ -264,32 +264,6 @@ namespace seq {
|
|||
|
||||
std::string snode_label_html(euf::snode const* n, ast_manager& m);
|
||||
|
||||
/**
|
||||
* Abstract interface for an incremental solver used by nielsen_graph
|
||||
* to check integer/arithmetic feasibility of path constraints.
|
||||
*
|
||||
* Users of nielsen_graph can wrap smt::kernel or any other solver
|
||||
* to serve as the arithmetic back-end. When no solver is provided,
|
||||
* integer feasibility checks are skipped (optimistically assumed feasible).
|
||||
*/
|
||||
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 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; }
|
||||
virtual bool upper_bound(expr* e, rational& hi) const { return false; }
|
||||
virtual bool current_value(expr *e, rational &v) const { return false; }
|
||||
|
||||
virtual void reset() = 0;
|
||||
};
|
||||
|
||||
// simplification result for constraint processing
|
||||
// mirrors ZIPT's SimplifyResult enum
|
||||
enum class simplify_result {
|
||||
|
|
@ -362,6 +336,31 @@ namespace seq {
|
|||
// nullptr represents the empty dependency set.
|
||||
using dep_tracker = dep_manager::dependency*;
|
||||
|
||||
/**
|
||||
* Abstract interface for an incremental solver used by nielsen_graph
|
||||
* to check integer/arithmetic feasibility of path constraints.
|
||||
*
|
||||
* Users of nielsen_graph can wrap smt::kernel or any other solver
|
||||
* to serve as the arithmetic back-end. When no solver is provided,
|
||||
* integer feasibility checks are skipped (optimistically assumed feasible).
|
||||
*/
|
||||
class simple_solver {
|
||||
public:
|
||||
virtual ~simple_solver() {}
|
||||
virtual lbool check() = 0;
|
||||
virtual void assert_expr(expr* e, dep_tracker dep = nullptr) = 0;
|
||||
virtual void push() = 0;
|
||||
virtual void pop(unsigned num_scopes) = 0;
|
||||
virtual void get_model(model_ref& mdl) { mdl = nullptr; }
|
||||
virtual dep_tracker core() { return nullptr; }
|
||||
// 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; }
|
||||
virtual bool upper_bound(expr* e, rational& hi) const { return false; }
|
||||
virtual bool current_value(expr* e, rational& v) const { return false; }
|
||||
virtual void reset() = 0;
|
||||
};
|
||||
|
||||
// partition dep_source leaves from deps into enode pairs, sat literals,
|
||||
// and arithmetic <= dependencies.
|
||||
void deps_to_lits(dep_tracker deps,
|
||||
|
|
@ -852,7 +851,6 @@ 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.
|
||||
|
|
@ -895,7 +893,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, simple_solver &core_solver);
|
||||
nielsen_graph(euf::sgraph& sg, simple_solver& solver);
|
||||
~nielsen_graph();
|
||||
|
||||
void set_literal_if_false(std::function<sat::literal(expr* e)> const& lif) {
|
||||
|
|
|
|||
|
|
@ -479,6 +479,26 @@ namespace smt {
|
|||
return val;
|
||||
}
|
||||
|
||||
// Gets the arithmetic value of e. In QF_SLIA mode theory_lra does not register
|
||||
// numeral constants as LP variables, so get_value_equiv misses cases like
|
||||
// (str.len w) being equivalent to numeral 5 via EUF. Walking the EUF class
|
||||
// and checking for numerals directly handles this.
|
||||
bool seq_model::get_arith_value(expr* e, rational& val) const {
|
||||
if (!m_ctx.e_internalized(e))
|
||||
return false;
|
||||
arith_util a(m);
|
||||
enode* root = m_ctx.get_enode(e);
|
||||
enode* it = root;
|
||||
do {
|
||||
if (a.is_numeral(it->get_expr(), val))
|
||||
return true;
|
||||
it = it->get_next();
|
||||
} while (it != root);
|
||||
arith_value avalue(m);
|
||||
avalue.init(const_cast<context*>(&m_ctx));
|
||||
return avalue.get_value_equiv(e, val);
|
||||
}
|
||||
|
||||
rational seq_model::int_value(expr *_e) {
|
||||
expr_ref e(_e, m);
|
||||
m_ctx.get_rewriter()(e);
|
||||
|
|
@ -487,9 +507,7 @@ namespace smt {
|
|||
if (a.is_numeral(e, val))
|
||||
return val;
|
||||
|
||||
arith_value avalue(m);
|
||||
avalue.init(&m_ctx);
|
||||
bool has_val = avalue.get_value(e, val);
|
||||
bool has_val = get_arith_value(e, val);
|
||||
CTRACE(seq, !has_val, tout << "no value associated with " << mk_pp(e, m) << "\n";);
|
||||
return val;
|
||||
}
|
||||
|
|
@ -508,11 +526,9 @@ namespace smt {
|
|||
SASSERT(re_expr);
|
||||
|
||||
arith_util arith(m);
|
||||
arith_value avalue(m);
|
||||
avalue.init(&m_ctx);
|
||||
expr_ref len_expr(m_seq.str.mk_length(var->get_expr()), m);
|
||||
rational len_val;
|
||||
bool has_len = avalue.get_value(len_expr, len_val);
|
||||
bool has_len = get_arith_value(len_expr, len_val);
|
||||
CTRACE(seq, !has_len, tout << "no value associated with " << mk_pp(len_expr, m) << "\n";);
|
||||
|
||||
if (has_len && len_val.is_unsigned()) {
|
||||
|
|
@ -539,10 +555,7 @@ namespace smt {
|
|||
arith_util arith(m);
|
||||
expr_ref len_expr(m_seq.str.mk_length(var->get_expr()), m);
|
||||
rational len_val;
|
||||
|
||||
arith_value avalue(m);
|
||||
avalue.init(&m_ctx);
|
||||
bool has_len = avalue.get_value(len_expr, len_val);
|
||||
bool has_len = get_arith_value(len_expr, len_val);
|
||||
CTRACE(seq, !has_len, tout << "no value associated with " << mk_pp(len_expr, m) << "\n";);
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -137,6 +137,9 @@ namespace smt {
|
|||
// extract integer value for an expression.
|
||||
rational int_value(expr *e);
|
||||
|
||||
// Get arithmetic value via EUF equivalence class, including numeral check.
|
||||
bool get_arith_value(expr* e, rational& val) const;
|
||||
|
||||
};
|
||||
|
||||
}
|
||||
|
|
|
|||
|
|
@ -796,6 +796,7 @@ namespace smt {
|
|||
}
|
||||
|
||||
void setup::setup_nseq() {
|
||||
setup_lra_arith(); // Avoid problems when querying length values when having QF_S(LIA)
|
||||
m_context.register_plugin(alloc(smt::theory_nseq, m_context));
|
||||
setup_char();
|
||||
}
|
||||
|
|
|
|||
|
|
@ -34,8 +34,7 @@ namespace smt {
|
|||
m_egraph(m),
|
||||
m_sgraph(m, m_egraph),
|
||||
m_context_solver(m),
|
||||
m_core_solver(m),
|
||||
m_nielsen(m_sgraph, m_context_solver, m_core_solver),
|
||||
m_nielsen(m_sgraph, m_context_solver),
|
||||
m_axioms(m_th_rewriter),
|
||||
m_regex(m_sgraph),
|
||||
m_model(m, ctx, m_seq, m_rewriter, m_sgraph),
|
||||
|
|
@ -1267,6 +1266,19 @@ namespace smt {
|
|||
// -----------------------------------------------------------------------
|
||||
|
||||
bool theory_nseq::get_num_value(expr* e, rational& val) const {
|
||||
// In QF_SLIA mode theory_lra does not register numeral constants as LP
|
||||
// variables, so get_value_equiv misses cases where a term is only known
|
||||
// through an EUF equality with a numeral (e.g. (str.len w) = 5).
|
||||
// Walk the equivalence class directly first.
|
||||
if (get_context().e_internalized(e)) {
|
||||
enode* root = get_context().get_enode(e);
|
||||
enode* it = root;
|
||||
do {
|
||||
if (m_autil.is_numeral(it->get_expr(), val) && val.is_int())
|
||||
return true;
|
||||
it = it->get_next();
|
||||
} while (it != root);
|
||||
}
|
||||
return m_arith_value.get_value_equiv(e, val) && val.is_int();
|
||||
}
|
||||
|
||||
|
|
@ -1650,7 +1662,8 @@ namespace smt {
|
|||
continue;
|
||||
|
||||
rational val_l;
|
||||
VERIFY(m_arith_value.get_value(len_expr, val_l));
|
||||
if (!get_num_value(len_expr, val_l))
|
||||
continue;
|
||||
|
||||
SASSERT(val_l.is_unsigned());
|
||||
|
||||
|
|
|
|||
|
|
@ -45,7 +45,6 @@ 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
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue