mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-23 16:04:35 +00:00
Code Activity

apply formatting

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-10-12 01:00:41 +02:00
parent e4cc27810f
commit e95162b054
1 changed files with 206 additions and 186 deletions
Download patch file Download diff file Expand all files Collapse all files

374
src/util/search_tree.h
View file

@ -35,26 +35,33 @@ namespace search_tree {
enum class status { open, closed, active }; enum class status { open, closed, active };
template<typename Config> template <typename Config> class node {
class node {
typedef typename Config::literal literal; typedef typename Config::literal literal;
literal m_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; status m_status;
vector<literal> m_core; vector<literal> m_core;
public: public:
node(literal const& l, node* parent) : node(literal const &l, node *parent) : m_literal(l), m_parent(parent), m_status(status::open) {}
m_literal(l), m_parent(parent), m_status(status::open) {}
~node() { ~node() {
dealloc(m_left); dealloc(m_left);
dealloc(m_right); dealloc(m_right);
} }
status get_status() const { return m_status; } status get_status() const {
void set_status(status s) { m_status = s; } return m_status;
literal const& get_literal() const { return m_literal; } }
bool literal_is_null() const { return Config::is_null(m_literal); } void set_status(status s) {
void split(literal const& a, literal const& b) { 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(a));
SASSERT(!Config::literal_is_null(b)); SASSERT(!Config::literal_is_null(b));
if (m_status != status::active) if (m_status != status::active)
@ -66,16 +73,22 @@ namespace search_tree {
m_status = status::open; m_status = status::open;
} }
node* left() const { return m_left; } node *left() const {
node* right() const { return m_right; } return m_left;
node* parent() const { return m_parent; } }
node *right() const {
return m_right;
}
node *parent() const {
return m_parent;
}
node* find_active_node() { node *find_active_node() {
if (m_status == status::active) if (m_status == status::active)
return this; return this;
if (m_status != status::open) if (m_status != status::open)
return nullptr; return nullptr;
node* nodes[2] = { m_left, m_right }; node *nodes[2] = {m_left, m_right};
for (unsigned i = 0; i < 2; ++i) { for (unsigned i = 0; i < 2; ++i) {
auto res = nodes[i] ? nodes[i]->find_active_node() : nullptr; auto res = nodes[i] ? nodes[i]->find_active_node() : nullptr;
if (res) if (res)
@ -86,7 +99,7 @@ namespace search_tree {
return nullptr; 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) for (unsigned i = 0; i < indent; ++i)
out << " "; out << " ";
Config::display_literal(out, m_literal); Config::display_literal(out, m_literal);
@ -98,16 +111,21 @@ namespace search_tree {
m_right->display(out, indent + 2); m_right->display(out, indent + 2);
} }
bool has_core() const { return !m_core.empty(); } bool has_core() const {
return !m_core.empty();
}
void set_core(vector<literal> const &core) { void set_core(vector<literal> const &core) {
m_core = core; m_core = core;
} }
vector<literal> const & get_core() const { return m_core; } vector<literal> const &get_core() const {
void clear_core() { m_core.clear(); } return m_core;
}
void clear_core() {
m_core.clear();
}
}; };
template<typename Config> template <typename Config> class tree {
class tree {
typedef typename Config::literal literal; typedef typename Config::literal literal;
scoped_ptr<node<Config>> m_root = nullptr; scoped_ptr<node<Config>> m_root = nullptr;
literal m_null_literal; literal m_null_literal;
@ -115,7 +133,7 @@ namespace search_tree {
// return an active node in the subtree rooted at n, or nullptr if there is none // 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) // 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) if (!n)
return nullptr; return nullptr;
if (n->get_status() != status::open) if (n->get_status() != status::open)
@ -126,7 +144,7 @@ namespace search_tree {
n->set_status(status::active); n->set_status(status::active);
return n; return n;
} }
node<Config>* nodes[2] = { left, right }; node<Config> *nodes[2] = {left, right};
unsigned index = m_rand(2); unsigned index = m_rand(2);
auto child = activate_from_root(nodes[index]); auto child = activate_from_root(nodes[index]);
if (child) if (child)
@ -139,180 +157,182 @@ namespace search_tree {
return nullptr; return nullptr;
} }
void close(node<Config>* n) { void close(node<Config> *n) {
if (!n || n->get_status() == status::closed) if (!n || n->get_status() == status::closed)
return; return;
n->set_status(status::closed); n->set_status(status::closed);
close(n->left); close(n->left);
close(n->right); close(n->right);
} }
// Invariants: // Invariants:
// Cores labeling nodes are subsets of the literals on the path to the node and the (external) assumption literals. // Cores labeling nodes are subsets of the literals on the path to the node and the (external) assumption
// If a parent is open, then the one of the children is open. // 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) { void close_with_core(node<Config> *n, vector<literal> const &C) {
if (!n || n->get_status() == status::closed) if (!n || n->get_status() == status::closed)
return; return;
node<Config>* p = n->parent(); node<Config> *p = n->parent();
if (p && any_of(C, [](auto const& l) { return l == n->get_literal(); }})) { if (p && any_of(C, [](auto const& l) {
close_with_core(p, C); return l == n->get_literal(); }
return; })) {
} close_with_core(p, C);
close(n->left()); return;
close(n->right());
n->set_core(C);
n->set_status(status::closed);
if (p)
try_resolve_upwards(p);
}
// 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_l && !res.contains(lit))
res.push_back(lit);
return res;
}
void try_resolve_upwards(node<Config>* p) {
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);
}
public:
tree(literal const& null_literal) : m_null_literal(null_literal) {
reset();
} }
close(n->left());
close(n->right());
n->set_core(C);
n->set_status(status::closed);
void set_seed(unsigned seed) { if (p)
m_rand.set_seed(seed); try_resolve_upwards(p);
}
// 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_l && !res.contains(lit))
res.push_back(lit);
return res;
}
void try_resolve_upwards(node<Config> *p) {
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);
}
public:
tree(literal const &null_literal) : m_null_literal(null_literal) {
reset();
}
void set_seed(unsigned seed) {
m_rand.set_seed(seed);
}
void reset() {
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) {
n->split(a, b);
}
// conflict is given by a set of literals.
// 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_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); })););
void reset() { while (n) {
m_root = alloc(node<Config>, m_null_literal, nullptr); if (any_of(conflict, [&](auto const &a) { return a == n->get_literal(); })) {
m_root->set_status(status::active); // close the subtree under n (preserves core attached to n), and attempt to resolve upwards
} close_with_core(n, conflict);
// 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) {
n->split(a, b);
}
// conflict is given by a set of literals.
// 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_with_core(m_root.get(), conflict);
return; 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); }));
);
while (n) { n = n->parent();
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();
} }
UNREACHABLE();
}
// return an active node in the tree, or nullptr if there is none // 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 // 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 (!n) {
if (m_root->get_status() == status::active) if (m_root->get_status() == status::active)
return m_root.get(); return m_root.get();
n = m_root.get(); n = m_root.get();
} }
auto res = activate_from_root(n); auto res = activate_from_root(n);
if (res) if (res)
return res; return res;
auto p = n->parent(); auto p = n->parent();
while (p) { while (p) {
if (p->left() && p->left()->get_status() == status::closed && if (p->left() && p->left()->get_status() == status::closed && p->right() &&
p->right() && p->right()->get_status() == status::closed) { p->right()->get_status() == status::closed) {
p->set_status(status::closed); p->set_status(status::closed);
n = p;
p = n->parent();
continue;
}
if (n == p->left()) {
res = activate_from_root(p->right());
if (res)
return res;
}
else {
VERIFY(n == p->right());
res = activate_from_root(p->left());
if (res)
return res;
}
n = p; n = p;
p = n->parent(); p = n->parent();
continue;
} }
return nullptr; if (n == p->left()) {
res = activate_from_root(p->right());
if (res)
return res;
}
else {
VERIFY(n == p->right());
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(); return m_root->find_active_node();
} }
vector<literal> const& get_core_from_root() const { vector<literal> const &get_core_from_root() const {
return m_root->get_core(); return m_root->get_core();
} }
bool is_closed() const { bool is_closed() const {
return m_root->get_status() == status::closed; 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); m_root->display(out, 0);
return out; return out;
} }
}; };
} }