diff --git a/src/ast/csp_decl_plugin.cpp b/src/ast/csp_decl_plugin.cpp index cfe67fd2d..a6255d676 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"); @@ -148,6 +153,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)); @@ -233,10 +239,20 @@ 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); } diff --git a/src/ast/csp_decl_plugin.h b/src/ast/csp_decl_plugin.h index b450f1fc2..faaaf344c 100644 --- a/src/ast/csp_decl_plugin.h +++ b/src/ast/csp_decl_plugin.h @@ -75,13 +75,14 @@ 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 }; class csp_decl_plugin : public decl_plugin { @@ -116,29 +117,30 @@ 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); - bool is_job2resource(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_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); bool is_add_job_resource(expr * e, expr *& job, expr*& res, unsigned& loadpct, uint64_t& capacity, uint64_t& end); bool is_set_preemptable(expr* e, expr *& job); - bool is_model(expr* e) const { return is_app_of(e, m_fid, OP_JS_MODEL); } +private: + unsigned job2id(expr* j); + unsigned resource2id(expr* r); + }; diff --git a/src/smt/theory_jobscheduler.cpp b/src/smt/theory_jobscheduler.cpp index a415212c3..ce1b2a82b 100644 --- a/src/smt/theory_jobscheduler.cpp +++ b/src/smt/theory_jobscheduler.cpp @@ -37,6 +37,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 @@ -638,6 +639,9 @@ 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)); } @@ -823,18 +827,19 @@ namespace smt { 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) { lo = mid + 1; - mid += (hi - mid) / 2; + mid += (hi - mid + 1) / 2; } else { break; diff --git a/src/smt/theory_jobscheduler.h b/src/smt/theory_jobscheduler.h index 43f55f35a..f18299a12 100644 --- a/src/smt/theory_jobscheduler.h +++ b/src/smt/theory_jobscheduler.h @@ -91,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;