mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

na

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-08-14 21:15:55 -07:00
parent 40a79694ea
commit d67bfd78b9
4 changed files with 39 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/ast/csp_decl_plugin.cpp
View file

@ -68,6 +68,11 @@ func_decl * csp_decl_plugin::mk_func_decl(
name = symbol("resource");
rng = m_resource_sort;
break;
case OP_JS_RESOURCE_MAKESPAN:
if (arity != 1 || domain[0] != m_resource_sort) m_manager->raise_exception("makespan expects a resource argument");
name = symbol("makespan");
rng = m_int_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");
@ -148,6 +153,7 @@ void csp_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol cons
if (logic == symbol("CSP")) {
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("makespan", OP_JS_RESOURCE_MAKESPAN));
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));
@ -233,10 +239,20 @@ app* csp_util::mk_job2resource(unsigned j) {
return m.mk_app(m.mk_func_decl(m_fid, OP_JS_JOB2RESOURCE, 0, nullptr, 1, &js, nullptr), job);
}
app* csp_util::mk_makespan(unsigned r) {
app_ref resource(mk_resource(r), m);
sort* rs = m.get_sort(resource);
return m.mk_app(m.mk_func_decl(m_fid, OP_JS_RESOURCE_MAKESPAN, 0, nullptr, 1, &rs, nullptr), resource);
}
bool csp_util::is_resource(expr* e, unsigned& r) {
return is_app_of(e, m_fid, OP_JS_RESOURCE) && (r = resource2id(e), true);
}
bool csp_util::is_makespan(expr * e, unsigned& r) {
return is_app_of(e, m_fid, OP_JS_RESOURCE_MAKESPAN) && is_resource(to_app(e)->get_arg(0), r);
}
bool csp_util::is_job(expr* e, unsigned& j) {
return is_app_of(e, m_fid, OP_JS_JOB) && (j = job2id(e), true);
}

26
src/ast/csp_decl_plugin.h
View file

@ -75,13 +75,14 @@ enum js_sort_kind {
enum js_op_kind {
OP_JS_JOB, // value of type job
OP_JS_RESOURCE, // value of type resource
OP_JS_RESOURCE_MAKESPAN, // makespan of resource: the minimal resource time required for assigned jobs.
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_MODEL, // jobscheduler model
OP_JS_JOB_RESOURCE,
OP_JS_JOB_PREEMPTABLE,
OP_JS_RESOURCE_AVAILABLE
OP_JS_JOB_RESOURCE, // model declaration for job assignment to resource
OP_JS_JOB_PREEMPTABLE, // model declaration for whether job is pre-emptable
OP_JS_RESOURCE_AVAILABLE // model declaration for availability intervals of resource
};
class csp_decl_plugin : public decl_plugin {
@ -116,29 +117,30 @@ private:
class csp_util {
ast_manager& m;
family_id m_fid;
csp_decl_plugin* m_plugin;
csp_decl_plugin* m_plugin;
public:
csp_util(ast_manager& m);
sort* mk_job_sort();
sort* mk_resource_sort();
app* mk_job(unsigned j);
bool is_job(expr* e, unsigned& j);
bool is_job2resource(expr* e, unsigned& j);
unsigned job2id(expr* j);
app* mk_resource(unsigned r);
bool is_resource(expr* e, unsigned& r);
unsigned resource2id(expr* r);
app* mk_start(unsigned j);
app* mk_end(unsigned j);
app* mk_job2resource(unsigned j);
app* mk_makespan(unsigned r);
bool is_job(expr* e, unsigned& j);
bool is_job2resource(expr* e, unsigned& j);
bool is_resource(expr* e, unsigned& r);
bool is_makespan(expr* e, unsigned& r);
bool is_add_resource_available(expr * e, expr *& res, unsigned& loadpct, uint64_t& start, uint64_t& end);
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);
bool is_model(expr* e) const { return is_app_of(e, m_fid, OP_JS_MODEL); }
private:
unsigned job2id(expr* j);
unsigned resource2id(expr* r);
};

9
src/smt/theory_jobscheduler.cpp
View file

@ -37,6 +37,7 @@ Features:
- try optimization based on arithmetic solver.
- earliest start, latest start
- constraint level
- add constraints gradually
- resource groups
- resource groups like a resource
- resources bound to resource groups within time intervals
@ -638,6 +639,9 @@ namespace smt {
app_ref res(u.mk_resource(r), m);
if (!ctx.e_internalized(res)) ctx.internalize(res, false);
ri.m_resource = ctx.get_enode(res);
app_ref ms(u.mk_makespan(r), m);
if (!ctx.e_internalized(ms)) ctx.internalize(ms, false);
ri.m_makespan = ctx.get_enode(ms);
}
ri.m_available.push_back(res_available(max_loadpct, start, end, ps));
}
@ -823,18 +827,19 @@ namespace smt {
vector<res_available>& available = m_resources[r].m_available;
unsigned lo = 0, hi = available.size(), mid = hi / 2;
while (lo < hi) {
SASSERT(lo <= mid && mid < hi);
res_available const& ra = available[mid];
if (ra.m_start <= t && t <= ra.m_end) {
idx = mid;
return true;
}
else if (ra.m_start > t && mid > 0) {
hi = mid - 1;
hi = mid;
mid = lo + (mid - lo) / 2;
}
else if (ra.m_end < t) {
lo = mid + 1;
mid += (hi - mid) / 2;
mid += (hi - mid + 1) / 2;
}
else {
break;

3
src/smt/theory_jobscheduler.h
View file

@ -91,7 +91,8 @@ namespace smt {
vector<res_available> m_available; // time intervals where resource is available
time_t m_end; // can't run after
enode* m_resource;
res_info(): m_end(std::numeric_limits<time_t>::max()), m_resource(nullptr) {}
enode* m_makespan;
res_info(): m_end(std::numeric_limits<time_t>::max()), m_resource(nullptr), m_makespan(nullptr) {}
};
ast_manager& m;