diff --git a/src/ast/CMakeLists.txt b/src/ast/CMakeLists.txt index 5340d4e7b..54e3c27e4 100644 --- a/src/ast/CMakeLists.txt +++ b/src/ast/CMakeLists.txt @@ -14,6 +14,7 @@ z3_add_component(ast ast_translation.cpp ast_util.cpp bv_decl_plugin.cpp + csp_decl_plugin.cpp datatype_decl_plugin.cpp decl_collector.cpp dl_decl_plugin.cpp @@ -30,7 +31,6 @@ 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/csp_decl_plugin.cpp similarity index 66% rename from src/ast/jobshop_decl_plugin.cpp rename to src/ast/csp_decl_plugin.cpp index 0eb14aad3..395677a4c 100644 --- a/src/ast/jobshop_decl_plugin.cpp +++ b/src/ast/csp_decl_plugin.cpp @@ -3,7 +3,7 @@ Copyright (c) 2018 Microsoft Corporation Module Name: - jobshop_decl_plugin.h + csp_decl_plugin.h Abstract: @@ -17,10 +17,10 @@ Revision History: --*/ -#include "ast/jobshop_decl_plugin.h" +#include "ast/csp_decl_plugin.h" #include "ast/arith_decl_plugin.h" -void jobshop_decl_plugin::set_manager(ast_manager* m, family_id fid) { +void csp_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_alist_sort = m_manager->mk_sort(symbol("AList"), sort_info(m_family_id, ALIST_SORT)); @@ -32,14 +32,14 @@ void jobshop_decl_plugin::set_manager(ast_manager* m, family_id fid) { m_manager->inc_ref(m_alist_sort); } -void jobshop_decl_plugin::finalize() { +void csp_decl_plugin::finalize() { m_manager->dec_ref(m_alist_sort); 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) { +sort * csp_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"); } @@ -51,43 +51,47 @@ sort * jobshop_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, parame } } -func_decl * jobshop_decl_plugin::mk_func_decl( +func_decl * csp_decl_plugin::mk_func_decl( decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort *) { + symbol name; + sort* rng = nullptr; switch (static_cast(k)) { case OP_JS_JOB: check_arity(arity); check_index1(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)); + name = symbol("job"); + rng = m_job_sort; + break; case OP_JS_RESOURCE: check_arity(arity); check_index1(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)); + name = symbol("resource"); + rng = m_resource_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"); - return m_manager->mk_func_decl(symbol("job-start"), arity, domain, m_int_sort, func_decl_info(m_family_id, k, num_parameters, parameters)); + name = symbol("job-start"); + rng = m_int_sort; + break; case OP_JS_END: 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)); + name = symbol("job-end"); + rng = m_int_sort; + break; case OP_JS_JOB2RESOURCE: 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)); - - + name = symbol("job2resource"); + rng = m_resource_sort; + break; case OP_JS_MODEL: // has no parameters // all arguments are of sort alist - return m_manager->mk_func_decl(symbol("js-model"), arity, domain, m_manager->mk_bool_sort(), func_decl_info(m_family_id, k, num_parameters, parameters)); - case OP_AL_KV: - // has two parameters, first is symbol - // has no arguments - return m_manager->mk_func_decl(symbol("kv"), arity, domain, m_alist_sort, func_decl_info(m_family_id, k, num_parameters, parameters)); - case OP_AL_LIST: - // has no parameters - // all arguments are of sort alist - return m_manager->mk_func_decl(symbol("alist"), arity, domain, m_alist_sort, func_decl_info(m_family_id, k, num_parameters, parameters)); + name = symbol("js-model"); + rng = m_manager->mk_bool_sort(); + break; case OP_JS_JOB_RESOURCE: if (arity != 5) m_manager->raise_exception("add-job-resource expects 5 arguments"); if (domain[0] != m_job_sort) m_manager->raise_exception("first argument of add-job-resource expects should be a job"); @@ -95,43 +99,52 @@ func_decl * jobshop_decl_plugin::mk_func_decl( if (domain[2] != m_int_sort) m_manager->raise_exception("3rd argument of add-job-resource expects should be an integer"); if (domain[3] != m_int_sort) m_manager->raise_exception("4th argument of add-job-resource expects should be an integer"); if (domain[4] != m_int_sort) m_manager->raise_exception("5th argument of add-job-resource expects should be an integer"); - return m_manager->mk_func_decl(symbol("add-job-resource"), arity, domain, m_alist_sort, func_decl_info(m_family_id, k, num_parameters, parameters)); + name = symbol("add-job-resource"); + rng = m_alist_sort; + break; case OP_JS_RESOURCE_AVAILABLE: if (arity != 4) m_manager->raise_exception("add-resource-available expects 4 arguments"); if (domain[0] != m_resource_sort) m_manager->raise_exception("first argument of add-resource-available expects should be a resource"); if (domain[1] != m_int_sort) m_manager->raise_exception("2nd argument of add-resource-available expects should be an integer"); if (domain[2] != m_int_sort) m_manager->raise_exception("3rd argument of add-resource-available expects should be an integer"); if (domain[3] != m_int_sort) m_manager->raise_exception("4th argument of add-resource-available expects should be an integer"); - return m_manager->mk_func_decl(symbol("add-resource-available"), arity, domain, m_alist_sort, func_decl_info(m_family_id, k, num_parameters, parameters)); + name = symbol("add-resource-available"); + rng = m_alist_sort; + break; case OP_JS_JOB_PREEMPTABLE: if (arity != 1 || domain[0] != m_job_sort) m_manager->raise_exception("set-preemptable expects one argument, which is a job"); - return m_manager->mk_func_decl(symbol("set-preemptable"), arity, domain, m_alist_sort, func_decl_info(m_family_id, k, num_parameters, parameters)); + name = symbol("set-preemptable"); + rng = m_alist_sort; + break; default: - UNREACHABLE(); return nullptr; + UNREACHABLE(); + return nullptr; } + return m_manager->mk_func_decl(name, arity, domain, rng, func_decl_info(m_family_id, k, num_parameters, parameters)); + } -void jobshop_decl_plugin::check_arity(unsigned arity) { +void csp_decl_plugin::check_arity(unsigned arity) { if (arity > 0) - m_manager->raise_exception("jobshop variables use parameters only and take no arguments"); + m_manager->raise_exception("csp variables use parameters only and take no arguments"); } -void jobshop_decl_plugin::check_index1(unsigned num_parameters, parameter const* ps) { +void csp_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"); + m_manager->raise_exception("csp variable expects a single integer parameter"); } -void jobshop_decl_plugin::check_index2(unsigned num_parameters, parameter const* ps) { +void csp_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"); + m_manager->raise_exception("csp variable expects two integer parameters"); } -bool jobshop_decl_plugin::is_value(app * e) const { +bool csp_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) { +void csp_decl_plugin::get_op_names(svector & op_names, symbol const & logic) { if (logic == symbol("CSP")) { op_names.push_back(builtin_name("job", OP_JS_JOB)); op_names.push_back(builtin_name("resource", OP_JS_RESOURCE)); @@ -139,8 +152,6 @@ void jobshop_decl_plugin::get_op_names(svector & op_names, symbol 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("js-model", OP_JS_MODEL)); - op_names.push_back(builtin_name("kv", OP_AL_KV)); - op_names.push_back(builtin_name("alist", OP_AL_LIST)); op_names.push_back(builtin_name("add-job-resource", OP_JS_JOB_RESOURCE)); op_names.push_back(builtin_name("add-resource-available", OP_JS_RESOURCE_AVAILABLE)); op_names.push_back(builtin_name("set-preemptable", OP_JS_JOB_PREEMPTABLE)); @@ -148,14 +159,14 @@ void jobshop_decl_plugin::get_op_names(svector & op_names, symbol } } -void jobshop_decl_plugin::get_sort_names(svector & sort_names, symbol const & logic) { +void csp_decl_plugin::get_sort_names(svector & sort_names, symbol const & logic) { if (logic == symbol("CSP")) { 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) { +expr * csp_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)); @@ -166,25 +177,25 @@ expr * jobshop_decl_plugin::get_some_value(sort * s) { } -jobshop_util::jobshop_util(ast_manager& m): m(m) { +csp_util::csp_util(ast_manager& m): m(m) { m_fid = m.mk_family_id("csp"); - m_plugin = static_cast(m.get_plugin(m_fid)); + m_plugin = static_cast(m.get_plugin(m_fid)); } -sort* jobshop_util::mk_job_sort() { +sort* csp_util::mk_job_sort() { return m_plugin->mk_job_sort(); } -sort* jobshop_util::mk_resource_sort() { +sort* csp_util::mk_resource_sort() { return m_plugin->mk_resource_sort(); } -app* jobshop_util::mk_job(unsigned j) { +app* csp_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) { +unsigned csp_util::job2id(expr* j) { if (is_app_of(j, m_fid, OP_JS_JOB)) { return to_app(j)->get_decl()->get_parameter(0).get_int(); } @@ -194,43 +205,43 @@ unsigned jobshop_util::job2id(expr* j) { return job2id(to_app(j)->get_arg(0)); } -app* jobshop_util::mk_resource(unsigned r) { +app* csp_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) { +unsigned csp_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) { +app* csp_util::mk_start(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_START, 0, nullptr, 1, &js, nullptr), job); } -app* jobshop_util::mk_end(unsigned j) { +app* csp_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) { +app* csp_util::mk_job2resource(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_JOB2RESOURCE, 0, nullptr, 1, &js, nullptr), job); } -bool jobshop_util::is_resource(expr* e, unsigned& r) { +bool csp_util::is_resource(expr* e, unsigned& r) { return is_app_of(e, m_fid, OP_JS_RESOURCE) && (r = resource2id(e), true); } -bool jobshop_util::is_job(expr* e, unsigned& j) { +bool csp_util::is_job(expr* e, unsigned& j) { return is_app_of(e, m_fid, OP_JS_JOB) && (j = job2id(e), true); } -bool jobshop_util::is_add_resource_available(expr * e, expr *& res, unsigned& loadpct, uint64_t& start, uint64_t& end) { +bool csp_util::is_add_resource_available(expr * e, expr *& res, unsigned& loadpct, uint64_t& start, uint64_t& end) { if (!is_app_of(e, m_fid, OP_JS_RESOURCE_AVAILABLE)) return false; res = to_app(e)->get_arg(0); arith_util a(m); @@ -244,7 +255,7 @@ bool jobshop_util::is_add_resource_available(expr * e, expr *& res, unsigned& lo return true; } -bool jobshop_util::is_add_job_resource(expr * e, expr *& job, expr*& res, unsigned& loadpct, uint64_t& capacity, uint64_t& end) { +bool csp_util::is_add_job_resource(expr * e, expr *& job, expr*& res, unsigned& loadpct, uint64_t& capacity, uint64_t& end) { if (!is_app_of(e, m_fid, OP_JS_JOB_RESOURCE)) return false; job = to_app(e)->get_arg(0); res = to_app(e)->get_arg(1); @@ -259,7 +270,7 @@ bool jobshop_util::is_add_job_resource(expr * e, expr *& job, expr*& res, unsign return true; } -bool jobshop_util::is_set_preemptable(expr* e, expr *& job) { +bool csp_util::is_set_preemptable(expr* e, expr *& job) { if (!is_app_of(e, m_fid, OP_JS_JOB_PREEMPTABLE)) return false; job = to_app(e)->get_arg(0); return true; diff --git a/src/ast/jobshop_decl_plugin.h b/src/ast/csp_decl_plugin.h similarity index 86% rename from src/ast/jobshop_decl_plugin.h rename to src/ast/csp_decl_plugin.h index e7751436c..5443180a4 100644 --- a/src/ast/jobshop_decl_plugin.h +++ b/src/ast/csp_decl_plugin.h @@ -3,7 +3,7 @@ Copyright (c) 2018 Microsoft Corporation Module Name: - jobshop_decl_plugin.h + csp_decl_plugin.h Abstract: @@ -81,18 +81,16 @@ enum js_op_kind { OP_JS_MODEL, // jobscheduler model OP_JS_JOB_RESOURCE, OP_JS_JOB_PREEMPTABLE, - OP_JS_RESOURCE_AVAILABLE, - OP_AL_KV, // key-value pair - OP_AL_LIST // tagged list + OP_JS_RESOURCE_AVAILABLE }; -class jobshop_decl_plugin : public decl_plugin { +class csp_decl_plugin : public decl_plugin { public: - jobshop_decl_plugin() {} - ~jobshop_decl_plugin() override {} + csp_decl_plugin() {} + ~csp_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); } + decl_plugin * mk_fresh() override { return alloc(csp_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; @@ -115,12 +113,12 @@ private: void check_index2(unsigned n, parameter const* ps); }; -class jobshop_util { +class csp_util { ast_manager& m; family_id m_fid; - jobshop_decl_plugin* m_plugin; + csp_decl_plugin* m_plugin; public: - jobshop_util(ast_manager& m); + csp_util(ast_manager& m); sort* mk_job_sort(); sort* mk_resource_sort(); @@ -141,12 +139,5 @@ public: bool is_set_preemptable(expr* e, expr *& job); 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 { - return is_alist(e) && - to_app(e)->get_decl()->get_num_parameters() == 1 && - to_app(e)->get_decl()->get_parameter(0).is_symbol() && - (key = to_app(e)->get_decl()->get_parameter(0).get_symbol(), true); - } }; diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 8387722b9..da495968a 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -30,7 +30,7 @@ Notes: #include "ast/seq_decl_plugin.h" #include "ast/pb_decl_plugin.h" #include "ast/fpa_decl_plugin.h" -#include "ast/jobshop_decl_plugin.h" +#include "ast/csp_decl_plugin.h" #include "ast/ast_pp.h" #include "ast/rewriter/var_subst.h" #include "ast/pp.h" @@ -696,7 +696,7 @@ void cmd_context::init_manager_core(bool new_manager) { register_plugin(symbol("pb"), alloc(pb_decl_plugin), logic_has_pb()); register_plugin(symbol("fpa"), alloc(fpa_decl_plugin), logic_has_fpa()); register_plugin(symbol("datalog_relation"), alloc(datalog::dl_decl_plugin), !has_logic()); - register_plugin(symbol("csp"), alloc(jobshop_decl_plugin), smt_logics::logic_is_csp(m_logic)); + register_plugin(symbol("csp"), alloc(csp_decl_plugin), smt_logics::logic_is_csp(m_logic)); } else { // the manager was created by an external module diff --git a/src/smt/theory_jobscheduler.h b/src/smt/theory_jobscheduler.h index 778d8baa8..9031f9e78 100644 --- a/src/smt/theory_jobscheduler.h +++ b/src/smt/theory_jobscheduler.h @@ -21,7 +21,7 @@ Revision History: #pragma once; #include "util/uint_set.h" -#include "ast/jobshop_decl_plugin.h" +#include "ast/csp_decl_plugin.h" #include "ast/arith_decl_plugin.h" #include "smt/smt_theory.h" @@ -94,7 +94,7 @@ namespace smt { }; ast_manager& m; - jobshop_util u; + csp_util u; arith_util a; vector m_jobs; vector m_resources;