initial decl plugin

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

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

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<js_sort_kind>(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<js_op_kind>(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<builtin_name> & 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<builtin_name> & 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<jobshop_decl_plugin*>(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));
+}
+

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<builtin_name> & op_names, symbol const & logic) override;
+    void get_sort_names(svector<builtin_name> & 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);
+};