From 386c511f54b48cde503cb33ad698fa61ef6a83bd Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 21 May 2022 10:27:32 -0400 Subject: [PATCH] core opt --- src/opt/maxcore.cpp | 1 + src/opt/maxsmt.cpp | 6 +- src/opt/opt_context.cpp | 14 ++-- src/opt/opt_preprocess.cpp | 53 ++++++++++++++- src/opt/opt_preprocess.h | 2 + src/sat/sat_solver/inc_sat_solver.cpp | 92 +++++++++++++++++++-------- src/sat/tactic/goal2sat.cpp | 58 +++++++++++++---- src/sat/tactic/goal2sat.h | 12 +++- 8 files changed, 182 insertions(+), 56 deletions(-) diff --git a/src/opt/maxcore.cpp b/src/opt/maxcore.cpp index 216ca1877..1a89129c5 100644 --- a/src/opt/maxcore.cpp +++ b/src/opt/maxcore.cpp @@ -510,6 +510,7 @@ public: for (auto const & [core, w] : cores) { if (core.empty()) return l_false; + ++m_stats.m_num_cores; remove_soft(core, m_asms); split_core(core); process_unsat(core, w); diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp index 02de67bb5..6064ef899 100644 --- a/src/opt/maxsmt.cpp +++ b/src/opt/maxsmt.cpp @@ -342,15 +342,13 @@ namespace opt { void maxsmt::updt_params(params_ref& p) { m_params.append(p); - if (m_msolver) { + if (m_msolver) m_msolver->updt_params(p); - } } void maxsmt::collect_statistics(statistics& st) const { - if (m_msolver) { + if (m_msolver) m_msolver->collect_statistics(st); - } } solver& maxsmt::s() { diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 85835f08d..fcc8cdd46 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -1533,20 +1533,16 @@ namespace opt { } void context::collect_statistics(statistics& stats) const { - if (m_solver) { + if (m_solver) m_solver->collect_statistics(stats); - } - if (m_simplify) { - m_simplify->collect_statistics(stats); - } - for (auto const& kv : m_maxsmts) { + if (m_simplify) + m_simplify->collect_statistics(stats); + for (auto const& kv : m_maxsmts) kv.m_value->collect_statistics(stats); - } get_memory_statistics(stats); get_rlimit_statistics(m.limit(), stats); - if (m_qmax) { + if (m_qmax) m_qmax->collect_statistics(stats); - } } void context::collect_param_descrs(param_descrs & r) { diff --git a/src/opt/opt_preprocess.cpp b/src/opt/opt_preprocess.cpp index bbf119266..268aa8986 100644 --- a/src/opt/opt_preprocess.cpp +++ b/src/opt/opt_preprocess.cpp @@ -15,6 +15,19 @@ Author: Nikolaj Bjorner (nbjorner) 2022-04-11 + +Notes: + + maxsat x, y, z, u . x + y + z <= 1 and F +=> + maxsst x or y or z, u . x + y + z <= 1 and F + lower bound increased by 2 + + maxsat x, y, z, u . x + y + z >= 2 and F +=> + maxsst x and y and z, u . x + y + z >= 2 and F + lower bound decreased by 2 + --*/ #pragma once @@ -113,13 +126,28 @@ namespace opt { m_trail.push_back(sf.s); if (new_soft.contains(sf.s)) new_soft[sf.s] += sf.weight; - else + else { new_soft.insert(sf.s, sf.weight); - fmls.push_back(sf.s); + fmls.push_back(sf.s); + } } return new_soft; } + obj_map preprocess::dualize(obj_map const& soft, expr_ref_vector& fmls) { + obj_map new_soft; + for (auto const& [k, v] : soft) { + expr* nk = mk_not(m, k); + m_trail.push_back(nk); + new_soft.insert(nk, v); + } + unsigned i = 0; + for (expr* f : fmls) + fmls[i++] = mk_not(m, f); + + return new_soft; + } + bool preprocess::find_mutexes(vector& softs, rational& lower) { expr_ref_vector fmls(m); obj_map new_soft = soft2map(softs, fmls); @@ -131,6 +159,24 @@ namespace opt { return false; for (auto& mux : mutexes) process_mutex(mux, new_soft, lower); + + + if (mutexes.empty()) + { + obj_map dual_soft = dualize(new_soft, fmls); + mutexes.reset(); + lbool is_sat = s.find_mutexes(fmls, mutexes); + if (is_sat == l_false) + return true; + if (is_sat == l_undef) + return false; + rational llower(0); + for (auto& mux : mutexes) + process_mutex(mux, dual_soft, llower); + if (dual_soft.size() != new_soft.size()) + new_soft = dualize(dual_soft, fmls); + } + softs.reset(); for (auto const& [k, v] : new_soft) softs.push_back(soft(expr_ref(k, m), v, false)); @@ -175,7 +221,7 @@ namespace opt { weight = w - weight; lower += weight*rational(i); IF_VERBOSE(1, verbose_stream() << "(opt.maxsat mutex size: " << i + 1 << " weight: " << weight << ")\n";); - sum2 += weight*rational(i+1); + sum2 += weight * rational(i + 1); new_soft.insert(soft, weight); for (; i > 0 && weights[i-1] == w; --i) {} weight = w; @@ -183,6 +229,7 @@ namespace opt { SASSERT(sum1 == sum2); } + preprocess::preprocess(solver& s): m(s.get_manager()), s(s), m_trail(m) {} bool preprocess::operator()(vector& soft, rational& lower) { diff --git a/src/opt/opt_preprocess.h b/src/opt/opt_preprocess.h index 567a750ed..71e06eb2c 100644 --- a/src/opt/opt_preprocess.h +++ b/src/opt/opt_preprocess.h @@ -34,6 +34,8 @@ namespace opt { bool prop_mutexes(vector& softs, rational& lower); void process_mutex(expr_ref_vector& mutex, obj_map& new_soft, rational& lower); + obj_map dualize(obj_map const& soft, expr_ref_vector& fmls); + public: preprocess(solver& s); bool operator()(vector& soft, rational& lower); diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index af0d9dd1b..cf46b1f27 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -698,6 +698,33 @@ public: private: + lbool check_uninterpreted() { + func_decl_ref_vector funs(m); + m_goal2sat.get_interpreted_funs(funs); + + if (!funs.empty()) { + m_has_uninterpreted = true; + std::stringstream strm; + strm << "(sat.giveup interpreted functions sent to SAT solver " << funs <<")"; + TRACE("sat", tout << strm.str() << "\n";); + IF_VERBOSE(1, verbose_stream() << strm.str() << "\n";); + set_reason_unknown(strm.str()); + return l_undef; + } + return l_true; + } + + lbool internalize_goal(unsigned sz, expr* const* fmls) { + m_solver.pop_to_base_level(); + if (m_solver.inconsistent()) + return l_false; + m_pc.reset(); + m_goal2sat(m, sz, fmls, m_params, m_solver, m_map, m_dep2asm, is_incremental()); + if (!m_sat_mc) m_sat_mc = alloc(sat2goal::mc, m); + m_sat_mc->flush_smc(m_solver, m_map); + return check_uninterpreted(); + } + lbool internalize_goal(goal_ref& g) { m_solver.pop_to_base_level(); if (m_solver.inconsistent()) @@ -712,12 +739,14 @@ private: } SASSERT(!g->proofs_enabled()); TRACE("sat", m_solver.display(tout); g->display(tout);); + try { if (m_is_cnf) { m_subgoals.push_back(g.get()); } else { (*m_preprocess)(g, m_subgoals); + m_is_cnf = true; } } catch (tactic_exception & ex) { @@ -737,8 +766,8 @@ private: IF_VERBOSE(0, verbose_stream() << "size of subgoals is not 1, it is: " << m_subgoals.size() << "\n"); return l_undef; } + g = m_subgoals[0]; - func_decl_ref_vector funs(m); m_pc = g->pc(); m_mcs.set(m_mcs.size()-1, concat(m_mcs.back(), g->mc())); TRACE("sat", g->display_with_dependencies(tout);); @@ -746,19 +775,10 @@ private: // ensure that if goal is already internalized, then import mc from m_solver. m_goal2sat(*g, m_params, m_solver, m_map, m_dep2asm, is_incremental()); - m_goal2sat.get_interpreted_funs(funs); + if (!m_sat_mc) m_sat_mc = alloc(sat2goal::mc, m); m_sat_mc->flush_smc(m_solver, m_map); - if (!funs.empty()) { - m_has_uninterpreted = true; - std::stringstream strm; - strm << "(sat.giveup interpreted functions sent to SAT solver " << funs <<")"; - TRACE("sat", tout << strm.str() << "\n";); - IF_VERBOSE(1, verbose_stream() << strm.str() << "\n";); - set_reason_unknown(strm.str()); - return l_undef; - } - return l_true; + return check_uninterpreted(); } lbool internalize_assumptions(unsigned sz, expr* const* asms) { @@ -766,17 +786,30 @@ private: m_asms.shrink(0); return l_true; } + for (unsigned i = 0; i < sz; ++i) + m_is_cnf &= is_literal(asms[i]); + for (unsigned i = 0; i < get_num_assumptions(); ++i) + m_is_cnf &= is_literal(get_assumption(i)); + + if (m_is_cnf) { + // std::cout << "assumptions " << sz << " " << get_num_assumptions() << " " << m_fmls_head << " " << m_fmls.size() << "\n"; + expr_ref_vector fmls(m); + fmls.append(sz, asms); + for (unsigned i = 0; i < get_num_assumptions(); ++i) + fmls.push_back(get_assumption(i)); + m_goal2sat.assumptions(m, fmls.size(), fmls.data(), m_params, m_solver, m_map, m_dep2asm, is_incremental()); + extract_assumptions(fmls.size(), fmls.data()); + return l_true; + } + goal_ref g = alloc(goal, m, true, true); // models and cores are enabled. - for (unsigned i = 0; i < sz; ++i) { + for (unsigned i = 0; i < sz; ++i) g->assert_expr(asms[i], m.mk_leaf(asms[i])); - } - for (unsigned i = 0; i < get_num_assumptions(); ++i) { + for (unsigned i = 0; i < get_num_assumptions(); ++i) g->assert_expr(get_assumption(i), m.mk_leaf(get_assumption(i))); - } lbool res = internalize_goal(g); - if (res == l_true) { + if (res == l_true) extract_assumptions(sz, asms); - } return res; } @@ -905,18 +938,25 @@ private: } lbool internalize_formulas() { - if (m_fmls_head == m_fmls.size()) { + if (m_fmls_head == m_fmls.size()) return l_true; + + lbool res; + + if (m_is_cnf) { + std::cout << "cnf\n"; + res = internalize_goal(m_fmls.size() - m_fmls_head, m_fmls.data() + m_fmls_head); } - goal_ref g = alloc(goal, m, true, false); // models, maybe cores are enabled - for (unsigned i = m_fmls_head ; i < m_fmls.size(); ++i) { - expr* fml = m_fmls.get(i); - g->assert_expr(fml); + else { + goal_ref g = alloc(goal, m, true, false); // models, maybe cores are enabled + for (unsigned i = m_fmls_head ; i < m_fmls.size(); ++i) { + expr* fml = m_fmls.get(i); + g->assert_expr(fml); + } + res = internalize_goal(g); } - lbool res = internalize_goal(g); - if (res != l_undef) { + if (res != l_undef) m_fmls_head = m_fmls.size(); - } m_internalized_converted = false; return res; } diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index af07001e3..73d8561df 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -894,16 +894,36 @@ struct goal2sat::imp : public sat::sat_internalizer { m_result_stack.pop_back(); } + struct scoped_reset { + imp& i; + scoped_reset(imp& i) :i(i) {} + ~scoped_reset() { + i.m_interface_vars.reset(); + i.m_app2lit.reset(); + i.m_lit2app.reset(); + } + }; + + void operator()(unsigned n, expr* const* fmls) { + scoped_reset _reset(*this); + // collect_boolean_interface(g, m_interface_vars); + for (unsigned i = 0; i < n; ++i) + process(fmls[i]); + } + + void assumptions(unsigned n, expr* const* fmls) { + scoped_reset _reset(*this); + // collect_boolean_interface(g, m_interface_vars); + for (unsigned i = 0; i < n; ++i) { + expr* f = fmls[i]; + expr* f1 = f; + bool sign = m.is_not(f, f1); + insert_dep(f, f1, sign); + } + } + + void operator()(goal const & g) { - struct scoped_reset { - imp& i; - scoped_reset(imp& i) :i(i) {} - ~scoped_reset() { - i.m_interface_vars.reset(); - i.m_app2lit.reset(); - i.m_lit2app.reset(); - } - }; scoped_reset _reset(*this); collect_boolean_interface(g, m_interface_vars); unsigned size = g.size(); @@ -1002,16 +1022,30 @@ void goal2sat::collect_param_descrs(param_descrs & r) { r.insert("ite_extra", CPK_BOOL, "(default: true) add redundant clauses (that improve unit propagation) when encoding if-then-else formulas"); } - -void goal2sat::operator()(goal const & g, params_ref const & p, sat::solver_core & t, atom2bool_var & m, dep2asm_map& dep2asm, bool default_external) { +void goal2sat::init(ast_manager& m, params_ref const & p, sat::solver_core & t, atom2bool_var & map, dep2asm_map& dep2asm, bool default_external) { if (!m_imp) { - m_imp = alloc(imp, g.m(), p, t, m, dep2asm, default_external); + m_imp = alloc(imp, m, p, t, map, dep2asm, default_external); for (unsigned i = 0; i < m_scopes; ++i) m_imp->user_push(); } +} + +void goal2sat::operator()(goal const & g, params_ref const & p, sat::solver_core & t, atom2bool_var & m, dep2asm_map& dep2asm, bool default_external) { + init(g.m(), p, t, m, dep2asm, default_external); (*m_imp)(g); } +void goal2sat::operator()(ast_manager& m, unsigned n, expr* const* fmls, params_ref const & p, sat::solver_core & t, atom2bool_var & map, dep2asm_map& dep2asm, bool default_external) { + init(m, p, t, map, dep2asm, default_external); + (*m_imp)(n, fmls); +} + +void goal2sat::assumptions(ast_manager& m, unsigned n, expr* const* fmls, params_ref const & p, sat::solver_core & t, atom2bool_var & map, dep2asm_map& dep2asm, bool default_external) { + init(m, p, t, map, dep2asm, default_external); + m_imp->assumptions(n, fmls); +} + + void goal2sat::get_interpreted_funs(func_decl_ref_vector& funs) { if (m_imp) funs.append(m_imp->interpreted_funs()); diff --git a/src/sat/tactic/goal2sat.h b/src/sat/tactic/goal2sat.h index 8b344c9c3..08fd5f088 100644 --- a/src/sat/tactic/goal2sat.h +++ b/src/sat/tactic/goal2sat.h @@ -34,15 +34,19 @@ Notes: #include "sat/smt/sat_internalizer.h" class goal2sat { +public: + typedef obj_map dep2asm_map; +private: struct imp; imp * m_imp; - unsigned m_scopes { 0 }; + unsigned m_scopes = 0; + + void init(ast_manager& m, params_ref const & p, sat::solver_core & t, atom2bool_var & map, dep2asm_map& dep2asm, bool default_external); public: goal2sat(); ~goal2sat(); - typedef obj_map dep2asm_map; static void collect_param_descrs(param_descrs & r); @@ -60,6 +64,10 @@ public: */ void operator()(goal const & g, params_ref const & p, sat::solver_core & t, atom2bool_var & m, dep2asm_map& dep2asm, bool default_external = false); + void operator()(ast_manager& m, unsigned n, expr* const* fmls, params_ref const & p, sat::solver_core & t, atom2bool_var & map, dep2asm_map& dep2asm, bool default_external = false); + + void assumptions(ast_manager& m, unsigned n, expr* const* fmls, params_ref const & p, sat::solver_core & t, atom2bool_var & map, dep2asm_map& dep2asm, bool default_external = false); + void get_interpreted_funs(func_decl_ref_vector& funs); bool has_interpreted_funs() const;