mirror of
https://github.com/Z3Prover/z3
synced 2025-10-31 11:42:28 +00:00
integrate asms directly into cube tree, remove separate tracking
This commit is contained in:
Ilana Shapiro
parent
f75d137911
commit
e2432b0d50
3 changed files with 48 additions and 52 deletions
|
|
@ -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);
|
||||
|
|
@ -260,8 +256,7 @@ 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);
|
||||
|
||||
|
|
@ -411,11 +406,6 @@ 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.
|
||||
|
|
@ -424,11 +414,12 @@ namespace smt {
|
|||
// 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)
|
||||
|
||||
// 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;
|
||||
|
|
@ -496,16 +487,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);
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
|
||||
|
|
|
|||
|
|
@ -139,26 +139,43 @@ namespace search_tree {
|
|||
return nullptr;
|
||||
}
|
||||
|
||||
void close_node(node<Config>* n) {
|
||||
// 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(node<Config>* n, vector<literal> const &C) {
|
||||
if (!n)
|
||||
return;
|
||||
if (n->get_status() == status::closed)
|
||||
return;
|
||||
|
||||
n->set_core(C);
|
||||
|
||||
// label n and its children as closed
|
||||
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;
|
||||
|
||||
// is it ok to pass C here? I think it should work, but semantically it may attach an irrelevant core to children that never actually produced that conflict
|
||||
close(n->left(), C);
|
||||
close(n->right(), C);
|
||||
|
||||
// stop at root
|
||||
if (!n->parent())
|
||||
return;
|
||||
|
||||
node<Config>* p = n->parent();
|
||||
|
||||
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(p, C);
|
||||
// case 2: both siblings closed -> resolve
|
||||
} else if (p->left()->get_status() == status::closed && p->right()->get_status() == status::closed) {
|
||||
auto Cp = compute_sibling_resolvent(p->left(), p->right());
|
||||
close(p, Cp);
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -213,8 +230,7 @@ namespace search_tree {
|
|||
|
||||
// empty resolvent of sibling complement (i.e. tautology) -> global UNSAT
|
||||
if (resolvent.empty()) {
|
||||
m_root->set_core(resolvent);
|
||||
close_node(m_root.get());
|
||||
close(m_root.get(), resolvent);
|
||||
return;
|
||||
}
|
||||
|
||||
|
|
@ -253,8 +269,7 @@ namespace search_tree {
|
|||
|
||||
// attach the resolvent and close the subtree at attach_here
|
||||
if (!attach_here->has_core() || attach_here->get_core() != resolvent) {
|
||||
attach_here->set_core(resolvent);
|
||||
close_node(attach_here);
|
||||
close(attach_here, resolvent);
|
||||
}
|
||||
|
||||
// continue upward from parent of attach_here
|
||||
|
|
@ -284,11 +299,10 @@ namespace search_tree {
|
|||
}
|
||||
|
||||
// conflict is given by a set of literals.
|
||||
// they are a subset of literals on the path from root to n
|
||||
// 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()) {
|
||||
m_root->set_core(conflict);
|
||||
close_node(m_root.get());
|
||||
close(m_root.get(), conflict);
|
||||
return;
|
||||
}
|
||||
SASSERT(n != m_root.get());
|
||||
|
|
@ -309,10 +323,8 @@ namespace search_tree {
|
|||
|
||||
while (n) {
|
||||
if (any_of(conflict, [&](auto const& a) { return a == n->get_literal(); })) {
|
||||
n->set_core(conflict);
|
||||
|
||||
// close the subtree under n (preserves core attached to n), and attempt to resolve upwards
|
||||
close_node(n);
|
||||
close(n, conflict);
|
||||
try_resolve_upwards(n->parent());
|
||||
return;
|
||||
}
|
||||
|
|
@ -365,6 +377,10 @@ namespace search_tree {
|
|||
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;
|
||||
}
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue