From 2b968f9e6348a04893c2787ca3f66f1a27c61bc6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 9 Aug 2018 15:29:39 -0700 Subject: [PATCH] initial decl plugin Signed-off-by: Nikolaj Bjorner --- src/ast/CMakeLists.txt | 1 + src/ast/jobshop_decl_plugin.cpp | 178 ++++++++++++++++++++++++++++++++ src/ast/jobshop_decl_plugin.h | 129 +++++++++++++++++++++++ 3 files changed, 308 insertions(+) create mode 100644 src/ast/jobshop_decl_plugin.cpp create mode 100644 src/ast/jobshop_decl_plugin.h diff --git a/src/ast/CMakeLists.txt b/src/ast/CMakeLists.txt index 80543bb05..5340d4e7b 100644 --- a/src/ast/CMakeLists.txt +++ b/src/ast/CMakeLists.txt @@ -30,6 +30,7 @@ z3_add_component(ast fpa_decl_plugin.cpp func_decl_dependencies.cpp has_free_vars.cpp + jobshop_decl_plugin.cpp macro_substitution.cpp num_occurs.cpp occurs.cpp diff --git a/src/ast/jobshop_decl_plugin.cpp b/src/ast/jobshop_decl_plugin.cpp new file mode 100644 index 000000000..41d8ad241 --- /dev/null +++ b/src/ast/jobshop_decl_plugin.cpp @@ -0,0 +1,178 @@ +/*++ +Copyright (c) 2018 Microsoft Corporation + +Module Name: + + jobshop_decl_plugin.h + +Abstract: + + Declarations used for a job-shop scheduling domain. + +Author: + + Nikolaj Bjorner (nbjorner) 2018-8-9 + +Revision History: + + +--*/ +#include "ast/jobshop_decl_plugin.h" +#include "ast/arith_decl_plugin.h" + +void jobshop_decl_plugin::set_manager(ast_manager* m, family_id fid) { + decl_plugin::set_manager(m, fid); + m_int_sort = m_manager->mk_sort(m_manager->mk_family_id("arith"), INT_SORT); + m_job_sort = m_manager->mk_sort(symbol("Job"), sort_info(m_family_id, JOB_SORT)); + m_resource_sort = m_manager->mk_sort(symbol("Resource"), sort_info(m_family_id, RESOURCE_SORT)); + m_manager->inc_ref(m_int_sort); + m_manager->inc_ref(m_resource_sort); + m_manager->inc_ref(m_job_sort); +} + +void jobshop_decl_plugin::finalize() { + m_manager->dec_ref(m_job_sort); + m_manager->dec_ref(m_resource_sort); + m_manager->dec_ref(m_int_sort); +} + +sort * jobshop_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) { + if (num_parameters != 0) { + m_manager->raise_exception("no parameters expected with job-shop sort"); + } + switch (static_cast(k)) { + case JOB_SORT: return m_job_sort; + case RESOURCE_SORT: return m_resource_sort; + default: UNREACHABLE(); return nullptr; + } +} + +func_decl * jobshop_decl_plugin::mk_func_decl( + decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const *, sort *) { + switch (static_cast(k)) { + case OP_JS_JOB: + check_arity(arity); + check_index1(num_parameters, parameters); + return m_manager->mk_func_decl(symbol("job"), 0, (sort* const*)nullptr, m_job_sort, func_decl_info(m_family_id, k, num_parameters, parameters)); + case OP_JS_RESOURCE: + check_arity(arity); + check_index1(num_parameters, parameters); + return m_manager->mk_func_decl(symbol("resource"), 0, (sort* const*)nullptr, m_resource_sort, func_decl_info(m_family_id, k, num_parameters, parameters)); + case OP_JS_START: + check_arity(arity); + check_index1(num_parameters, parameters); + return m_manager->mk_func_decl(symbol("job-start"), 0, (sort* const*)nullptr, m_int_sort, func_decl_info(m_family_id, k, num_parameters, parameters)); + case OP_JS_END: + check_arity(arity); + check_index1(num_parameters, parameters); + return m_manager->mk_func_decl(symbol("job-end"), 0, (sort* const*)nullptr, m_int_sort, func_decl_info(m_family_id, k, num_parameters, parameters)); + case OP_JS_JOB2RESOURCE: + check_arity(arity); + check_index1(num_parameters, parameters); + return m_manager->mk_func_decl(symbol("job2resource"), 0, (sort* const*)nullptr, m_int_sort, func_decl_info(m_family_id, k, num_parameters, parameters)); + case OP_JS_JOB_ON_RESOURCE: + check_arity(arity); + check_index1(num_parameters, parameters); + return m_manager->mk_func_decl(symbol("job-on-resource"), 0, (sort* const*)nullptr, m_manager->mk_bool_sort(), func_decl_info(m_family_id, k, num_parameters, parameters)); + default: + UNREACHABLE(); return nullptr; + } +} + +void jobshop_decl_plugin::check_arity(unsigned arity) { + if (arity > 0) + m_manager->raise_exception("jobshop variables use parameters only and take no arguments"); +} + +void jobshop_decl_plugin::check_index1(unsigned num_parameters, parameter const* ps) { + if (num_parameters != 1 || !ps[0].is_int()) + m_manager->raise_exception("jobshop variable expects a single integer parameter"); +} + +void jobshop_decl_plugin::check_index2(unsigned num_parameters, parameter const* ps) { + if (num_parameters != 2 || !ps[0].is_int() || !ps[1].is_int()) + m_manager->raise_exception("jobshop variable expects two integer parameters"); +} + + +bool jobshop_decl_plugin::is_value(app * e) const { + return is_app_of(e, m_family_id, OP_JS_JOB) || is_app_of(e, m_family_id, OP_JS_RESOURCE); +} + +void jobshop_decl_plugin::get_op_names(svector & op_names, symbol const & logic) { + if (logic == symbol("JOBSHOP")) { + 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("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)); + op_names.push_back(builtin_name("job-on-resource", OP_JS_JOB_ON_RESOURCE)); + } +} + +void jobshop_decl_plugin::get_sort_names(svector & sort_names, symbol const & logic) { + if (logic == symbol("JOBSHOP")) { + sort_names.push_back(builtin_name("Job", JOB_SORT)); + sort_names.push_back(builtin_name("Resource", RESOURCE_SORT)); + } +} + +expr * jobshop_decl_plugin::get_some_value(sort * s) { + parameter p(0); + if (is_sort_of(s, m_family_id, JOB_SORT)) + return m_manager->mk_const(mk_func_decl(OP_JS_JOB, 1, &p, 0, nullptr, nullptr)); + if (is_sort_of(s, m_family_id, RESOURCE_SORT)) + return m_manager->mk_const(mk_func_decl(OP_JS_RESOURCE, 1, &p, 0, nullptr, nullptr)); + UNREACHABLE(); + return nullptr; +} + + +jobshop_util::jobshop_util(ast_manager& m): m(m) { + m_fid = m.mk_family_id("jobshop"); + m_plugin = static_cast(m.get_plugin(m_fid)); +} + +sort* jobshop_util::mk_job_sort() { + return m_plugin->mk_job_sort(); +} + +sort* jobshop_util::mk_resource_sort() { + return m_plugin->mk_resource_sort(); +} + +app* jobshop_util::mk_job(unsigned j) { + parameter p(j); + return m.mk_const(m.mk_func_decl(m_fid, OP_JS_JOB, 1, &p, 0, (sort*const*)nullptr, nullptr)); +} + +unsigned jobshop_util::job2id(expr* j) { + SASSERT(is_app_of(j, m_fid, OP_JS_JOB)); + return to_app(j)->get_decl()->get_parameter(0).get_int(); +} + +app* jobshop_util::mk_resource(unsigned r) { + parameter p(r); + return m.mk_const(m.mk_func_decl(m_fid, OP_JS_RESOURCE, 1, &p, 0, (sort*const*)nullptr, nullptr)); +} + +unsigned jobshop_util::resource2id(expr* r) { + SASSERT(is_app_of(r, m_fid, OP_JS_RESOURCE)); + return to_app(r)->get_decl()->get_parameter(0).get_int(); +} + +app* jobshop_util::mk_start(unsigned j) { + parameter p(j); + return m.mk_const(m.mk_func_decl(m_fid, OP_JS_START, 1, &p, 0, (sort*const*)nullptr, nullptr)); +} + +app* jobshop_util::mk_end(unsigned j) { + parameter p(j); + return m.mk_const(m.mk_func_decl(m_fid, OP_JS_END, 1, &p, 0, (sort*const*)nullptr, nullptr)); +} + +app* jobshop_util::mk_on_resource(unsigned j) { + parameter p(j); + return m.mk_const(m.mk_func_decl(m_fid, OP_JS_END, 1, &p, 0, (sort*const*)nullptr, nullptr)); +} + diff --git a/src/ast/jobshop_decl_plugin.h b/src/ast/jobshop_decl_plugin.h new file mode 100644 index 000000000..94936c5aa --- /dev/null +++ b/src/ast/jobshop_decl_plugin.h @@ -0,0 +1,129 @@ +/*++ +Copyright (c) 2018 Microsoft Corporation + +Module Name: + + jobshop_decl_plugin.h + +Abstract: + + Declarations used for a job-shop scheduling domain. + + The job-shop domain comprises of constants job(j), resource(r) + + It finds values to variables: + - start(j), end(j), job2resource(j), job-on-resource(j, r) + + It assumes a background of: + - resources : Job -> Resource -> Int * LoadPct - time to run job j on resource r assuming LoadPct + - runtime : Job -> Int - time to run job j if not associated with any resource + - capacity : Resource -> Int -> LoadPct - capacity of resource r at time t, given as sequence of time intervals + + // Theory: + job-on-resource(j) => resource(j) in dom j.resources; + end(j) - start(j) = time-to-execute(j) + time-to-execute(j) := runtime(j) if !job-on-resource(j) + time-to-execute(j) := time-to-execute(j, resource(j)) otherwise + + time-to-execute(j, r) := (T - start(j)) + where capacity(j,r) = sum_{t = start(j)}^{T} load(loadpct(j,r), r, t) + + capacity(j, r) := cap where (cap, loadpct) = resources j r + loadpct(j, r) := loadpct where (cap, loadpct) = resources j r + + load(loadpct, r, t) := min(capacity r t, loadpct) / loadpct + + capacity(r, t) >= sum_{j | job-on-resource(j, r, t) } min(capacity r t, loadpct(j, r)) + + // Macros: + job-on-resource(j, r) := (job-on-resource(j) & r = resource(j)); + job-on-resource(j, r, t) := (job-on-resource(j, r) & start(j) <= t <= end(j)); + start_min(j, t) := start(j) >= t; + end_max(j, t) := end(j) <= t; + job_link(j1, j2, startstart, hard) := start(j1) = start(j2); + job_link(j1, j2, startstart, soft) := start(j1) <= start(j2); + job_link(j1, j2, endend, hard) := end(j1) = end(j2); + job_link(j1, j2, endend, soft) := end(j2) <= end(j1); + job_link(j1, j2, endstart, hard) := end(j1) = start(j2); + job_link(j1, j2, endstart, soft) := end(j2) <= start(j1); + job_link(j1, j2, startend, hard) := end(j2) = start(j1); + job_link(j1, j2, startend, soft) := end(j1) <= start(j2); + job_delay(j1, j2, t) := end(j1) + t <= end(j2); + job_on_same_resource(j1, j2) := job-on-resource(j1) & job-on-resource(j2) & resource(j1) = resource(j2); + job_not_on_same_resource(j1, j2) := !(job-on-resource(j1) & job-on-resource(j2) & resource(j1) = resource(j2)); + job_time_intersect(j1, j2) := start(j1) <= end(j2) <= end(j1) || start(j2) <= end(j1) <= end(j2); + run_time_bound(j) := !(job-on-resource(j)); + + job-on-resource(j, r, t) => job-property(j) = null or job_property(j) in working_time_property(r, t); + +Author: + + Nikolaj Bjorner (nbjorner) 2018-8-9 + +Revision History: + + +--*/ +#pragma once; +#include "ast/ast.h" + +enum js_sort_kind { + JOB_SORT, + RESOURCE_SORT +}; + +enum js_op_kind { + OP_JS_JOB, // value of type job + OP_JS_RESOURCE, // value of type resource + 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_JOB_ON_RESOURCE // is a job associated with a resource +}; + +class jobshop_decl_plugin : public decl_plugin { +public: + jobshop_decl_plugin() {} + ~jobshop_decl_plugin() override {} + void finalize() override; + void set_manager(ast_manager* m, family_id fid) override; + decl_plugin * mk_fresh() override { return alloc(jobshop_decl_plugin); } + sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) override; + func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, + unsigned arity, sort * const * domain, sort * range) override; + bool is_value(app * e) const override; + bool is_unique_value(app * e) const override { return is_value(e); } + void get_op_names(svector & op_names, symbol const & logic) override; + void get_sort_names(svector & sort_names, symbol const & logic) override; + expr * get_some_value(sort * s) override; + sort * mk_job_sort() const { return m_job_sort; } + sort * mk_resource_sort() const { return m_resource_sort; } +private: + sort* m_job_sort; + sort* m_resource_sort; + sort* m_int_sort; + + void check_arity(unsigned arity); + void check_index1(unsigned n, parameter const* ps); + void check_index2(unsigned n, parameter const* ps); +}; + +class jobshop_util { + ast_manager& m; + family_id m_fid; + jobshop_decl_plugin* m_plugin; +public: + jobshop_util(ast_manager& m); + sort* mk_job_sort(); + sort* mk_resource_sort(); + + app* mk_job(unsigned j); + unsigned job2id(expr* j); + + app* mk_resource(unsigned r); + unsigned resource2id(expr* r); + + app* mk_start(unsigned j); + app* mk_end(unsigned j); + app* mk_on_resource(unsigned j); +};