mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-19 08:29:31 +00:00
Code Activity

split into context and sub-solver, move length force predicates to context-solver

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-05-17 19:01:03 -07:00
parent 9d4feed0ae
commit 2a36b9a68e
9 changed files with 441 additions and 240 deletions
Download patch file Download diff file Expand all files Collapse all files

73
src/smt/nseq_context_solver.h
View file

@ -45,10 +45,9 @@ namespace smt {
*
* Assertions with dep == nullptr are asserted directly (always active).
*/
class context_solver : public seq::simple_solver {
class sub_solver : public seq::sub_solver_i {
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
@ -69,12 +68,10 @@ namespace smt {
}
public:
context_solver(ast_manager& m) :
sub_solver(ast_manager& m) :
m_params(make_seq_len_params()),
m_kernel(m, m_params),
m_arith_value(m),
m_assump_lits(m) {
m_arith_value.init(&m_kernel.get_context());
}
lbool check() override {
@ -137,23 +134,8 @@ namespace smt {
seq::dep_tracker core() override { return m_last_core; }
bool lower_bound(expr* e, rational& lo, literal_vector& lits, enode_pair_vector& eqs) const override {
bool is_strict = true;
return m_arith_value.get_lo(e, lo, is_strict, lits, eqs) && !is_strict && lo.is_int();
}
bool upper_bound(expr* e, rational& hi, literal_vector& lits, enode_pair_vector& eqs) const override {
bool is_strict = true;
return m_arith_value.get_up(e, hi, is_strict, lits, eqs) && !is_strict && hi.is_int();
}
bool current_value(expr* e, rational& v) const override {
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_assump_lit2id.reset();
m_frame_bounds.reset();
@ -163,4 +145,55 @@ namespace smt {
}
};
class context_solver : public seq::context_solver_i {
smt::context &ctx;
arith_value m_arith_value;
public:
context_solver(smt::context& ctx):
ctx(ctx),
m_arith_value(ctx.get_manager()) {
m_arith_value.init(&ctx);
}
bool lower_bound(expr *e, rational &lo, literal_vector &lits, enode_pair_vector &eqs) const override {
bool is_strict = true;
return m_arith_value.get_lo(e, lo, is_strict, lits, eqs) && !is_strict && lo.is_int();
}
bool upper_bound(expr *e, rational &hi, literal_vector &lits, enode_pair_vector &eqs) const override {
bool is_strict = true;
return m_arith_value.get_up(e, hi, is_strict, lits, eqs) && !is_strict && hi.is_int();
}
bool current_value(expr *e, rational &v) const override {
return m_arith_value.get_value(e, v) && v.is_int();
}
sat::literal literal_if_false(expr *e) {
bool is_not = ctx.get_manager().is_not(e, e);
if (m_should_internalize && !ctx.b_internalized(e)) {
// it can happen that the element is not internalized, but as soon as we do it, it becomes false.
// In case we just skip one of those uninternalized expressions,
// adding the Nielsen assumption later will fail
// Alternatively, we could just retry Nielsen saturation in case
// adding the Nielsen assumption yields the assumption being false after internalizing
ctx.internalize(to_app(e), false);
}
if (!ctx.b_internalized(e))
return sat::null_literal;
literal lit = ctx.get_literal(e);
if (is_not)
lit.neg();
if (ctx.get_assignment(lit) == l_false) {
// TRACE(seq, tout << "literal_if_false: " << lit << " " << mk_pp(e, m) << " is assigned false\n");
return lit;
}
// TRACE(seq, tout << "literal_if_false: " << mk_pp(e, m) << " is assigned " << ctx.get_assignment(lit) <<
// "\n");
return sat::null_literal;
}
};
}

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

@ -284,7 +284,7 @@ namespace seq {
enode_pair_vector eqs;
if (m_graph.a.is_numeral(e, lo))
return true;
if (!m_graph.m_solver.lower_bound(e, lo, lits, eqs))
if (!m_graph.m_context_solver.lower_bound(e, lo, lits, eqs))
return false;
for (auto lit : lits)
dep = m_graph.dep_mgr().mk_join(dep, m_graph.dep_mgr().mk_leaf(lit));
@ -301,7 +301,7 @@ namespace seq {
enode_pair_vector eqs;
if (m_graph.a.is_numeral(e, up))
return true;
if (!m_graph.m_solver.upper_bound(e, up, lits, eqs))
if (!m_graph.m_context_solver.upper_bound(e, up, lits, eqs))
return false;
for (auto lit : lits)
dep = m_graph.dep_mgr().mk_join(dep, m_graph.dep_mgr().mk_leaf(lit));
@ -432,12 +432,13 @@ namespace seq {
// nielsen_graph
// -----------------------------------------------
nielsen_graph::nielsen_graph(euf::sgraph &sg, simple_solver &solver):
nielsen_graph::nielsen_graph(euf::sgraph &sg, sub_solver_i &solver, context_solver_i& ctx_solver):
m(sg.get_manager()),
a(sg.get_manager()),
m_seq(sg.get_seq_util()),
m_sg(sg),
m_solver(solver),
m_length_solver(solver),
m_context_solver(ctx_solver),
m_parikh(alloc(seq_parikh, sg)),
m_seq_regex(alloc(seq::seq_regex, sg)) {}
@ -550,7 +551,7 @@ namespace seq {
m_length_trail.reset();
m_length_info.reset();
m_dep_mgr.reset();
m_solver.reset();
m_length_solver.reset();
SASSERT(m_nodes.empty());
SASSERT(m_edges.empty());
SASSERT(m_root == nullptr);
@ -1891,7 +1892,7 @@ namespace seq {
// constraints. The child's own new constraints will be asserted
// inside the recursive call (above). On return, pop the scope so
// that backtracking removes those assertions.
m_solver.push();
m_length_solver.push();
// Lazily compute substitution length constraints (|x| = |u|) on first
// traversal. This must happen before asserting side_constraints and before
@ -1916,7 +1917,7 @@ namespace seq {
// Restore modification counts on backtrack.
dec_edge_mod_counts(e);
m_solver.pop(1);
m_length_solver.pop(1);
if (r == search_result::sat)
return search_result::sat;
cur_path.pop_back();
@ -4501,11 +4502,11 @@ namespace seq {
}
void nielsen_graph::assert_to_subsolver(const constraint& c) {
m_solver.assert_expr(c.fml, c.dep);
m_length_solver.assert_expr(c.fml, c.dep);
}
void nielsen_graph::assert_to_subsolver(expr* e) {
m_solver.assert_expr(e);
m_length_solver.assert_expr(e);
}
void nielsen_graph::assert_node_new_int_constraints(nielsen_node* node) {
@ -4514,10 +4515,9 @@ namespace seq {
// already present in the enclosing solver scope; asserting them again would
// be redundant (though harmless). This is called by search_dfs right after
// simplify_and_init, which is where new constraints are produced.
SASSERT(m_literal_if_false);
for (unsigned i = node->m_parent_ic_count; i < node->constraints().size(); ++i) {
auto& c = node->constraints()[i];
auto lit = m_literal_if_false(c.fml);
auto lit = m_context_solver.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) {
@ -4584,13 +4584,13 @@ namespace seq {
// (root length constraints at the base level, edge side_constraints and node
// constraints pushed/popped as the DFS descends and backtracks).
// A plain check() is therefore sufficient.
return m_solver.check() != l_false;
return m_length_solver.check() != l_false;
}
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();
return m_length_solver.core();
}
bool nielsen_graph::check_lp_le(expr* lhs, expr* rhs, nielsen_node* n, dep_tracker& dep) {
@ -4599,8 +4599,8 @@ namespace seq {
rational lhs_lo, rhs_up;
literal_vector lits;
enode_pair_vector eqs;
if (m_solver.lower_bound(lhs, lhs_lo, lits, eqs) &&
m_solver.upper_bound(rhs, rhs_up, lits, eqs) && lhs_lo > rhs_up)
if (m_context_solver.lower_bound(lhs, lhs_lo, lits, eqs) &&
m_context_solver.upper_bound(rhs, rhs_up, lits, eqs) && lhs_lo > rhs_up)
return false;
// lhs <= lhs_up <= rhs_lo <= rhs
@ -4609,8 +4609,8 @@ namespace seq {
lits.reset();
eqs.reset();
rational rhs_lo, lhs_up;
if (m_solver.upper_bound(lhs, lhs_up, lits, eqs) &&
m_solver.lower_bound(rhs, rhs_lo, lits, eqs) &&
if (m_context_solver.upper_bound(lhs, lhs_up, lits, eqs) &&
m_context_solver.lower_bound(rhs, rhs_lo, lits, eqs) &&
lhs_up <= rhs_lo) {
for (auto lit : lits)
dep = m_dep_mgr.mk_join(dep, m_dep_mgr.mk_leaf(lit));
@ -4629,12 +4629,12 @@ namespace seq {
expr_ref one(a.mk_int(1), m);
expr_ref rhs_plus_one(a.mk_add(rhs, one), m);
m_solver.push();
m_length_solver.push();
assert_to_subsolver(a.mk_ge(lhs, rhs_plus_one));
lbool result = m_solver.check();
lbool result = m_length_solver.check();
if (result == l_false)
dep = m_solver.core();
m_solver.pop(1);
dep = m_length_solver.core();
m_length_solver.pop(1);
if (result == l_false) {
n->add_constraint(constraint(a.mk_le(lhs, rhs), dep, m));
return true;

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

@ -316,7 +316,6 @@ namespace seq {
using enode_pair = std::pair<smt::enode *, smt::enode *>;
using literal_vector = svector<sat::literal>;
using enode_pair_vector = svector<enode_pair>;
using dep_source = std::variant<sat::literal, enode_pair>;
@ -338,21 +337,39 @@ namespace seq {
* to serve as the arithmetic back-end. When no solver is provided,
* integer feasibility checks are skipped (optimistically assumed feasible).
*/
class simple_solver {
class sub_solver_i {
public:
virtual ~simple_solver() {}
virtual ~sub_solver_i() {}
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; }
virtual void reset() = 0;
};
class context_solver_i {
public:
virtual ~context_solver_i() {}
bool m_should_internalize = false;
// Optional bound queries on arithmetic expressions (non-strict integer bounds).
// Default implementation reports "unsupported".
virtual bool lower_bound(expr* e, rational& l, literal_vector& lits, enode_pair_vector& eqs) const { return false; }
virtual bool upper_bound(expr* e, rational& hi, literal_vector& lits, enode_pair_vector& eqs) const { return false; }
virtual bool current_value(expr* e, rational& v) const { return false; }
virtual void reset() = 0;
virtual bool lower_bound(expr *e, rational &l, literal_vector &lits, enode_pair_vector &eqs) const {
return false;
}
virtual bool upper_bound(expr *e, rational &hi, literal_vector &lits, enode_pair_vector &eqs) const {
return false;
}
virtual bool current_value(expr *e, rational &v) const {
return false;
}
virtual sat::literal literal_if_false(expr* e) {
return sat::null_literal;
}
};
// partition dep_source leaves from deps into enode pairs, sat literals,
@ -840,10 +857,13 @@ namespace seq {
// -----------------------------------------------
// Integer subsolver (abstract interface)
// When m_solver is null, check_int_feasibility skips arithmetic checking
// and optimistically assumes feasibility.
// -----------------------------------------------
simple_solver& m_solver;
sub_solver_i& m_length_solver;
// -----------------------------------------------
// Interface to solver context
// -----------------------------------------------
context_solver_i &m_context_solver;
// Constraint.Shared: guards re-assertion of root-level constraints.
// Set to true after assert_root_constraints_to_solver() is first called.
@ -857,9 +877,6 @@ namespace seq {
// inclusion, derivatives. Allocated in the constructor; owned by this graph.
seq::seq_regex* m_seq_regex = nullptr;
// Callback to check that literals assumed in branches are not already assigned to false.
// returns the literal that is assigned to false, otherwise returns a null_literal
std::function<sat::literal(expr *)> m_literal_if_false;
// Maps each variable to its current length term
@ -886,12 +903,9 @@ 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, sub_solver_i& solver, context_solver_i& ctx);
~nielsen_graph();
void set_literal_if_false(std::function<sat::literal(expr* e)> const& lif) {
m_literal_if_false = lif;
}
ast_manager &get_manager() {
return m;

40
src/smt/theory_nseq.cpp
View file

@ -33,8 +33,9 @@ namespace smt {
m_arith_value(m),
m_egraph(m),
m_sgraph(m, m_egraph),
m_context_solver(m),
m_nielsen(m_sgraph, m_context_solver),
m_length_solver(m),
m_context_solver(ctx),
m_nielsen(m_sgraph, m_length_solver, m_context_solver),
m_axioms(m_th_rewriter),
m_regex(m_sgraph),
m_model(m, ctx, m_seq, m_rewriter, m_sgraph),
@ -82,34 +83,8 @@ namespace smt {
m_axioms.set_ensure_digits(ensure_digit_axiom);
m_axioms.set_mark_no_diseq(mark_no_diseq);
m_should_internalize = true; // delete this if using internalize as fallback
std::function<sat::literal(expr*)> literal_if_false = [&](expr* e) {
bool is_not = m.is_not(e, e);
if (m_should_internalize && !ctx.b_internalized(e)) {
// it can happen that the element is not internalized, but as soon as we do it, it becomes false.
// In case we just skip one of those uninternalized expressions,
// adding the Nielsen assumption later will fail
// Alternatively, we could just retry Nielsen saturation in case
// adding the Nielsen assumption yields the assumption being false after internalizing
ctx.internalize(to_app(e), false);
}
if (!ctx.b_internalized(e))
return sat::null_literal;
literal lit = ctx.get_literal(e);
if (is_not)
lit.neg();
if (ctx.get_assignment(lit) == l_false) {
// TRACE(seq, tout << "literal_if_false: " << lit << " " << mk_pp(e, m) << " is assigned false\n");
return lit;
}
// TRACE(seq, tout << "literal_if_false: " << mk_pp(e, m) << " is assigned " << ctx.get_assignment(lit) << "\n");
return sat::null_literal;
};
m_nielsen.set_literal_if_false(literal_if_false);
m_context_solver.m_should_internalize = true; // delete this if using internalize as fallback
}
// -----------------------------------------------------------------------
@ -848,12 +823,11 @@ namespace smt {
break;
case l_false:
// this should not happen because nielsen checks for this before returning a satisfying path.
// or maybe it can happen if we have a "le" dependency
TRACE(seq, tout << "nseq final_check: nielsen assumption " << c.fml << " is false; internalized - " << ctx.e_internalized(c.fml) << "\n");
all_sat = false;
// std::cout << "False [" << lit << "]: " << mk_pp(c.fml, m) << std::endl;
ctx.push_trail(value_trail(m_should_internalize));
m_should_internalize = true;
ctx.push_trail(value_trail(m_context_solver.m_should_internalize));
m_context_solver.m_should_internalize = true;
break;
}
// use assumptions to bound search

2
src/smt/theory_nseq.h
View file

@ -44,12 +44,12 @@ namespace smt {
euf::sgraph m_sgraph; // private sgraph
// 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.
sub_solver m_length_solver;
context_solver m_context_solver;
seq::nielsen_graph m_nielsen;
seq::axioms m_axioms;
seq::seq_regex m_regex; // regex membership pre-processing
seq_model m_model; // model construction helper
bool m_should_internalize = false;
// propagation queue items (variant over the distinct propagation cases)
using eq_item = tracked_str_eq; // string equality

27
src/test/nseq_basic.cpp
View file

@ -22,7 +22,7 @@ Abstract:
#include <iostream>
// Trivial solver that always returns sat and ignores all assertions.
class nseq_basic_dummy_solver : public seq::simple_solver {
class nseq_basic_dummy_solver : public seq::sub_solver_i {
public:
void push() override {}
void pop(unsigned) override {}
@ -40,7 +40,8 @@ static void test_nseq_instantiation() {
euf::egraph eg(m);
euf::sgraph sg(m, eg);
nseq_basic_dummy_solver solver;
seq::nielsen_graph ng(sg, solver);
seq::context_solver_i context_solver;
seq::nielsen_graph ng(sg, solver, context_solver);
SASSERT(ng.root() == nullptr);
SASSERT(ng.num_nodes() == 0);
std::cout << " ok\n";
@ -97,7 +98,8 @@ static void test_nseq_simplification() {
euf::egraph eg(m);
euf::sgraph sg(m, eg);
nseq_basic_dummy_solver solver;
seq::nielsen_graph ng(sg, solver);
seq::context_solver_i context_solver;
seq::nielsen_graph ng(sg, solver, context_solver);
// Add a trivial equality: empty = empty
euf::snode* empty1 = sg.mk_empty_seq(su.str.mk_string_sort());
@ -120,7 +122,8 @@ static void test_nseq_node_satisfied() {
euf::egraph eg(m);
euf::sgraph sg(m, eg);
nseq_basic_dummy_solver solver;
seq::nielsen_graph ng(sg, solver);
seq::context_solver_i context_solver;
seq::nielsen_graph ng(sg, solver, context_solver);
seq::nielsen_node *node = ng.mk_node();
// empty node has no constraints => satisfied
@ -149,7 +152,8 @@ static void test_nseq_symbol_clash() {
euf::egraph eg(m);
euf::sgraph sg(m, eg);
nseq_basic_dummy_solver solver;
seq::nielsen_graph ng(sg, solver);
seq::context_solver_i context_solver;
seq::nielsen_graph ng(sg, solver, context_solver);
euf::snode* a = sg.mk_char('a');
euf::snode* b = sg.mk_char('b');
@ -176,7 +180,8 @@ static void test_nseq_var_eq_self() {
euf::egraph eg(m);
euf::sgraph sg(m, eg);
nseq_basic_dummy_solver solver;
seq::nielsen_graph ng(sg, solver);
seq::context_solver_i context_solver;
seq::nielsen_graph ng(sg, solver, context_solver);
euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort());
ng.add_str_eq(x, x);
@ -194,7 +199,8 @@ static void test_nseq_prefix_clash() {
euf::egraph eg(m);
euf::sgraph sg(m, eg);
nseq_basic_dummy_solver solver;
seq::nielsen_graph ng(sg, solver);
seq::context_solver_i context_solver;
seq::nielsen_graph ng(sg, solver, context_solver);
euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort());
euf::snode* a = sg.mk_char('a');
@ -216,7 +222,8 @@ static void test_nseq_const_nielsen_solvable() {
euf::egraph eg(m);
euf::sgraph sg(m, eg);
nseq_basic_dummy_solver solver;
seq::nielsen_graph ng(sg, solver);
seq::context_solver_i context_solver;
seq::nielsen_graph ng(sg, solver, context_solver);
euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort());
euf::snode* y = sg.mk_var(symbol("y"), sg.get_str_sort());
@ -239,8 +246,8 @@ static void test_nseq_length_mismatch() {
euf::egraph eg(m);
euf::sgraph sg(m, eg);
nseq_basic_dummy_solver solver;
seq::nielsen_graph ng(sg, solver);
seq::context_solver_i context_solver;
seq::nielsen_graph ng(sg, solver, context_solver);
euf::snode* a = sg.mk_char('a');
euf::snode* b = sg.mk_char('b');
euf::snode* ab = sg.mk_concat(a, b);

7
src/test/nseq_zipt.cpp
View file

@ -30,7 +30,7 @@ Abstract:
#include <chrono>
// Trivial solver that always returns sat and ignores all assertions.
class nseq_zipt_dummy_solver : public seq::simple_solver {
class nseq_zipt_dummy_solver : public seq::sub_solver_i {
public:
void push() override {}
void pop(unsigned) override {}
@ -43,7 +43,7 @@ public:
// Trivial simple_solver stub: optimistically assumes integer constraints
// are always feasible (returns l_true without actually checking).
// -----------------------------------------------------------------------
class zipt_dummy_simple_solver : public seq::simple_solver {
class zipt_dummy_simple_solver : public seq::sub_solver_i {
public:
void push() override {}
void pop(unsigned) override {}
@ -184,6 +184,7 @@ struct nseq_fixture {
euf::egraph eg;
euf::sgraph sg;
zipt_dummy_simple_solver dummy_solver;
seq::context_solver_i context_solver;
seq::nielsen_graph ng;
seq_util su;
str_builder sb;
@ -193,7 +194,7 @@ struct nseq_fixture {
static ast_manager& init(ast_manager& m) { reg_decl_plugins(m); return m; }
nseq_fixture()
: eg(init(m)), sg(m, eg), ng(sg, dummy_solver), su(m), sb(sg, su), rb(m, su, sg)
: eg(init(m)), sg(m, eg), dummy_solver(), context_solver(), ng(sg, dummy_solver, context_solver), su(m), sb(sg, su), rb(m, su, sg)
{}
euf::snode* S(const char* s) { return sb.parse(s); }

434
src/test/seq_nielsen.cpp
View file

File diff suppressed because it is too large Load diff

8
src/test/seq_parikh.cpp
View file

@ -38,7 +38,7 @@ Author:
// ---------------------------------------------------------------------------
// Minimal solver stub (no-op)
// ---------------------------------------------------------------------------
class parikh_test_solver : public seq::simple_solver {
class parikh_test_solver : public seq::sub_solver_i {
public:
void push() override {}
void pop(unsigned) override {}
@ -486,7 +486,8 @@ static void test_apply_to_node_adds_constraints() {
euf::sgraph sg(m, eg);
seq_util seq(m);
parikh_test_solver solver;
seq::nielsen_graph ng(sg, solver);
seq::context_solver_i context_solver;
seq::nielsen_graph ng(sg, solver, context_solver);
seq::seq_parikh parikh(sg);
euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort());
@ -518,7 +519,8 @@ static void test_apply_to_node_stride_one_no_constraints() {
seq_util seq(m);
sort_ref str_sort(seq.str.mk_string_sort(), m);
parikh_test_solver solver;
seq::nielsen_graph ng(sg, solver);
seq::context_solver_i context_solver;
seq::nielsen_graph ng(sg, solver, context_solver);
seq::seq_parikh parikh(sg);
euf::snode* x = sg.mk_var(symbol("x"), sg.get_str_sort());