mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-09 04:31:24 +00:00
Code Activity

na

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-08-10 17:52:34 -07:00
parent baeff82e59
commit 55f15b0921
3 changed files with 273 additions and 28 deletions
Download patch file Download diff file Expand all files Collapse all files

66
src/smt/theory_jobscheduler.h
View file

@ -22,20 +22,35 @@ Revision History:
#include "smt/smt_theory.h"
#include "ast/jobshop_decl_plugin.h"
#include "ast/arith_decl_plugin.h"
namespace smt {
typedef uint64_t time_t;
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):
time_t m_end; // must run before
job_resource(unsigned r, unsigned cap, unsigned loadpct, time_t end):
m_resource_id(r), m_capacity(cap), m_loadpct(loadpct), m_end(end) {}
};
struct job_time {
unsigned m_job;
time_t m_time;
job_time(unsigned j, time_t time): m_job(j), m_time(time) {}
struct compare {
bool operator()(job_time const& jt1, job_time const& jt2) const {
return jt1.m_time < jt2.m_time;
}
};
};
struct job_info {
vector<job_resource> m_resources; // resources allowed to run job.
u_map<unsigned> m_resource2index; // resource to index into vector
@ -47,24 +62,31 @@ namespace smt {
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):
time_t m_start;
time_t m_end;
res_available(unsigned load_pct, time_t start, time_t end):
m_loadpct(load_pct),
m_start(start),
m_end(end)
{}
struct compare {
bool operator()(res_available const& ra1, res_available const& ra2) const {
return ra1.m_start < ra2.m_start;
}
};
};
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()) {}
time_t m_end; // can't run after
res_info(): m_end(std::numeric_limits<time_t>::max()) {}
};
ast_manager& m;
jobshop_util u;
arith_util a;
unsigned_vector m_var2index;
vector<job_info> m_jobs;
vector<res_info> m_resources;
@ -113,17 +135,31 @@ namespace smt {
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
time_t est(unsigned j); // earliest start time of job j
time_t lst(unsigned j); // last start time
time_t ect(unsigned j); // earliest completion time
time_t lct(unsigned j); // last completion time
time_t start(unsigned j); // start time of job j
time_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);
void add_job_resource(unsigned j, unsigned r, unsigned cap, unsigned loadpct, time_t end);
void add_resource_available(unsigned r, unsigned max_loadpct, time_t start, time_t end);
void add_done();
// validate assignment
void validate_assignment();
bool resource_available(unsigned r, time_t t, unsigned& load_pct, time_t& end, unsigned& idx); // load available on resource r at time t.
time_t capacity_used(unsigned j, unsigned r, time_t start, time_t end); // capacity used between start and end
job_resource const& get_job_resource(unsigned j, unsigned r) const;
std::ostream& display(std::ostream & out, res_info const& r) const;
std::ostream& display(std::ostream & out, res_available const& r) const;
std::ostream& display(std::ostream & out, job_info const& r) const;
std::ostream& display(std::ostream & out, job_resource const& r) const;
};
};