From 0d8de8f65fd4d3500d1db093bd5148d645bbfb97 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 9 Aug 2018 20:19:26 -0700 Subject: [PATCH] add theory outlline Signed-off-by: Nikolaj Bjorner --- src/ast/jobshop_decl_plugin.cpp | 10 --- src/ast/jobshop_decl_plugin.h | 21 ++--- src/smt/CMakeLists.txt | 1 + src/smt/theory_jobscheduler.cpp | 146 ++++++++++++++++++++++++++++++++ src/smt/theory_jobscheduler.h | 124 +++++++++++++++++++++++++++ 5 files changed, 280 insertions(+), 22 deletions(-) create mode 100644 src/smt/theory_jobscheduler.cpp create mode 100644 src/smt/theory_jobscheduler.h diff --git a/src/ast/jobshop_decl_plugin.cpp b/src/ast/jobshop_decl_plugin.cpp index 41d8ad241..ced77690d 100644 --- a/src/ast/jobshop_decl_plugin.cpp +++ b/src/ast/jobshop_decl_plugin.cpp @@ -70,10 +70,6 @@ func_decl * jobshop_decl_plugin::mk_func_decl( 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; } @@ -106,7 +102,6 @@ void jobshop_decl_plugin::get_op_names(svector & op_names, symbol 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)); } } @@ -171,8 +166,3 @@ app* jobshop_util::mk_end(unsigned 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 index 94936c5aa..6a78646b0 100644 --- a/src/ast/jobshop_decl_plugin.h +++ b/src/ast/jobshop_decl_plugin.h @@ -12,17 +12,17 @@ Abstract: 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) + - start(j), end(j), job2resource(j) 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 - + // assume each job has at least one resource associated with it. + // introduce a dummy resource if needed. + // 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)) @@ -36,7 +36,7 @@ Abstract: 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) := 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; @@ -49,11 +49,10 @@ Abstract: 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_on_same_resource(j1, j2) := resource(j1) = resource(j2); + job_not_on_same_resource(j1, 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: @@ -77,8 +76,7 @@ enum js_op_kind { 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 + OP_JS_JOB2RESOURCE // resource associated with job }; class jobshop_decl_plugin : public decl_plugin { @@ -125,5 +123,4 @@ public: app* mk_start(unsigned j); app* mk_end(unsigned j); - app* mk_on_resource(unsigned j); }; diff --git a/src/smt/CMakeLists.txt b/src/smt/CMakeLists.txt index fb1997fb4..13a00d44e 100644 --- a/src/smt/CMakeLists.txt +++ b/src/smt/CMakeLists.txt @@ -55,6 +55,7 @@ z3_add_component(smt theory_dl.cpp theory_dummy.cpp theory_fpa.cpp + theory_jobscheduler.cpp theory_lra.cpp theory_opt.cpp theory_pb.cpp diff --git a/src/smt/theory_jobscheduler.cpp b/src/smt/theory_jobscheduler.cpp new file mode 100644 index 000000000..bf49a00fb --- /dev/null +++ b/src/smt/theory_jobscheduler.cpp @@ -0,0 +1,146 @@ +/*++ +Copyright (c) 2018 Microsoft Corporation + +Module Name: + + theory_jobscheduler.cpp + +Abstract: + + +Author: + + Nikolaj Bjorner (nbjorner) 2018-09-08. + +Revision History: + +--*/ + +#include "smt/theory_jobscheduler.h" +#include "smt/smt_context.h" + +namespace smt { + + theory_var theory_jobscheduler::mk_var(enode * n) { + theory_var v = theory::mk_var(n); + return v; + } + + bool theory_jobscheduler::internalize_atom(app * atom, bool gate_ctx) { + return false; + } + + bool theory_jobscheduler::internalize_term(app * term) { + return false; + } + + void theory_jobscheduler::assign_eh(bool_var v, bool is_true) { + + } + + void theory_jobscheduler::new_eq_eh(theory_var v1, theory_var v2) { + + } + + void theory_jobscheduler::new_diseq_eh(theory_var v1, theory_var v2) { + + } + + void theory_jobscheduler::push_scope_eh() { + + } + + void theory_jobscheduler::pop_scope_eh(unsigned num_scopes) { + + } + + final_check_status theory_jobscheduler::final_check_eh() { + return FC_DONE; + } + + bool theory_jobscheduler::can_propagate() { + return false; + } + + void theory_jobscheduler::propagate() { + + } + + theory_jobscheduler::theory_jobscheduler(ast_manager& m): theory(m.get_family_id("jobshop")), m(m), u(m) { + + } + + void theory_jobscheduler::display(std::ostream & out) const { + + } + + void theory_jobscheduler::collect_statistics(::statistics & st) const { + + } + + void theory_jobscheduler::init_model(model_generator & m) { + + } + + model_value_proc * theory_jobscheduler::mk_value(enode * n, model_generator & mg) { + return nullptr; + } + + bool theory_jobscheduler::get_value(enode * n, expr_ref & r) { + return false; + } + + theory * theory_jobscheduler::mk_fresh(context * new_ctx) { + return alloc(theory_jobscheduler, new_ctx->get_manager()); + } + + uint64_t theory_jobscheduler::est(unsigned j) { + return 0; + } + + uint64_t theory_jobscheduler::lst(unsigned j) { + return 0; + } + + uint64_t theory_jobscheduler::ect(unsigned j) { + return 0; + } + + uint64_t theory_jobscheduler::lct(unsigned j) { + return 0; + } + + uint64_t theory_jobscheduler::start(unsigned j) { + return 0; + } + + uint64_t theory_jobscheduler::end(unsigned j) { + return 0; + } + + unsigned theory_jobscheduler::resource(unsigned j) { + return 0; + } + + + void theory_jobscheduler::add_job_resource(unsigned j, unsigned r, unsigned cap, unsigned loadpct, uint64_t end) { + m_jobs.reserve(j + 1); + m_resources.reserve(r + 1); + job_info& ji = m_jobs[j]; + if (ji.m_resource2index.contains(r)) { + throw default_exception("resource already bound to job"); + } + ji.m_resource2index.insert(r, ji.m_resources.size()); + ji.m_resources.push_back(job_resource(r, cap, loadpct, end)); + SASSERT(!m_resources[r].m_jobs.contains(j)); + m_resources[r].m_jobs.push_back(j); + } + + void theory_jobscheduler::add_resource_available(unsigned r, unsigned max_loadpct, uint64_t start, uint64_t end) { + SASSERT(start < end); + m_resources.reserve(r + 1); + m_resources[r].m_available.push_back(res_available(max_loadpct, start, end)); + } + +}; + diff --git a/src/smt/theory_jobscheduler.h b/src/smt/theory_jobscheduler.h new file mode 100644 index 000000000..7e93e3454 --- /dev/null +++ b/src/smt/theory_jobscheduler.h @@ -0,0 +1,124 @@ +/*++ +Copyright (c) 2018 Microsoft Corporation + +Module Name: + + theory_jobscheduling.h + +Abstract: + + Propagation solver for jobscheduling problems. + It relies on an external module to tighten bounds of + job variables. + +Author: + + Nikolaj Bjorner (nbjorner) 2018-09-08. + +Revision History: + +--*/ +#pragma once; + +#include "smt/smt_theory.h" +#include "ast/jobshop_decl_plugin.h" + +namespace smt { + + class theory_jobscheduler : public theory { + + struct job_resource { + unsigned m_resource_id; // id of resource + unsigned m_capacity; // amount of resource to use + unsigned m_loadpct; // assuming loadpct + uint64_t m_end; // must run before + job_resource(unsigned r, unsigned cap, unsigned loadpct, uint64_t end): + m_resource_id(r), m_capacity(cap), m_loadpct(loadpct), m_end(end) {} + }; + + struct job_info { + vector m_resources; // resources allowed to run job. + u_map m_resource2index; // resource to index into vector + }; + + struct res_available { + unsigned m_loadpct; + uint64_t m_start; + uint64_t m_end; + res_available(unsigned load_pct, uint64_t start, uint64_t end): + m_loadpct(load_pct), + m_start(start), + m_end(end) + {} + }; + + struct res_info { + unsigned_vector m_jobs; // jobs allocated to run on resource + vector m_available; // time intervals where resource is available + uint64_t m_end; // can't run after + res_info(): m_end(std::numeric_limits::max()) {} + }; + + ast_manager& m; + jobshop_util u; + vector m_jobs; + vector m_resources; + + protected: + + theory_var mk_var(enode * n) override; + + bool internalize_atom(app * atom, bool gate_ctx) override; + + bool internalize_term(app * term) override; + + void assign_eh(bool_var v, bool is_true) override; + + void new_eq_eh(theory_var v1, theory_var v2) override; + + void new_diseq_eh(theory_var v1, theory_var v2) override; + + void push_scope_eh() override; + + void pop_scope_eh(unsigned num_scopes) override; + + final_check_status final_check_eh() override; + + bool can_propagate() override; + + void propagate() override; + + public: + + theory_jobscheduler(ast_manager& m); + + ~theory_jobscheduler() override {} + + void display(std::ostream & out) const override; + + void collect_statistics(::statistics & st) const override; + + void init_model(model_generator & m) override; + + model_value_proc * mk_value(enode * n, model_generator & mg) override; + + bool get_value(enode * n, expr_ref & r) override; + + theory * mk_fresh(context * new_ctx) override; // { return alloc(theory_jobscheduler, new_ctx->get_manager()); } + + public: + // assignments: + uint64_t est(unsigned j); // earliest start time of job j + uint64_t lst(unsigned j); // last start time + uint64_t ect(unsigned j); // earliest completion time + uint64_t lct(unsigned j); // last completion time + uint64_t start(unsigned j); // start time of job j + uint64_t end(unsigned j); // end time of job j + unsigned resource(unsigned j); // resource of job j + + // set up model + void add_job_resource(unsigned j, unsigned r, unsigned cap, unsigned loadpct, uint64_t end); + void add_resource_available(unsigned r, unsigned max_loadpct, uint64_t start, uint64_t end); + }; +}; +