mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 02:15:19 +00:00
totalizer
This commit is contained in:
parent
959a0ba370
commit
94a2477fa0
|
@ -85,7 +85,6 @@ public:
|
|||
s_primal_dual,
|
||||
s_primal_binary,
|
||||
s_rc2,
|
||||
s_rc2tot,
|
||||
s_primal_binary_rc2
|
||||
};
|
||||
private:
|
||||
|
@ -136,6 +135,7 @@ private:
|
|||
bool m_enable_lns = false; // enable LNS improvements
|
||||
unsigned m_lns_conflicts = 1000; // number of conflicts used for LNS improvement
|
||||
bool m_enable_core_rotate = false; // enable core rotation
|
||||
bool m_use_totalizer = true; // use totalizer instead of cardinality encoding
|
||||
std::string m_trace_id;
|
||||
typedef ptr_vector<expr> exprs;
|
||||
|
||||
|
@ -165,9 +165,6 @@ public:
|
|||
case s_rc2:
|
||||
m_trace_id = "rc2";
|
||||
break;
|
||||
case s_rc2tot:
|
||||
m_trace_id = "rc2tot";
|
||||
break;
|
||||
case s_primal_binary_rc2:
|
||||
m_trace_id = "rc2bin";
|
||||
break;
|
||||
|
@ -177,7 +174,10 @@ public:
|
|||
}
|
||||
}
|
||||
|
||||
~maxcore() override {}
|
||||
~maxcore() override {
|
||||
for (auto& [k,t] : m_totalizers)
|
||||
dealloc(t);
|
||||
}
|
||||
|
||||
bool is_literal(expr* l) {
|
||||
return
|
||||
|
@ -374,7 +374,6 @@ public:
|
|||
case s_primal:
|
||||
case s_primal_binary:
|
||||
case s_rc2:
|
||||
case s_rc2tot:
|
||||
case s_primal_binary_rc2:
|
||||
return mus_solver();
|
||||
case s_primal_dual:
|
||||
|
@ -567,7 +566,6 @@ public:
|
|||
bin_max_resolve(core, w);
|
||||
break;
|
||||
case strategy_t::s_rc2:
|
||||
case strategy_t::s_rc2tot:
|
||||
max_resolve_rc2(core, w);
|
||||
break;
|
||||
case strategy_t::s_primal_binary_rc2:
|
||||
|
@ -820,7 +818,7 @@ public:
|
|||
}
|
||||
|
||||
expr* mk_atmost(expr_ref_vector const& es, unsigned bound, rational const& weight) {
|
||||
if (m_st == strategy_t::s_rc2tot)
|
||||
if (m_use_totalizer)
|
||||
return mk_atmost_tot(es, bound, weight);
|
||||
pb_util pb(m);
|
||||
expr_ref am(pb.mk_at_most_k(es, bound), m);
|
||||
|
@ -1064,6 +1062,7 @@ public:
|
|||
m_enable_lns = p.enable_lns();
|
||||
m_enable_core_rotate = p.enable_core_rotate();
|
||||
m_lns_conflicts = p.lns_conflicts();
|
||||
m_use_totalizer = p.rc2_totalizer();
|
||||
if (m_c.num_objectives() > 1)
|
||||
m_add_upper_bound_block = false;
|
||||
}
|
||||
|
@ -1152,10 +1151,6 @@ opt::maxsmt_solver_base* opt::mk_rc2(
|
|||
return alloc(maxcore, c, id, soft, maxcore::s_rc2);
|
||||
}
|
||||
|
||||
opt::maxsmt_solver_base* opt::mk_rc2tot(
|
||||
maxsat_context& c, unsigned id, vector<soft>& soft) {
|
||||
return alloc(maxcore, c, id, soft, maxcore::s_rc2tot);
|
||||
}
|
||||
|
||||
opt::maxsmt_solver_base* opt::mk_rc2bin(
|
||||
maxsat_context& c, unsigned id, vector<soft>& soft) {
|
||||
|
|
|
@ -23,8 +23,6 @@ namespace opt {
|
|||
|
||||
maxsmt_solver_base* mk_rc2(maxsat_context& c, unsigned id, vector<soft>& soft);
|
||||
|
||||
maxsmt_solver_base* mk_rc2tot(maxsat_context& c, unsigned id, vector<soft>& soft);
|
||||
|
||||
maxsmt_solver_base* mk_rc2bin(maxsat_context& c, unsigned id, vector<soft>& soft);
|
||||
|
||||
maxsmt_solver_base* mk_maxres(maxsat_context& c, unsigned id, vector<soft>& soft);
|
||||
|
|
|
@ -193,8 +193,6 @@ namespace opt {
|
|||
m_msolver = mk_maxres_binary(m_c, m_index, m_soft);
|
||||
else if (maxsat_engine == symbol("rc2"))
|
||||
m_msolver = mk_rc2(m_c, m_index, m_soft);
|
||||
else if (maxsat_engine == symbol("rc2tot"))
|
||||
m_msolver = mk_rc2tot(m_c, m_index, m_soft);
|
||||
else if (maxsat_engine == symbol("rc2bin"))
|
||||
m_msolver = mk_rc2bin(m_c, m_index, m_soft);
|
||||
else if (maxsat_engine == symbol("pd-maxres"))
|
||||
|
|
|
@ -19,6 +19,7 @@ def_module_params('opt',
|
|||
('pb.compile_equality', BOOL, False, 'compile arithmetical equalities into pseudo-Boolean equality (instead of two inequalites)'),
|
||||
('pp.wcnf', BOOL, False, 'print maxsat benchmark into wcnf format'),
|
||||
('maxlex.enable', BOOL, True, 'enable maxlex heuristic for lexicographic MaxSAT problems'),
|
||||
('rc2.totalizer', BOOL, True, 'use totalizer for rc2 encoding'),
|
||||
('maxres.hill_climb', BOOL, True, 'give preference for large weight cores'),
|
||||
('maxres.add_upper_bound_block', BOOL, False, 'restict upper bound with constraint'),
|
||||
('maxres.max_num_cores', UINT, 200, 'maximal number of cores per round'),
|
||||
|
|
|
@ -37,7 +37,7 @@ namespace opt {
|
|||
expr_ref c(m), def(m);
|
||||
expr_ref_vector ors(m), clause(m);
|
||||
for (unsigned i = k; i > 0 && !lits.get(i - 1); --i) {
|
||||
if (l->m_literals.size() + r->m_literals.size() < i) {
|
||||
if (l->size() + r->size() < i) {
|
||||
lits[i - 1] = m.mk_false();
|
||||
continue;
|
||||
}
|
||||
|
@ -55,9 +55,9 @@ namespace opt {
|
|||
|
||||
for (unsigned j1 = 0; j1 <= i; ++j1) {
|
||||
unsigned j2 = i - j1;
|
||||
if (j1 > l->m_literals.size())
|
||||
if (j1 > l->size())
|
||||
continue;
|
||||
if (j2 > r->m_literals.size())
|
||||
if (j2 > r->size())
|
||||
continue;
|
||||
clause.reset();
|
||||
if (0 < j1) {
|
||||
|
@ -93,37 +93,27 @@ namespace opt {
|
|||
node* left = trees[i];
|
||||
node* right = trees[i + 1];
|
||||
expr_ref_vector ls(m);
|
||||
ls.resize(left->m_literals.size() + right->m_literals.size());
|
||||
ls.resize(left->size() + right->size());
|
||||
node* n = alloc(node, ls);
|
||||
n->m_left = left;
|
||||
n->m_right = right;
|
||||
trees.push_back(n);
|
||||
}
|
||||
m_tree = trees.back();
|
||||
m_root = trees.back();
|
||||
}
|
||||
|
||||
totalizer::~totalizer() {
|
||||
ptr_vector<node> trees;
|
||||
trees.push_back(m_tree);
|
||||
while (!trees.empty()) {
|
||||
node* n = trees.back();
|
||||
trees.pop_back();
|
||||
if (n->m_left)
|
||||
trees.push_back(n->m_left);
|
||||
if (n->m_right)
|
||||
trees.push_back(n->m_right);
|
||||
dealloc(n);
|
||||
}
|
||||
dealloc(m_root);
|
||||
}
|
||||
|
||||
expr* totalizer::at_least(unsigned k) {
|
||||
if (k == 0)
|
||||
return m.mk_true();
|
||||
if (m_tree->m_literals.size() < k)
|
||||
if (m_root->size() < k)
|
||||
return m.mk_false();
|
||||
SASSERT(1 <= k && k <= m_tree->m_literals.size());
|
||||
ensure_bound(m_tree, k);
|
||||
return m_tree->m_literals.get(k - 1);
|
||||
SASSERT(1 <= k && k <= m_root->size());
|
||||
ensure_bound(m_root, k);
|
||||
return m_root->m_literals.get(k - 1);
|
||||
}
|
||||
|
||||
}
|
||||
|
|
|
@ -26,11 +26,17 @@ namespace opt {
|
|||
node* m_right = nullptr;
|
||||
expr_ref_vector m_literals;
|
||||
node(expr_ref_vector& l): m_literals(l) {}
|
||||
~node() {
|
||||
dealloc(m_left);
|
||||
dealloc(m_right);
|
||||
}
|
||||
unsigned size() const { return m_literals.size(); }
|
||||
|
||||
};
|
||||
|
||||
ast_manager& m;
|
||||
expr_ref_vector m_literals;
|
||||
node* m_tree = nullptr;
|
||||
node* m_root = nullptr;
|
||||
expr_ref_vector m_clauses;
|
||||
vector<std::pair<expr_ref, expr_ref>> m_defs;
|
||||
|
||||
|
|
Loading…
Reference in a new issue