From 502c07126640f7912b34c01c35cb7a06c37941ea Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 14 Aug 2018 09:57:06 -0700 Subject: [PATCH] na Signed-off-by: Nikolaj Bjorner --- src/ast/jobshop_decl_plugin.cpp | 49 ++++++++++++++++++--------------- src/ast/jobshop_decl_plugin.h | 35 ----------------------- src/smt/theory_jobscheduler.cpp | 7 +---- src/smt/theory_jobscheduler.h | 1 - 4 files changed, 28 insertions(+), 64 deletions(-) diff --git a/src/ast/jobshop_decl_plugin.cpp b/src/ast/jobshop_decl_plugin.cpp index 79a2cf177..0eb14aad3 100644 --- a/src/ast/jobshop_decl_plugin.cpp +++ b/src/ast/jobshop_decl_plugin.cpp @@ -57,23 +57,23 @@ func_decl * jobshop_decl_plugin::mk_func_decl( 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)); + return m_manager->mk_func_decl(symbol("job"), arity, domain, 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)); + return m_manager->mk_func_decl(symbol("resource"), arity, domain, 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)); + 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"); + return m_manager->mk_func_decl(symbol("job-start"), arity, domain, 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)); + if (arity != 1 || domain[0] != m_job_sort) m_manager->raise_exception("resource expects a job argument"); + if (num_parameters > 0) m_manager->raise_exception("no parameters"); + return m_manager->mk_func_decl(symbol("job-end"), arity, domain, 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_resource_sort, func_decl_info(m_family_id, k, num_parameters, parameters)); + if (arity != 1 || domain[0] != m_job_sort) m_manager->raise_exception("job2resource expects a job argument"); + if (num_parameters > 0) m_manager->raise_exception("no parameters"); + return m_manager->mk_func_decl(symbol("job2resource"), arity, domain, m_resource_sort, func_decl_info(m_family_id, k, num_parameters, parameters)); case OP_JS_MODEL: @@ -185,11 +185,13 @@ app* jobshop_util::mk_job(unsigned j) { } unsigned jobshop_util::job2id(expr* j) { - SASSERT(is_app_of(j, m_fid, OP_JS_JOB) || - is_app_of(j, m_fid, OP_JS_START) || + if (is_app_of(j, m_fid, OP_JS_JOB)) { + return to_app(j)->get_decl()->get_parameter(0).get_int(); + } + SASSERT(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(); + return job2id(to_app(j)->get_arg(0)); } app* jobshop_util::mk_resource(unsigned r) { @@ -203,18 +205,21 @@ unsigned jobshop_util::resource2id(expr* r) { } 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_ref job(mk_job(j), m); + sort* js = m.get_sort(job); + return m.mk_app(m.mk_func_decl(m_fid, OP_JS_START, 0, nullptr, 1, &js, nullptr), job); } - -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_end(unsigned j) { + app_ref job(mk_job(j), m); + sort* js = m.get_sort(job); + return m.mk_app(m.mk_func_decl(m_fid, OP_JS_END, 0, nullptr, 1, &js, nullptr), job); } 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)); + app_ref job(mk_job(j), m); + sort* js = m.get_sort(job); + return m.mk_app(m.mk_func_decl(m_fid, OP_JS_JOB2RESOURCE, 0, nullptr, 1, &js, nullptr), job); } bool jobshop_util::is_resource(expr* e, unsigned& r) { diff --git a/src/ast/jobshop_decl_plugin.h b/src/ast/jobshop_decl_plugin.h index f295c901f..e7751436c 100644 --- a/src/ast/jobshop_decl_plugin.h +++ b/src/ast/jobshop_decl_plugin.h @@ -140,40 +140,6 @@ public: 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); - // alist features - app* mk_kv(symbol const& key, rational const& r) { - parameter ps[2] = { parameter(key), parameter(r) }; - return m.mk_const(m.mk_func_decl(m_fid, OP_AL_KV, 2, ps, 0, (sort*const*)nullptr, nullptr)); - } - app* mk_kv(symbol const& key, symbol const& val) { - parameter ps[2] = { parameter(key), parameter(val) }; - return m.mk_const(m.mk_func_decl(m_fid, OP_AL_KV, 2, ps, 0, (sort*const*)nullptr, nullptr)); - } - app* mk_alist(symbol const& key, unsigned n, expr* const* args) { - parameter p(key); - return m.mk_app(m.mk_func_decl(m_fid, OP_AL_LIST, 1, &p, n, args, nullptr), n, args); - - } - bool is_kv(expr* e, symbol& key, rational& r) { - return - (is_app_of(e, m_fid, OP_AL_KV) && - to_app(e)->get_decl()->get_num_parameters() == 2 && - to_app(e)->get_decl()->get_parameter(1).is_rational() && - (r = to_app(e)->get_decl()->get_parameter(1).get_rational(), key = to_app(e)->get_decl()->get_parameter(0).get_symbol(), true)) || - (is_app_of(e, m_fid, OP_AL_KV) && - to_app(e)->get_decl()->get_num_parameters() == 2 && - to_app(e)->get_decl()->get_parameter(1).is_int() && - (r = rational(to_app(e)->get_decl()->get_parameter(1).get_int()), key = to_app(e)->get_decl()->get_parameter(0).get_symbol(), true)); - - - } - bool is_kv(expr* e, symbol& key, symbol& s) { - return is_app_of(e, m_fid, OP_AL_KV) && - to_app(e)->get_decl()->get_num_parameters() == 2 && - to_app(e)->get_decl()->get_parameter(1).is_symbol() && - (s = to_app(e)->get_decl()->get_parameter(1).get_symbol(), key = to_app(e)->get_decl()->get_parameter(0).get_symbol(), true); - } - bool is_model(expr* e) const { return is_app_of(e, m_fid, OP_JS_MODEL); } bool is_alist(expr* e) const { return is_app_of(e, m_fid, OP_AL_LIST); } bool is_alist(expr* e, symbol& key) const { @@ -183,5 +149,4 @@ public: (key = to_app(e)->get_decl()->get_parameter(0).get_symbol(), true); } - // app* mk_model(unsigned n, expr* const* alist); }; diff --git a/src/smt/theory_jobscheduler.cpp b/src/smt/theory_jobscheduler.cpp index c138b6012..918f349cd 100644 --- a/src/smt/theory_jobscheduler.cpp +++ b/src/smt/theory_jobscheduler.cpp @@ -240,7 +240,7 @@ namespace smt { if (ctx.get_assignment(start_ge_lo) != l_true) { return; } - enode_pair eq(ji.m_job2resource, resource2enode(r)); + enode_pair eq(ji.m_job2resource, m_resources[r].m_resource); if (eq.first->get_root() != eq.second->get_root()) { return; } @@ -528,10 +528,6 @@ namespace smt { return 0; } - enode* theory_jobscheduler::resource2enode(unsigned r) { - return get_context().get_enode(u.mk_resource(r)); - } - void theory_jobscheduler::set_preemptable(unsigned j, bool is_preemptable) { m_jobs.reserve(j + 1); m_jobs[j].m_is_preemptable = is_preemptable; @@ -610,7 +606,6 @@ namespace smt { for (unsigned j = 0; j < m_jobs.size(); ++j) { job_info const& ji = m_jobs[j]; literal_vector disj; - app_ref job(u.mk_job(j), m); if (ji.m_resources.empty()) { throw default_exception("every job should be associated with at least one resource"); } diff --git a/src/smt/theory_jobscheduler.h b/src/smt/theory_jobscheduler.h index b83f99251..778d8baa8 100644 --- a/src/smt/theory_jobscheduler.h +++ b/src/smt/theory_jobscheduler.h @@ -161,7 +161,6 @@ namespace smt { time_t get_up(expr* e); time_t get_value(expr* e); unsigned resource(unsigned j); // resource of job j - enode* resource2enode(unsigned r); // derived bounds time_t ect(unsigned j, unsigned r, time_t start);