diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 547f90bd7..a16654614 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -957,7 +957,7 @@ namespace opt { break; } } - out << "(optimize)\n"; + out << "(check-sat)\n"; return out.str(); } diff --git a/src/opt/opt_sls_solver.h b/src/opt/opt_sls_solver.h index f33282fa2..001a33ed4 100644 --- a/src/opt/opt_sls_solver.h +++ b/src/opt/opt_sls_solver.h @@ -43,7 +43,7 @@ namespace opt { sls_solver(ast_manager & m, solver* s, expr_ref_vector const& soft, vector const& weights, - params_ref const& p): + params_ref & p): solver_na2as(m), m(m), m_solver(s), @@ -53,6 +53,7 @@ namespace opt { m_weights(weights), m_soft(soft) { + updt_params(p); } virtual ~sls_solver() {} @@ -89,6 +90,7 @@ namespace opt { m_solver->get_labels(r); } virtual void set_cancel(bool f) { + std::cout << "set cancel\n"; m_solver->set_cancel(f); m_pb2bv.set_cancel(f); #pragma omp critical (this) @@ -205,7 +207,7 @@ namespace opt { } lbool is_sat = (*m_pbsls.get())(); if (is_sat == l_true) { - m_bvsls->get_model(m_model); + m_pbsls->get_model(m_model); } } @@ -216,7 +218,13 @@ namespace opt { } assertions2sls(); expr_ref objective = soft2bv(); - opt_result or = m_bvsls->optimize(objective, m_model, true); + opt_result or(m); + try { + or = m_bvsls->optimize(objective, m_model, true); + } + catch (...) { + + } SASSERT(or.is_sat == l_true || or.is_sat == l_undef); if (or.is_sat == l_true) { m_bvsls->get_model(m_model); diff --git a/src/opt/pb_sls.cpp b/src/opt/pb_sls.cpp index d000350e5..2d7586300 100644 --- a/src/opt/pb_sls.cpp +++ b/src/opt/pb_sls.cpp @@ -107,28 +107,33 @@ namespace smt { vector m_hard_occ, m_soft_occ; // variable occurrence svector m_assignment; // current assignment. svector m_best_assignment; - obj_map m_decl2var; // map declarations to Boolean variables. - ptr_vector m_var2decl; // reverse map + expr_ref_vector m_trail; + obj_map m_decl2var; // map declarations to Boolean variables. + ptr_vector m_var2decl; // reverse map index_set m_hard_false; // list of hard clauses that are false. index_set m_soft_false; // list of soft clauses that are false. unsigned m_max_flips; // maximal number of flips unsigned m_non_greedy_percent; // percent of moves to do non-greedy style random_gen m_rng; + scoped_mpz one; imp(ast_manager& m): m(m), pb(m), m_rewrite(m), m_cancel(false), - m_orig_clauses(m) + m_orig_clauses(m), + m_trail(m), + one(mgr) { init_max_flips(); m_non_greedy_percent = 30; - m_decl2var.insert(m.mk_true()->get_decl(), 0); - m_var2decl.push_back(m.mk_true()->get_decl()); + m_decl2var.insert(m.mk_true(), 0); + m_var2decl.push_back(m.mk_true()); m_assignment.push_back(true); m_hard_occ.push_back(unsigned_vector()); m_soft_occ.push_back(unsigned_vector()); + one = mpz(1); } ~imp() { @@ -155,14 +160,10 @@ namespace smt { void set_model(model_ref & mdl) { m_orig_model = mdl; - unsigned sz = mdl->get_num_constants(); - for (unsigned i = 0; i < sz; ++i) { - func_decl* f = mdl->get_constant(i); - if (m.is_bool(f->get_range())) { - literal lit = mk_literal(f); - SASSERT(!lit.sign()); - m_assignment[lit.var()] = m.is_true(mdl->get_const_interp(f)); - } + for (unsigned i = 0; i < m_var2decl.size(); ++i) { + expr_ref tmp(m); + VERIFY(mdl->eval(m_var2decl[i], tmp)); + m_assignment[i] = m.is_true(tmp); } } @@ -229,7 +230,10 @@ namespace smt { void get_model(model_ref& mdl) { mdl = alloc(model, m); for (unsigned i = 1; i < m_var2decl.size(); ++i) { - mdl->register_decl(m_var2decl[i], m_assignment[i]?m.mk_true():m.mk_false()); + expr* d = m_var2decl[i]; + if (is_uninterp_const(d)) { + mdl->register_decl(to_app(d)->get_decl(), m_assignment[i] ? m.mk_true() : m.mk_false()); + } } } @@ -248,6 +252,7 @@ namespace smt { for (unsigned i = 0; i < cls.m_lits.size(); ++i) { w = cls.m_weights[i]; out << w << "*" << cls.m_lits[i] << " "; + out << "(" << mk_pp(m_var2decl[cls.m_lits[i].var()], m) << ") "; if (i + 1 < cls.m_lits.size()) { out << "+ "; } @@ -271,7 +276,7 @@ namespace smt { display(out << m_weights[i] << ": ", m_soft[i]); } for (unsigned i = 0; i < m_assignment.size(); ++i) { - out << literal(i) << ": " << m_var2decl[i]->get_name() << " |-> " << (m_assignment[i]?"true":"false") << "\n"; + out << literal(i) << ": " << mk_pp(m_var2decl[i], m) << " |-> " << (m_assignment[i]?"true":"false") << "\n"; } } @@ -319,8 +324,11 @@ namespace smt { if (!eval(m_clauses[i])) { m_hard_false.insert(i); expr_ref tmp(m); - VERIFY(m_orig_model->eval(m_orig_clauses[i].get(), tmp)); - std::cout << "original evaluation: " << tmp << "\n"; + VERIFY(m_orig_model->eval(m_orig_clauses[i].get(), tmp)); + IF_VERBOSE(0, + verbose_stream() << "original evaluation: " << tmp << "\n"; + verbose_stream() << mk_pp(m_orig_clauses[i].get(), m) << "\n"; + display(verbose_stream(), m_clauses[i]);); } } for (unsigned i = 0; i < m_soft.size(); ++i) { @@ -482,45 +490,131 @@ namespace smt { return break_count; } - literal mk_literal(func_decl* f) { - SASSERT(f->get_family_id() == null_family_id); + literal mk_aux_literal(expr* f) { unsigned var; + expr_ref tmp(m); if (!m_decl2var.find(f, var)) { var = m_hard_occ.size(); SASSERT(m_var2decl.size() == var); SASSERT(m_soft_occ.size() == var); m_hard_occ.push_back(unsigned_vector()); m_soft_occ.push_back(unsigned_vector()); - m_assignment.push_back(false); + VERIFY(m_orig_model->eval(f, tmp)); + m_assignment.push_back(m.is_true(tmp)); m_decl2var.insert(f, var); m_var2decl.push_back(f); } return literal(var); } - + void pad(scoped_mpz_vector& vec, unsigned sz, mpz& val) { + for (unsigned i = 0; i < sz; ++i) { + vec.push_back(val); + } + } literal mk_literal(expr* f) { - literal result; - bool sign = false; - while (m.is_not(f, f)) { - sign = !sign; + if (m.is_not(f, f)) { + literal result = mk_literal(f); + if (result != null_literal) { + result.neg(); + } + return result; } - if (m.is_true(f)) { - result = true_literal; + if (is_uninterp_const(f)) + return mk_aux_literal(to_app(f)); + if (m.is_true(f)) + return true_literal; + if (m.is_false(f)) + return false_literal; + if (m.is_and(f)) { + literal_vector lits; + app* g = to_app(f); + for (unsigned i = 0; i < g->get_num_args(); ++i) { + lits.push_back(mk_literal(g->get_arg(i))); + } + literal result = mk_aux_literal(f); + for (unsigned i = 0; i < lits.size(); ++i) { + clause cls(mgr); + cls.m_lits.push_back(~result); + cls.m_weights.push_back(one); + cls.m_lits.push_back(lits[i]); + cls.m_weights.push_back(one); + cls.m_k = one; + cls.m_eq = false; + m_clauses.push_back(cls); + m_orig_clauses.push_back(f); + lits[i].neg(); + } + lits.push_back(result); + clause cls(mgr); + cls.m_lits.append(lits); + pad(cls.m_weights, lits.size(), one); + cls.m_k = one; + cls.m_eq = false; + m_clauses.push_back(cls); + m_orig_clauses.push_back(f); + return result; } - else if (m.is_false(f)) { - result = false_literal; + if (m.is_or(f)) { + literal_vector lits; + app* g = to_app(f); + for (unsigned i = 0; i < g->get_num_args(); ++i) { + lits.push_back(mk_literal(g->get_arg(i))); + } + literal result = mk_aux_literal(f); + for (unsigned i = 0; i < lits.size(); ++i) { + clause cls(mgr); + cls.m_lits.push_back(result); + cls.m_weights.push_back(one); + cls.m_lits.push_back(~lits[i]); + cls.m_weights.push_back(one); + cls.m_k = one; + cls.m_eq = false; + m_clauses.push_back(cls); + m_orig_clauses.push_back(f); + } + lits.push_back(~result); + clause cls(mgr); + cls.m_lits.append(lits); + pad(cls.m_weights, lits.size(), one); + cls.m_k = one; + cls.m_eq = false; + m_clauses.push_back(cls); + m_orig_clauses.push_back(f); + return result; } - else if (is_uninterp_const(f)) { - result = mk_literal(to_app(f)->get_decl()); + expr* x, *y; + if (m.is_eq(f, x, y) || m.is_iff(f, x, y)) { + literal a = mk_literal(x); + literal b = mk_literal(y); + literal result = mk_aux_literal(f); + clause cls(mgr); + cls.m_lits.push_back(~result); + cls.m_lits.push_back(~a); + cls.m_lits.push_back(b); + pad(cls.m_weights, 3, one); + cls.m_k = one; + cls.m_eq = false; + m_clauses.push_back(cls); + m_orig_clauses.push_back(f); // actually, the clause that defines f + cls.m_lits[0] = ~result; + cls.m_lits[1] = a; + cls.m_lits[2] = ~b; + m_clauses.push_back(cls); + m_orig_clauses.push_back(f); + cls.m_lits[0] = result; + cls.m_lits[1] = a; + cls.m_lits[2] = b; + m_clauses.push_back(cls); + m_orig_clauses.push_back(f); + cls.m_lits[0] = result; + cls.m_lits[1] = ~a; + cls.m_lits[2] = ~b; + m_clauses.push_back(cls); + m_orig_clauses.push_back(f); + return result; } - else { - IF_VERBOSE(0, verbose_stream() << "not handled: " << mk_pp(f, m) << "\n";); - result = null_literal; - } - if (sign) { - result.neg(); - } - return result; + IF_VERBOSE(0, verbose_stream() << "not handled: " << mk_pp(f, m) << "\n";); + return null_literal; } bool compile_clause(expr* _f, clause& cls) { diff --git a/src/opt/weighted_maxsat.cpp b/src/opt/weighted_maxsat.cpp index 9862c2b28..141bf49c7 100644 --- a/src/opt/weighted_maxsat.cpp +++ b/src/opt/weighted_maxsat.cpp @@ -69,7 +69,7 @@ namespace opt { virtual rational get_lower() const { return m_lower; } virtual rational get_upper() const { return m_upper; } virtual bool get_assignment(unsigned index) const { return m_assignment[index]; } - virtual void set_cancel(bool f) { m_cancel = f; } + virtual void set_cancel(bool f) { m_cancel = f; m_s->set_cancel(f); } virtual void collect_statistics(statistics& st) const { } virtual void get_model(model_ref& mdl) { mdl = m_model.get(); } virtual void updt_params(params_ref& p) { @@ -127,7 +127,6 @@ namespace opt { }; bool probe_bv() { - if (!m_enable_sat) return false; expr_fast_mark1 visited; is_bv proc(m); try { @@ -553,7 +552,7 @@ namespace opt { expr_ref fml(m), val(m); app_ref b(m); expr_ref_vector nsoft(m); - init(); + init(); if (m_use_aux) { s().push(); } @@ -582,6 +581,7 @@ namespace opt { } if (is_sat == l_true) { m_upper.reset(); + s().get_model(m_model); for (unsigned i = 0; i < m_soft.size(); ++i) { VERIFY(m_model->eval(nsoft[i].get(), val)); TRACE("opt", tout << "eval " << mk_pp(m_soft[i].get(), m) << " " << val << "\n";); @@ -820,6 +820,7 @@ namespace opt { lbool is_sat = s().check_sat(0, 0); if (is_sat == l_true) { s().get_model(m_model); + m_upper.reset(); for (unsigned i = 0; i < m_soft.size(); ++i) { expr_ref tmp(m); m_model->eval(m_soft[i].get(), tmp, true); diff --git a/tests/chat1.smt2 b/tests/chat1.smt2 index 0b489e192..e6e11076b 100644 --- a/tests/chat1.smt2 +++ b/tests/chat1.smt2 @@ -3374,7 +3374,7 @@ (optimize ; :wmaxsat_engine wpm2 ; :wmaxsat_engine pwmax - :wmaxsat_engine bvmax +; :wmaxsat_engine bvmax :print_statistics true :timeout 1200000 )