mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-08 17:01:55 +00:00
Code Activity

clean up a little

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-09-07 19:01:51 -07:00
parent 3fd8d2cd8c
commit a119c0d864
1 changed files with 6 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

14
src/util/search_tree.h
View file

@ -54,6 +54,8 @@ namespace search_tree {
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)
return;
SASSERT(!m_left);
@ -136,13 +138,8 @@ namespace search_tree {
// 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) {
SASSERT(!Config::literal_is_null(a));
SASSERT(!Config::literal_is_null(b));
if (n->get_status() == status::active) {
n->split(a, b);
n->set_status(status::open);
}
void split(node<Config>* n, literal const& a, literal const& b) {
n->split(a, b);
}
// conflict is given by a set of literals.
@ -155,6 +152,7 @@ namespace search_tree {
}
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;
@ -226,4 +224,4 @@ namespace search_tree {
}
};
}
}