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

fix build issues

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-10-12 06:56:15 +02:00
parent 94cdbe5d87
commit c5d65cdedd
2 changed files with 146 additions and 164 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/smt/smt_parallel.cpp
View file

@ -412,17 +412,7 @@ namespace smt {
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");
// case when all cubes were unsat, but depend on nonempty asms, so we need to add these asms to final unsat core
// these asms are stored in the cube tree, at the root node
if (p.ctx.m_unsat_core.empty()) {
SASSERT(root && root->is_closed());
for (auto a : m_search_tree.get_core_from_root())
p.ctx.m_unsat_core.push_back(a);
}
return l_false;
case state::is_unsat:
return l_false;
case state::is_sat:

48
src/util/search_tree.h
View file

@ -111,9 +111,6 @@ namespace search_tree {
m_right->display(out, indent + 2);
}
bool has_core() const {
return !m_core.empty();
}
void set_core(vector<literal> const &core) {
m_core = core;
}
@ -161,8 +158,8 @@ namespace search_tree {
if (!n || n->get_status() == status::closed)
return;
n->set_status(status::closed);
close(n->left);
close(n->right);
close(n->left());
close(n->right());
}
// Invariants:
@ -172,8 +169,7 @@ namespace search_tree {
if (!n || n->get_status() == status::closed)
return;
node<Config> *p = n->parent();
if (p && any_of(C, [n](auto const& l) {
return l == n->get_literal(); })) {
if (p && all_of(C, [n](auto const &l) { return l != n->get_literal(); })) {
close_with_core(p, C);
return;
}
@ -182,13 +178,24 @@ namespace search_tree {
n->set_core(C);
n->set_status(status::closed);
if (p)
try_resolve_upwards(p);
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) {
// 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();
@ -209,20 +216,6 @@ namespace search_tree {
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();
@ -332,6 +325,5 @@ public:
m_root->display(out, 0);
return out;
}
};
}
} // namespace search_tree