diff --git a/src/api/api_datalog.cpp b/src/api/api_datalog.cpp index b0a4def55..61c0dc3a5 100644 --- a/src/api/api_datalog.cpp +++ b/src/api/api_datalog.cpp @@ -623,6 +623,99 @@ extern "C" { to_fixedpoint_ref(d)->ctx().add_constraint(to_expr(e), lvl); } -#include "api_datalog_spacer.inc" + Z3_lbool Z3_API Z3_fixedpoint_query_from_lvl (Z3_context c, Z3_fixedpoint d, Z3_ast q, unsigned lvl) { + Z3_TRY; + LOG_Z3_fixedpoint_query_from_lvl (c, d, q, lvl); + RESET_ERROR_CODE(); + lbool r = l_undef; + unsigned timeout = to_fixedpoint(d)->m_params.get_uint("timeout", mk_c(c)->get_timeout()); + unsigned rlimit = to_fixedpoint(d)->m_params.get_uint("rlimit", mk_c(c)->get_rlimit()); + { + scoped_rlimit _rlimit(mk_c(c)->m().limit(), rlimit); + cancel_eh eh(mk_c(c)->m().limit()); + api::context::set_interruptable si(*(mk_c(c)), eh); + scoped_timer timer(timeout, &eh); + try { + r = to_fixedpoint_ref(d)->ctx().query_from_lvl (to_expr(q), lvl); + } + catch (z3_exception& ex) { + mk_c(c)->handle_exception(ex); + r = l_undef; + } + to_fixedpoint_ref(d)->ctx().cleanup(); + } + return of_lbool(r); + Z3_CATCH_RETURN(Z3_L_UNDEF); + } + + Z3_ast Z3_API Z3_fixedpoint_get_ground_sat_answer(Z3_context c, Z3_fixedpoint d) { + Z3_TRY; + LOG_Z3_fixedpoint_get_ground_sat_answer(c, d); + RESET_ERROR_CODE(); + expr* e = to_fixedpoint_ref(d)->ctx().get_ground_sat_answer(); + mk_c(c)->save_ast_trail(e); + RETURN_Z3(of_expr(e)); + Z3_CATCH_RETURN(nullptr); + } + + Z3_ast_vector Z3_API Z3_fixedpoint_get_rules_along_trace( + Z3_context c, + Z3_fixedpoint d) + { + Z3_TRY; + LOG_Z3_fixedpoint_get_rules_along_trace(c, d); + ast_manager& m = mk_c(c)->m(); + Z3_ast_vector_ref* v = alloc(Z3_ast_vector_ref, *mk_c(c), m); + mk_c(c)->save_object(v); + expr_ref_vector rules(m); + svector names; + + to_fixedpoint_ref(d)->ctx().get_rules_along_trace_as_formulas(rules, names); + for (unsigned i = 0; i < rules.size(); ++i) { + v->m_ast_vector.push_back(rules[i].get()); + } + RETURN_Z3(of_ast_vector(v)); + Z3_CATCH_RETURN(nullptr); + } + + Z3_symbol Z3_API Z3_fixedpoint_get_rule_names_along_trace( + Z3_context c, + Z3_fixedpoint d) + { + Z3_TRY; + LOG_Z3_fixedpoint_get_rule_names_along_trace(c, d); + ast_manager& m = mk_c(c)->m(); + Z3_ast_vector_ref* v = alloc(Z3_ast_vector_ref, *mk_c(c), m); + mk_c(c)->save_object(v); + expr_ref_vector rules(m); + svector names; + std::stringstream ss; + + to_fixedpoint_ref(d)->ctx().get_rules_along_trace_as_formulas(rules, names); + for (unsigned i = 0; i < names.size(); ++i) { + ss << ";" << names[i].str(); + } + RETURN_Z3(of_symbol(symbol(ss.str().substr(1).c_str()))); + Z3_CATCH_RETURN(nullptr); + } + + void Z3_API Z3_fixedpoint_add_invariant(Z3_context c, Z3_fixedpoint d, Z3_func_decl pred, Z3_ast property) { + Z3_TRY; + LOG_Z3_fixedpoint_add_invariant(c, d, pred, property); + RESET_ERROR_CODE(); + to_fixedpoint_ref(d)->ctx ().add_invariant(to_func_decl(pred), to_expr(property)); + Z3_CATCH; + } + + Z3_ast Z3_API Z3_fixedpoint_get_reachable(Z3_context c, Z3_fixedpoint d, Z3_func_decl pred) { + Z3_TRY; + LOG_Z3_fixedpoint_get_reachable(c, d, pred); + RESET_ERROR_CODE(); + expr_ref r = to_fixedpoint_ref(d)->ctx().get_reachable(to_func_decl(pred)); + mk_c(c)->save_ast_trail(r); + RETURN_Z3(of_expr(r.get())); + Z3_CATCH_RETURN(nullptr); + } + }; diff --git a/src/api/api_qe.cpp b/src/api/api_qe.cpp index 94e83144f..167a694aa 100644 --- a/src/api/api_qe.cpp +++ b/src/api/api_qe.cpp @@ -1,5 +1,5 @@ /*++ -Copyright (c) 2017 Arie Gurfinkel +Copyright (c) 2018 Microsoft Corporation Module Name: diff --git a/src/ast/csp_decl_plugin.cpp b/src/ast/csp_decl_plugin.cpp index 395677a4c..27feadc6d 100644 --- a/src/ast/csp_decl_plugin.cpp +++ b/src/ast/csp_decl_plugin.cpp @@ -68,6 +68,11 @@ func_decl * csp_decl_plugin::mk_func_decl( name = symbol("resource"); rng = m_resource_sort; break; + case OP_JS_RESOURCE_MAKESPAN: + if (arity != 1 || domain[0] != m_resource_sort) m_manager->raise_exception("makespan expects a resource argument"); + name = symbol("makespan"); + rng = m_int_sort; + break; case OP_JS_START: if (arity != 1 || domain[0] != m_job_sort) m_manager->raise_exception("start expects a job argument"); if (num_parameters > 0) m_manager->raise_exception("no parameters"); @@ -93,21 +98,23 @@ func_decl * csp_decl_plugin::mk_func_decl( rng = m_manager->mk_bool_sort(); break; case OP_JS_JOB_RESOURCE: - if (arity != 5) m_manager->raise_exception("add-job-resource expects 5 arguments"); + if (arity != 6) m_manager->raise_exception("add-job-resource expects 6 arguments"); if (domain[0] != m_job_sort) m_manager->raise_exception("first argument of add-job-resource expects should be a job"); if (domain[1] != m_resource_sort) m_manager->raise_exception("second argument of add-job-resource expects should be a resource"); if (domain[2] != m_int_sort) m_manager->raise_exception("3rd argument of add-job-resource expects should be an integer"); if (domain[3] != m_int_sort) m_manager->raise_exception("4th argument of add-job-resource expects should be an integer"); if (domain[4] != m_int_sort) m_manager->raise_exception("5th argument of add-job-resource expects should be an integer"); + if (domain[5] != m_alist_sort) m_manager->raise_exception("6th argument of add-job-resource should be an a list of properties"); name = symbol("add-job-resource"); rng = m_alist_sort; break; case OP_JS_RESOURCE_AVAILABLE: - if (arity != 4) m_manager->raise_exception("add-resource-available expects 4 arguments"); + if (arity != 5) m_manager->raise_exception("add-resource-available expects 5 arguments"); if (domain[0] != m_resource_sort) m_manager->raise_exception("first argument of add-resource-available expects should be a resource"); if (domain[1] != m_int_sort) m_manager->raise_exception("2nd argument of add-resource-available expects should be an integer"); if (domain[2] != m_int_sort) m_manager->raise_exception("3rd argument of add-resource-available expects should be an integer"); if (domain[3] != m_int_sort) m_manager->raise_exception("4th argument of add-resource-available expects should be an integer"); + if (domain[4] != m_alist_sort) m_manager->raise_exception("5th argument of add-resource-available should be an a list of properties"); name = symbol("add-resource-available"); rng = m_alist_sort; break; @@ -116,6 +123,14 @@ func_decl * csp_decl_plugin::mk_func_decl( name = symbol("set-preemptable"); rng = m_alist_sort; break; + case OP_JS_PROPERTIES: + if (arity != 0) m_manager->raise_exception("js-properties takes no arguments"); + for (unsigned i = 0; i < num_parameters; ++i) { + if (!parameters[i].is_symbol()) m_manager->raise_exception("js-properties expects a list of keyword parameters"); + } + name = symbol("js-properties"); + rng = m_alist_sort; + break; default: UNREACHABLE(); return nullptr; @@ -148,6 +163,7 @@ void csp_decl_plugin::get_op_names(svector & op_names, symbol cons if (logic == symbol("CSP")) { op_names.push_back(builtin_name("job", OP_JS_JOB)); op_names.push_back(builtin_name("resource", OP_JS_RESOURCE)); + op_names.push_back(builtin_name("makespan", OP_JS_RESOURCE_MAKESPAN)); op_names.push_back(builtin_name("job-start", OP_JS_START)); op_names.push_back(builtin_name("job-end", OP_JS_END)); op_names.push_back(builtin_name("job2resource", OP_JS_JOB2RESOURCE)); @@ -155,7 +171,7 @@ void csp_decl_plugin::get_op_names(svector & op_names, symbol cons op_names.push_back(builtin_name("add-job-resource", OP_JS_JOB_RESOURCE)); op_names.push_back(builtin_name("add-resource-available", OP_JS_RESOURCE_AVAILABLE)); op_names.push_back(builtin_name("set-preemptable", OP_JS_JOB_PREEMPTABLE)); - + op_names.push_back(builtin_name("js-properties", OP_JS_PROPERTIES)); } } @@ -233,15 +249,29 @@ app* csp_util::mk_job2resource(unsigned j) { return m.mk_app(m.mk_func_decl(m_fid, OP_JS_JOB2RESOURCE, 0, nullptr, 1, &js, nullptr), job); } +app* csp_util::mk_makespan(unsigned r) { + app_ref resource(mk_resource(r), m); + sort* rs = m.get_sort(resource); + return m.mk_app(m.mk_func_decl(m_fid, OP_JS_RESOURCE_MAKESPAN, 0, nullptr, 1, &rs, nullptr), resource); +} + bool csp_util::is_resource(expr* e, unsigned& r) { return is_app_of(e, m_fid, OP_JS_RESOURCE) && (r = resource2id(e), true); } +bool csp_util::is_makespan(expr * e, unsigned& r) { + return is_app_of(e, m_fid, OP_JS_RESOURCE_MAKESPAN) && is_resource(to_app(e)->get_arg(0), r); +} + bool csp_util::is_job(expr* e, unsigned& j) { return is_app_of(e, m_fid, OP_JS_JOB) && (j = job2id(e), true); } -bool csp_util::is_add_resource_available(expr * e, expr *& res, unsigned& loadpct, uint64_t& start, uint64_t& end) { +bool csp_util::is_job2resource(expr* e, unsigned& j) { + return is_app_of(e, m_fid, OP_JS_JOB2RESOURCE) && (j = job2id(e), true); +} + +bool csp_util::is_add_resource_available(expr * e, expr *& res, unsigned& loadpct, uint64_t& start, uint64_t& end, svector& properties) { if (!is_app_of(e, m_fid, OP_JS_RESOURCE_AVAILABLE)) return false; res = to_app(e)->get_arg(0); arith_util a(m); @@ -252,10 +282,11 @@ bool csp_util::is_add_resource_available(expr * e, expr *& res, unsigned& loadpc start = r.get_uint64(); if (!a.is_numeral(to_app(e)->get_arg(3), r) || !r.is_uint64()) return false; end = r.get_uint64(); + if (!is_js_properties(to_app(e)->get_arg(4), properties)) return false; return true; } -bool csp_util::is_add_job_resource(expr * e, expr *& job, expr*& res, unsigned& loadpct, uint64_t& capacity, uint64_t& end) { +bool csp_util::is_add_job_resource(expr * e, expr *& job, expr*& res, unsigned& loadpct, uint64_t& capacity, uint64_t& end, svector& properties) { if (!is_app_of(e, m_fid, OP_JS_JOB_RESOURCE)) return false; job = to_app(e)->get_arg(0); res = to_app(e)->get_arg(1); @@ -267,6 +298,7 @@ bool csp_util::is_add_job_resource(expr * e, expr *& job, expr*& res, unsigned& capacity = r.get_uint64(); if (!a.is_numeral(to_app(e)->get_arg(4), r) || !r.is_uint64()) return false; end = r.get_uint64(); + if (!is_js_properties(to_app(e)->get_arg(5), properties)) return false; return true; } @@ -275,3 +307,14 @@ bool csp_util::is_set_preemptable(expr* e, expr *& job) { job = to_app(e)->get_arg(0); return true; } + +bool csp_util::is_js_properties(expr* e, svector& properties) { + if (!is_app_of(e, m_fid, OP_JS_PROPERTIES)) return false; + unsigned sz = to_app(e)->get_decl()->get_num_parameters(); + for (unsigned i = 0; i < sz; ++i) { + properties.push_back(to_app(e)->get_decl()->get_parameter(i).get_symbol()); + } + return true; +} + + diff --git a/src/ast/csp_decl_plugin.h b/src/ast/csp_decl_plugin.h index 5443180a4..8d6ad56fa 100644 --- a/src/ast/csp_decl_plugin.h +++ b/src/ast/csp_decl_plugin.h @@ -75,13 +75,15 @@ enum js_sort_kind { enum js_op_kind { OP_JS_JOB, // value of type job OP_JS_RESOURCE, // value of type resource + OP_JS_RESOURCE_MAKESPAN, // makespan of resource: the minimal resource time required for assigned jobs. OP_JS_START, // start time of a job OP_JS_END, // end time of a job OP_JS_JOB2RESOURCE, // resource associated with job OP_JS_MODEL, // jobscheduler model - OP_JS_JOB_RESOURCE, - OP_JS_JOB_PREEMPTABLE, - OP_JS_RESOURCE_AVAILABLE + OP_JS_JOB_RESOURCE, // model declaration for job assignment to resource + OP_JS_JOB_PREEMPTABLE, // model declaration for whether job is pre-emptable + OP_JS_RESOURCE_AVAILABLE, // model declaration for availability intervals of resource + OP_JS_PROPERTIES // model declaration of a set of properties. Each property is a keyword. }; class csp_decl_plugin : public decl_plugin { @@ -116,28 +118,31 @@ private: class csp_util { ast_manager& m; family_id m_fid; - csp_decl_plugin* m_plugin; + csp_decl_plugin* m_plugin; public: csp_util(ast_manager& m); sort* mk_job_sort(); sort* mk_resource_sort(); app* mk_job(unsigned j); - bool is_job(expr* e, unsigned& j); - unsigned job2id(expr* j); - app* mk_resource(unsigned r); - bool is_resource(expr* e, unsigned& r); - unsigned resource2id(expr* r); - app* mk_start(unsigned j); app* mk_end(unsigned j); app* mk_job2resource(unsigned j); + app* mk_makespan(unsigned r); - bool is_add_resource_available(expr * e, expr *& res, unsigned& loadpct, uint64_t& start, uint64_t& end); - bool is_add_job_resource(expr * e, expr *& job, expr*& res, unsigned& loadpct, uint64_t& capacity, uint64_t& end); + bool is_job(expr* e, unsigned& j); + bool is_job2resource(expr* e, unsigned& j); + bool is_resource(expr* e, unsigned& r); + bool is_makespan(expr* e, unsigned& r); + bool is_add_resource_available(expr * e, expr *& res, unsigned& loadpct, uint64_t& start, uint64_t& end, svector& properites); + bool is_add_job_resource(expr * e, expr *& job, expr*& res, unsigned& loadpct, uint64_t& capacity, uint64_t& end, svector& properites); bool is_set_preemptable(expr* e, expr *& job); - bool is_model(expr* e) const { return is_app_of(e, m_fid, OP_JS_MODEL); } + bool is_js_properties(expr* e, svector& properties); + +private: + unsigned job2id(expr* j); + unsigned resource2id(expr* r); }; diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index e5c0bcddb..5d4eb3fc5 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -351,7 +351,7 @@ namespace opt { void context::get_model_core(model_ref& mdl) { mdl = m_model; fix_model(mdl); - mdl->set_model_completion(true); + if (mdl) mdl->set_model_completion(true); TRACE("opt", tout << *mdl;); } diff --git a/src/sat/ba_solver.cpp b/src/sat/ba_solver.cpp index 4226b9791..acc3bbd21 100644 --- a/src/sat/ba_solver.cpp +++ b/src/sat/ba_solver.cpp @@ -49,6 +49,11 @@ namespace sat { return static_cast(*this); } + ba_solver::pb_base const& ba_solver::constraint::to_pb_base() const{ + SASSERT(is_pb() || is_card()); + return static_cast(*this); + } + ba_solver::xr& ba_solver::constraint::to_xr() { SASSERT(is_xr()); return static_cast(*this); @@ -1009,27 +1014,13 @@ namespace sat { // --------------------------- // conflict resolution - void ba_solver::normalize_active_coeffs() { - reset_active_var_set(); - unsigned i = 0, j = 0, sz = m_active_vars.size(); - for (; i < sz; ++i) { - bool_var v = m_active_vars[i]; - if (!m_active_var_set.contains(v) && get_coeff(v) != 0) { - m_active_var_set.insert(v); - if (j != i) { - m_active_vars[j] = m_active_vars[i]; - } - ++j; - } - } - m_active_vars.shrink(j); - } void ba_solver::inc_coeff(literal l, unsigned offset) { SASSERT(offset > 0); bool_var v = l.var(); SASSERT(v != null_bool_var); m_coeffs.reserve(v + 1, 0); + TRACE("ba_verbose", tout << l << " " << offset << "\n";); int64_t coeff0 = m_coeffs[v]; if (coeff0 == 0) { @@ -1066,59 +1057,114 @@ namespace sat { return m_coeffs.get(v, 0); } + uint64_t ba_solver::get_coeff(literal lit) const { + int64_t c1 = get_coeff(lit.var()); + SASSERT(c1 < 0 == lit.sign()); + uint64_t c = static_cast(std::abs(c1)); + m_overflow |= c != c1; + return c; + } + + ba_solver::wliteral ba_solver::get_wliteral(bool_var v) { + int64_t c1 = get_coeff(v); + literal l = literal(v, c1 < 0); + c1 = std::abs(c1); + unsigned c = static_cast(c1); + // TRACE("ba", tout << l << " " << c << "\n";); + m_overflow |= c != c1; + return wliteral(c, l); + } + unsigned ba_solver::get_abs_coeff(bool_var v) const { - int64_t c = get_coeff(v); - if (c < INT_MIN+1 || c > UINT_MAX) { - m_overflow = true; - return UINT_MAX; - } - return static_cast(std::abs(c)); + int64_t c1 = std::abs(get_coeff(v)); + unsigned c = static_cast(c1); + m_overflow |= c != c1; + return c; } int ba_solver::get_int_coeff(bool_var v) const { - int64_t c = m_coeffs.get(v, 0); - if (c < INT_MIN || c > INT_MAX) { - m_overflow = true; - return 0; - } - return static_cast(c); + int64_t c1 = m_coeffs.get(v, 0); + int c = static_cast(c1); + m_overflow |= c != c1; + return c; } void ba_solver::inc_bound(int64_t i) { - if (i < INT_MIN || i > INT_MAX) { - m_overflow = true; - return; - } int64_t new_bound = m_bound; new_bound += i; - if (new_bound < 0) { - m_overflow = true; - } - else if (new_bound > UINT_MAX) { - m_overflow = true; - } - else { - m_bound = static_cast(new_bound); - } + unsigned nb = static_cast(new_bound); + m_overflow |= new_bound < 0 || nb != new_bound; + m_bound = nb; } void ba_solver::reset_coeffs() { - for (unsigned i = 0; i < m_active_vars.size(); ++i) { + for (unsigned i = m_active_vars.size(); i-- > 0; ) { m_coeffs[m_active_vars[i]] = 0; } m_active_vars.reset(); } + void ba_solver::init_visited() { + m_visited_ts++; + if (m_visited_ts == 0) { + m_visited_ts = 1; + m_visited.reset(); + } + while (m_visited.size() < 2*s().num_vars()) { + m_visited.push_back(0); + } + } + static bool _debug_conflict = false; static literal _debug_consequent = null_literal; static unsigned_vector _debug_var2position; // #define DEBUG_CODE(_x_) _x_ - lbool ba_solver::resolve_conflict() { + void ba_solver::bail_resolve_conflict(unsigned idx) { + literal_vector const& lits = s().m_trail; + while (m_num_marks > 0) { + bool_var v = lits[idx].var(); + if (s().is_marked(v)) { + s().reset_mark(v); + --m_num_marks; + } + if (idx == 0 && !_debug_conflict) { + _debug_conflict = true; + _debug_var2position.reserve(s().num_vars()); + for (unsigned i = 0; i < lits.size(); ++i) { + _debug_var2position[lits[i].var()] = i; + } + IF_VERBOSE(0, + active2pb(m_A); + uint64_t c = 0; + for (wliteral l : m_A.m_wlits) c += l.first; + verbose_stream() << "sum of coefficients: " << c << "\n"; + display(verbose_stream(), m_A, true); + verbose_stream() << "conflicting literal: " << s().m_not_l << "\n";); + + for (literal l : lits) { + if (s().is_marked(l.var())) { + IF_VERBOSE(0, verbose_stream() << "missing mark: " << l << "\n";); + s().reset_mark(l.var()); + } + } + m_num_marks = 0; + resolve_conflict(); + } + --idx; + } + } + + lbool ba_solver::resolve_conflict() { if (0 == m_num_propagations_since_pop) { return l_undef; } + + if (s().m_config.m_pb_resolve == PB_ROUNDING) { + return resolve_conflict_rs(); + } + m_overflow = false; reset_coeffs(); m_num_marks = 0; @@ -1127,6 +1173,9 @@ namespace sat { justification js = s().m_conflict; TRACE("ba", tout << consequent << " " << js << "\n";); m_conflict_lvl = s().get_max_lvl(consequent, js); + if (m_conflict_lvl == 0) { + return l_undef; + } if (consequent != null_literal) { consequent.neg(); process_antecedent(consequent, 1); @@ -1256,7 +1305,6 @@ namespace sat { process_next_resolvent: // find the next marked variable in the assignment stack - // bool_var v; while (true) { consequent = lits[idx]; @@ -1290,77 +1338,353 @@ namespace sat { DEBUG_CODE(for (bool_var i = 0; i < static_cast(s().num_vars()); ++i) SASSERT(!s().is_marked(i));); SASSERT(validate_lemma()); - normalize_active_coeffs(); - if (!create_asserting_lemma()) { goto bail_out; } + active2lemma(); + DEBUG_CODE(VERIFY(validate_conflict(m_lemma, m_A));); - TRACE("ba", tout << m_lemma << "\n";); - - if (get_config().m_drat) { - svector ps; // TBD fill in - drat_add(m_lemma, ps); - } - - s().m_lemma.reset(); - s().m_lemma.append(m_lemma); - for (unsigned i = 1; i < m_lemma.size(); ++i) { - CTRACE("ba", s().is_marked(m_lemma[i].var()), tout << "marked: " << m_lemma[i] << "\n";); - s().mark(m_lemma[i].var()); - } - return l_true; bail_out: + if (m_overflow) { + ++m_stats.m_num_overflow; + m_overflow = false; + } + bail_resolve_conflict(idx); + return l_undef; + } - m_overflow = false; + unsigned ba_solver::ineq::bv_coeff(bool_var v) const { + for (unsigned i = size(); i-- > 0; ) { + if (lit(i).var() == v) return coeff(i); + } + UNREACHABLE(); + return 0; + } + + void ba_solver::ineq::divide(unsigned c) { + if (c == 1) return; + for (unsigned i = size(); i-- > 0; ) { + m_wlits[i].first = (coeff(i) + c - 1) / c; + } + m_k = (m_k + c - 1) / c; + } + + /** + * Remove literal at position i, subtract coefficient from bound. + */ + void ba_solver::ineq::weaken(unsigned i) { + unsigned ci = coeff(i); + SASSERT(m_k >= ci); + m_k -= ci; + m_wlits[i] = m_wlits.back(); + m_wlits.pop_back(); + } + + /** + * Round coefficient of inequality to 1. + */ + void ba_solver::round_to_one(ineq& ineq, bool_var v) { + unsigned c = ineq.bv_coeff(v); + if (c == 1) return; + unsigned sz = ineq.size(); + for (unsigned i = 0; i < sz; ++i) { + unsigned ci = ineq.coeff(i); + unsigned q = ci % c; + if (q != 0 && !is_false(ineq.lit(i))) { + if (q == ci) { + ineq.weaken(i); + --i; + --sz; + } + else { + ineq.m_wlits[i].first -= q; + ineq.m_k -= q; + } + } + } + ineq.divide(c); + TRACE("ba", display(tout << "var: " << v << " " << c << ": ", ineq, true);); + } + + void ba_solver::round_to_one(bool_var w) { + unsigned c = get_abs_coeff(w); + if (c == 1 || c == 0) return; + for (bool_var v : m_active_vars) { + wliteral wl = get_wliteral(v); + unsigned q = wl.first % c; + if (q != 0 && !is_false(wl.second)) { + m_coeffs[v] = wl.first - q; + m_bound -= q; + SASSERT(m_bound > 0); + } + } + SASSERT(validate_lemma()); + divide(c); + SASSERT(validate_lemma()); + TRACE("ba", active2pb(m_B); display(tout, m_B, true);); + } + + void ba_solver::divide(unsigned c) { + SASSERT(c != 0); + if (c == 1) return; + reset_active_var_set(); + unsigned j = 0, sz = m_active_vars.size(); + for (unsigned i = 0; i < sz; ++i) { + bool_var v = m_active_vars[i]; + int ci = get_int_coeff(v); + if (!test_and_set_active(v) || ci == 0) continue; + if (ci > 0) { + m_coeffs[v] = (ci + c - 1) / c; + } + else { + m_coeffs[v] = -static_cast((-ci + c - 1) / c); + } + m_active_vars[j++] = v; + } + m_active_vars.shrink(j); + m_bound = static_cast((m_bound + c - 1) / c); + } + + void ba_solver::resolve_on(literal consequent) { + round_to_one(consequent.var()); + m_coeffs[consequent.var()] = 0; + } + + void ba_solver::resolve_with(ineq const& ineq) { + TRACE("ba", display(tout, ineq, true);); + inc_bound(ineq.m_k); + TRACE("ba", tout << "bound: " << m_bound << "\n";); + + for (unsigned i = ineq.size(); i-- > 0; ) { + literal l = ineq.lit(i); + inc_coeff(l, static_cast(ineq.coeff(i))); + TRACE("ba", tout << "bound: " << m_bound << " lit: " << l << " coeff: " << ineq.coeff(i) << "\n";); + } + } + + void ba_solver::reset_marks(unsigned idx) { while (m_num_marks > 0) { - bool_var v = lits[idx].var(); + SASSERT(idx > 0); + bool_var v = s().m_trail[idx].var(); if (s().is_marked(v)) { s().reset_mark(v); --m_num_marks; } - if (idx == 0 && !_debug_conflict) { - _debug_conflict = true; - _debug_var2position.reserve(s().num_vars()); - for (unsigned i = 0; i < lits.size(); ++i) { - _debug_var2position[lits[i].var()] = i; - } - IF_VERBOSE(0, - active2pb(m_A); - uint64_t c = 0; - for (uint64_t c1 : m_A.m_coeffs) c += c1; - verbose_stream() << "sum of coefficients: " << c << "\n"; - display(verbose_stream(), m_A, true); - verbose_stream() << "conflicting literal: " << s().m_not_l << "\n";); + --idx; + } + } + + /** + * \brief mark variables that are on the assignment stack but + * below the current processing level. + */ + void ba_solver::mark_variables(ineq const& ineq) { + for (wliteral wl : ineq.m_wlits) { + literal l = wl.second; + if (!is_false(l)) continue; + bool_var v = l.var(); + unsigned level = lvl(v); + if (!s().is_marked(v) && !is_visited(v) && level == m_conflict_lvl) { + s().mark(v); + ++m_num_marks; + } + } + } - for (literal l : lits) { - if (s().is_marked(l.var())) { - IF_VERBOSE(0, verbose_stream() << "missing mark: " << l << "\n";); - s().reset_mark(l.var()); + lbool ba_solver::resolve_conflict_rs() { + if (0 == m_num_propagations_since_pop) { + return l_undef; + } + m_overflow = false; + reset_coeffs(); + init_visited(); + m_num_marks = 0; + m_bound = 0; + literal consequent = s().m_not_l; + justification js = s().m_conflict; + m_conflict_lvl = s().get_max_lvl(consequent, js); + if (m_conflict_lvl == 0) { + return l_undef; + } + if (consequent != null_literal) { + consequent.neg(); + process_antecedent(consequent, 1); + } + TRACE("ba", tout << consequent << " " << js << "\n";); + unsigned idx = s().m_trail.size() - 1; + + do { + TRACE("ba", s().display_justification(tout << "process consequent: " << consequent << " : ", js) << "\n"; + if (consequent != null_literal) { active2pb(m_A); display(tout, m_A, true); } + ); + + switch (js.get_kind()) { + case justification::NONE: + SASSERT(consequent != null_literal); + round_to_one(consequent.var()); + inc_bound(1); + inc_coeff(consequent, 1); + break; + case justification::BINARY: + SASSERT(consequent != null_literal); + round_to_one(consequent.var()); + inc_bound(1); + inc_coeff(consequent, 1); + process_antecedent(js.get_literal()); + break; + case justification::TERNARY: + SASSERT(consequent != null_literal); + round_to_one(consequent.var()); + inc_bound(1); + inc_coeff(consequent, 1); + process_antecedent(js.get_literal1()); + process_antecedent(js.get_literal2()); + break; + case justification::CLAUSE: { + clause & c = s().get_clause(js); + unsigned i = 0; + if (consequent != null_literal) { + round_to_one(consequent.var()); + inc_coeff(consequent, 1); + if (c[0] == consequent) { + i = 1; + } + else { + SASSERT(c[1] == consequent); + process_antecedent(c[0]); + i = 2; } } - m_num_marks = 0; - resolve_conflict(); + inc_bound(1); + unsigned sz = c.size(); + for (; i < sz; i++) + process_antecedent(c[i]); + break; } + case justification::EXT_JUSTIFICATION: { + ++m_stats.m_num_resolves; + ext_justification_idx index = js.get_ext_justification_idx(); + constraint& cnstr = index2constraint(index); + switch (cnstr.tag()) { + case card_t: + case pb_t: { + pb_base const& p = cnstr.to_pb_base(); + unsigned k = p.k(), sz = p.size(); + m_A.reset(0); + for (unsigned i = 0; i < sz; ++i) { + literal l = p.get_lit(i); + unsigned c = p.get_coeff(i); + if (l == consequent || !is_visited(l.var())) { + m_A.push(l, c); + } + else { + SASSERT(k > c); + TRACE("ba", tout << "visited: " << l << "\n";); + k -= c; + } + } + SASSERT(k > 0); + if (p.lit() != null_literal) m_A.push(~p.lit(), k); + m_A.m_k = k; + break; + } + default: + constraint2pb(cnstr, consequent, 1, m_A); + break; + } + mark_variables(m_A); + if (consequent == null_literal) { + SASSERT(validate_ineq(m_A)); + m_bound = static_cast(m_A.m_k); + for (wliteral wl : m_A.m_wlits) { + process_antecedent(wl.second, wl.first); + } + } + else { + round_to_one(consequent.var()); + if (cnstr.is_pb()) round_to_one(m_A, consequent.var()); + SASSERT(validate_ineq(m_A)); + resolve_with(m_A); + } + break; + } + default: + UNREACHABLE(); + break; + } + + SASSERT(validate_lemma()); + cut(); + + // find the next marked variable in the assignment stack + bool_var v; + while (true) { + consequent = s().m_trail[idx]; + v = consequent.var(); + mark_visited(v); + if (s().is_marked(v)) { + int64_t c = get_coeff(v); + if (c == 0 || (c < 0 == consequent.sign())) { + s().reset_mark(v); + --m_num_marks; + } + else { + break; + } + } + if (idx == 0) { + TRACE("ba", tout << "there is no consequent\n";); + goto bail_out; + } + --idx; + } + + SASSERT(lvl(v) == m_conflict_lvl); + s().reset_mark(v); --idx; + --m_num_marks; + js = s().m_justification[v]; + } + while (m_num_marks > 0 && !m_overflow); + TRACE("ba", active2pb(m_A); display(tout, m_A, true);); + + // TBD: check if this is useful + if (!m_overflow && consequent != null_literal) { + round_to_one(consequent.var()); + } + if (!m_overflow && create_asserting_lemma()) { + active2lemma(); + return l_true; + } + + bail_out: + TRACE("ba", tout << "bail " << m_overflow << "\n";); + if (m_overflow) { + ++m_stats.m_num_overflow; + m_overflow = false; } return l_undef; } - bool ba_solver::create_asserting_lemma() { - bool adjusted = false; - adjust_conflict_level: + bool ba_solver::create_asserting_lemma() { int64_t bound64 = m_bound; int64_t slack = -bound64; - for (bool_var v : m_active_vars) { - slack += get_abs_coeff(v); + reset_active_var_set(); + unsigned j = 0, sz = m_active_vars.size(); + for (unsigned i = 0; i < sz; ++i) { + bool_var v = m_active_vars[i]; + unsigned c = get_abs_coeff(v); + if (!test_and_set_active(v) || c == 0) continue; + slack += c; + m_active_vars[j++] = v; } + m_active_vars.shrink(j); m_lemma.reset(); m_lemma.push_back(null_literal); unsigned num_skipped = 0; @@ -1395,29 +1719,34 @@ namespace sat { } } if (slack >= 0) { + TRACE("ba", tout << "slack is non-negative\n";); IF_VERBOSE(20, verbose_stream() << "(sat.card slack: " << slack << " skipped: " << num_skipped << ")\n";); return false; } if (m_overflow) { + TRACE("ba", tout << "overflow\n";); return false; } if (m_lemma[0] == null_literal) { if (m_lemma.size() == 1) { s().set_conflict(justification()); - return false; } + TRACE("ba", tout << "no asserting literal\n";); return false; - unsigned old_level = m_conflict_lvl; - m_conflict_lvl = 0; - for (unsigned i = 1; i < m_lemma.size(); ++i) { - m_conflict_lvl = std::max(m_conflict_lvl, lvl(m_lemma[i])); - } - IF_VERBOSE(1, verbose_stream() << "(sat.backjump :new-level " << m_conflict_lvl << " :old-level " << old_level << ")\n";); - adjusted = true; - goto adjust_conflict_level; } - if (!adjusted) { - active2card(); + + TRACE("ba", tout << m_lemma << "\n";); + + if (get_config().m_drat) { + svector ps; // TBD fill in + drat_add(m_lemma, ps); + } + + s().m_lemma.reset(); + s().m_lemma.append(m_lemma); + for (unsigned i = 1; i < m_lemma.size(); ++i) { + CTRACE("ba", s().is_marked(m_lemma[i].var()), tout << "marked: " << m_lemma[i] << "\n";); + s().mark(m_lemma[i].var()); } return true; } @@ -1461,10 +1790,16 @@ namespace sat { } if (g >= 2) { - normalize_active_coeffs(); - for (bool_var v : m_active_vars) { + reset_active_var_set(); + unsigned j = 0, sz = m_active_vars.size(); + for (unsigned i = 0; i < sz; ++i) { + bool_var v = m_active_vars[i]; + int64_t c = m_coeffs[v]; + if (!test_and_set_active(v) || c == 0) continue; m_coeffs[v] /= static_cast(g); + m_active_vars[j++] = v; } + m_active_vars.shrink(j); m_bound = (m_bound + g - 1) / g; ++m_stats.m_num_cut; } @@ -1500,9 +1835,8 @@ namespace sat { bool_var v = l.var(); unsigned level = lvl(v); - if (level > 0 && !s().is_marked(v) && level == m_conflict_lvl) { + if (!s().is_marked(v) && level == m_conflict_lvl) { s().mark(v); - TRACE("sat_verbose", tout << "Mark: v" << v << "\n";); ++m_num_marks; if (_debug_conflict && _debug_consequent != null_literal && _debug_var2position[_debug_consequent.var()] < _debug_var2position[l.var()]) { IF_VERBOSE(0, verbose_stream() << "antecedent " << l << " is above consequent in stack\n";); @@ -1527,7 +1861,8 @@ namespace sat { return p; } - ba_solver::ba_solver(): m_solver(0), m_lookahead(0), m_unit_walk(0), m_constraint_id(0), m_ba(*this), m_sort(m_ba) { + ba_solver::ba_solver(): m_solver(0), m_lookahead(0), m_unit_walk(0), + m_allocator("ba"), m_constraint_id(0), m_ba(*this), m_sort(m_ba) { TRACE("ba", tout << this << "\n";); m_num_propagations_since_pop = 0; } @@ -1551,10 +1886,10 @@ namespace sat { if (k == 1 && lit == null_literal) { literal_vector _lits(lits); s().mk_clause(_lits.size(), _lits.c_ptr(), learned); - return 0; + return nullptr; } if (!learned && clausify(lit, lits.size(), lits.c_ptr(), k)) { - return 0; + return nullptr; } void * mem = m_allocator.allocate(card::get_obj_size(lits.size())); card* c = new (mem) card(next_id(), lit, lits, k); @@ -1615,7 +1950,7 @@ namespace sat { bool units = true; for (wliteral wl : wlits) units &= wl.first == 1; if (k == 0 && lit == null_literal) { - return 0; + return nullptr; } if (units || k == 1) { literal_vector lits; @@ -2342,8 +2677,12 @@ namespace sat { constraint* c = m_learned[i]; if (!m_constraint_to_reinit.contains(c)) { remove_constraint(*c, "gc"); + m_allocator.deallocate(c->obj_size(), c); ++removed; } + else { + m_learned[new_sz++] = c; + } } m_stats.m_num_gc += removed; m_learned.shrink(new_sz); @@ -2493,7 +2832,8 @@ namespace sat { set_non_external(); if (get_config().m_elim_vars) elim_pure(); for (unsigned sz = m_constraints.size(), i = 0; i < sz; ++i) subsumption(*m_constraints[i]); - for (unsigned sz = m_learned.size(), i = 0; i < sz; ++i) subsumption(*m_learned[i]); + for (unsigned sz = m_learned.size(), i = 0; i < sz; ++i) subsumption(*m_learned[i]); + unit_strengthen(); cleanup_clauses(); cleanup_constraints(); update_pure(); @@ -2939,9 +3279,10 @@ namespace sat { bool found_dup = false; bool found_root = false; + init_visited(); for (unsigned i = 0; i < c.size(); ++i) { literal l = c.get_lit(i); - if (is_marked(l)) { + if (is_visited(l)) { found_dup = true; break; } @@ -2951,10 +3292,7 @@ namespace sat { } } for (unsigned i = 0; i < c.size(); ++i) { - literal l = c.get_lit(i); - unmark_visited(l); - unmark_visited(~l); - found_root |= l.var() == root.var(); + found_root |= c.get_lit(i).var() == root.var(); } if (found_root) { @@ -3111,6 +3449,98 @@ namespace sat { return pure_literals; } + /** + * Strengthen inequalities using binary implication information. + * + * x -> ~y, x -> ~z, y + z + u >= 2 + * ---------------------------------- + * y + z + u + ~x >= 3 + * + * for c : constraints + * for l : c: + * slack <- of c under root(~l) + * if slack < 0: + * add ~root(~l) to c, k <- k + 1 + */ + void ba_solver::unit_strengthen() { + big big(s().m_rand); + big.init(s(), true); + for (unsigned sz = m_constraints.size(), i = 0; i < sz; ++i) + unit_strengthen(big, *m_constraints[i]); + for (unsigned sz = m_learned.size(), i = 0; i < sz; ++i) + unit_strengthen(big, *m_learned[i]); + } + + void ba_solver::unit_strengthen(big& big, constraint& c) { + if (c.was_removed()) return; + switch (c.tag()) { + case card_t: + unit_strengthen(big, c.to_card()); + break; + case pb_t: + unit_strengthen(big, c.to_pb()); + break; + default: + break; + } + } + + void ba_solver::unit_strengthen(big& big, pb_base& p) { + if (p.lit() != null_literal) return; + unsigned sz = p.size(); + for (unsigned i = 0; i < sz; ++i) { + literal u = p.get_lit(i); + literal r = big.get_root(u); + if (r == u) continue; + unsigned k = p.k(), b = 0; + for (unsigned j = 0; j < sz; ++j) { + literal v = p.get_lit(j); + if (r == big.get_root(v)) { + b += p.get_coeff(j); + } + } + if (b > k) { + r.neg(); + unsigned coeff = b - k; + + svector wlits; + // add coeff * r to p + wlits.push_back(wliteral(coeff, r)); + for (unsigned j = 0; j < sz; ++j) { + u = p.get_lit(j); + unsigned c = p.get_coeff(j); + if (r == u) { + wlits[0].first += c; + } + else if (~r == u) { + if (coeff == c) { + wlits[0] = wlits.back(); + wlits.pop_back(); + b -= c; + } + else if (coeff < c) { + wlits[0].first = c - coeff; + wlits[0].second.neg(); + b -= coeff; + } + else { + // coeff > c + wlits[0].first = coeff - c; + b -= c; + } + } + else { + wlits.push_back(wliteral(c, u)); + } + } + ++m_stats.m_num_big_strengthenings; + p.set_removed(); + constraint* c = add_pb_ge(null_literal, wlits, b, p.learned()); + return; + } + } + } + void ba_solver::subsumption(constraint& cnstr) { if (cnstr.was_removed()) return; switch (cnstr.tag()) { @@ -3199,10 +3629,10 @@ namespace sat { unsigned common = 0; comp.reset(); for (literal l : c2) { - if (is_marked(l)) { + if (is_visited(l)) { ++common; } - else if (is_marked(~l)) { + else if (is_visited(~l)) { comp.push_back(l); } else { @@ -3224,10 +3654,10 @@ namespace sat { self = false; for (literal l : c2) { - if (is_marked(l)) { + if (is_visited(l)) { ++common; } - else if (is_marked(~l)) { + else if (is_visited(~l)) { ++complement; } else { @@ -3251,10 +3681,10 @@ namespace sat { unsigned num_sub = 0; for (unsigned i = 0; i < p2.size(); ++i) { literal l = p2.get_lit(i); - if (is_marked(l) && m_weights[l.index()] <= p2.get_coeff(i)) { + if (is_visited(l) && m_weights[l.index()] <= p2.get_coeff(i)) { ++num_sub; } - if (p1.size() + i > p2.size() + num_sub) return false; + if (p1.size() + i > p2.size() + num_sub) return false; } return num_sub == p1.size(); } @@ -3319,7 +3749,7 @@ namespace sat { clear_watch(c2); unsigned j = 0; for (unsigned i = 0; i < c2.size(); ++i) { - if (!is_marked(~c2[i])) { + if (!is_visited(~c2[i])) { c2[j++] = c2[i]; } } @@ -3355,7 +3785,7 @@ namespace sat { void ba_solver::binary_subsumption(card& c1, literal lit) { if (c1.k() + 1 != c1.size()) return; - SASSERT(is_marked(lit)); + SASSERT(is_visited(lit)); SASSERT(!c1.was_removed()); watch_list & wlist = get_wlist(~lit); watch_list::iterator it = wlist.begin(); @@ -3363,7 +3793,7 @@ namespace sat { watch_list::iterator end = wlist.end(); for (; it != end; ++it) { watched w = *it; - if (w.is_binary_clause() && is_marked(w.get_literal())) { + if (w.is_binary_clause() && is_visited(w.get_literal())) { ++m_stats.m_num_bin_subsumes; IF_VERBOSE(10, verbose_stream() << c1 << " subsumes (" << lit << " " << w.get_literal() << ")\n";); if (!w.is_learned()) { @@ -3385,6 +3815,7 @@ namespace sat { return; } clause_vector removed_clauses; + init_visited(); for (literal l : c1) mark_visited(l); for (unsigned i = 0; i < std::min(c1.size(), c1.k() + 1); ++i) { literal lit = c1[i]; @@ -3392,7 +3823,6 @@ namespace sat { clause_subsumption(c1, lit, removed_clauses); binary_subsumption(c1, lit); } - for (literal l : c1) unmark_visited(l); m_clause_removed |= !removed_clauses.empty(); for (clause *c : removed_clauses) { c->set_removed(true); @@ -3404,8 +3834,9 @@ namespace sat { if (p1.was_removed() || p1.lit() != null_literal) { return; } + init_visited(); for (wliteral l : p1) { - SASSERT(m_weights[l.second.index()] == 0); + SASSERT(m_weights.get(l.second.index(), 0) == 0); m_weights.setx(l.second.index(), l.first, 0); mark_visited(l.second); } @@ -3415,7 +3846,6 @@ namespace sat { } for (wliteral l : p1) { m_weights[l.second.index()] = 0; - unmark_visited(l.second); } } @@ -3612,10 +4042,11 @@ namespace sat { } } - void ba_solver::display(std::ostream& out, ineq& ineq, bool values) const { - for (unsigned i = 0; i < ineq.m_lits.size(); ++i) { - out << ineq.m_coeffs[i] << "*" << ineq.m_lits[i] << " "; - if (values) out << value(ineq.m_lits[i]) << " "; + void ba_solver::display(std::ostream& out, ineq const& ineq, bool values) const { + for (unsigned i = 0; i < ineq.size(); ++i) { + if (ineq.coeff(i) != 1) out << ineq.coeff(i) << "*"; + out << ineq.lit(i) << " "; + if (values) out << value(ineq.lit(i)) << " "; } out << ">= " << ineq.m_k << "\n"; } @@ -3705,6 +4136,10 @@ namespace sat { st.update("ba resolves", m_stats.m_num_resolves); st.update("ba cuts", m_stats.m_num_cut); st.update("ba gc", m_stats.m_num_gc); + st.update("ba overflow", m_stats.m_num_overflow); + st.update("ba big strengthenings", m_stats.m_num_big_strengthenings); + st.update("ba lemmas", m_stats.m_num_lemmas); + st.update("ba subsumes", m_stats.m_num_bin_subsumes + m_stats.m_num_clause_subsumes + m_stats.m_num_pb_subsumes); } bool ba_solver::validate_unit_propagation(card const& c, literal alit) const { @@ -3799,62 +4234,88 @@ namespace sat { int64_t val = -bound64; reset_active_var_set(); for (bool_var v : m_active_vars) { - if (m_active_var_set.contains(v)) continue; - int64_t coeff = get_coeff(v); - if (coeff == 0) continue; - m_active_var_set.insert(v); - literal lit(v, false); - if (coeff < 0 && value(lit) != l_true) { - val -= coeff; - } - else if (coeff > 0 && value(lit) != l_false) { - val += coeff; + if (!test_and_set_active(v)) continue; + wliteral wl = get_wliteral(v); + if (wl.first == 0) continue; + if (!is_false(wl.second)) { + val += wl.first; } } - CTRACE("ba", val >= 0, active2pb(m_A); display(tout, m_A);); + CTRACE("ba", val >= 0, active2pb(m_A); display(tout, m_A, true);); return val < 0; } + /** + * the slack of inequalities on the stack should be non-positive. + */ + bool ba_solver::validate_ineq(ineq const& ineq) const { + int64_t k = -static_cast(ineq.m_k); + for (wliteral wl : ineq.m_wlits) { + if (!is_false(wl.second)) + k += wl.first; + } + CTRACE("ba", k > 0, display(tout, ineq, true);); + return k <= 0; + } + void ba_solver::reset_active_var_set() { while (!m_active_var_set.empty()) m_active_var_set.erase(); } - void ba_solver::active2pb(ineq& p) { - reset_active_var_set(); - p.reset(m_bound); - for (bool_var v : m_active_vars) { - if (m_active_var_set.contains(v)) continue; - int64_t coeff = get_coeff(v); - if (coeff == 0) continue; + bool ba_solver::test_and_set_active(bool_var v) { + if (m_active_var_set.contains(v)) { + return false; + } + else { m_active_var_set.insert(v); - literal lit(v, coeff < 0); - p.m_lits.push_back(lit); - p.m_coeffs.push_back(std::abs(coeff)); + return true; + } + } + + void ba_solver::active2pb(ineq& p) { + p.reset(m_bound); + active2wlits(p.m_wlits); + } + + void ba_solver::active2wlits() { + m_wlits.reset(); + active2wlits(m_wlits); + } + + void ba_solver::active2wlits(svector& wlits) { + uint64_t sum = 0; + reset_active_var_set(); + for (bool_var v : m_active_vars) { + if (!test_and_set_active(v)) continue; + wliteral wl = get_wliteral(v); + if (wl.first == 0) continue; + wlits.push_back(wl); + sum += wl.first; + } + m_overflow |= sum >= UINT_MAX/2; + } + + ba_solver::constraint* ba_solver::active2lemma() { + switch (s().m_config.m_pb_lemma_format) { + case PB_LEMMA_CARDINALITY: + return active2card(); + case PB_LEMMA_PB: + return active2constraint(); + default: + UNREACHABLE(); + return nullptr; } } ba_solver::constraint* ba_solver::active2constraint() { - reset_active_var_set(); - m_wlits.reset(); - uint64_t sum = 0; - if (m_bound == 1) return 0; - if (m_overflow) return 0; - - for (bool_var v : m_active_vars) { - int coeff = get_int_coeff(v); - if (m_active_var_set.contains(v) || coeff == 0) continue; - m_active_var_set.insert(v); - literal lit(v, coeff < 0); - m_wlits.push_back(wliteral(get_abs_coeff(v), lit)); - sum += get_abs_coeff(v); + active2wlits(); + if (m_overflow) { + return nullptr; } - - if (m_overflow || sum >= UINT_MAX/2) { - return 0; - } - else { - return add_pb_ge(null_literal, m_wlits, m_bound, true); - } + constraint* c = add_pb_ge(null_literal, m_wlits, m_bound, true); + TRACE("ba", if (c) display(tout, *c, true);); + ++m_stats.m_num_lemmas; + return c; } /* @@ -3889,11 +4350,9 @@ namespace sat { ba_solver::constraint* ba_solver::active2card() { - normalize_active_coeffs(); - m_wlits.reset(); - for (bool_var v : m_active_vars) { - int coeff = get_int_coeff(v); - m_wlits.push_back(std::make_pair(get_abs_coeff(v), literal(v, coeff < 0))); + active2wlits(); + if (m_overflow) { + return nullptr; } std::sort(m_wlits.begin(), m_wlits.end(), compare_wlit()); unsigned k = 0; @@ -3905,7 +4364,7 @@ namespace sat { ++k; } if (k == 1) { - return 0; + return nullptr; } while (!m_wlits.empty()) { wliteral wl = m_wlits.back(); @@ -3928,16 +4387,12 @@ namespace sat { ++num_max_level; } } - if (m_overflow) return 0; + if (m_overflow) { + return nullptr; + } if (slack >= k) { -#if 0 - return active2constraint(); - active2pb(m_A); - std::cout << "not asserting\n"; - display(std::cout, m_A, true); -#endif - return 0; + return nullptr; } // produce asserting cardinality constraint @@ -3947,8 +4402,9 @@ namespace sat { } constraint* c = add_at_least(null_literal, lits, k, true); + ++m_stats.m_num_lemmas; + if (c) { - // IF_VERBOSE(0, verbose_stream() << *c << "\n";); lits.reset(); for (wliteral wl : m_wlits) { if (value(wl.second) == l_false) lits.push_back(wl.second); @@ -3963,15 +4419,18 @@ namespace sat { void ba_solver::justification2pb(justification const& js, literal lit, unsigned offset, ineq& ineq) { switch (js.get_kind()) { case justification::NONE: + SASSERT(lit != null_literal); ineq.reset(offset); ineq.push(lit, offset); break; case justification::BINARY: + SASSERT(lit != null_literal); ineq.reset(offset); ineq.push(lit, offset); ineq.push(js.get_literal(), offset); break; case justification::TERNARY: + SASSERT(lit != null_literal); ineq.reset(offset); ineq.push(lit, offset); ineq.push(js.get_literal1(), offset); @@ -3986,35 +4445,7 @@ namespace sat { case justification::EXT_JUSTIFICATION: { ext_justification_idx index = js.get_ext_justification_idx(); constraint& cnstr = index2constraint(index); - switch (cnstr.tag()) { - case card_t: { - card& c = cnstr.to_card(); - ineq.reset(offset*c.k()); - for (literal l : c) ineq.push(l, offset); - if (c.lit() != null_literal) ineq.push(~c.lit(), offset*c.k()); - break; - } - case pb_t: { - pb& p = cnstr.to_pb(); - ineq.reset(p.k()); - for (wliteral wl : p) ineq.push(wl.second, wl.first); - if (p.lit() != null_literal) ineq.push(~p.lit(), p.k()); - break; - } - case xr_t: { - xr& x = cnstr.to_xr(); - literal_vector ls; - get_antecedents(lit, x, ls); - ineq.reset(offset); - for (literal l : ls) ineq.push(~l, offset); - literal lxr = x.lit(); - if (lxr != null_literal) ineq.push(~lxr, offset); - break; - } - default: - UNREACHABLE(); - break; - } + constraint2pb(cnstr, lit, offset, ineq); break; } default: @@ -4023,6 +4454,38 @@ namespace sat { } } + void ba_solver::constraint2pb(constraint& cnstr, literal lit, unsigned offset, ineq& ineq) { + switch (cnstr.tag()) { + case card_t: { + card& c = cnstr.to_card(); + ineq.reset(offset*c.k()); + for (literal l : c) ineq.push(l, offset); + if (c.lit() != null_literal) ineq.push(~c.lit(), offset*c.k()); + break; + } + case pb_t: { + pb& p = cnstr.to_pb(); + ineq.reset(offset * p.k()); + for (wliteral wl : p) ineq.push(wl.second, offset * wl.first); + if (p.lit() != null_literal) ineq.push(~p.lit(), offset * p.k()); + break; + } + case xr_t: { + xr& x = cnstr.to_xr(); + literal_vector ls; + SASSERT(lit != null_literal); + get_antecedents(lit, x, ls); + ineq.reset(offset); + for (literal l : ls) ineq.push(~l, offset); + literal lxr = x.lit(); + if (lxr != null_literal) ineq.push(~lxr, offset); + break; + } + default: + UNREACHABLE(); + break; + } + } // validate that m_A & m_B implies m_C @@ -4030,14 +4493,14 @@ namespace sat { return true; u_map coeffs; uint64_t k = m_A.m_k + m_B.m_k; - for (unsigned i = 0; i < m_A.m_lits.size(); ++i) { - uint64_t coeff = m_A.m_coeffs[i]; - SASSERT(!coeffs.contains(m_A.m_lits[i].index())); - coeffs.insert(m_A.m_lits[i].index(), coeff); + for (unsigned i = 0; i < m_A.size(); ++i) { + uint64_t coeff = m_A.coeff(i); + SASSERT(!coeffs.contains(m_A.lit(i).index())); + coeffs.insert(m_A.lit(i).index(), coeff); } - for (unsigned i = 0; i < m_B.m_lits.size(); ++i) { - uint64_t coeff1 = m_B.m_coeffs[i], coeff2; - literal lit = m_B.m_lits[i]; + for (unsigned i = 0; i < m_B.size(); ++i) { + uint64_t coeff1 = m_B.coeff(i), coeff2; + literal lit = m_B.lit(i); if (coeffs.find((~lit).index(), coeff2)) { if (coeff1 == coeff2) { coeffs.remove((~lit).index()); @@ -4062,11 +4525,11 @@ namespace sat { } } // C is above the sum of A and B - for (unsigned i = 0; i < m_C.m_lits.size(); ++i) { - literal lit = m_C.m_lits[i]; + for (unsigned i = 0; i < m_C.size(); ++i) { + literal lit = m_C.lit(i); uint64_t coeff; if (coeffs.find(lit.index(), coeff)) { - if (coeff > m_C.m_coeffs[i] && m_C.m_coeffs[i] < m_C.m_k) { + if (coeff > m_C.coeff(i) && m_C.coeff(i) < m_C.m_k) { goto violated; } coeffs.remove(lit.index()); @@ -4113,15 +4576,15 @@ namespace sat { */ literal ba_solver::translate_to_sat(solver& s, u_map& translation, ineq const& pb) { SASSERT(pb.m_k > 0); - if (pb.m_lits.size() > 1) { + if (pb.size() > 1) { ineq a, b; a.reset(pb.m_k); b.reset(pb.m_k); - for (unsigned i = 0; i < pb.m_lits.size()/2; ++i) { - a.push(pb.m_lits[i], pb.m_coeffs[i]); + for (unsigned i = 0; i < pb.size()/2; ++i) { + a.push(pb.lit(i), pb.coeff(i)); } - for (unsigned i = pb.m_lits.size()/2; i < pb.m_lits.size(); ++i) { - b.push(pb.m_lits[i], pb.m_coeffs[i]); + for (unsigned i = pb.size()/2; i < pb.size(); ++i) { + b.push(pb.lit(i), pb.coeff(i)); } bool_var v = s.mk_var(); literal lit(v, false); @@ -4133,8 +4596,8 @@ namespace sat { s.mk_clause(lits); return lit; } - if (pb.m_coeffs[0] >= pb.m_k) { - return translate_to_sat(s, translation, pb.m_lits[0]); + if (pb.coeff(0) >= pb.m_k) { + return translate_to_sat(s, translation, pb.lit(0)); } else { return null_literal; @@ -4186,9 +4649,9 @@ namespace sat { ba_solver::ineq ba_solver::negate(ineq const& a) const { ineq result; uint64_t sum = 0; - for (unsigned i = 0; i < a.m_lits.size(); ++i) { - result.push(~a.m_lits[i], a.m_coeffs[i]); - sum += a.m_coeffs[i]; + for (unsigned i = 0; i < a.size(); ++i) { + result.push(~a.lit(i), a.coeff(i)); + sum += a.coeff(i); } SASSERT(sum >= a.m_k + 1); result.m_k = sum + 1 - a.m_k; @@ -4207,15 +4670,15 @@ namespace sat { TRACE("ba", tout << "literal " << l << " is not false\n";); return false; } - if (!p.m_lits.contains(l)) { + if (!p.contains(l)) { TRACE("ba", tout << "lemma contains literal " << l << " not in inequality\n";); return false; } } uint64_t value = 0; - for (unsigned i = 0; i < p.m_lits.size(); ++i) { - uint64_t coeff = p.m_coeffs[i]; - if (!lits.contains(p.m_lits[i])) { + for (unsigned i = 0; i < p.size(); ++i) { + uint64_t coeff = p.coeff(i); + if (!lits.contains(p.lit(i))) { value += coeff; } } diff --git a/src/sat/ba_solver.h b/src/sat/ba_solver.h index bae59f45a..8f9488167 100644 --- a/src/sat/ba_solver.h +++ b/src/sat/ba_solver.h @@ -25,6 +25,7 @@ Revision History: #include "sat/sat_solver.h" #include "sat/sat_lookahead.h" #include "sat/sat_unit_walk.h" +#include "sat/sat_big.h" #include "util/scoped_ptr_vector.h" #include "util/sorting_network.h" @@ -41,8 +42,11 @@ namespace sat { unsigned m_num_bin_subsumes; unsigned m_num_clause_subsumes; unsigned m_num_pb_subsumes; + unsigned m_num_big_strengthenings; unsigned m_num_cut; unsigned m_num_gc; + unsigned m_num_overflow; + unsigned m_num_lemmas; stats() { reset(); } void reset() { memset(this, 0, sizeof(*this)); } }; @@ -57,6 +61,7 @@ namespace sat { class card; class pb; class xr; + class pb_base; class constraint { protected: @@ -104,6 +109,7 @@ namespace sat { card const& to_card() const; pb const& to_pb() const; xr const& to_xr() const; + pb_base const& to_pb_base() const; bool is_card() const { return m_tag == card_t; } bool is_pb() const { return m_tag == pb_t; } bool is_xr() const { return m_tag == xr_t; } @@ -118,7 +124,7 @@ namespace sat { }; friend std::ostream& operator<<(std::ostream& out, constraint const& c); - + // base class for pb and cardinality constraints class pb_base : public constraint { protected: @@ -204,12 +210,18 @@ namespace sat { protected: struct ineq { - literal_vector m_lits; - svector m_coeffs; + svector m_wlits; uint64_t m_k; ineq(): m_k(0) {} - void reset(uint64_t k) { m_lits.reset(); m_coeffs.reset(); m_k = k; } - void push(literal l, uint64_t c) { m_lits.push_back(l); m_coeffs.push_back(c); } + unsigned size() const { return m_wlits.size(); } + literal lit(unsigned i) const { return m_wlits[i].second; } + unsigned coeff(unsigned i) const { return m_wlits[i].first; } + void reset(uint64_t k) { m_wlits.reset(); m_k = k; } + void push(literal l, unsigned c) { m_wlits.push_back(wliteral(c,l)); } + unsigned bv_coeff(bool_var v) const; + void divide(unsigned c); + void weaken(unsigned i); + bool contains(literal l) const { for (auto wl : m_wlits) if (wl.second == l) return true; return false; } }; solver* m_solver; @@ -273,7 +285,8 @@ namespace sat { // simplification routines - svector m_visited; + svector m_visited; + unsigned m_visited_ts; vector> m_cnstr_use_list; use_list m_clause_use_list; bool m_simplify_change; @@ -292,9 +305,11 @@ namespace sat { void binary_subsumption(card& c1, literal lit); void clause_subsumption(card& c1, literal lit, clause_vector& removed_clauses); void card_subsumption(card& c1, literal lit); - void mark_visited(literal l) { m_visited[l.index()] = true; } - void unmark_visited(literal l) { m_visited[l.index()] = false; } - bool is_marked(literal l) const { return m_visited[l.index()] != 0; } + void init_visited(); + void mark_visited(literal l) { m_visited[l.index()] = m_visited_ts; } + void mark_visited(bool_var v) { mark_visited(literal(v, false)); } + bool is_visited(bool_var v) const { return is_visited(literal(v, false)); } + bool is_visited(literal l) const { return m_visited[l.index()] == m_visited_ts; } unsigned get_num_unblocked_bin(literal l); literal get_min_occurrence_literal(card const& c); void init_use_lists(); @@ -302,6 +317,9 @@ namespace sat { unsigned set_non_external(); unsigned elim_pure(); bool elim_pure(literal lit); + void unit_strengthen(); + void unit_strengthen(big& big, constraint& cs); + void unit_strengthen(big& big, pb_base& p); void subsumption(constraint& c1); void subsumption(card& c1); void gc_half(char const* _method); @@ -396,10 +414,23 @@ namespace sat { lbool eval(model const& m, pb const& p) const; double get_reward(pb const& p, literal_occs_fun& occs) const; + // RoundingPb conflict resolution + lbool resolve_conflict_rs(); + void round_to_one(ineq& ineq, bool_var v); + void round_to_one(bool_var v); + void divide(unsigned c); + void resolve_on(literal lit); + void resolve_with(ineq const& ineq); + void reset_marks(unsigned idx); + void mark_variables(ineq const& ineq); + + void bail_resolve_conflict(unsigned idx); + // access solver inline lbool value(bool_var v) const { return value(literal(v, false)); } inline lbool value(literal lit) const { return m_lookahead ? m_lookahead->value(lit) : m_solver->value(lit); } inline lbool value(model const& m, literal l) const { return l.sign() ? ~m[l.var()] : m[l.var()]; } + inline bool is_false(literal lit) const { return l_false == value(lit); } inline unsigned lvl(literal lit) const { return m_lookahead || m_unit_walk ? 0 : m_solver->lvl(lit); } inline unsigned lvl(bool_var v) const { return m_lookahead || m_unit_walk ? 0 : m_solver->lvl(v); } @@ -426,9 +457,11 @@ namespace sat { mutable bool m_overflow; void reset_active_var_set(); - void normalize_active_coeffs(); + bool test_and_set_active(bool_var v); void inc_coeff(literal l, unsigned offset); int64_t get_coeff(bool_var v) const; + uint64_t get_coeff(literal lit) const; + wliteral get_wliteral(bool_var v); unsigned get_abs_coeff(bool_var v) const; int get_int_coeff(bool_var v) const; unsigned get_bound() const; @@ -436,6 +469,7 @@ namespace sat { literal get_asserting_literal(literal conseq); void process_antecedent(literal l, unsigned offset); + void process_antecedent(literal l) { process_antecedent(l, 1); } void process_card(card& c, unsigned offset); void cut(); bool create_asserting_lemma(); @@ -446,6 +480,7 @@ namespace sat { bool validate_conflict(pb const& p) const; bool validate_assign(literal_vector const& lits, literal lit); bool validate_lemma(); + bool validate_ineq(ineq const& ineq) const; bool validate_unit_propagation(card const& c, literal alit) const; bool validate_unit_propagation(pb const& p, literal alit) const; bool validate_unit_propagation(pb const& p, literal_vector const& r, literal alit) const; @@ -464,12 +499,17 @@ namespace sat { ineq m_A, m_B, m_C; void active2pb(ineq& p); + constraint* active2lemma(); constraint* active2constraint(); constraint* active2card(); + void active2wlits(); + void active2wlits(svector& wlits); void justification2pb(justification const& j, literal lit, unsigned offset, ineq& p); + void constraint2pb(constraint& cnstr, literal lit, unsigned offset, ineq& p); bool validate_resolvent(); + unsigned get_coeff(ineq const& pb, literal lit); - void display(std::ostream& out, ineq& p, bool values = false) const; + void display(std::ostream& out, ineq const& p, bool values = false) const; void display(std::ostream& out, card const& c, bool values) const; void display(std::ostream& out, pb const& p, bool values) const; void display(std::ostream& out, xr const& c, bool values) const; diff --git a/src/sat/sat_big.cpp b/src/sat/sat_big.cpp index 35898a110..c1eeecd27 100644 --- a/src/sat/sat_big.cpp +++ b/src/sat/sat_big.cpp @@ -22,7 +22,8 @@ Revision History: namespace sat { big::big(random_gen& rand): - m_rand(rand) { + m_rand(rand), + m_include_cardinality(false) { } void big::init(solver& s, bool learned) { @@ -42,22 +43,22 @@ namespace sat { m_roots[v.index()] = false; edges.push_back(v); } -#if 0 - if (w.is_ext_constraint() && + if (m_include_cardinality && + w.is_ext_constraint() && s.m_ext && - learned && + learned && // cannot (yet) observe if ext constraints are learned !seen_idx.contains(w.get_ext_constraint_idx()) && s.m_ext->is_extended_binary(w.get_ext_constraint_idx(), r)) { seen_idx.insert(w.get_ext_constraint_idx(), true); - for (unsigned i = 0; i < r.size(); ++i) { - literal u = r[i]; - for (unsigned j = i + 1; j < r.size(); ++j) { - // add ~r[i] -> r[j] - literal v = r[j]; - literal u = ~r[j]; + for (unsigned i = 0; i < std::min(4u, r.size()); ++i) { + shuffle(r.size(), r.c_ptr(), m_rand); + literal u = r[0]; + for (unsigned j = 1; j < r.size(); ++j) { + literal v = ~r[j]; + // add u -> v m_roots[v.index()] = false; m_dag[u.index()].push_back(v); - // add ~r[j] -> r[i] + // add ~v -> ~u v.neg(); u.neg(); m_roots[u.index()] = false; @@ -65,7 +66,6 @@ namespace sat { } } } -#endif } } done_adding_edges(); @@ -268,6 +268,16 @@ namespace sat { return out << v; } + literal big::get_root(literal l) { + literal r = l; + do { + l = r; + r = m_root[l.index()]; + } + while (r != l); + return r; + } + void big::display(std::ostream& out) const { unsigned idx = 0; for (auto& next : m_dag) { diff --git a/src/sat/sat_big.h b/src/sat/sat_big.h index 898ddd1e8..25093fd60 100644 --- a/src/sat/sat_big.h +++ b/src/sat/sat_big.h @@ -34,6 +34,7 @@ namespace sat { svector m_left, m_right; literal_vector m_root, m_parent; bool m_learned; + bool m_include_cardinality; svector> m_del_bin; @@ -54,6 +55,9 @@ namespace sat { // static svector> s_del_bin; big(random_gen& rand); + + void set_include_cardinality(bool f) { m_include_cardinality = f; } + /** \brief initialize a BIG from a solver. */ @@ -77,7 +81,7 @@ namespace sat { int get_left(literal l) const { return m_left[l.index()]; } int get_right(literal l) const { return m_right[l.index()]; } literal get_parent(literal l) const { return m_parent[l.index()]; } - literal get_root(literal l) const { return m_root[l.index()]; } + literal get_root(literal l); bool reaches(literal u, literal v) const { return m_left[u.index()] < m_left[v.index()] && m_right[v.index()] < m_right[u.index()]; } bool connected(literal u, literal v) const { return reaches(u, v) || reaches(~v, ~u); } void display(std::ostream& out) const; diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp index c7f2377c9..07aacd9ee 100644 --- a/src/sat/sat_config.cpp +++ b/src/sat/sat_config.cpp @@ -196,6 +196,22 @@ namespace sat { else throw sat_param_exception("invalid PB solver: solver, totalizer, circuit, sorting, segmented"); + s = p.pb_resolve(); + if (s == "cardinality") + m_pb_resolve = PB_CARDINALITY; + else if (s == "rounding") + m_pb_resolve = PB_ROUNDING; + else + throw sat_param_exception("invalid PB resolve: 'cardinality' or 'rounding' expected"); + + s = p.pb_lemma_format(); + if (s == "cardinality") + m_pb_lemma_format = PB_LEMMA_CARDINALITY; + else if (s == "pb") + m_pb_lemma_format = PB_LEMMA_PB; + else + throw sat_param_exception("invalid PB lemma format: 'cardinality' or 'pb' expected"); + m_card_solver = p.cardinality_solver(); sat_simplifier_params sp(_p); diff --git a/src/sat/sat_config.h b/src/sat/sat_config.h index 37efe69ed..b5cfb9e28 100644 --- a/src/sat/sat_config.h +++ b/src/sat/sat_config.h @@ -60,6 +60,16 @@ namespace sat { PB_SEGMENTED }; + enum pb_resolve { + PB_CARDINALITY, + PB_ROUNDING + }; + + enum pb_lemma_format { + PB_LEMMA_CARDINALITY, + PB_LEMMA_PB + }; + enum reward_t { ternary_reward, unit_literal_reward, @@ -148,6 +158,8 @@ namespace sat { pb_solver m_pb_solver; bool m_card_solver; + pb_resolve m_pb_resolve; + pb_lemma_format m_pb_lemma_format; // branching heuristic settings. branching_heuristic m_branching_heuristic; diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg index 89776c479..390cdfa53 100644 --- a/src/sat/sat_params.pyg +++ b/src/sat/sat_params.pyg @@ -42,8 +42,10 @@ def_module_params('sat', ('drat.check_sat', BOOL, False, 'build up internal trace, check satisfying model'), ('cardinality.solver', BOOL, True, 'use cardinality solver'), ('pb.solver', SYMBOL, 'solver', 'method for handling Pseudo-Boolean constraints: circuit (arithmetical circuit), sorting (sorting circuit), totalizer (use totalizer encoding), solver (use native solver)'), - ('xor.solver', BOOL, False, 'use xor solver'), + ('xor.solver', BOOL, False, 'use xor solver'), ('cardinality.encoding', SYMBOL, 'grouped', 'encoding used for at-most-k constraints: grouped, bimander, ordered, unate, circuit'), + ('pb.resolve', SYMBOL, 'cardinality', 'resolution strategy for boolean algebra solver: cardinality, rounding'), + ('pb.lemma_format', SYMBOL, 'cardinality', 'generate either cardinality or pb lemmas'), ('local_search', BOOL, False, 'use local search instead of CDCL'), ('local_search_threads', UINT, 0, 'number of local search threads to find satisfiable solution'), ('local_search_mode', SYMBOL, 'wsat', 'local search algorithm, either default wsat or qsat'), diff --git a/src/sat/sat_scc.h b/src/sat/sat_scc.h index 146bd2366..1ba646992 100644 --- a/src/sat/sat_scc.h +++ b/src/sat/sat_scc.h @@ -60,7 +60,6 @@ namespace sat { void ensure_big(bool learned) { m_big.ensure_big(m_solver, learned); } int get_left(literal l) const { return m_big.get_left(l); } int get_right(literal l) const { return m_big.get_right(l); } - literal get_root(literal l) const { return m_big.get_root(l); } bool connected(literal u, literal v) const { return m_big.connected(u, v); } }; }; diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 7ddc80813..065dc1d39 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -340,12 +340,6 @@ namespace sat { } void solver::mk_bin_clause(literal l1, literal l2, bool learned) { -#if 0 - if ((l1.var() == 2039 || l2.var() == 2039) && - (l1.var() == 27042 || l2.var() == 27042)) { - IF_VERBOSE(1, verbose_stream() << "mk_bin: " << l1 << " " << l2 << " " << learned << "\n"); - } -#endif if (find_binary_watch(get_wlist(~l1), ~l2)) { assign(l1, justification()); return; diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index 7faa89370..9d0d29ac0 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -82,6 +82,7 @@ struct goal2sat::imp { m_is_lemma(false) { updt_params(p); m_true = sat::null_bool_var; + mk_true(); } void updt_params(params_ref const & p) { diff --git a/src/smt/theory_jobscheduler.cpp b/src/smt/theory_jobscheduler.cpp index a372a274f..0cf2d9be4 100644 --- a/src/smt/theory_jobscheduler.cpp +++ b/src/smt/theory_jobscheduler.cpp @@ -19,13 +19,9 @@ TODO: - arithmetic interface - propagation queue: - - register theory variables for catching when jobs are bound to resources - register bounds on start times to propagate energy constraints - more general registration mechanism for arithmetic theory. -- csp_cmds - - use predicates for add_ feature set? Closed world. - set up environment in one swoop. - - interact with opt +- interact with opt - jobs without resources - complain or add dummy resource? At which level. @@ -37,6 +33,7 @@ Features: - try optimization based on arithmetic solver. - earliest start, latest start - constraint level + - add constraints gradually - resource groups - resource groups like a resource - resources bound to resource groups within time intervals @@ -86,6 +83,13 @@ namespace smt { return true; } + struct symbol_cmp { + bool operator()(symbol const& s1, symbol const& s2) const { + return lt(s1, s2); + } + }; + + // TBD: stronger parameter validation void theory_jobscheduler::internalize_cmd(expr* cmd) { symbol key, val; rational r; @@ -96,10 +100,12 @@ namespace smt { if (u.is_set_preemptable(cmd, job) && u.is_job(job, j)) { set_preemptable(j, true); } - else if (u.is_add_resource_available(cmd, resource, loadpct, start, end) && u.is_resource(resource, res)) { + else if (u.is_add_resource_available(cmd, resource, loadpct, start, end, ps) && u.is_resource(resource, res)) { + std::sort(ps.begin(), ps.end(), symbol_cmp()); add_resource_available(res, loadpct, start, end, ps); } - else if (u.is_add_job_resource(cmd, job, resource, loadpct, capacity, end) && u.is_job(job, j) && u.is_resource(resource, res)) { + else if (u.is_add_job_resource(cmd, job, resource, loadpct, capacity, end, ps) && u.is_job(job, j) && u.is_resource(resource, res)) { + std::sort(ps.begin(), ps.end(), symbol_cmp()); add_job_resource(j, res, loadpct, capacity, end, ps); } else { @@ -113,15 +119,57 @@ namespace smt { throw default_exception(strm.str()); } + void theory_jobscheduler::new_eq_eh(theory_var v1, theory_var v2) { + enode* e1 = get_enode(v1); + enode* e2 = get_enode(v2); + enode* root = e1->get_root(); + unsigned r; + if (u.is_resource(root->get_owner(), r)) { + enode* next = e1; + do { + unsigned j; + if (u.is_job2resource(next->get_owner(), j) && !m_jobs[j].m_is_bound) { + m_bound_jobs.push_back(j); + m_jobs[j].m_is_bound = true; + } + next = next->get_next(); + } + while (e1 != next); + } + } + + + void theory_jobscheduler::new_diseq_eh(theory_var v1, theory_var v2) { + + } + void theory_jobscheduler::push_scope_eh() { + scope s; + s.m_bound_jobs_lim = m_bound_jobs.size(); + s.m_bound_qhead = m_bound_qhead; + m_scopes.push_back(s); } void theory_jobscheduler::pop_scope_eh(unsigned num_scopes) { + unsigned new_lvl = m_scopes.size() - num_scopes; + scope const& s = m_scopes[new_lvl]; + for (unsigned i = s.m_bound_jobs_lim; i < m_bound_jobs.size(); ++i) { + unsigned j = m_bound_jobs[i]; + m_jobs[j].m_is_bound = false; + } + m_bound_jobs.shrink(s.m_bound_jobs_lim); + m_bound_qhead = s.m_bound_qhead; + m_scopes.shrink(new_lvl); } final_check_status theory_jobscheduler::final_check_eh() { TRACE("csp", tout << "\n";); bool blocked = false; + for (unsigned j = 0; j < m_jobs.size(); ++j) { + if (split_job2resource(j)) { + return FC_CONTINUE; + } + } for (unsigned r = 0; r < m_resources.size(); ++r) { if (constrain_resource_energy(r)) { blocked = true; @@ -138,7 +186,7 @@ namespace smt { } bool theory_jobscheduler::can_propagate() { - return false; + return m_bound_qhead < m_bound_jobs.size(); } literal theory_jobscheduler::mk_literal(expr * e) { @@ -227,6 +275,9 @@ namespace smt { /** * r = resource(j) & start(j) >= slb => end(j) >= ect(j, r, slb) + * + * note: not used so far + * note: subsumed by constrain_end_time_interval used in final-check */ void theory_jobscheduler::propagate_end_time(unsigned j, unsigned r) { time_t slb = est(j); @@ -263,12 +314,15 @@ namespace smt { bool theory_jobscheduler::constrain_end_time_interval(unsigned j, unsigned r) { unsigned idx1 = 0, idx2 = 0; time_t s = start(j); + job_resource const& jr = get_job_resource(j, r); TRACE("csp", tout << "job: " << j << " resource: " << r << " start: " << s << "\n";); - if (!resource_available(r, s, idx1)) return false; vector& available = m_resources[r].m_available; + if (!resource_available(r, s, idx1)) return false; + if (!resource_available(jr, available[idx1])) return false; time_t e = ect(j, r, s); TRACE("csp", tout << "job: " << j << " resource: " << r << " ect: " << e << "\n";); if (!resource_available(r, e, idx2)) return false; // infeasible.. + if (!resource_available(jr, available[idx2])) return false; time_t start1 = available[idx1].m_start; time_t end1 = available[idx1].m_end; unsigned cap1 = available[idx1].m_loadpct; @@ -317,9 +371,6 @@ namespace smt { return true; } - void theory_jobscheduler::propagate_resource_energy(unsigned r) { - - } /** * Ensure that job overlaps don't exceed available energy @@ -386,23 +437,52 @@ namespace smt { } void theory_jobscheduler::propagate() { - return; - for (unsigned j = 0; j < m_jobs.size(); ++j) { + while (m_bound_qhead < m_bound_jobs.size()) { + unsigned j = m_bound_jobs[m_bound_qhead++]; + unsigned r = 0; job_info const& ji = m_jobs[j]; - unsigned r = resource(j); - propagate_end_time(j, r); + VERIFY(u.is_resource(ji.m_job2resource->get_root()->get_owner(), r)); + TRACE("csp", tout << "job: " << j << " resource: " << r << "\n";); + propagate_job2resource(j, r); } - for (unsigned r = 0; r < m_resources.size(); ++r) { - // TBD: check energy constraints on resources. + } + + void theory_jobscheduler::propagate_job2resource(unsigned j, unsigned r) { + job_info const& ji = m_jobs[j]; + res_info const& ri = m_resources[r]; + job_resource const& jr = get_job_resource(j, r); + literal eq = mk_eq_lit(ji.m_job2resource, ri.m_resource); + assert_last_end_time(j, r, jr, eq); + assert_last_start_time(j, r, eq); + assert_first_start_time(j, r, eq); + vector const& available = ri.m_available; + // TBD: needs to take properties into account + + unsigned i = 0; + if (!first_available(jr, ri, i)) return; + while (true) { + unsigned next = i + 1; + if (!first_available(jr, ri, next)) return; + SASSERT(available[i].m_end < available[next].m_start); + assert_job_not_in_gap(j, r, i, next, eq); + if (!ji.m_is_preemptable && available[i].m_end + 1 < available[i+1].m_start) { + assert_job_non_preemptable(j, r, i, next, eq); + } + i = next; } } theory_jobscheduler::theory_jobscheduler(ast_manager& m): - theory(m.get_family_id("csp")), m(m), u(m), a(m) { + theory(m.get_family_id("csp")), + m(m), + u(m), + a(m), + m_bound_qhead(0) { } std::ostream& theory_jobscheduler::display(std::ostream & out, job_resource const& jr) const { - return out << "r:" << jr.m_resource_id << " cap:" << jr.m_capacity << " load:" << jr.m_loadpct << " end:" << jr.m_end << "\n"; + return out << "r:" << jr.m_resource_id << " cap:" << jr.m_capacity << " load:" << jr.m_loadpct << " end:" << jr.m_end; + for (auto const& s : jr.m_properties) out << " " << s; out << "\n"; } std::ostream& theory_jobscheduler::display(std::ostream & out, job_info const& j) const { @@ -413,7 +493,8 @@ namespace smt { } std::ostream& theory_jobscheduler::display(std::ostream & out, res_available const& r) const { - return out << "[" << r.m_start << ":" << r.m_end << "] @ " << r.m_loadpct << "%\n"; + return out << "[" << r.m_start << ":" << r.m_end << "] @ " << r.m_loadpct << "%"; + for (auto const& s : r.m_properties) out << " " << s; out << "\n"; } std::ostream& theory_jobscheduler::display(std::ostream & out, res_info const& r) const { @@ -548,7 +629,7 @@ namespace smt { app_ref start(u.mk_start(j), m); app_ref end(u.mk_end(j), m); app_ref res(u.mk_job2resource(j), m); - if (!ctx.e_internalized(job)) ctx.internalize(job, false); + if (!ctx.e_internalized(job)) ctx.internalize(job, false); if (!ctx.e_internalized(start)) ctx.internalize(start, false); if (!ctx.e_internalized(end)) ctx.internalize(end, false); if (!ctx.e_internalized(res)) ctx.internalize(res, false); @@ -563,6 +644,7 @@ namespace smt { m_resources[r].m_jobs.push_back(j); } + void theory_jobscheduler::add_resource_available(unsigned r, unsigned max_loadpct, time_t start, time_t end, properties const& ps) { SASSERT(get_context().at_base_level()); SASSERT(1 <= max_loadpct && max_loadpct <= 100); @@ -574,37 +656,42 @@ namespace smt { app_ref res(u.mk_resource(r), m); if (!ctx.e_internalized(res)) ctx.internalize(res, false); ri.m_resource = ctx.get_enode(res); + app_ref ms(u.mk_makespan(r), m); + if (!ctx.e_internalized(ms)) ctx.internalize(ms, false); + ri.m_makespan = ctx.get_enode(ms); } ri.m_available.push_back(res_available(max_loadpct, start, end, ps)); } /* * Initialze the state based on the set of jobs and resources added. - * For each job j, with possible resources r1, ..., r_n assert - * resource(j) = r_1 || resource(j) = r_2 || ... || resource(j) = r_n - * For each job and resource r with deadline end(j,r) assert - * resource(j) = r => end(j) <= end(j,r) - * * Ensure that the availability slots for each resource is sorted by time. + * + * For each resource j: + * est(j) <= start(j) <= end(j) <= lct(j) + * + * possible strengthenings: + * - start(j) <= lst(j) + * - start(j) + min_completion_time(j) <= end(j) + * - start(j) + max_completion_time(j) >= end(j) + * + * makespan constraints? + * */ void theory_jobscheduler::add_done() { TRACE("csp", tout << "add-done begin\n";); context & ctx = get_context(); // sort availability intervals - for (unsigned r = 0; r < m_resources.size(); ++r) { - res_info& ri = m_resources[r]; + for (res_info& ri : m_resources) { vector& available = ri.m_available; res_available::compare cmp; std::sort(available.begin(), available.end(), cmp); } - expr_ref fml(m); - literal lit, l1, l2, l3; + literal lit; - for (unsigned j = 0; j < m_jobs.size(); ++j) { - job_info const& ji = m_jobs[j]; - literal_vector disj; + for (job_info const& ji : m_jobs) { if (ji.m_resources.empty()) { throw default_exception("every job should be associated with at least one resource"); } @@ -614,23 +701,24 @@ namespace smt { ctx.mk_th_axiom(get_id(), 1, &lit); time_t start_lb = std::numeric_limits::max(); - time_t end_ub = 0; + time_t runtime_lb = std::numeric_limits::max(); + time_t end_ub = 0, runtime_ub = 0; for (job_resource const& jr : ji.m_resources) { - // resource(j) = r => end(j) <= end(j, r) - // resource(j) = r => start(j) <= lst(j, r, end(j, r)) unsigned r = jr.m_resource_id; res_info const& ri = m_resources[r]; - enode* j2r = m_jobs[j].m_job2resource; - literal eq = mk_eq_lit(j2r, ri.m_resource); - assert_last_end_time(j, r, jr, eq); - assert_last_start_time(j, r, eq); - disj.push_back(eq); - start_lb = std::min(start_lb, ri.m_available[0].m_start); - end_ub = std::max(end_ub, ri.m_available.back().m_end); - + if (ri.m_available.empty()) continue; + unsigned idx = 0; + if (first_available(jr, ri, idx)) { + start_lb = std::min(start_lb, ri.m_available[idx].m_start); + } + idx = ri.m_available.size(); + if (last_available(jr, ri, idx)) { + end_ub = std::max(end_ub, ri.m_available[idx].m_end); + } + runtime_lb = std::min(runtime_lb, jr.m_capacity); + // TBD: more accurate estimates for runtime_lb based on gaps + // TBD: correct estimate of runtime_ub taking gaps into account. } - // resource(j) = r1 || ... || resource(j) = r_n - ctx.mk_th_axiom(get_id(), disj.size(), disj.c_ptr()); // start(j) >= start_lb lit = mk_ge(ji.m_start, start_lb); @@ -639,45 +727,22 @@ namespace smt { // end(j) <= end_ub lit = mk_le(ji.m_end, end_ub); ctx.mk_th_axiom(get_id(), 1, &lit); - } - for (unsigned r = 0; r < m_resources.size(); ++r) { - res_info& ri = m_resources[r]; - vector& available = ri.m_available; - if (available.empty()) continue; - enode* res = m_resources[r].m_resource; - for (unsigned j : ri.m_jobs) { - // resource(j) == r => start(j) >= available[0].m_start; - enode* j2r = m_jobs[j].m_job2resource; - assert_first_start_time(j, r, mk_eq_lit(j2r, res)); - } - for (unsigned i = 0; i + 1 < available.size(); ++i) { - if (available[i].m_end > available[i + 1].m_start) { - throw default_exception("availability intervals should be disjoint"); - } - for (unsigned j : ri.m_jobs) { - // jobs start within an interval. - // resource(j) == r => start(j) <= available[i].m_end || start(j) >= available[i + 1].m_start; - enode* j2r = m_jobs[j].m_job2resource; - literal eq = mk_eq_lit(j2r, res); - assert_job_not_in_gap(j, r, i, eq); - // if job is not pre-emptable, start and end have to align within contiguous interval. - // resource(j) == r => end(j) <= available[i].m_end || start(j) >= available[i + 1].m_start - if (!m_jobs[j].m_is_preemptable && available[i].m_end + 1 < available[i+1].m_start) { - assert_job_non_preemptable(j, r, i, eq); - } - } - } - } + // start(j) + runtime_lb <= end(j) + // end(j) <= start(j) + runtime_ub + } + TRACE("csp", tout << "add-done end\n";); } + // resource(j) = r => end(j) <= end(j, r) void theory_jobscheduler::assert_last_end_time(unsigned j, unsigned r, job_resource const& jr, literal eq) { job_info const& ji = m_jobs[j]; literal l2 = mk_le(ji.m_end, jr.m_end); get_context().mk_th_axiom(get_id(), ~eq, l2); } + // resource(j) = r => start(j) <= lst(j, r, end(j, r)) void theory_jobscheduler::assert_last_start_time(unsigned j, unsigned r, literal eq) { context& ctx = get_context(); time_t t; @@ -690,27 +755,70 @@ namespace smt { } } + // resource(j) = r => start(j) >= available[0].m_start void theory_jobscheduler::assert_first_start_time(unsigned j, unsigned r, literal eq) { + job_resource const& jr = get_job_resource(j, r); + unsigned idx = 0; + if (!first_available(jr, m_resources[r], idx)) return; vector& available = m_resources[r].m_available; - literal l2 = mk_ge(m_jobs[j].m_start, available[0].m_start); + literal l2 = mk_ge(m_jobs[j].m_start, available[idx].m_start); get_context().mk_th_axiom(get_id(), ~eq, l2); } - void theory_jobscheduler::assert_job_not_in_gap(unsigned j, unsigned r, unsigned idx, literal eq) { + // resource(j) = r => start(j) <= end[idx] || start[idx+1] <= start(j); + void theory_jobscheduler::assert_job_not_in_gap(unsigned j, unsigned r, unsigned idx, unsigned idx1, literal eq) { + job_resource const& jr = get_job_resource(j, r); vector& available = m_resources[r].m_available; - literal l2 = mk_ge(m_jobs[j].m_start, available[idx + 1].m_start); + SASSERT(resource_available(jr, available[idx])); + literal l2 = mk_ge(m_jobs[j].m_start, available[idx1].m_start); literal l3 = mk_le(m_jobs[j].m_start, available[idx].m_end); get_context().mk_th_axiom(get_id(), ~eq, l2, l3); } - void theory_jobscheduler::assert_job_non_preemptable(unsigned j, unsigned r, unsigned idx, literal eq) { + // resource(j) = r => end(j) <= end[idx] || start[idx+1] <= start(j); + void theory_jobscheduler::assert_job_non_preemptable(unsigned j, unsigned r, unsigned idx, unsigned idx1, literal eq) { vector& available = m_resources[r].m_available; + job_resource const& jr = get_job_resource(j, r); + SASSERT(resource_available(jr, available[idx])); literal l2 = mk_le(m_jobs[j].m_end, available[idx].m_end); - literal l3 = mk_ge(m_jobs[j].m_start, available[idx + 1].m_start); + literal l3 = mk_ge(m_jobs[j].m_start, available[idx1].m_start); get_context().mk_th_axiom(get_id(), ~eq, l2, l3); - } + } - + /** + * bind a job to one of the resources it can run on. + */ + bool theory_jobscheduler::split_job2resource(unsigned j) { + job_info const& ji = m_jobs[j]; + context& ctx = get_context(); + if (ji.m_is_bound) return false; + auto const& jrs = ji.m_resources; + for (job_resource const& jr : jrs) { + unsigned r = jr.m_resource_id; + res_info const& ri = m_resources[r]; + enode* e1 = ji.m_job2resource; + enode* e2 = ri.m_resource; + if (ctx.is_diseq(e1, e2)) + continue; + literal eq = mk_eq_lit(e1, e2); + if (ctx.get_assignment(eq) != l_false) { + ctx.mark_as_relevant(eq); + if (assume_eq(e1, e2)) { + return true; + } + } + } + literal_vector lits; + for (job_resource const& jr : jrs) { + unsigned r = jr.m_resource_id; + res_info const& ri = m_resources[r]; + enode* e1 = ji.m_job2resource; + enode* e2 = ri.m_resource; + lits.push_back(mk_eq_lit(e1, e2)); + } + ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr()); + return true; + } /** * check that each job is run on some resource according to @@ -757,17 +865,21 @@ namespace smt { return ji.m_resources[ji.m_resource2index[r]]; } + /** + * find idx, if any, such that t is within the time interval of available[idx] + */ bool theory_jobscheduler::resource_available(unsigned r, time_t t, unsigned& idx) { vector& available = m_resources[r].m_available; unsigned lo = 0, hi = available.size(), mid = hi / 2; while (lo < hi) { + SASSERT(lo <= mid && mid < hi); res_available const& ra = available[mid]; if (ra.m_start <= t && t <= ra.m_end) { idx = mid; return true; } else if (ra.m_start > t && mid > 0) { - hi = mid - 1; + hi = mid; mid = lo + (mid - lo) / 2; } else if (ra.m_end < t) { @@ -781,7 +893,6 @@ namespace smt { return false; } - /** * compute earliest completion time for job j on resource r starting at time start. */ @@ -799,20 +910,14 @@ namespace smt { SASSERT(cap > 0); for (; idx < available.size(); ++idx) { + if (!resource_available(jr, available[idx])) continue; start = std::max(start, available[idx].m_start); time_t end = available[idx].m_end; unsigned load_pct = available[idx].m_loadpct; time_t delta = solve_for_capacity(load_pct, j_load_pct, start, end); - TRACE("csp", tout << "delta: " << delta << " capacity: " << cap << " load " << load_pct << " jload: " << j_load_pct << " start: " << start << " end " << end << "\n";); + TRACE("csp", tout << "delta: " << delta << " capacity: " << cap << " load " + << load_pct << " jload: " << j_load_pct << " start: " << start << " end " << end << "\n";); if (delta > cap) { - // - // solve for end: - // cap = load * (end - start + 1) - // <=> - // cap / load = (end - start + 1) - // <=> - // end = cap / load + start - 1 - // end = solve_for_end(load_pct, j_load_pct, start, cap); cap = 0; } @@ -826,6 +931,9 @@ namespace smt { return std::numeric_limits::max(); } + /** + * find end, such that cap = (load / job_load_pct) * (end - start + 1) + */ time_t theory_jobscheduler::solve_for_end(unsigned load_pct, unsigned job_load_pct, time_t start, time_t cap) { SASSERT(load_pct > 0); SASSERT(job_load_pct > 0); @@ -840,6 +948,9 @@ namespace smt { return (load * (start - 1) + cap * job_load_pct) / load; } + /** + * find start, such that cap = (load / job_load_pct) * (end - start + 1) + */ time_t theory_jobscheduler::solve_for_start(unsigned load_pct, unsigned job_load_pct, time_t end, time_t cap) { SASSERT(load_pct > 0); SASSERT(job_load_pct > 0); @@ -854,6 +965,9 @@ namespace smt { return (load * (end + 1) - cap * job_load_pct) / load; } + /** + * find cap, such that cap = (load / job_load_pct) * (end - start + 1) + */ time_t theory_jobscheduler::solve_for_capacity(unsigned load_pct, unsigned job_load_pct, time_t start, time_t end) { SASSERT(job_load_pct > 0); unsigned load = std::min(load_pct, job_load_pct); @@ -870,6 +984,7 @@ namespace smt { unsigned j_load_pct = jr.m_loadpct; time_t cap = jr.m_capacity; for (unsigned idx = available.size(); idx-- > 0; ) { + if (!resource_available(jr, available[idx])) continue; start = available[idx].m_start; time_t end = available[idx].m_end; unsigned load_pct = available[idx].m_loadpct; @@ -882,12 +997,58 @@ namespace smt { cap -= delta; } if (cap == 0) { - std::cout << "start " << start << "\n"; return true; } } return false; } + + /** + * \brief check that job properties is a subset of resource properties. + * It assumes that both vectors are sorted. + */ + + bool theory_jobscheduler::resource_available(job_resource const& jr, res_available const& ra) const { + auto const& jps = jr.m_properties; + auto const& rps = ra.m_properties; + if (jps.size() > rps.size()) return false; + unsigned j = 0, i = 0; + for (; i < jps.size() && j < rps.size(); ) { + if (jps[i] == rps[j]) { + ++i; ++j; + } + else if (lt(rps[j], jps[i])) { + ++j; + } + else { + break; + } + } + return i == jps.size(); + } + + /** + * \brief minimal current resource available for job resource, includes idx. + */ + bool theory_jobscheduler::first_available(job_resource const& jr, res_info const& ri, unsigned& idx) const { + for (; idx < ri.m_available.size(); ++idx) { + if (resource_available(jr, ri.m_available[idx])) + return true; + } + return false; + } + + /** + * \brief maximal previous resource available for job resource, excludes idx. + */ + bool theory_jobscheduler::last_available(job_resource const& jr, res_info const& ri, unsigned& idx) const { + while (idx-- > 0) { + if (resource_available(jr, ri.m_available[idx])) + return true; + } + return false; + } + }; diff --git a/src/smt/theory_jobscheduler.h b/src/smt/theory_jobscheduler.h index 9031f9e78..59c3b975d 100644 --- a/src/smt/theory_jobscheduler.h +++ b/src/smt/theory_jobscheduler.h @@ -31,7 +31,7 @@ namespace smt { class theory_jobscheduler : public theory { public: - typedef map properties; + typedef svector properties; protected: struct job_resource { @@ -64,7 +64,8 @@ namespace smt { enode* m_start; enode* m_end; enode* m_job2resource; - job_info(): m_is_preemptable(false), m_job(nullptr), m_start(nullptr), m_end(nullptr), m_job2resource(nullptr) {} + bool m_is_bound; + job_info(): m_is_preemptable(false), m_job(nullptr), m_start(nullptr), m_end(nullptr), m_job2resource(nullptr), m_is_bound(false) {} }; struct res_available { @@ -90,7 +91,8 @@ namespace smt { vector m_available; // time intervals where resource is available time_t m_end; // can't run after enode* m_resource; - res_info(): m_end(std::numeric_limits::max()), m_resource(nullptr) {} + enode* m_makespan; + res_info(): m_end(std::numeric_limits::max()), m_resource(nullptr), m_makespan(nullptr) {} }; ast_manager& m; @@ -98,6 +100,13 @@ namespace smt { arith_util a; vector m_jobs; vector m_resources; + unsigned_vector m_bound_jobs; + unsigned m_bound_qhead; + struct scope { + unsigned m_bound_jobs_lim; + unsigned m_bound_qhead; + }; + svector m_scopes; protected: @@ -109,9 +118,9 @@ namespace smt { void assign_eh(bool_var v, bool is_true) override {} - void new_eq_eh(theory_var v1, theory_var v2) override {} + void new_eq_eh(theory_var v1, theory_var v2) override; - void new_diseq_eh(theory_var v1, theory_var v2) override {} + void new_diseq_eh(theory_var v1, theory_var v2) override; void push_scope_eh() override; @@ -166,6 +175,10 @@ namespace smt { time_t ect(unsigned j, unsigned r, time_t start); bool lst(unsigned j, unsigned r, time_t& t); + bool resource_available(job_resource const& jr, res_available const& ra) const; + bool first_available(job_resource const& jr, res_info const& ri, unsigned& idx) const; + bool last_available(job_resource const& jr, res_info const& ri, unsigned& idx) const; + time_t solve_for_start(unsigned load_pct, unsigned job_load_pct, time_t end, time_t cap); time_t solve_for_end(unsigned load_pct, unsigned job_load_pct, time_t start, time_t cap); time_t solve_for_capacity(unsigned load_pct, unsigned job_load_pct, time_t start, time_t end); @@ -179,17 +192,18 @@ namespace smt { // propagation void propagate_end_time(unsigned j, unsigned r); - void propagate_resource_energy(unsigned r); + void propagate_job2resource(unsigned j, unsigned r); // final check constraints bool constrain_end_time_interval(unsigned j, unsigned r); bool constrain_resource_energy(unsigned r); + bool split_job2resource(unsigned j); void assert_last_end_time(unsigned j, unsigned r, job_resource const& jr, literal eq); void assert_last_start_time(unsigned j, unsigned r, literal eq); void assert_first_start_time(unsigned j, unsigned r, literal eq); - void assert_job_not_in_gap(unsigned j, unsigned r, unsigned idx, literal eq); - void assert_job_non_preemptable(unsigned j, unsigned r, unsigned idx, literal eq); + void assert_job_not_in_gap(unsigned j, unsigned r, unsigned idx, unsigned idx1, literal eq); + void assert_job_non_preemptable(unsigned j, unsigned r, unsigned idx, unsigned idx1, literal eq); void block_job_overlap(unsigned r, uint_set const& jobs, unsigned last_job); diff --git a/src/util/uint_set.h b/src/util/uint_set.h index 0f3715cb1..e6518b435 100644 --- a/src/util/uint_set.h +++ b/src/util/uint_set.h @@ -269,10 +269,9 @@ public: void remove(unsigned v) { if (contains(v)) { m_in_set[v] = false; - unsigned i = 0; - for (i = 0; i < m_set.size() && m_set[i] != v; ++i) - ; - SASSERT(i < m_set.size()); + unsigned i = m_set.size(); + for (; i > 0 && m_set[--i] != v; ) ; + SASSERT(m_set[i] == v); m_set[i] = m_set.back(); m_set.pop_back(); }