mirror of
https://github.com/Z3Prover/z3
synced 2025-04-29 03:45:51 +00:00
wip
This commit is contained in:
Nikolaj Bjorner
parent
8e70112832
commit
807121aa03
5 changed files with 212 additions and 24 deletions
|
|
@ -649,6 +649,7 @@ public:
|
|||
}
|
||||
}
|
||||
|
||||
|
||||
void max_resolve(exprs const& core, rational const& w) {
|
||||
SASSERT(!core.empty());
|
||||
expr_ref fml(m), asum(m);
|
||||
|
|
@ -699,6 +700,88 @@ public:
|
|||
}
|
||||
}
|
||||
|
||||
#if 0
|
||||
|
||||
void bin_max_resolve(exprs const& _core, rational const& w) {
|
||||
expr_ref_vector core(m, _core.size(), _core.data());
|
||||
expr_ref fml(m), cls(m);
|
||||
for (unsigned i = 0; i + 1 < core.size(); ++i) {
|
||||
expr* a = core.get(i);
|
||||
expr* b = core.get(i + 1);
|
||||
expr_ref u = mk_fresh_bool("u");
|
||||
expr_ref v = mk_fresh_bool("v");
|
||||
// u = a or b
|
||||
// v = a and b
|
||||
cls = m.mk_or(a, b);
|
||||
fml = m.mk_implies(u, cls);
|
||||
add(fml);
|
||||
update_model(u, cls);
|
||||
m_defs.push_back(fml);
|
||||
cls = m.mk_and(a, b);
|
||||
fml = m.mk_implies(v, cls);
|
||||
add(fml);
|
||||
update_model(v, cls);
|
||||
m_defs.push_back(fml);
|
||||
new_assumption(u, w);
|
||||
core.push_back(v);
|
||||
}
|
||||
}
|
||||
|
||||
struct unfold_record {
|
||||
ptr_vector<expr> ws;
|
||||
rational weight;
|
||||
};
|
||||
|
||||
void bin_delay_max_resolve(exprs const& _core, rational const& w) {
|
||||
expr_ref_vector core(m, _core.size(), _core.data()), us(m), partial(m);
|
||||
expr_ref fml(m), cls(m);
|
||||
for (expr* c : core) {
|
||||
unfold_record ws;
|
||||
if (!m_unfold.find(c, ws))
|
||||
continue;
|
||||
for (expr* f : ws.ws)
|
||||
new_assumption(f, ws.weight);
|
||||
}
|
||||
if (core.size() <= 1)
|
||||
return;
|
||||
|
||||
for (expr* core)
|
||||
partial.push_back(nullptr);
|
||||
|
||||
for (unsigned i = 0; i + 1 < core.size(); ++i) {
|
||||
expr* a = core.get(i);
|
||||
expr* b = core.get(i + 1);
|
||||
expr_ref u = mk_fresh_bool("u");
|
||||
expr_ref v = mk_fresh_bool("v");
|
||||
// u = a or b
|
||||
// v = a and b
|
||||
cls = m.mk_or(a, b);
|
||||
fml = m.mk_implies(u, cls);
|
||||
add(fml);
|
||||
update_model(u, cls);
|
||||
m_defs.push_back(fml);
|
||||
cls = m.mk_and(a, b);
|
||||
fml = m.mk_implies(v, cls);
|
||||
add(fml);
|
||||
update_model(v, cls);
|
||||
m_defs.push_back(fml);
|
||||
us.push_back(u);
|
||||
core.push_back(v);
|
||||
|
||||
unfold_record r;
|
||||
r.ws.push_back(u);
|
||||
if (partial.get(i))
|
||||
r.ws.push_back(partia.get(i));
|
||||
if (partial.get(i + 1))
|
||||
r.ws.push_back(partia.get(i + 1));
|
||||
partial.push_back(m.mk_and(r.ws));
|
||||
m_unfold.insert(partial.back(), r);
|
||||
}
|
||||
expr_ref u = mk_and(us);
|
||||
new_assumption(u, w);
|
||||
}
|
||||
#endif
|
||||
|
||||
// cs is a correction set (a complement of a (maximal) satisfying assignment).
|
||||
void cs_max_resolve(exprs const& cs, rational const& w) {
|
||||
if (cs.empty()) return;
|
||||
|
|
|
|||
|
|
@ -20,9 +20,93 @@ Author:
|
|||
#pragma once
|
||||
|
||||
#include "opt/opt_preprocess.h"
|
||||
#include "util/max_cliques.h"
|
||||
|
||||
namespace opt {
|
||||
|
||||
expr_ref_vector preprocess::propagate(expr* f, lbool& is_sat) {
|
||||
expr_ref_vector asms(m);
|
||||
asms.push_back(f);
|
||||
is_sat = s.check_sat(asms);
|
||||
return s.get_trail(1);
|
||||
}
|
||||
|
||||
bool preprocess::prop_mutexes(vector<soft>& softs, rational& lower) {
|
||||
expr_ref_vector fmls(m);
|
||||
obj_map<expr, rational> new_soft = soft2map(softs, fmls);
|
||||
|
||||
params_ref p;
|
||||
p.set_uint("max_conflicts", 1);
|
||||
s.updt_params(p);
|
||||
|
||||
obj_hashtable<expr> pfmls, nfmls;
|
||||
for (expr* f : fmls)
|
||||
if (m.is_not(f, f))
|
||||
nfmls.insert(f);
|
||||
else
|
||||
pfmls.insert(f);
|
||||
|
||||
u_map<expr*> ids;
|
||||
unsigned_vector ps;
|
||||
for (expr* f : fmls) {
|
||||
ids.insert(f->get_id(), f);
|
||||
ps.push_back(f->get_id());
|
||||
}
|
||||
|
||||
u_map<uint_set> conns;
|
||||
|
||||
for (expr* f : fmls) {
|
||||
lbool is_sat;
|
||||
expr_ref_vector trail = propagate(f, is_sat);
|
||||
if (is_sat == l_false) {
|
||||
rational w = new_soft[f];
|
||||
lower += w;
|
||||
s.assert_expr(m.mk_not(f));
|
||||
new_soft.remove(f);
|
||||
continue;
|
||||
}
|
||||
|
||||
expr_ref_vector mux(m);
|
||||
for (expr* g : trail) {
|
||||
if (m.is_not(g, g)) {
|
||||
if (pfmls.contains(g))
|
||||
mux.push_back(g);
|
||||
}
|
||||
else if (nfmls.contains(g))
|
||||
mux.push_back(m.mk_not(g));
|
||||
}
|
||||
uint_set reach;
|
||||
for (expr* g : mux)
|
||||
reach.insert(g->get_id());
|
||||
conns.insert(f->get_id(), reach);
|
||||
}
|
||||
|
||||
p.set_uint("max_conflicts", UINT_MAX);
|
||||
s.updt_params(p);
|
||||
|
||||
struct neg_literal {
|
||||
unsigned negate(unsigned id) {
|
||||
throw default_exception("unexpected call");
|
||||
}
|
||||
};
|
||||
max_cliques<neg_literal> mc;
|
||||
vector<unsigned_vector> mutexes;
|
||||
mc.cliques(ps, conns, mutexes);
|
||||
|
||||
for (auto& mux : mutexes) {
|
||||
expr_ref_vector _mux(m);
|
||||
for (auto p : mux)
|
||||
_mux.push_back(ids[p]);
|
||||
process_mutex(_mux, new_soft, lower);
|
||||
}
|
||||
|
||||
softs.reset();
|
||||
for (auto const& [k, v] : new_soft)
|
||||
softs.push_back(soft(expr_ref(k, m), v, false));
|
||||
m_trail.reset();
|
||||
return true;
|
||||
}
|
||||
|
||||
obj_map<expr, rational> preprocess::soft2map(vector<soft> const& softs, expr_ref_vector& fmls) {
|
||||
obj_map<expr, rational> new_soft;
|
||||
for (soft const& sf : softs) {
|
||||
|
|
@ -104,6 +188,8 @@ namespace opt {
|
|||
bool preprocess::operator()(vector<soft>& soft, rational& lower) {
|
||||
if (!find_mutexes(soft, lower))
|
||||
return false;
|
||||
if (false && !prop_mutexes(soft, lower))
|
||||
return false;
|
||||
return true;
|
||||
}
|
||||
};
|
||||
|
|
|
|||
|
|
@ -28,8 +28,10 @@ namespace opt {
|
|||
solver& s;
|
||||
expr_ref_vector m_trail;
|
||||
|
||||
expr_ref_vector propagate(expr* f, lbool& is_sat);
|
||||
obj_map<expr, rational> soft2map(vector<soft> const& softs, expr_ref_vector& fmls);
|
||||
bool find_mutexes(vector<soft>& softs, rational& lower);
|
||||
bool prop_mutexes(vector<soft>& softs, rational& lower);
|
||||
void process_mutex(expr_ref_vector& mutex, obj_map<expr, rational>& new_soft, rational& lower);
|
||||
|
||||
public:
|
||||
|
|
|
|||
|
|
@ -612,7 +612,7 @@ namespace smt {
|
|||
}
|
||||
}
|
||||
vector<unsigned_vector> _mutexes;
|
||||
mc.cliques(ps, _mutexes);
|
||||
mc.cliques2(ps, _mutexes);
|
||||
for (auto const& mux : _mutexes) {
|
||||
expr_ref_vector lits(m);
|
||||
for (unsigned idx : mux) {
|
||||
|
|
|
|||
|
|
@ -83,6 +83,29 @@ class max_cliques : public T {
|
|||
m_next.reserve(max);
|
||||
m_tc.reserve(m_next.size());
|
||||
}
|
||||
|
||||
struct compare_degree {
|
||||
u_map<uint_set>& conns;
|
||||
compare_degree(u_map<uint_set>& conns): conns(conns) {}
|
||||
bool operator()(unsigned x, unsigned y) const {
|
||||
return conns[x].num_elems() < conns[y].num_elems();
|
||||
}
|
||||
};
|
||||
|
||||
|
||||
void init(unsigned_vector const& ps, u_map<uint_set>& conns) {
|
||||
|
||||
uint_set vars;
|
||||
|
||||
for (unsigned p : ps)
|
||||
vars.insert(p);
|
||||
|
||||
for (unsigned v : ps) {
|
||||
uint_set reach;
|
||||
get_reachable(v, vars, reach);
|
||||
conns.insert(v, reach);
|
||||
}
|
||||
}
|
||||
|
||||
public:
|
||||
void add_edge(unsigned src, unsigned dst) {
|
||||
|
|
@ -92,7 +115,7 @@ public:
|
|||
m_next[dst].push_back(src);
|
||||
}
|
||||
|
||||
void cliques(unsigned_vector const& ps, vector<unsigned_vector>& cliques) {
|
||||
void cliques1(unsigned_vector const& ps, vector<unsigned_vector>& cliques) {
|
||||
init(ps);
|
||||
unsigned_vector clique;
|
||||
uint_set vars;
|
||||
|
|
@ -124,35 +147,29 @@ public:
|
|||
}
|
||||
}
|
||||
|
||||
|
||||
// better quality cliques
|
||||
void cliques2(unsigned_vector const& ps, vector<unsigned_vector>& cliques) {
|
||||
|
||||
uint_set all_vars, todo;
|
||||
void cliques2(unsigned_vector const& ps, vector<unsigned_vector>& cs) {
|
||||
u_map<uint_set> conns;
|
||||
|
||||
init(ps);
|
||||
// compute connections using TC of implication graph
|
||||
init(ps, conns);
|
||||
cliques(ps, conns, cs);
|
||||
}
|
||||
|
||||
struct compare_degree {
|
||||
u_map<uint_set>& conns;
|
||||
compare_degree(u_map<uint_set>& conns): conns(conns) {}
|
||||
bool operator()(unsigned x, unsigned y) const {
|
||||
return conns[x].num_elems() < conns[y].num_elems();
|
||||
}
|
||||
};
|
||||
// cliques after connections are computed.
|
||||
void cliques(unsigned_vector const& ps, u_map<uint_set>& conns, vector<unsigned_vector>& cliques) {
|
||||
|
||||
unsigned maxp = 1;
|
||||
for (unsigned p : ps)
|
||||
maxp = std::max(p, maxp);
|
||||
|
||||
uint_set todo;
|
||||
compare_degree lt(conns);
|
||||
heap<compare_degree> heap(m_next.size(), lt);
|
||||
heap<compare_degree> heap(maxp + 1, lt);
|
||||
|
||||
for (unsigned p : ps) {
|
||||
all_vars.insert(p);
|
||||
for (unsigned p : ps) {
|
||||
todo.insert(p);
|
||||
}
|
||||
|
||||
for (unsigned v : ps) {
|
||||
uint_set reach;
|
||||
get_reachable(v, all_vars, reach);
|
||||
conns.insert(v, reach);
|
||||
heap.insert(v);
|
||||
heap.insert(p);
|
||||
}
|
||||
|
||||
while (!todo.empty()) {
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue