mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-31 16:33:18 +00:00
Code Activity

na

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-05-01 21:04:35 +02:00
parent b5c7f000de
commit 9cc5f6901a
1 changed files with 15 additions and 30 deletions
Download patch file Download diff file Expand all files Collapse all files

45
src/opt/maxcore.cpp
View file

@ -78,7 +78,6 @@ public:
s_primal, s_primal,
s_primal_dual, s_primal_dual,
s_primal_binary, s_primal_binary,
s_primal_binary_delay,
s_rc2 s_rc2
}; };
private: private:
@ -115,21 +114,20 @@ private:
model_ref m_csmodel; model_ref m_csmodel;
lns_maxcore m_lnsctx; lns_maxcore m_lnsctx;
lns m_lns; lns m_lns;
unsigned m_correction_set_size; unsigned m_correction_set_size = 0;
bool m_found_feasible_optimum; bool m_found_feasible_optimum = false;
bool m_hill_climb; // prefer large weight soft clauses for cores bool m_hill_climb = true; // prefer large weight soft clauses for cores
unsigned m_last_index; // last index used during hill-climbing bool m_add_upper_bound_block = false; // restrict upper bound with constraint
bool m_add_upper_bound_block; // restrict upper bound with constraint unsigned m_max_core_size = 3; // max core size per round.
unsigned m_max_core_size; // max core size per round. bool m_maximize_assignment = false; // maximize assignment to find MCS
bool m_maximize_assignment; // maximize assignment to find MCS unsigned m_max_correction_set_size = 3; // maximal set of correction set that is tolerated.
unsigned m_max_correction_set_size;// maximal set of correction set that is tolerated. bool m_wmax = false; // Block upper bound using wmax
bool m_wmax; // Block upper bound using wmax // this option is disabled if SAT core is used.
// this option is disabled if SAT core is used. bool m_pivot_on_cs = true; // prefer smaller correction set to core.
bool m_pivot_on_cs; // prefer smaller correction set to core. bool m_dump_benchmarks; // display benchmarks (into wcnf format)
bool m_dump_benchmarks; // display benchmarks (into wcnf format) bool m_enable_lns = false; // enable LNS improvements
bool m_enable_lns = false; // enable LNS improvements unsigned m_lns_conflicts = 1000; // number of conflicts used for LNS improvement
unsigned m_lns_conflicts = 1000; // number of conflicts used for LNS improvement bool m_enable_core_rotate = false; // enable core rotation
bool m_enable_core_rotate = false;
std::string m_trace_id; std::string m_trace_id;
typedef ptr_vector<expr> exprs; typedef ptr_vector<expr> exprs;
@ -144,16 +142,7 @@ public:
m_trail(m), m_trail(m),
m_st(st), m_st(st),
m_lnsctx(*this), m_lnsctx(*this),
m_lns(s(), m_lnsctx), m_lns(s(), m_lnsctx)
m_correction_set_size(0),
m_found_feasible_optimum(false),
m_hill_climb(true),
m_add_upper_bound_block(false),
m_max_num_cores(UINT_MAX),
m_max_core_size(3),
m_maximize_assignment(false),
m_max_correction_set_size(3),
m_pivot_on_cs(true)
{ {
switch(st) { switch(st) {
case s_primal: case s_primal:
@ -165,9 +154,6 @@ public:
case s_primal_binary: case s_primal_binary:
m_trace_id = "maxres-bin"; m_trace_id = "maxres-bin";
break; break;
case s_primal_binary_delay:
m_trace_id = "maxres-bin-delay";
break;
case s_rc2: case s_rc2:
m_trace_id = "rc2"; m_trace_id = "rc2";
break; break;
@ -373,7 +359,6 @@ public:
switch(m_st) { switch(m_st) {
case s_primal: case s_primal:
case s_primal_binary: case s_primal_binary:
case s_primal_binary_delay:
case s_rc2: case s_rc2:
return mus_solver(); return mus_solver();
case s_primal_dual: case s_primal_dual: