From b28f83e2e03cf4496b551d137cc4d51f4b93134f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 25 Apr 2026 08:09:25 -0700 Subject: [PATCH] add initial scaffolding for using assumption literals Signed-off-by: Nikolaj Bjorner --- src/smt/theory_nseq.cpp | 46 ++++++++++++++++++++++++++++++++++++++++- src/smt/theory_nseq.h | 4 ++++ 2 files changed, 49 insertions(+), 1 deletion(-) diff --git a/src/smt/theory_nseq.cpp b/src/smt/theory_nseq.cpp index 326dbe201..ccde98519 100644 --- a/src/smt/theory_nseq.cpp +++ b/src/smt/theory_nseq.cpp @@ -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)); + } + } } diff --git a/src/smt/theory_nseq.h b/src/smt/theory_nseq.h index 3e18cabea..229b4f293 100644 --- a/src/smt/theory_nseq.h +++ b/src/smt/theory_nseq.h @@ -66,6 +66,8 @@ namespace smt { expr_ref_vector m_relevant_lengths; // track variables whose lengths are relevant obj_map 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"; }