add theory outlline

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

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<builtin_name> & 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));
-}
-

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);
 };

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

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));
+    }
+    
+};
+

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<job_resource> m_resources; // resources allowed to run job.
+            u_map<unsigned>      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<res_available> m_available; // time intervals where resource is available
+            uint64_t              m_end;       // can't run after
+            res_info(): m_end(std::numeric_limits<uint64_t>::max()) {}
+        };
+        
+        ast_manager&     m;
+        jobshop_util     u;
+        vector<job_info> m_jobs;
+        vector<res_info> 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);
+    };    
+};
+