mirror of
https://github.com/Z3Prover/z3
synced 2025-10-31 03:32:28 +00:00
Merge branch 'parallel' into param-tuning
This commit is contained in:
Ilana Shapiro
GitHub
commit
39ec6764b6
2 changed files with 122 additions and 189 deletions
|
|
@ -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:
|
||||
|
|
|
|||
|
|
@ -35,26 +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)
|
||||
|
|
@ -66,16 +73,22 @@ namespace search_tree {
|
|||
m_status = status::open;
|
||||
}
|
||||
|
||||
node* left() const { return m_left; }
|
||||
node* right() const { return m_right; }
|
||||
node* parent() const { return m_parent; }
|
||||
node *left() const {
|
||||
return m_left;
|
||||
}
|
||||
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)
|
||||
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)
|
||||
|
|
@ -86,7 +99,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);
|
||||
|
|
@ -98,16 +111,18 @@ 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;
|
||||
}
|
||||
vector<literal> const & get_core() const { return m_core; }
|
||||
void clear_core() { m_core.clear(); }
|
||||
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;
|
||||
|
|
@ -115,7 +130,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)
|
||||
|
|
@ -126,7 +141,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)
|
||||
|
|
@ -139,140 +154,70 @@ namespace search_tree {
|
|||
return nullptr;
|
||||
}
|
||||
|
||||
// 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, bool allow_resolve = true) {
|
||||
void close(node<Config> *n) {
|
||||
if (!n || n->get_status() == status::closed)
|
||||
return;
|
||||
n->set_status(status::closed);
|
||||
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);
|
||||
|
||||
close_with_core(n->left(), C, false);
|
||||
close_with_core(n->right(), C, false);
|
||||
if (!p)
|
||||
return;
|
||||
auto left = p->left();
|
||||
auto right = p->right();
|
||||
if (!left || !right)
|
||||
return;
|
||||
|
||||
// stop at root
|
||||
if (!n->parent()) 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;
|
||||
|
||||
node<Config>* p = n->parent();
|
||||
if (!p) return; // root reached
|
||||
|
||||
auto is_literal_in_core = [](literal const& l, vector<literal> const& C) {
|
||||
for (unsigned i = 0; i < C.size(); ++i)
|
||||
if (C[i] == l) return true;
|
||||
return false;
|
||||
};
|
||||
|
||||
// case 1: current splitting literal not in the conflict core
|
||||
if (!is_literal_in_core(n->get_literal(), C)) {
|
||||
close_with_core(p, C);
|
||||
// case 2: both siblings closed -> resolve
|
||||
} else if (allow_resolve && p->left()->get_status() == status::closed && p->right()->get_status() == status::closed) {
|
||||
try_resolve_upwards(p);
|
||||
}
|
||||
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;
|
||||
|
||||
if (!left->has_core() || !right->has_core()) return res;
|
||||
|
||||
bool are_sibling_complements = left->parent() == right->parent();
|
||||
if (!are_sibling_complements)
|
||||
return res;
|
||||
|
||||
auto &core_l = left->get_core();
|
||||
auto &core_r = right->get_core();
|
||||
|
||||
auto contains = [](vector<literal> const &v, literal const &l) {
|
||||
for (unsigned i = 0; i < v.size(); ++i)
|
||||
if (v[i] == l) return true;
|
||||
return false;
|
||||
};
|
||||
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();
|
||||
|
||||
// Add literals from left core, skipping lit_l
|
||||
for (unsigned i = 0; i < core_l.size(); ++i) {
|
||||
if (core_l[i] != lit_l && !contains(res, core_l[i]))
|
||||
res.push_back(core_l[i]);
|
||||
}
|
||||
|
||||
// Add literals from right core, skipping lit_r
|
||||
for (unsigned i = 0; i < core_r.size(); ++i) {
|
||||
if (core_r[i] != lit_r && !contains(res, core_r[i]))
|
||||
res.push_back(core_r[i]);
|
||||
}
|
||||
|
||||
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) {
|
||||
while (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;
|
||||
if (!left->has_core() || !right->has_core()) return;
|
||||
|
||||
auto resolvent = compute_sibling_resolvent(left, right);
|
||||
|
||||
// empty resolvent of sibling complement (i.e. tautology) -> global UNSAT
|
||||
if (resolvent.empty()) {
|
||||
close_with_core(m_root.get(), resolvent, false);
|
||||
return;
|
||||
}
|
||||
|
||||
// if p already has the same core, nothing more to do
|
||||
if (p->has_core() && resolvent == p->get_core())
|
||||
return;
|
||||
|
||||
// Bubble to the highest ancestor where ALL literals in the resolvent
|
||||
// are present somewhere on the path from that ancestor to root
|
||||
node<Config>* candidate = p;
|
||||
node<Config>* attach_here = p; // fallback
|
||||
|
||||
while (candidate) {
|
||||
bool all_found = true;
|
||||
|
||||
for (auto const& r : resolvent) {
|
||||
bool found = false;
|
||||
for (node<Config>* q = candidate; q; q = q->parent()) {
|
||||
if (q->get_literal() == r) {
|
||||
found = true;
|
||||
break;
|
||||
}
|
||||
}
|
||||
if (!found) {
|
||||
all_found = false;
|
||||
break;
|
||||
}
|
||||
}
|
||||
|
||||
if (all_found) {
|
||||
attach_here = candidate; // bubble up to this node
|
||||
}
|
||||
|
||||
candidate = candidate->parent();
|
||||
}
|
||||
|
||||
// attach the resolvent and close the subtree at attach_here
|
||||
if (!attach_here->has_core() || attach_here->get_core() != resolvent) {
|
||||
close_with_core(attach_here, resolvent, false);
|
||||
}
|
||||
|
||||
// continue upward from parent of attach_here
|
||||
p = attach_here->parent();
|
||||
}
|
||||
}
|
||||
|
||||
public:
|
||||
tree(literal const& null_literal) : m_null_literal(null_literal) {
|
||||
tree(literal const &null_literal) : m_null_literal(null_literal) {
|
||||
reset();
|
||||
}
|
||||
|
||||
|
|
@ -287,13 +232,13 @@ 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) {
|
||||
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) {
|
||||
void backtrack(node<Config> *n, vector<literal> const &conflict) {
|
||||
if (conflict.empty()) {
|
||||
close_with_core(m_root.get(), conflict);
|
||||
return;
|
||||
|
|
@ -301,9 +246,9 @@ 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;
|
||||
DEBUG_CODE(auto on_path =
|
||||
[&](literal const &a) {
|
||||
node<Config> *p = n;
|
||||
while (p) {
|
||||
if (p->get_literal() == a)
|
||||
return true;
|
||||
|
|
@ -311,11 +256,10 @@ namespace search_tree {
|
|||
}
|
||||
return false;
|
||||
};
|
||||
SASSERT(all_of(conflict, [&](auto const& a) { return on_path(a); }));
|
||||
);
|
||||
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(); })) {
|
||||
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;
|
||||
|
|
@ -329,7 +273,7 @@ namespace search_tree {
|
|||
// return an active node in the tree, or nullptr if there is none
|
||||
// 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();
|
||||
|
|
@ -341,8 +285,8 @@ 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;
|
||||
p = n->parent();
|
||||
|
|
@ -365,11 +309,11 @@ namespace search_tree {
|
|||
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 {
|
||||
vector<literal> const &get_core_from_root() const {
|
||||
return m_root->get_core();
|
||||
}
|
||||
|
||||
|
|
@ -377,10 +321,9 @@ namespace search_tree {
|
|||
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
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue