From baeff82e5995dd9d7da9bd2a5095c6833fa1c8fc Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 10 Aug 2018 09:46:21 -0700 Subject: [PATCH] na Signed-off-by: Nikolaj Bjorner --- src/ast/jobshop_decl_plugin.cpp | 10 +++++- src/ast/jobshop_decl_plugin.h | 1 + src/smt/theory_jobscheduler.cpp | 61 +++++++++++++++++++++++---------- src/smt/theory_jobscheduler.h | 13 ++++--- 4 files changed, 62 insertions(+), 23 deletions(-) diff --git a/src/ast/jobshop_decl_plugin.cpp b/src/ast/jobshop_decl_plugin.cpp index ced77690d..7a7b1b590 100644 --- a/src/ast/jobshop_decl_plugin.cpp +++ b/src/ast/jobshop_decl_plugin.cpp @@ -142,7 +142,10 @@ app* jobshop_util::mk_job(unsigned j) { } unsigned jobshop_util::job2id(expr* j) { - SASSERT(is_app_of(j, m_fid, OP_JS_JOB)); + SASSERT(is_app_of(j, m_fid, OP_JS_JOB) || + is_app_of(j, m_fid, OP_JS_START) || + is_app_of(j, m_fid, OP_JS_END) || + is_app_of(j, m_fid, OP_JS_JOB2RESOURCE)); return to_app(j)->get_decl()->get_parameter(0).get_int(); } @@ -166,3 +169,8 @@ 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_job2resource(unsigned j) { + parameter p(j); + return m.mk_const(m.mk_func_decl(m_fid, OP_JS_JOB2RESOURCE, 1, &p, 0, (sort*const*)nullptr, nullptr)); +} + diff --git a/src/ast/jobshop_decl_plugin.h b/src/ast/jobshop_decl_plugin.h index 6a78646b0..48bdde6c1 100644 --- a/src/ast/jobshop_decl_plugin.h +++ b/src/ast/jobshop_decl_plugin.h @@ -123,4 +123,5 @@ public: app* mk_start(unsigned j); app* mk_end(unsigned j); + app* mk_job2resource(unsigned j); }; diff --git a/src/smt/theory_jobscheduler.cpp b/src/smt/theory_jobscheduler.cpp index bf49a00fb..f8439917e 100644 --- a/src/smt/theory_jobscheduler.cpp +++ b/src/smt/theory_jobscheduler.cpp @@ -26,32 +26,55 @@ namespace smt { return v; } - bool theory_jobscheduler::internalize_atom(app * atom, bool gate_ctx) { - return false; - } - bool theory_jobscheduler::internalize_term(app * term) { - return false; + context & ctx = get_context(); + if (ctx.e_internalized(term)) + return true; + enode* e = ctx.mk_enode(term, false, false, true); + switch (static_cast(term->get_decl()->get_decl_kind())) { + case OP_JS_JOB: { + unsigned j = u.job2id(term); + app_ref start(u.mk_start(j), m); + app_ref end(u.mk_end(j), m); + app_ref res(u.mk_resource(j), m); + 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); + theory_var v = mk_var(e); + SASSERT(m_var2index.size() == v); + m_var2index.push_back(j); + m_jobs.reserve(j + 1); + m_jobs[j].m_start = ctx.get_enode(start); + m_jobs[j].m_end = ctx.get_enode(end); + m_jobs[j].m_resource = ctx.get_enode(res); + ctx.attach_th_var(e, this, v); + break; + } + case OP_JS_RESOURCE: { + theory_var v = mk_var(e); + SASSERT(m_var2index.size() == v); + unsigned r = u.resource2id(term); + m_var2index.push_back(r); + ctx.attach_th_var(e, this, v); + break; + } + case OP_JS_START: + case OP_JS_END: + case OP_JS_JOB2RESOURCE: { + unsigned j = u.job2id(term); + app_ref job(u.mk_job(j), m); + if (!ctx.e_internalized(job)) ctx.internalize(job, false); + break; + } + } + return true; } - 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() { @@ -124,6 +147,7 @@ namespace smt { void theory_jobscheduler::add_job_resource(unsigned j, unsigned r, unsigned cap, unsigned loadpct, uint64_t end) { + // assert: done at base level m_jobs.reserve(j + 1); m_resources.reserve(r + 1); job_info& ji = m_jobs[j]; @@ -137,6 +161,7 @@ namespace smt { } void theory_jobscheduler::add_resource_available(unsigned r, unsigned max_loadpct, uint64_t start, uint64_t end) { + // assert: done at base level 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 index 7e93e3454..ec09ce0ce 100644 --- a/src/smt/theory_jobscheduler.h +++ b/src/smt/theory_jobscheduler.h @@ -39,6 +39,10 @@ namespace smt { struct job_info { vector m_resources; // resources allowed to run job. u_map m_resource2index; // resource to index into vector + enode* m_start; + enode* m_end; + enode* m_resource; + job_info(): m_start(nullptr), m_end(nullptr), m_resource(nullptr) {} }; struct res_available { @@ -61,6 +65,7 @@ namespace smt { ast_manager& m; jobshop_util u; + unsigned_vector m_var2index; vector m_jobs; vector m_resources; @@ -68,15 +73,15 @@ namespace smt { theory_var mk_var(enode * n) override; - bool internalize_atom(app * atom, bool gate_ctx) override; + bool internalize_atom(app * atom, bool gate_ctx) override { return false; } bool internalize_term(app * term) override; - void assign_eh(bool_var v, bool is_true) override; + 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;