From 72304616712b5366993218ca9c5812520342f7d9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 20 Aug 2018 23:51:51 +0200 Subject: [PATCH] adding properities Signed-off-by: Nikolaj Bjorner --- src/api/api_datalog.cpp | 95 +++++++++++++++++++++++++- src/api/api_qe.cpp | 2 +- src/ast/csp_decl_plugin.cpp | 33 +++++++-- src/ast/csp_decl_plugin.h | 8 ++- src/smt/theory_jobscheduler.cpp | 116 +++++++++++++++++++++++++++----- src/smt/theory_jobscheduler.h | 10 ++- 6 files changed, 235 insertions(+), 29 deletions(-) diff --git a/src/api/api_datalog.cpp b/src/api/api_datalog.cpp index b0a4def55..61c0dc3a5 100644 --- a/src/api/api_datalog.cpp +++ b/src/api/api_datalog.cpp @@ -623,6 +623,99 @@ extern "C" { to_fixedpoint_ref(d)->ctx().add_constraint(to_expr(e), lvl); } -#include "api_datalog_spacer.inc" + Z3_lbool Z3_API Z3_fixedpoint_query_from_lvl (Z3_context c, Z3_fixedpoint d, Z3_ast q, unsigned lvl) { + Z3_TRY; + LOG_Z3_fixedpoint_query_from_lvl (c, d, q, lvl); + RESET_ERROR_CODE(); + lbool r = l_undef; + unsigned timeout = to_fixedpoint(d)->m_params.get_uint("timeout", mk_c(c)->get_timeout()); + unsigned rlimit = to_fixedpoint(d)->m_params.get_uint("rlimit", mk_c(c)->get_rlimit()); + { + scoped_rlimit _rlimit(mk_c(c)->m().limit(), rlimit); + cancel_eh eh(mk_c(c)->m().limit()); + api::context::set_interruptable si(*(mk_c(c)), eh); + scoped_timer timer(timeout, &eh); + try { + r = to_fixedpoint_ref(d)->ctx().query_from_lvl (to_expr(q), lvl); + } + catch (z3_exception& ex) { + mk_c(c)->handle_exception(ex); + r = l_undef; + } + to_fixedpoint_ref(d)->ctx().cleanup(); + } + return of_lbool(r); + Z3_CATCH_RETURN(Z3_L_UNDEF); + } + + Z3_ast Z3_API Z3_fixedpoint_get_ground_sat_answer(Z3_context c, Z3_fixedpoint d) { + Z3_TRY; + LOG_Z3_fixedpoint_get_ground_sat_answer(c, d); + RESET_ERROR_CODE(); + expr* e = to_fixedpoint_ref(d)->ctx().get_ground_sat_answer(); + mk_c(c)->save_ast_trail(e); + RETURN_Z3(of_expr(e)); + Z3_CATCH_RETURN(nullptr); + } + + Z3_ast_vector Z3_API Z3_fixedpoint_get_rules_along_trace( + Z3_context c, + Z3_fixedpoint d) + { + Z3_TRY; + LOG_Z3_fixedpoint_get_rules_along_trace(c, d); + ast_manager& m = mk_c(c)->m(); + Z3_ast_vector_ref* v = alloc(Z3_ast_vector_ref, *mk_c(c), m); + mk_c(c)->save_object(v); + expr_ref_vector rules(m); + svector names; + + to_fixedpoint_ref(d)->ctx().get_rules_along_trace_as_formulas(rules, names); + for (unsigned i = 0; i < rules.size(); ++i) { + v->m_ast_vector.push_back(rules[i].get()); + } + RETURN_Z3(of_ast_vector(v)); + Z3_CATCH_RETURN(nullptr); + } + + Z3_symbol Z3_API Z3_fixedpoint_get_rule_names_along_trace( + Z3_context c, + Z3_fixedpoint d) + { + Z3_TRY; + LOG_Z3_fixedpoint_get_rule_names_along_trace(c, d); + ast_manager& m = mk_c(c)->m(); + Z3_ast_vector_ref* v = alloc(Z3_ast_vector_ref, *mk_c(c), m); + mk_c(c)->save_object(v); + expr_ref_vector rules(m); + svector names; + std::stringstream ss; + + to_fixedpoint_ref(d)->ctx().get_rules_along_trace_as_formulas(rules, names); + for (unsigned i = 0; i < names.size(); ++i) { + ss << ";" << names[i].str(); + } + RETURN_Z3(of_symbol(symbol(ss.str().substr(1).c_str()))); + Z3_CATCH_RETURN(nullptr); + } + + void Z3_API Z3_fixedpoint_add_invariant(Z3_context c, Z3_fixedpoint d, Z3_func_decl pred, Z3_ast property) { + Z3_TRY; + LOG_Z3_fixedpoint_add_invariant(c, d, pred, property); + RESET_ERROR_CODE(); + to_fixedpoint_ref(d)->ctx ().add_invariant(to_func_decl(pred), to_expr(property)); + Z3_CATCH; + } + + Z3_ast Z3_API Z3_fixedpoint_get_reachable(Z3_context c, Z3_fixedpoint d, Z3_func_decl pred) { + Z3_TRY; + LOG_Z3_fixedpoint_get_reachable(c, d, pred); + RESET_ERROR_CODE(); + expr_ref r = to_fixedpoint_ref(d)->ctx().get_reachable(to_func_decl(pred)); + mk_c(c)->save_ast_trail(r); + RETURN_Z3(of_expr(r.get())); + Z3_CATCH_RETURN(nullptr); + } + }; diff --git a/src/api/api_qe.cpp b/src/api/api_qe.cpp index 94e83144f..167a694aa 100644 --- a/src/api/api_qe.cpp +++ b/src/api/api_qe.cpp @@ -1,5 +1,5 @@ /*++ -Copyright (c) 2017 Arie Gurfinkel +Copyright (c) 2018 Microsoft Corporation Module Name: diff --git a/src/ast/csp_decl_plugin.cpp b/src/ast/csp_decl_plugin.cpp index a6255d676..27feadc6d 100644 --- a/src/ast/csp_decl_plugin.cpp +++ b/src/ast/csp_decl_plugin.cpp @@ -98,21 +98,23 @@ func_decl * csp_decl_plugin::mk_func_decl( rng = m_manager->mk_bool_sort(); break; case OP_JS_JOB_RESOURCE: - if (arity != 5) m_manager->raise_exception("add-job-resource expects 5 arguments"); + if (arity != 6) m_manager->raise_exception("add-job-resource expects 6 arguments"); if (domain[0] != m_job_sort) m_manager->raise_exception("first argument of add-job-resource expects should be a job"); if (domain[1] != m_resource_sort) m_manager->raise_exception("second argument of add-job-resource expects should be a resource"); if (domain[2] != m_int_sort) m_manager->raise_exception("3rd argument of add-job-resource expects should be an integer"); if (domain[3] != m_int_sort) m_manager->raise_exception("4th argument of add-job-resource expects should be an integer"); if (domain[4] != m_int_sort) m_manager->raise_exception("5th argument of add-job-resource expects should be an integer"); + if (domain[5] != m_alist_sort) m_manager->raise_exception("6th argument of add-job-resource should be an a list of properties"); name = symbol("add-job-resource"); rng = m_alist_sort; break; case OP_JS_RESOURCE_AVAILABLE: - if (arity != 4) m_manager->raise_exception("add-resource-available expects 4 arguments"); + if (arity != 5) m_manager->raise_exception("add-resource-available expects 5 arguments"); if (domain[0] != m_resource_sort) m_manager->raise_exception("first argument of add-resource-available expects should be a resource"); if (domain[1] != m_int_sort) m_manager->raise_exception("2nd argument of add-resource-available expects should be an integer"); if (domain[2] != m_int_sort) m_manager->raise_exception("3rd argument of add-resource-available expects should be an integer"); if (domain[3] != m_int_sort) m_manager->raise_exception("4th argument of add-resource-available expects should be an integer"); + if (domain[4] != m_alist_sort) m_manager->raise_exception("5th argument of add-resource-available should be an a list of properties"); name = symbol("add-resource-available"); rng = m_alist_sort; break; @@ -121,6 +123,14 @@ func_decl * csp_decl_plugin::mk_func_decl( name = symbol("set-preemptable"); rng = m_alist_sort; break; + case OP_JS_PROPERTIES: + if (arity != 0) m_manager->raise_exception("js-properties takes no arguments"); + for (unsigned i = 0; i < num_parameters; ++i) { + if (!parameters[i].is_symbol()) m_manager->raise_exception("js-properties expects a list of keyword parameters"); + } + name = symbol("js-properties"); + rng = m_alist_sort; + break; default: UNREACHABLE(); return nullptr; @@ -161,7 +171,7 @@ void csp_decl_plugin::get_op_names(svector & op_names, symbol cons op_names.push_back(builtin_name("add-job-resource", OP_JS_JOB_RESOURCE)); op_names.push_back(builtin_name("add-resource-available", OP_JS_RESOURCE_AVAILABLE)); op_names.push_back(builtin_name("set-preemptable", OP_JS_JOB_PREEMPTABLE)); - + op_names.push_back(builtin_name("js-properties", OP_JS_PROPERTIES)); } } @@ -261,7 +271,7 @@ bool csp_util::is_job2resource(expr* e, unsigned& j) { return is_app_of(e, m_fid, OP_JS_JOB2RESOURCE) && (j = job2id(e), true); } -bool csp_util::is_add_resource_available(expr * e, expr *& res, unsigned& loadpct, uint64_t& start, uint64_t& end) { +bool csp_util::is_add_resource_available(expr * e, expr *& res, unsigned& loadpct, uint64_t& start, uint64_t& end, svector& properties) { if (!is_app_of(e, m_fid, OP_JS_RESOURCE_AVAILABLE)) return false; res = to_app(e)->get_arg(0); arith_util a(m); @@ -272,10 +282,11 @@ bool csp_util::is_add_resource_available(expr * e, expr *& res, unsigned& loadpc start = r.get_uint64(); if (!a.is_numeral(to_app(e)->get_arg(3), r) || !r.is_uint64()) return false; end = r.get_uint64(); + if (!is_js_properties(to_app(e)->get_arg(4), properties)) return false; return true; } -bool csp_util::is_add_job_resource(expr * e, expr *& job, expr*& res, unsigned& loadpct, uint64_t& capacity, uint64_t& end) { +bool csp_util::is_add_job_resource(expr * e, expr *& job, expr*& res, unsigned& loadpct, uint64_t& capacity, uint64_t& end, svector& properties) { if (!is_app_of(e, m_fid, OP_JS_JOB_RESOURCE)) return false; job = to_app(e)->get_arg(0); res = to_app(e)->get_arg(1); @@ -287,6 +298,7 @@ bool csp_util::is_add_job_resource(expr * e, expr *& job, expr*& res, unsigned& capacity = r.get_uint64(); if (!a.is_numeral(to_app(e)->get_arg(4), r) || !r.is_uint64()) return false; end = r.get_uint64(); + if (!is_js_properties(to_app(e)->get_arg(5), properties)) return false; return true; } @@ -295,3 +307,14 @@ bool csp_util::is_set_preemptable(expr* e, expr *& job) { job = to_app(e)->get_arg(0); return true; } + +bool csp_util::is_js_properties(expr* e, svector& properties) { + if (!is_app_of(e, m_fid, OP_JS_PROPERTIES)) return false; + unsigned sz = to_app(e)->get_decl()->get_num_parameters(); + for (unsigned i = 0; i < sz; ++i) { + properties.push_back(to_app(e)->get_decl()->get_parameter(i).get_symbol()); + } + return true; +} + + diff --git a/src/ast/csp_decl_plugin.h b/src/ast/csp_decl_plugin.h index faaaf344c..8d6ad56fa 100644 --- a/src/ast/csp_decl_plugin.h +++ b/src/ast/csp_decl_plugin.h @@ -82,7 +82,8 @@ enum js_op_kind { OP_JS_MODEL, // jobscheduler model 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 + OP_JS_RESOURCE_AVAILABLE, // model declaration for availability intervals of resource + OP_JS_PROPERTIES // model declaration of a set of properties. Each property is a keyword. }; class csp_decl_plugin : public decl_plugin { @@ -134,10 +135,11 @@ public: 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_add_resource_available(expr * e, expr *& res, unsigned& loadpct, uint64_t& start, uint64_t& end, svector& properites); + bool is_add_job_resource(expr * e, expr *& job, expr*& res, unsigned& loadpct, uint64_t& capacity, uint64_t& end, svector& properites); bool is_set_preemptable(expr* e, expr *& job); bool is_model(expr* e) const { return is_app_of(e, m_fid, OP_JS_MODEL); } + bool is_js_properties(expr* e, svector& properties); private: unsigned job2id(expr* j); diff --git a/src/smt/theory_jobscheduler.cpp b/src/smt/theory_jobscheduler.cpp index f27efd5a3..48009be31 100644 --- a/src/smt/theory_jobscheduler.cpp +++ b/src/smt/theory_jobscheduler.cpp @@ -83,6 +83,12 @@ namespace smt { return true; } + struct symbol_cmp { + bool operator()(symbol const& s1, symbol const& s2) const { + return lt(s1, s2); + } + }; + // TBD: stronger parameter validation void theory_jobscheduler::internalize_cmd(expr* cmd) { symbol key, val; @@ -94,10 +100,12 @@ namespace smt { if (u.is_set_preemptable(cmd, job) && u.is_job(job, j)) { set_preemptable(j, true); } - else if (u.is_add_resource_available(cmd, resource, loadpct, start, end) && u.is_resource(resource, res)) { + else if (u.is_add_resource_available(cmd, resource, loadpct, start, end, ps) && u.is_resource(resource, res)) { + std::sort(ps.begin(), ps.end(), symbol_cmp()); add_resource_available(res, loadpct, start, end, ps); } - else if (u.is_add_job_resource(cmd, job, resource, loadpct, capacity, end) && u.is_job(job, j) && u.is_resource(resource, res)) { + else if (u.is_add_job_resource(cmd, job, resource, loadpct, capacity, end, ps) && u.is_job(job, j) && u.is_resource(resource, res)) { + std::sort(ps.begin(), ps.end(), symbol_cmp()); add_job_resource(j, res, loadpct, capacity, end, ps); } else { @@ -306,12 +314,15 @@ namespace smt { bool theory_jobscheduler::constrain_end_time_interval(unsigned j, unsigned r) { unsigned idx1 = 0, idx2 = 0; time_t s = start(j); + job_resource const& jr = get_job_resource(j, r); TRACE("csp", tout << "job: " << j << " resource: " << r << " start: " << s << "\n";); - if (!resource_available(r, s, idx1)) return false; vector& available = m_resources[r].m_available; + if (!resource_available(r, s, idx1)) return false; + if (!resource_available(jr, available[idx1])) return false; time_t e = ect(j, r, s); TRACE("csp", tout << "job: " << j << " resource: " << r << " ect: " << e << "\n";); if (!resource_available(r, e, idx2)) return false; // infeasible.. + if (!resource_available(jr, available[idx2])) return false; time_t start1 = available[idx1].m_start; time_t end1 = available[idx1].m_end; unsigned cap1 = available[idx1].m_loadpct; @@ -445,12 +456,19 @@ namespace smt { assert_last_start_time(j, r, eq); assert_first_start_time(j, r, eq); vector const& available = ri.m_available; - for (unsigned i = 0; i + 1 < available.size(); ++i) { - SASSERT(available[i].m_end < available[i + 1].m_start); - assert_job_not_in_gap(j, r, i, eq); + // TBD: needs to take properties into account + + unsigned i = 0; + if (!first_available(jr, ri, i)) return; + while (true) { + unsigned next = i + 1; + if (!first_available(jr, ri, next)) return; + SASSERT(available[i].m_end < available[next].m_start); + assert_job_not_in_gap(j, r, i, next, eq); if (!ji.m_is_preemptable && available[i].m_end + 1 < available[i+1].m_start) { - assert_job_non_preemptable(j, r, i, eq); + assert_job_non_preemptable(j, r, i, next, eq); } + i = next; } } @@ -463,7 +481,8 @@ namespace smt { } std::ostream& theory_jobscheduler::display(std::ostream & out, job_resource const& jr) const { - return out << "r:" << jr.m_resource_id << " cap:" << jr.m_capacity << " load:" << jr.m_loadpct << " end:" << jr.m_end << "\n"; + return out << "r:" << jr.m_resource_id << " cap:" << jr.m_capacity << " load:" << jr.m_loadpct << " end:" << jr.m_end; + for (auto const& s : jr.m_properties) out << " " << s; out << "\n"; } std::ostream& theory_jobscheduler::display(std::ostream & out, job_info const& j) const { @@ -474,7 +493,8 @@ namespace smt { } std::ostream& theory_jobscheduler::display(std::ostream & out, res_available const& r) const { - return out << "[" << r.m_start << ":" << r.m_end << "] @ " << r.m_loadpct << "%\n"; + return out << "[" << r.m_start << ":" << r.m_end << "] @ " << r.m_loadpct << "%"; + for (auto const& s : r.m_properties) out << " " << s; out << "\n"; } std::ostream& theory_jobscheduler::display(std::ostream & out, res_info const& r) const { @@ -624,6 +644,7 @@ namespace smt { m_resources[r].m_jobs.push_back(j); } + void theory_jobscheduler::add_resource_available(unsigned r, unsigned max_loadpct, time_t start, time_t end, properties const& ps) { SASSERT(get_context().at_base_level()); SASSERT(1 <= max_loadpct && max_loadpct <= 100); @@ -684,8 +705,15 @@ namespace smt { for (job_resource const& jr : ji.m_resources) { unsigned r = jr.m_resource_id; res_info const& ri = m_resources[r]; - start_lb = std::min(start_lb, ri.m_available[0].m_start); - end_ub = std::max(end_ub, ri.m_available.back().m_end); + if (ri.m_available.empty()) continue; + unsigned idx = 0; + if (first_available(jr, ri, idx)) { + start_lb = std::min(start_lb, ri.m_available[idx].m_start); + } + idx = ri.m_available.size(); + if (last_available(jr, ri, idx)) { + end_ub = std::max(end_ub, ri.m_available[idx].m_end); + } } // start(j) >= start_lb @@ -722,24 +750,31 @@ namespace smt { // resource(j) = r => start(j) >= available[0].m_start void theory_jobscheduler::assert_first_start_time(unsigned j, unsigned r, literal eq) { + job_resource const& jr = get_job_resource(j, r); + unsigned idx = 0; + if (!first_available(jr, m_resources[r], idx)) return; vector& available = m_resources[r].m_available; - literal l2 = mk_ge(m_jobs[j].m_start, available[0].m_start); + literal l2 = mk_ge(m_jobs[j].m_start, available[idx].m_start); get_context().mk_th_axiom(get_id(), ~eq, l2); } // resource(j) = r => start(j) <= end[idx] || start[idx+1] <= start(j); - void theory_jobscheduler::assert_job_not_in_gap(unsigned j, unsigned r, unsigned idx, literal eq) { + void theory_jobscheduler::assert_job_not_in_gap(unsigned j, unsigned r, unsigned idx, unsigned idx1, literal eq) { + job_resource const& jr = get_job_resource(j, r); vector& available = m_resources[r].m_available; - literal l2 = mk_ge(m_jobs[j].m_start, available[idx + 1].m_start); + SASSERT(resource_available(jr, available[idx])); + literal l2 = mk_ge(m_jobs[j].m_start, available[idx1].m_start); literal l3 = mk_le(m_jobs[j].m_start, available[idx].m_end); get_context().mk_th_axiom(get_id(), ~eq, l2, l3); } // resource(j) = r => end(j) <= end[idx] || start[idx+1] <= start(j); - void theory_jobscheduler::assert_job_non_preemptable(unsigned j, unsigned r, unsigned idx, literal eq) { + void theory_jobscheduler::assert_job_non_preemptable(unsigned j, unsigned r, unsigned idx, unsigned idx1, literal eq) { vector& available = m_resources[r].m_available; + job_resource const& jr = get_job_resource(j, r); + SASSERT(resource_available(jr, available[idx])); literal l2 = mk_le(m_jobs[j].m_end, available[idx].m_end); - literal l3 = mk_ge(m_jobs[j].m_start, available[idx + 1].m_start); + literal l3 = mk_ge(m_jobs[j].m_start, available[idx1].m_start); get_context().mk_th_axiom(get_id(), ~eq, l2, l3); } @@ -868,6 +903,7 @@ namespace smt { SASSERT(cap > 0); for (; idx < available.size(); ++idx) { + if (!resource_available(jr, available[idx])) continue; start = std::max(start, available[idx].m_start); time_t end = available[idx].m_end; unsigned load_pct = available[idx].m_loadpct; @@ -941,6 +977,7 @@ namespace smt { unsigned j_load_pct = jr.m_loadpct; time_t cap = jr.m_capacity; for (unsigned idx = available.size(); idx-- > 0; ) { + if (!resource_available(jr, available[idx])) continue; start = available[idx].m_start; time_t end = available[idx].m_end; unsigned load_pct = available[idx].m_loadpct; @@ -958,6 +995,53 @@ namespace smt { } return false; } + + /** + * \brief check that job properties is a subset of resource properties. + * It assumes that both vectors are sorted. + */ + + bool theory_jobscheduler::resource_available(job_resource const& jr, res_available const& ra) const { + auto const& jps = jr.m_properties; + auto const& rps = ra.m_properties; + if (jps.size() > rps.size()) return false; + unsigned j = 0, i = 0; + for (; i < jps.size() && j < rps.size(); ) { + if (jps[i] == rps[j]) { + ++i; ++j; + } + else if (lt(rps[j], jps[i])) { + ++j; + } + else { + break; + } + } + return i == jps.size(); + } + + /** + * \brief minimal current resource available for job resource, includes idx. + */ + bool theory_jobscheduler::first_available(job_resource const& jr, res_info const& ri, unsigned& idx) const { + for (; idx < ri.m_available.size(); ++idx) { + if (resource_available(jr, ri.m_available[idx])) + return true; + } + return false; + } + + /** + * \brief maximal previous resource available for job resource, excludes idx. + */ + bool theory_jobscheduler::last_available(job_resource const& jr, res_info const& ri, unsigned& idx) const { + while (idx-- > 0) { + if (resource_available(jr, ri.m_available[idx])) + return true; + } + return false; + } + }; diff --git a/src/smt/theory_jobscheduler.h b/src/smt/theory_jobscheduler.h index 4fc5ba567..59c3b975d 100644 --- a/src/smt/theory_jobscheduler.h +++ b/src/smt/theory_jobscheduler.h @@ -31,7 +31,7 @@ namespace smt { class theory_jobscheduler : public theory { public: - typedef map properties; + typedef svector properties; protected: struct job_resource { @@ -175,6 +175,10 @@ namespace smt { time_t ect(unsigned j, unsigned r, time_t start); bool lst(unsigned j, unsigned r, time_t& t); + bool resource_available(job_resource const& jr, res_available const& ra) const; + bool first_available(job_resource const& jr, res_info const& ri, unsigned& idx) const; + bool last_available(job_resource const& jr, res_info const& ri, unsigned& idx) const; + time_t solve_for_start(unsigned load_pct, unsigned job_load_pct, time_t end, time_t cap); time_t solve_for_end(unsigned load_pct, unsigned job_load_pct, time_t start, time_t cap); time_t solve_for_capacity(unsigned load_pct, unsigned job_load_pct, time_t start, time_t end); @@ -198,8 +202,8 @@ namespace smt { void assert_last_end_time(unsigned j, unsigned r, job_resource const& jr, literal eq); void assert_last_start_time(unsigned j, unsigned r, literal eq); void assert_first_start_time(unsigned j, unsigned r, literal eq); - void assert_job_not_in_gap(unsigned j, unsigned r, unsigned idx, literal eq); - void assert_job_non_preemptable(unsigned j, unsigned r, unsigned idx, literal eq); + void assert_job_not_in_gap(unsigned j, unsigned r, unsigned idx, unsigned idx1, literal eq); + void assert_job_non_preemptable(unsigned j, unsigned r, unsigned idx, unsigned idx1, literal eq); void block_job_overlap(unsigned r, uint_set const& jobs, unsigned last_job);