mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

fix debug assertion code, make maxlex optional

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-01-25 08:23:41 -08:00
parent d3d392da41
commit 1ed68906fa
3 changed files with 5 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/opt/maxlex.cpp
View file

@ -26,10 +26,6 @@ Author:
namespace opt { namespace opt {
bool is_maxlex(weights_t & _ws) { bool is_maxlex(weights_t & _ws) {
// disable for now
#if true
return false;
#else
vector<rational> ws(_ws); vector<rational> ws(_ws);
std::sort(ws.begin(), ws.end()); std::sort(ws.begin(), ws.end());
ws.reverse(); ws.reverse();
@ -42,7 +38,6 @@ namespace opt {
sum -= w; sum -= w;
} }
return true; return true;
#endif
} }
class maxlex : public maxsmt_solver_base { class maxlex : public maxsmt_solver_base {
@ -141,7 +136,7 @@ namespace opt {
if (soft.value == l_true) { if (soft.value == l_true) {
continue; continue;
} }
SASSERT(soft.value() == l_undef); SASSERT(soft.value == l_undef);
expr* a = soft.s; expr* a = soft.s;
lbool is_sat = s().check_sat(1, &a); lbool is_sat = s().check_sat(1, &a);
switch (is_sat) { switch (is_sat) {
@ -169,7 +164,7 @@ namespace opt {
if (soft.value != l_undef) { if (soft.value != l_undef) {
continue; continue;
} }
SASSERT(soft.value() == l_undef); SASSERT(soft.value == l_undef);
if (i + 1 == sz) { if (i + 1 == sz) {
expr* a = soft.s; expr* a = soft.s;
lbool is_sat = s().check_sat(1, &a); lbool is_sat = s().check_sat(1, &a);

3
src/opt/maxsmt.cpp
View file

@ -232,10 +232,11 @@ namespace opt {
lbool maxsmt::operator()() { lbool maxsmt::operator()() {
lbool is_sat = l_undef; lbool is_sat = l_undef;
m_msolver = nullptr; m_msolver = nullptr;
opt_params optp(m_params);
symbol const& maxsat_engine = m_c.maxsat_engine(); symbol const& maxsat_engine = m_c.maxsat_engine();
IF_VERBOSE(1, verbose_stream() << "(maxsmt)\n";); IF_VERBOSE(1, verbose_stream() << "(maxsmt)\n";);
TRACE("opt_verbose", s().display(tout << "maxsmt\n") << "\n";); TRACE("opt_verbose", s().display(tout << "maxsmt\n") << "\n";);
if (is_maxlex(m_weights)) { if (optp.maxlex_enable() && is_maxlex(m_weights)) {
m_msolver = mk_maxlex(m_c, m_index, m_weights, m_soft_constraints); m_msolver = mk_maxlex(m_c, m_index, m_weights, m_soft_constraints);
} }
else if (m_soft_constraints.empty() || maxsat_engine == symbol("maxres") || maxsat_engine == symbol::null) { else if (m_soft_constraints.empty() || maxsat_engine == symbol("maxres") || maxsat_engine == symbol::null) {

1
src/opt/opt_params.pyg
View file

@ -14,6 +14,7 @@ def_module_params('opt',
('elim_01', BOOL, True, 'eliminate 01 variables'), ('elim_01', BOOL, True, 'eliminate 01 variables'),
('pp.neat', BOOL, True, 'use neat (as opposed to less readable, but faster) pretty printer when displaying context'), ('pp.neat', BOOL, True, 'use neat (as opposed to less readable, but faster) pretty printer when displaying context'),
('pb.compile_equality', BOOL, False, 'compile arithmetical equalities into pseudo-Boolean equality (instead of two inequalites)'), ('pb.compile_equality', BOOL, False, 'compile arithmetical equalities into pseudo-Boolean equality (instead of two inequalites)'),
('maxlex.enable', BOOL, False, 'enable maxlex heuristic for lexicographic MaxSAT problems'),
('maxres.hill_climb', BOOL, True, 'give preference for large weight cores'), ('maxres.hill_climb', BOOL, True, 'give preference for large weight cores'),
('maxres.add_upper_bound_block', BOOL, False, 'restict upper bound with constraint'), ('maxres.add_upper_bound_block', BOOL, False, 'restict upper bound with constraint'),
('maxres.max_num_cores', UINT, UINT_MAX, 'maximal number of cores per round'), ('maxres.max_num_cores', UINT, UINT_MAX, 'maximal number of cores per round'),