mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-01-27 20:38:42 +00:00
Code Activity

Search tree core resolution optimization (#8066)

Browse source 
* Add cube tree optimization about resolving cores recursively up the path, to prune. Also integrate asms into the tree so they're not tracked separately (#7960)

* draft attempt at optimizing cube tree with resolvents. have not tested/ran yet

* adding comments

* fix bug about needing to bubble resolvent upwards to highest ancestor

* fix bug where we need to cover the whole resolvent in the path when bubbling up

* clean up comments

* close entire tree when sibling resolvent is empty

* integrate asms directly into cube tree, remove separate tracking

* try to fix bug about redundant resolutions, merging close and try_resolve_upwards into once function

* separate the logic again to avoid mutual recursion

* Refactor search tree closure and resolution logic

Refactor close_with_core to simplify logic and remove unnecessary parameters. Update sibling resolvent computation and try_resolve_upwards for clarity.

* apply formatting

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* Refactor close_with_core to use current node in lambda

* Fix formatting issues in search_tree.h

* fix build issues

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* Update smt_parallel.cpp

* Change loop variable type in unsat core processing

* Change method to retrieve unsat core from root

---------

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Ilana Shapiro 2025-12-13 04:06:56 -08:00 • committed by GitHub
parent 313be1ca1b
commit 0076e3bf97
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
3 changed files with 135 additions and 104 deletions
Download patch file Download diff file Expand all files Collapse all files

30
src/smt/smt_parallel.cpp
View file

@ -115,10 +115,6 @@ namespace smt {
b.set_unsat(m_l2g, unsat_core);
return;
}
// report assumptions used in unsat core, so they can be used in final core
for (expr *e : unsat_core)
if (asms.contains(e))
b.report_assumption_used(m_l2g, e);
LOG_WORKER(1, " found unsat cube\n");
b.backtrack(m_l2g, unsat_core, node);
@ -262,14 +258,16 @@ namespace smt {
vector<cube_config::literal> g_core;
for (auto c : core) {
expr_ref g_c(l2g(c), m);
if (!is_assumption(g_c))
g_core.push_back(expr_ref(l2g(c), m));
g_core.push_back(expr_ref(l2g(c), m));
}
m_search_tree.backtrack(node, g_core);
IF_VERBOSE(1, m_search_tree.display(verbose_stream() << bounded_pp_exprs(core) << "\n"););
if (m_search_tree.is_closed()) {
m_state = state::is_unsat;
SASSERT(p.ctx.m_unsat_core.empty());
for (auto e : m_search_tree.get_core_from_root())
p.ctx.m_unsat_core.push_back(e);
cancel_workers();
}
}
@ -415,27 +413,13 @@ namespace smt {
cancel_workers();
}
void parallel::batch_manager::report_assumption_used(ast_translation &l2g, expr *assumption) {
std::scoped_lock lock(mux);
p.m_assumptions_used.insert(l2g(assumption));
}
lbool parallel::batch_manager::get_result() const {
if (m.limit().is_canceled())
return l_undef; // the main context was cancelled, so we return undef.
switch (m_state) {
case state::is_running: // batch manager is still running, but all threads have processed their cubes, which
// means all cubes were unsat
if (!m_search_tree.is_closed())
throw default_exception("inconsistent end state");
if (!p.m_assumptions_used.empty()) {
// collect unsat core from assumptions used, if any --> case when all cubes were unsat, but depend on
// nonempty asms, so we need to add these asms to final unsat core
SASSERT(p.ctx.m_unsat_core.empty());
for (auto a : p.m_assumptions_used)
p.ctx.m_unsat_core.push_back(a);
}
return l_false;
throw default_exception("inconsistent end state");
case state::is_unsat:
return l_false;
case state::is_sat:
@ -500,16 +484,12 @@ namespace smt {
scoped_clear(parallel &p) : p(p) {}
~scoped_clear() {
p.m_workers.reset();
p.m_assumptions_used.reset();
p.m_assumptions.reset();
}
};
scoped_clear clear(*this);
m_batch_manager.initialize();
m_workers.reset();
for (auto e : asms)
m_assumptions.insert(e);
scoped_limits sl(m.limit());
flet<unsigned> _nt(ctx.m_fparams.m_threads, 1);
SASSERT(num_threads > 1);

7
src/smt/smt_parallel.h
View file

@ -79,10 +79,6 @@ namespace smt {
void init_parameters_state();
bool is_assumption(expr* e) const {
return p.m_assumptions.contains(e);
}
public:
batch_manager(ast_manager& m, parallel& p) : m(m), p(p), m_search_tree(expr_ref(m)) { }
@ -98,7 +94,6 @@ namespace smt {
void backtrack(ast_translation& l2g, expr_ref_vector const& core, node* n);
void split(ast_translation& l2g, unsigned id, node* n, expr* atom);
void report_assumption_used(ast_translation& l2g, expr* assumption);
void collect_clause(ast_translation& l2g, unsigned source_worker_id, expr* clause);
expr_ref_vector return_shared_clauses(ast_translation& g2l, unsigned& worker_limit, unsigned worker_id);
@ -162,8 +157,6 @@ namespace smt {
};
obj_hashtable<expr> m_assumptions_used; // assumptions used in unsat cores, to be used in final core
obj_hashtable<expr> m_assumptions; // all assumptions
batch_manager m_batch_manager;
scoped_ptr_vector<worker> m_workers;

202
src/util/search_tree.h
View file

@ -14,7 +14,7 @@ Abstract:
- Closed nodes are fully explored (both children are closed).
- Active nodes have no children and are currently being explored.
- Open nodes either have children that are open or are leaves.
A node can be split if it is active. After splitting, it becomes open and has two open children.
Backtracking on a conflict closes all nodes below the last node whose atom is in the conflict set.
@ -35,25 +35,33 @@ namespace search_tree {
enum class status { open, closed, active };
template<typename Config>
class node {
template <typename Config> class node {
typedef typename Config::literal literal;
literal m_literal;
node* m_left = nullptr, * m_right = nullptr, * m_parent = nullptr;
node *m_left = nullptr, *m_right = nullptr, *m_parent = nullptr;
status m_status;
vector<literal> m_core;
public:
node(literal const& l, node* parent) :
m_literal(l), m_parent(parent), m_status(status::open) {}
node(literal const &l, node *parent) : m_literal(l), m_parent(parent), m_status(status::open) {}
~node() {
dealloc(m_left);
dealloc(m_right);
}
status get_status() const { return m_status; }
void set_status(status s) { m_status = s; }
literal const& get_literal() const { return m_literal; }
bool literal_is_null() const { return Config::is_null(m_literal); }
void split(literal const& a, literal const& b) {
status get_status() const {
return m_status;
}
void set_status(status s) {
m_status = s;
}
literal const &get_literal() const {
return m_literal;
}
bool literal_is_null() const {
return Config::is_null(m_literal);
}
void split(literal const &a, literal const &b) {
SASSERT(!Config::literal_is_null(a));
SASSERT(!Config::literal_is_null(b));
if (m_status != status::active)
@ -78,12 +86,12 @@ namespace search_tree {
return d;
}
node* find_active_node() {
node *find_active_node() {
if (m_status == status::active)
return this;
if (m_status != status::open)
return nullptr;
node* nodes[2] = { m_left, m_right };
node *nodes[2] = {m_left, m_right};
for (unsigned i = 0; i < 2; ++i) {
auto res = nodes[i] ? nodes[i]->find_active_node() : nullptr;
if (res)
@ -94,7 +102,7 @@ namespace search_tree {
return nullptr;
}
void display(std::ostream& out, unsigned indent) const {
void display(std::ostream &out, unsigned indent) const {
for (unsigned i = 0; i < indent; ++i)
out << " ";
Config::display_literal(out, m_literal);
@ -105,10 +113,19 @@ namespace search_tree {
if (m_right)
m_right->display(out, indent + 2);
}
void set_core(vector<literal> const &core) {
m_core = core;
}
vector<literal> const &get_core() const {
return m_core;
}
void clear_core() {
m_core.clear();
}
};
template<typename Config>
class tree {
template <typename Config> class tree {
typedef typename Config::literal literal;
scoped_ptr<node<Config>> m_root = nullptr;
literal m_null_literal;
@ -116,7 +133,7 @@ namespace search_tree {
// return an active node in the subtree rooted at n, or nullptr if there is none
// close nodes that are fully explored (whose children are all closed)
node<Config>* activate_from_root(node<Config>* n) {
node<Config> *activate_from_root(node<Config> *n) {
if (!n)
return nullptr;
if (n->get_status() != status::open)
@ -127,7 +144,7 @@ namespace search_tree {
n->set_status(status::active);
return n;
}
node<Config>* nodes[2] = { left, right };
node<Config> *nodes[2] = {left, right};
unsigned index = m_rand(2);
auto child = activate_from_root(nodes[index]);
if (child)
@ -135,37 +152,75 @@ namespace search_tree {
child = activate_from_root(nodes[1 - index]);
if (child)
return child;
if (left && right && left->get_status() == status::closed && right->get_status() == status::closed)
n->set_status(status::closed);
if (left && right && left->get_status() == status::closed && right->get_status() == status::closed)
n->set_status(status::closed);
return nullptr;
}
void close_node(node<Config>* n) {
if (!n)
return;
if (n->get_status() == status::closed)
void close(node<Config> *n) {
if (!n || n->get_status() == status::closed)
return;
n->set_status(status::closed);
close_node(n->left());
close_node(n->right());
while (n) {
auto p = n->parent();
if (!p)
return;
if (p->get_status() != status::open)
return;
if (p->left()->get_status() != status::closed)
return;
if (p->right()->get_status() != status::closed)
return;
p->set_status(status::closed);
n = p;
close(n->left());
close(n->right());
}
// Invariants:
// Cores labeling nodes are subsets of the literals on the path to the node and the (external) assumption
// literals. If a parent is open, then the one of the children is open.
void close_with_core(node<Config> *n, vector<literal> const &C) {
if (!n || n->get_status() == status::closed)
return;
node<Config> *p = n->parent();
if (p && all_of(C, [n](auto const &l) { return l != n->get_literal(); })) {
close_with_core(p, C);
return;
}
close(n->left());
close(n->right());
n->set_core(C);
n->set_status(status::closed);
if (!p)
return;
auto left = p->left();
auto right = p->right();
if (!left || !right)
return;
// only attempt when both children are closed and each has a core
if (left->get_status() != status::closed || right->get_status() != status::closed)
return;
auto resolvent = compute_sibling_resolvent(left, right);
close_with_core(p, resolvent);
}
// Given complementary sibling nodes for literals x and ¬x, sibling resolvent = (core_left ∪ core_right) \ {x,
// ¬x}
vector<literal> compute_sibling_resolvent(node<Config> *left, node<Config> *right) {
vector<literal> res;
auto &core_l = left->get_core();
auto &core_r = right->get_core();
if (core_l.empty() || core_r.empty() || left->parent() != right->parent())
return res;
auto lit_l = left->get_literal();
auto lit_r = right->get_literal();
for (auto const &lit : core_l)
if (lit != lit_l && !res.contains(lit))
res.push_back(lit);
for (auto const &lit : core_r)
if (lit != lit_r && !res.contains(lit))
res.push_back(lit);
return res;
}
public:
tree(literal const& null_literal) : m_null_literal(null_literal) {
tree(literal const &null_literal) : m_null_literal(null_literal) {
reset();
}
@ -177,51 +232,51 @@ namespace search_tree {
m_root = alloc(node<Config>, m_null_literal, nullptr);
m_root->set_status(status::active);
}
// Split current node if it is active.
// After the call, n is open and has two children.
void split(node<Config>* n, literal const& a, literal const& b) {
void split(node<Config> *n, literal const &a, literal const &b) {
n->split(a, b);
}
// conflict is given by a set of literals.
// they are a subset of literals on the path from root to n
void backtrack(node<Config>* n, vector<literal> const& conflict) {
// they are subsets of the literals on the path from root to n AND the external assumption literals
void backtrack(node<Config> *n, vector<literal> const &conflict) {
if (conflict.empty()) {
close_node(m_root.get());
m_root->set_status(status::closed);
close_with_core(m_root.get(), conflict);
return;
}
}
SASSERT(n != m_root.get());
// all literals in conflict are on the path from root to n
// remove assumptions from conflict to ensure this.
DEBUG_CODE(
auto on_path = [&](literal const& a) {
node<Config>* p = n;
while (p) {
if (p->get_literal() == a)
return true;
p = p->parent();
}
return false;
};
SASSERT(all_of(conflict, [&](auto const& a) { return on_path(a); }));
);
DEBUG_CODE(auto on_path =
[&](literal const &a) {
node<Config> *p = n;
while (p) {
if (p->get_literal() == a)
return true;
p = p->parent();
}
return false;
};
SASSERT(all_of(conflict, [&](auto const &a) { return on_path(a); })););
while (n) {
if (any_of(conflict, [&](auto const& a) { return a == n->get_literal(); })) {
close_node(n);
if (any_of(conflict, [&](auto const &a) { return a == n->get_literal(); })) {
// close the subtree under n (preserves core attached to n), and attempt to resolve upwards
close_with_core(n, conflict);
return;
}
n = n->parent();
}
UNREACHABLE();
}
// return an active node in the tree, or nullptr if there is none
// first check if there is a node to activate under n,
// first check if there is a node to activate under n,
// if not, go up the tree and try to activate a sibling subtree
node<Config>* activate_node(node<Config>* n) {
node<Config> *activate_node(node<Config> *n) {
if (!n) {
if (m_root->get_status() == status::active)
return m_root.get();
@ -233,10 +288,10 @@ namespace search_tree {
auto p = n->parent();
while (p) {
if (p->left() && p->left()->get_status() == status::closed &&
p->right() && p->right()->get_status() == status::closed) {
if (p->left() && p->left()->get_status() == status::closed && p->right() &&
p->right()->get_status() == status::closed) {
p->set_status(status::closed);
n = p;
n = p;
p = n->parent();
continue;
}
@ -250,25 +305,28 @@ namespace search_tree {
res = activate_from_root(p->left());
if (res)
return res;
}
}
n = p;
p = n->parent();
}
return nullptr;
}
node<Config>* find_active_node() {
node<Config> *find_active_node() {
return m_root->find_active_node();
}
vector<literal> const &get_core_from_root() const {
return m_root->get_core();
}
bool is_closed() const {
return m_root->get_status() == status::closed;
}
std::ostream& display(std::ostream& out) const {
std::ostream &display(std::ostream &out) const {
m_root->display(out, 0);
return out;
}
};
}
} // namespace search_tree