mirror of
https://github.com/Z3Prover/z3
synced 2025-04-24 01:25:31 +00:00
add js-model interfacing
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
0af00e62de
commit
3478b8b924
11 changed files with 275 additions and 59 deletions
|
|
@ -30,7 +30,6 @@ namespace smt {
|
|||
|
||||
bool arith_value::get_lo(expr* e, rational& lo, bool& is_strict) {
|
||||
if (!m_ctx.e_internalized(e)) return false;
|
||||
expr_ref _lo(m);
|
||||
family_id afid = a.get_family_id();
|
||||
is_strict = false;
|
||||
enode* next = m_ctx.get_enode(e), *n = next;
|
||||
|
|
@ -42,15 +41,9 @@ namespace smt {
|
|||
theory_i_arith* thi = dynamic_cast<theory_i_arith*>(th);
|
||||
theory_lra* thr = dynamic_cast<theory_lra*>(th);
|
||||
do {
|
||||
if (tha && tha->get_lower(next, _lo) && a.is_numeral(_lo, lo1)) {
|
||||
if (!found || lo1 > lo) lo = lo1;
|
||||
found = true;
|
||||
}
|
||||
else if (thi && thi->get_lower(next, _lo) && a.is_numeral(_lo, lo1)) {
|
||||
if (!found || lo1 > lo) lo = lo1;
|
||||
found = true;
|
||||
}
|
||||
else if (thr && thr->get_lower(next, lo1, is_strict1)) {
|
||||
if ((tha && tha->get_lower(next, lo1, is_strict1)) ||
|
||||
(thi && thi->get_lower(next, lo1, is_strict1)) ||
|
||||
(thr && thr->get_lower(next, lo1, is_strict1))) {
|
||||
if (!found || lo1 > lo || (lo == lo1 && is_strict1)) lo = lo1, is_strict = is_strict1;
|
||||
found = true;
|
||||
}
|
||||
|
|
@ -62,7 +55,6 @@ namespace smt {
|
|||
|
||||
bool arith_value::get_up(expr* e, rational& up, bool& is_strict) {
|
||||
if (!m_ctx.e_internalized(e)) return false;
|
||||
expr_ref _up(m);
|
||||
family_id afid = a.get_family_id();
|
||||
is_strict = false;
|
||||
enode* next = m_ctx.get_enode(e), *n = next;
|
||||
|
|
@ -73,15 +65,9 @@ namespace smt {
|
|||
theory_i_arith* thi = dynamic_cast<theory_i_arith*>(th);
|
||||
theory_lra* thr = dynamic_cast<theory_lra*>(th);
|
||||
do {
|
||||
if (tha && tha->get_upper(next, _up) && a.is_numeral(_up, up1)) {
|
||||
if (!found || up1 < up) up = up1;
|
||||
found = true;
|
||||
}
|
||||
else if (thi && thi->get_upper(next, _up) && a.is_numeral(_up, up1)) {
|
||||
if (!found || up1 < up) up = up1;
|
||||
found = true;
|
||||
}
|
||||
else if (thr && thr->get_upper(next, up1, is_strict1)) {
|
||||
if ((tha && tha->get_upper(next, up1, is_strict1)) ||
|
||||
(thi && thi->get_upper(next, up1, is_strict1)) ||
|
||||
(thr && thr->get_upper(next, up1, is_strict1))) {
|
||||
if (!found || up1 < up || (up1 == up && is_strict1)) up = up1, is_strict = is_strict1;
|
||||
found = true;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1071,6 +1071,8 @@ namespace smt {
|
|||
|
||||
bool get_lower(enode* n, expr_ref& r);
|
||||
bool get_upper(enode* n, expr_ref& r);
|
||||
bool get_lower(enode* n, rational& r, bool &is_strict);
|
||||
bool get_upper(enode* n, rational& r, bool &is_strict);
|
||||
bool to_expr(inf_numeral const& val, bool is_int, expr_ref& r);
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -3303,6 +3303,20 @@ namespace smt {
|
|||
return b && to_expr(b->get_value(), is_int(v), r);
|
||||
}
|
||||
|
||||
template<typename Ext>
|
||||
bool theory_arith<Ext>::get_lower(enode * n, rational& r, bool& is_strict) {
|
||||
theory_var v = n->get_th_var(get_id());
|
||||
bound* b = (v == null_theory_var) ? nullptr : lower(v);
|
||||
return b && (r = b->get_value().get_rational().to_rational(), is_strict = b->get_value().get_infinitesimal().is_pos(), true);
|
||||
}
|
||||
|
||||
template<typename Ext>
|
||||
bool theory_arith<Ext>::get_upper(enode * n, rational& r, bool& is_strict) {
|
||||
theory_var v = n->get_th_var(get_id());
|
||||
bound* b = (v == null_theory_var) ? nullptr : upper(v);
|
||||
return b && (r = b->get_value().get_rational().to_rational(), is_strict = b->get_value().get_infinitesimal().is_neg(), true);
|
||||
}
|
||||
|
||||
// -----------------------------------
|
||||
//
|
||||
// Backtracking
|
||||
|
|
|
|||
|
|
@ -65,7 +65,7 @@ namespace smt {
|
|||
unsigned j = u.job2id(term);
|
||||
app_ref start(u.mk_start(j), m);
|
||||
app_ref end(u.mk_end(j), m);
|
||||
app_ref res(u.mk_resource(j), m);
|
||||
app_ref res(u.mk_job2resource(j), m);
|
||||
if (!ctx.e_internalized(start)) ctx.internalize(start, false);
|
||||
if (!ctx.e_internalized(end)) ctx.internalize(end, false);
|
||||
if (!ctx.e_internalized(res)) ctx.internalize(res, false);
|
||||
|
|
@ -75,7 +75,7 @@ namespace smt {
|
|||
m_jobs.reserve(j + 1);
|
||||
m_jobs[j].m_start = ctx.get_enode(start);
|
||||
m_jobs[j].m_end = ctx.get_enode(end);
|
||||
m_jobs[j].m_resource = ctx.get_enode(res);
|
||||
m_jobs[j].m_job2resource = ctx.get_enode(res);
|
||||
ctx.attach_th_var(e, this, v);
|
||||
break;
|
||||
}
|
||||
|
|
@ -99,6 +99,89 @@ namespace smt {
|
|||
return true;
|
||||
}
|
||||
|
||||
bool theory_jobscheduler::internalize_atom(app * atom, bool gate_ctx) {
|
||||
SASSERT(u.is_model(atom));
|
||||
for (expr* arg : *atom) {
|
||||
internalize_cmd(arg);
|
||||
}
|
||||
add_done();
|
||||
return true;
|
||||
}
|
||||
|
||||
// TBD: stronger parameter validation
|
||||
void theory_jobscheduler::internalize_cmd(expr* cmd) {
|
||||
symbol key, val;
|
||||
rational r;
|
||||
if (u.is_kv(cmd, key, r)) {
|
||||
if (key == ":set-preemptable" && r.is_unsigned()) {
|
||||
set_preemptable(r.get_unsigned(), true);
|
||||
return;
|
||||
}
|
||||
warning_msg("command not recognized");
|
||||
}
|
||||
else if (u.is_alist(cmd, key) && key == ":add-job-resource") {
|
||||
properties ps;
|
||||
unsigned j = 0, res = 0, cap = 0, loadpct = 100;
|
||||
time_t end = std::numeric_limits<time_t>::max();
|
||||
for (expr* arg : *to_app(cmd)) {
|
||||
if (u.is_kv(arg, key, r)) {
|
||||
if (key == ":job") {
|
||||
j = r.get_unsigned();
|
||||
}
|
||||
else if (key == ":resource") {
|
||||
res = r.get_unsigned();
|
||||
}
|
||||
else if (key == ":capacity") {
|
||||
cap = r.get_unsigned();
|
||||
}
|
||||
else if (key == ":loadpct") {
|
||||
loadpct = r.get_unsigned();
|
||||
}
|
||||
else if (key == ":end") {
|
||||
end = r.get_uint64();
|
||||
}
|
||||
}
|
||||
else if (u.is_alist(arg, key) && key == ":properties") {
|
||||
// TBD
|
||||
}
|
||||
}
|
||||
if (cap > 0) {
|
||||
add_job_resource(j, res, cap, loadpct, end, ps);
|
||||
}
|
||||
else {
|
||||
warning_msg("no job capacity provided");
|
||||
}
|
||||
}
|
||||
else if (u.is_alist(cmd, key) && key == ":add-resource-available") {
|
||||
properties ps;
|
||||
unsigned res = 0, loadpct = 100;
|
||||
time_t start = 0, end = 0;
|
||||
for (expr* arg : *to_app(cmd)) {
|
||||
if (u.is_kv(arg, key, r)) {
|
||||
if (key == ":resource") {
|
||||
res = r.get_unsigned();
|
||||
}
|
||||
else if (key == ":start") {
|
||||
start = r.get_unsigned();
|
||||
}
|
||||
else if (key == ":end") {
|
||||
end = r.get_unsigned();
|
||||
}
|
||||
else if (key == ":loadpct") {
|
||||
loadpct = r.get_unsigned();
|
||||
}
|
||||
}
|
||||
else if (u.is_alist(arg, key) && key == ":properties") {
|
||||
// TBD
|
||||
}
|
||||
add_resource_available(res, loadpct, start, end, ps);
|
||||
}
|
||||
|
||||
}
|
||||
else {
|
||||
warning_msg("command not recognized");
|
||||
}
|
||||
}
|
||||
|
||||
void theory_jobscheduler::push_scope_eh() {
|
||||
}
|
||||
|
|
@ -214,7 +297,7 @@ namespace smt {
|
|||
if (ctx.get_assignment(start_ge_lo) != l_true) {
|
||||
return;
|
||||
}
|
||||
enode_pair eq(ji.m_resource, ctx.get_enode(u.mk_resource(r)));
|
||||
enode_pair eq(ji.m_job2resource, resource2enode(r));
|
||||
if (eq.first->get_root() != eq.second->get_root()) {
|
||||
return;
|
||||
}
|
||||
|
|
@ -368,7 +451,7 @@ namespace smt {
|
|||
}
|
||||
|
||||
theory_jobscheduler::theory_jobscheduler(ast_manager& m):
|
||||
theory(m.get_family_id("jobshop")), m(m), u(m), a(m) {
|
||||
theory(m.get_family_id("csp")), m(m), u(m), a(m) {
|
||||
}
|
||||
|
||||
std::ostream& theory_jobscheduler::display(std::ostream & out, job_resource const& jr) const {
|
||||
|
|
@ -423,51 +506,76 @@ namespace smt {
|
|||
return alloc(theory_jobscheduler, new_ctx->get_manager());
|
||||
}
|
||||
|
||||
time_t theory_jobscheduler::est(unsigned j) {
|
||||
time_t theory_jobscheduler::get_lo(expr* e) {
|
||||
arith_value av(get_context());
|
||||
rational val;
|
||||
bool is_strict;
|
||||
if (av.get_lo(u.mk_start(j), val, is_strict) && !is_strict && val.is_uint64()) {
|
||||
if (av.get_lo(e, val, is_strict) && !is_strict && val.is_uint64()) {
|
||||
return val.get_uint64();
|
||||
}
|
||||
return 0;
|
||||
}
|
||||
|
||||
time_t theory_jobscheduler::lst(unsigned j) {
|
||||
time_t theory_jobscheduler::get_up(expr* e) {
|
||||
arith_value av(get_context());
|
||||
rational val;
|
||||
bool is_strict;
|
||||
if (av.get_up(u.mk_start(j), val, is_strict) && !is_strict && val.is_uint64()) {
|
||||
if (av.get_up(e, val, is_strict) && !is_strict && val.is_uint64()) {
|
||||
return val.get_uint64();
|
||||
}
|
||||
return std::numeric_limits<time_t>::max();
|
||||
}
|
||||
|
||||
time_t theory_jobscheduler::ect(unsigned j) {
|
||||
NOT_IMPLEMENTED_YET();
|
||||
time_t theory_jobscheduler::get_value(expr* e) {
|
||||
arith_value av(get_context());
|
||||
rational val;
|
||||
if (av.get_value(e, val) && val.is_uint64()) {
|
||||
return val.get_uint64();
|
||||
}
|
||||
return 0;
|
||||
}
|
||||
|
||||
time_t theory_jobscheduler::est(unsigned j) {
|
||||
return get_lo(m_jobs[j].m_start->get_owner());
|
||||
}
|
||||
|
||||
time_t theory_jobscheduler::lst(unsigned j) {
|
||||
return get_up(m_jobs[j].m_start->get_owner());
|
||||
}
|
||||
|
||||
time_t theory_jobscheduler::ect(unsigned j) {
|
||||
return get_lo(m_jobs[j].m_end->get_owner());
|
||||
}
|
||||
|
||||
time_t theory_jobscheduler::lct(unsigned j) {
|
||||
NOT_IMPLEMENTED_YET();
|
||||
return 0;
|
||||
return get_up(m_jobs[j].m_end->get_owner());
|
||||
}
|
||||
|
||||
time_t theory_jobscheduler::start(unsigned j) {
|
||||
NOT_IMPLEMENTED_YET();
|
||||
return 0;
|
||||
return get_value(m_jobs[j].m_start->get_owner());
|
||||
}
|
||||
|
||||
time_t theory_jobscheduler::end(unsigned j) {
|
||||
NOT_IMPLEMENTED_YET();
|
||||
return 0;
|
||||
return get_value(m_jobs[j].m_end->get_owner());
|
||||
}
|
||||
|
||||
unsigned theory_jobscheduler::resource(unsigned j) {
|
||||
NOT_IMPLEMENTED_YET();
|
||||
unsigned r;
|
||||
enode* next = m_jobs[j].m_job2resource, *n = next;
|
||||
do {
|
||||
if (u.is_resource(next->get_owner(), r)) {
|
||||
return r;
|
||||
}
|
||||
next = next->get_next();
|
||||
}
|
||||
while (next != n);
|
||||
return 0;
|
||||
}
|
||||
|
||||
enode* theory_jobscheduler::resource2enode(unsigned r) {
|
||||
return get_context().get_enode(u.mk_resource(r));
|
||||
}
|
||||
|
||||
void theory_jobscheduler::set_preemptable(unsigned j, bool is_preemptable) {
|
||||
m_jobs.reserve(j + 1);
|
||||
m_jobs[j].m_is_preemptable = is_preemptable;
|
||||
|
|
@ -494,7 +602,8 @@ namespace smt {
|
|||
SASSERT(1 <= max_loadpct && max_loadpct <= 100);
|
||||
SASSERT(start <= end);
|
||||
m_resources.reserve(r + 1);
|
||||
m_resources[r].m_available.push_back(res_available(max_loadpct, start, end, ps));
|
||||
res_info& ri = m_resources[r];
|
||||
ri.m_available.push_back(res_available(max_loadpct, start, end, ps));
|
||||
}
|
||||
|
||||
/*
|
||||
|
|
|
|||
|
|
@ -62,8 +62,8 @@ namespace smt {
|
|||
u_map<unsigned> m_resource2index; // resource to index into vector
|
||||
enode* m_start;
|
||||
enode* m_end;
|
||||
enode* m_resource;
|
||||
job_info(): m_is_preemptable(true), m_start(nullptr), m_end(nullptr), m_resource(nullptr) {}
|
||||
enode* m_job2resource;
|
||||
job_info(): m_is_preemptable(false), m_start(nullptr), m_end(nullptr), m_job2resource(nullptr) {}
|
||||
};
|
||||
|
||||
struct res_available {
|
||||
|
|
@ -88,7 +88,8 @@ namespace smt {
|
|||
unsigned_vector m_jobs; // jobs allocated to run on resource
|
||||
vector<res_available> m_available; // time intervals where resource is available
|
||||
time_t m_end; // can't run after
|
||||
res_info(): m_end(std::numeric_limits<time_t>::max()) {}
|
||||
enode* m_resource;
|
||||
res_info(): m_end(std::numeric_limits<time_t>::max()), m_resource(nullptr) {}
|
||||
};
|
||||
|
||||
ast_manager& m;
|
||||
|
|
@ -102,7 +103,7 @@ namespace smt {
|
|||
|
||||
theory_var mk_var(enode * n) override;
|
||||
|
||||
bool internalize_atom(app * atom, bool gate_ctx) override { return false; }
|
||||
bool internalize_atom(app * atom, bool gate_ctx) override;
|
||||
|
||||
bool internalize_term(app * term) override;
|
||||
|
||||
|
|
@ -154,7 +155,11 @@ namespace smt {
|
|||
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
|
||||
time_t get_lo(expr* e);
|
||||
time_t get_up(expr* e);
|
||||
time_t get_value(expr* e);
|
||||
unsigned resource(unsigned j); // resource of job j
|
||||
enode* resource2enode(unsigned r);
|
||||
|
||||
// derived bounds
|
||||
time_t ect(unsigned j, unsigned r, time_t start);
|
||||
|
|
@ -201,6 +206,8 @@ namespace smt {
|
|||
literal mk_le(enode* l, enode* r);
|
||||
literal mk_literal(expr* e);
|
||||
|
||||
void internalize_cmd(expr* cmd);
|
||||
|
||||
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;
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue