mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 21:38:44 +00:00
Code Activity

jscheduler

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-09-07 16:07:05 -07:00
parent 386cbade89 13abf5c6a6
commit 1e4681e0bc
18 changed files with 1251 additions and 395 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

95
src/api/api_datalog.cpp
View file

@ -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<reslimit> 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<symbol> 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<symbol> 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);
}
};

2
src/api/api_qe.cpp
View file

@ -1,5 +1,5 @@
/*++
Copyright (c) 2017 Arie Gurfinkel
Copyright (c) 2018 Microsoft Corporation
Module Name:

53
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");
@ -93,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;
@ -116,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;
@ -148,6 +163,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));
@ -155,7 +171,7 @@ void csp_decl_plugin::get_op_names(svector<builtin_name> & 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));
}
}
@ -233,15 +249,29 @@ 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);
}
bool csp_util::is_add_resource_available(expr * e, expr *& res, unsigned& loadpct, uint64_t& start, uint64_t& end) {
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, svector<symbol>& 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);
@ -252,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<symbol>& 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);
@ -267,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;
}
@ -275,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<symbol>& 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;
}

31
src/ast/csp_decl_plugin.h
View file

@ -75,13 +75,15 @@ 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
OP_JS_PROPERTIES // model declaration of a set of properties. Each property is a keyword.
};
class csp_decl_plugin : public decl_plugin {
@ -116,28 +118,31 @@ 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);
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_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_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, svector<symbol>& properites);
bool is_add_job_resource(expr * e, expr *& job, expr*& res, unsigned& loadpct, uint64_t& capacity, uint64_t& end, svector<symbol>& 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<symbol>& properties);
private:
unsigned job2id(expr* j);
unsigned resource2id(expr* r);
};

2
src/opt/opt_context.cpp
View file

@ -351,7 +351,7 @@ namespace opt {
void context::get_model_core(model_ref& mdl) {
mdl = m_model;
fix_model(mdl);
mdl->set_model_completion(true);
if (mdl) mdl->set_model_completion(true);
TRACE("opt", tout << *mdl;);
}

933
src/sat/ba_solver.cpp
View file

File diff suppressed because it is too large Load diff

62
src/sat/ba_solver.h
View file

@ -25,6 +25,7 @@ Revision History:
#include "sat/sat_solver.h"
#include "sat/sat_lookahead.h"
#include "sat/sat_unit_walk.h"
#include "sat/sat_big.h"
#include "util/scoped_ptr_vector.h"
#include "util/sorting_network.h"
@ -41,8 +42,11 @@ namespace sat {
unsigned m_num_bin_subsumes;
unsigned m_num_clause_subsumes;
unsigned m_num_pb_subsumes;
unsigned m_num_big_strengthenings;
unsigned m_num_cut;
unsigned m_num_gc;
unsigned m_num_overflow;
unsigned m_num_lemmas;
stats() { reset(); }
void reset() { memset(this, 0, sizeof(*this)); }
};
@ -57,6 +61,7 @@ namespace sat {
class card;
class pb;
class xr;
class pb_base;
class constraint {
protected:
@ -104,6 +109,7 @@ namespace sat {
card const& to_card() const;
pb const& to_pb() const;
xr const& to_xr() const;
pb_base const& to_pb_base() const;
bool is_card() const { return m_tag == card_t; }
bool is_pb() const { return m_tag == pb_t; }
bool is_xr() const { return m_tag == xr_t; }
@ -118,7 +124,7 @@ namespace sat {
};
friend std::ostream& operator<<(std::ostream& out, constraint const& c);
// base class for pb and cardinality constraints
class pb_base : public constraint {
protected:
@ -204,12 +210,18 @@ namespace sat {
protected:
struct ineq {
literal_vector m_lits;
svector<uint64_t> m_coeffs;
svector<wliteral> m_wlits;
uint64_t m_k;
ineq(): m_k(0) {}
void reset(uint64_t k) { m_lits.reset(); m_coeffs.reset(); m_k = k; }
void push(literal l, uint64_t c) { m_lits.push_back(l); m_coeffs.push_back(c); }
unsigned size() const { return m_wlits.size(); }
literal lit(unsigned i) const { return m_wlits[i].second; }
unsigned coeff(unsigned i) const { return m_wlits[i].first; }
void reset(uint64_t k) { m_wlits.reset(); m_k = k; }
void push(literal l, unsigned c) { m_wlits.push_back(wliteral(c,l)); }
unsigned bv_coeff(bool_var v) const;
void divide(unsigned c);
void weaken(unsigned i);
bool contains(literal l) const { for (auto wl : m_wlits) if (wl.second == l) return true; return false; }
};
solver* m_solver;
@ -273,7 +285,8 @@ namespace sat {
// simplification routines
svector<bool> m_visited;
svector<unsigned> m_visited;
unsigned m_visited_ts;
vector<svector<constraint*>> m_cnstr_use_list;
use_list m_clause_use_list;
bool m_simplify_change;
@ -292,9 +305,11 @@ namespace sat {
void binary_subsumption(card& c1, literal lit);
void clause_subsumption(card& c1, literal lit, clause_vector& removed_clauses);
void card_subsumption(card& c1, literal lit);
void mark_visited(literal l) { m_visited[l.index()] = true; }
void unmark_visited(literal l) { m_visited[l.index()] = false; }
bool is_marked(literal l) const { return m_visited[l.index()] != 0; }
void init_visited();
void mark_visited(literal l) { m_visited[l.index()] = m_visited_ts; }
void mark_visited(bool_var v) { mark_visited(literal(v, false)); }
bool is_visited(bool_var v) const { return is_visited(literal(v, false)); }
bool is_visited(literal l) const { return m_visited[l.index()] == m_visited_ts; }
unsigned get_num_unblocked_bin(literal l);
literal get_min_occurrence_literal(card const& c);
void init_use_lists();
@ -302,6 +317,9 @@ namespace sat {
unsigned set_non_external();
unsigned elim_pure();
bool elim_pure(literal lit);
void unit_strengthen();
void unit_strengthen(big& big, constraint& cs);
void unit_strengthen(big& big, pb_base& p);
void subsumption(constraint& c1);
void subsumption(card& c1);
void gc_half(char const* _method);
@ -396,10 +414,23 @@ namespace sat {
lbool eval(model const& m, pb const& p) const;
double get_reward(pb const& p, literal_occs_fun& occs) const;
// RoundingPb conflict resolution
lbool resolve_conflict_rs();
void round_to_one(ineq& ineq, bool_var v);
void round_to_one(bool_var v);
void divide(unsigned c);
void resolve_on(literal lit);
void resolve_with(ineq const& ineq);
void reset_marks(unsigned idx);
void mark_variables(ineq const& ineq);
void bail_resolve_conflict(unsigned idx);
// access solver
inline lbool value(bool_var v) const { return value(literal(v, false)); }
inline lbool value(literal lit) const { return m_lookahead ? m_lookahead->value(lit) : m_solver->value(lit); }
inline lbool value(model const& m, literal l) const { return l.sign() ? ~m[l.var()] : m[l.var()]; }
inline bool is_false(literal lit) const { return l_false == value(lit); }
inline unsigned lvl(literal lit) const { return m_lookahead || m_unit_walk ? 0 : m_solver->lvl(lit); }
inline unsigned lvl(bool_var v) const { return m_lookahead || m_unit_walk ? 0 : m_solver->lvl(v); }
@ -426,9 +457,11 @@ namespace sat {
mutable bool m_overflow;
void reset_active_var_set();
void normalize_active_coeffs();
bool test_and_set_active(bool_var v);
void inc_coeff(literal l, unsigned offset);
int64_t get_coeff(bool_var v) const;
uint64_t get_coeff(literal lit) const;
wliteral get_wliteral(bool_var v);
unsigned get_abs_coeff(bool_var v) const;
int get_int_coeff(bool_var v) const;
unsigned get_bound() const;
@ -436,6 +469,7 @@ namespace sat {
literal get_asserting_literal(literal conseq);
void process_antecedent(literal l, unsigned offset);
void process_antecedent(literal l) { process_antecedent(l, 1); }
void process_card(card& c, unsigned offset);
void cut();
bool create_asserting_lemma();
@ -446,6 +480,7 @@ namespace sat {
bool validate_conflict(pb const& p) const;
bool validate_assign(literal_vector const& lits, literal lit);
bool validate_lemma();
bool validate_ineq(ineq const& ineq) const;
bool validate_unit_propagation(card const& c, literal alit) const;
bool validate_unit_propagation(pb const& p, literal alit) const;
bool validate_unit_propagation(pb const& p, literal_vector const& r, literal alit) const;
@ -464,12 +499,17 @@ namespace sat {
ineq m_A, m_B, m_C;
void active2pb(ineq& p);
constraint* active2lemma();
constraint* active2constraint();
constraint* active2card();
void active2wlits();
void active2wlits(svector<wliteral>& wlits);
void justification2pb(justification const& j, literal lit, unsigned offset, ineq& p);
void constraint2pb(constraint& cnstr, literal lit, unsigned offset, ineq& p);
bool validate_resolvent();
unsigned get_coeff(ineq const& pb, literal lit);
void display(std::ostream& out, ineq& p, bool values = false) const;
void display(std::ostream& out, ineq const& p, bool values = false) const;
void display(std::ostream& out, card const& c, bool values) const;
void display(std::ostream& out, pb const& p, bool values) const;
void display(std::ostream& out, xr const& c, bool values) const;

34
src/sat/sat_big.cpp
View file

@ -22,7 +22,8 @@ Revision History:
namespace sat {
big::big(random_gen& rand):
m_rand(rand) {
m_rand(rand),
m_include_cardinality(false) {
}
void big::init(solver& s, bool learned) {
@ -42,22 +43,22 @@ namespace sat {
m_roots[v.index()] = false;
edges.push_back(v);
}
#if 0
if (w.is_ext_constraint() &&
if (m_include_cardinality &&
w.is_ext_constraint() &&
s.m_ext &&
learned &&
learned && // cannot (yet) observe if ext constraints are learned
!seen_idx.contains(w.get_ext_constraint_idx()) &&
s.m_ext->is_extended_binary(w.get_ext_constraint_idx(), r)) {
seen_idx.insert(w.get_ext_constraint_idx(), true);
for (unsigned i = 0; i < r.size(); ++i) {
literal u = r[i];
for (unsigned j = i + 1; j < r.size(); ++j) {
// add ~r[i] -> r[j]
literal v = r[j];
literal u = ~r[j];
for (unsigned i = 0; i < std::min(4u, r.size()); ++i) {
shuffle<literal>(r.size(), r.c_ptr(), m_rand);
literal u = r[0];
for (unsigned j = 1; j < r.size(); ++j) {
literal v = ~r[j];
// add u -> v
m_roots[v.index()] = false;
m_dag[u.index()].push_back(v);
// add ~r[j] -> r[i]
// add ~v -> ~u
v.neg();
u.neg();
m_roots[u.index()] = false;
@ -65,7 +66,6 @@ namespace sat {
}
}
}
#endif
}
}
done_adding_edges();
@ -268,6 +268,16 @@ namespace sat {
return out << v;
}
literal big::get_root(literal l) {
literal r = l;
do {
l = r;
r = m_root[l.index()];
}
while (r != l);
return r;
}
void big::display(std::ostream& out) const {
unsigned idx = 0;
for (auto& next : m_dag) {

6
src/sat/sat_big.h
View file

@ -34,6 +34,7 @@ namespace sat {
svector<int> m_left, m_right;
literal_vector m_root, m_parent;
bool m_learned;
bool m_include_cardinality;
svector<std::pair<literal, literal>> m_del_bin;
@ -54,6 +55,9 @@ namespace sat {
// static svector<std::pair<literal, literal>> s_del_bin;
big(random_gen& rand);
void set_include_cardinality(bool f) { m_include_cardinality = f; }
/**
\brief initialize a BIG from a solver.
*/
@ -77,7 +81,7 @@ namespace sat {
int get_left(literal l) const { return m_left[l.index()]; }
int get_right(literal l) const { return m_right[l.index()]; }
literal get_parent(literal l) const { return m_parent[l.index()]; }
literal get_root(literal l) const { return m_root[l.index()]; }
literal get_root(literal l);
bool reaches(literal u, literal v) const { return m_left[u.index()] < m_left[v.index()] && m_right[v.index()] < m_right[u.index()]; }
bool connected(literal u, literal v) const { return reaches(u, v) || reaches(~v, ~u); }
void display(std::ostream& out) const;

16
src/sat/sat_config.cpp
View file

@ -196,6 +196,22 @@ namespace sat {
else
throw sat_param_exception("invalid PB solver: solver, totalizer, circuit, sorting, segmented");
s = p.pb_resolve();
if (s == "cardinality")
m_pb_resolve = PB_CARDINALITY;
else if (s == "rounding")
m_pb_resolve = PB_ROUNDING;
else
throw sat_param_exception("invalid PB resolve: 'cardinality' or 'rounding' expected");
s = p.pb_lemma_format();
if (s == "cardinality")
m_pb_lemma_format = PB_LEMMA_CARDINALITY;
else if (s == "pb")
m_pb_lemma_format = PB_LEMMA_PB;
else
throw sat_param_exception("invalid PB lemma format: 'cardinality' or 'pb' expected");
m_card_solver = p.cardinality_solver();
sat_simplifier_params sp(_p);

12
src/sat/sat_config.h
View file

@ -60,6 +60,16 @@ namespace sat {
PB_SEGMENTED
};
enum pb_resolve {
PB_CARDINALITY,
PB_ROUNDING
};
enum pb_lemma_format {
PB_LEMMA_CARDINALITY,
PB_LEMMA_PB
};
enum reward_t {
ternary_reward,
unit_literal_reward,
@ -148,6 +158,8 @@ namespace sat {
pb_solver m_pb_solver;
bool m_card_solver;
pb_resolve m_pb_resolve;
pb_lemma_format m_pb_lemma_format;
// branching heuristic settings.
branching_heuristic m_branching_heuristic;

4
src/sat/sat_params.pyg
View file

@ -42,8 +42,10 @@ def_module_params('sat',
('drat.check_sat', BOOL, False, 'build up internal trace, check satisfying model'),
('cardinality.solver', BOOL, True, 'use cardinality solver'),
('pb.solver', SYMBOL, 'solver', 'method for handling Pseudo-Boolean constraints: circuit (arithmetical circuit), sorting (sorting circuit), totalizer (use totalizer encoding), solver (use native solver)'),
('xor.solver', BOOL, False, 'use xor solver'),
('xor.solver', BOOL, False, 'use xor solver'),
('cardinality.encoding', SYMBOL, 'grouped', 'encoding used for at-most-k constraints: grouped, bimander, ordered, unate, circuit'),
('pb.resolve', SYMBOL, 'cardinality', 'resolution strategy for boolean algebra solver: cardinality, rounding'),
('pb.lemma_format', SYMBOL, 'cardinality', 'generate either cardinality or pb lemmas'),
('local_search', BOOL, False, 'use local search instead of CDCL'),
('local_search_threads', UINT, 0, 'number of local search threads to find satisfiable solution'),
('local_search_mode', SYMBOL, 'wsat', 'local search algorithm, either default wsat or qsat'),

1
src/sat/sat_scc.h
View file

@ -60,7 +60,6 @@ namespace sat {
void ensure_big(bool learned) { m_big.ensure_big(m_solver, learned); }
int get_left(literal l) const { return m_big.get_left(l); }
int get_right(literal l) const { return m_big.get_right(l); }
literal get_root(literal l) const { return m_big.get_root(l); }
bool connected(literal u, literal v) const { return m_big.connected(u, v); }
};
};

6
src/sat/sat_solver.cpp
View file

@ -340,12 +340,6 @@ namespace sat {
}
void solver::mk_bin_clause(literal l1, literal l2, bool learned) {
#if 0
if ((l1.var() == 2039 || l2.var() == 2039) &&
(l1.var() == 27042 || l2.var() == 27042)) {
IF_VERBOSE(1, verbose_stream() << "mk_bin: " << l1 << " " << l2 << " " << learned << "\n");
}
#endif
if (find_binary_watch(get_wlist(~l1), ~l2)) {
assign(l1, justification());
return;

1
src/sat/tactic/goal2sat.cpp
View file

@ -82,6 +82,7 @@ struct goal2sat::imp {
m_is_lemma(false) {
updt_params(p);
m_true = sat::null_bool_var;
mk_true();
}
void updt_params(params_ref const & p) {

351
src/smt/theory_jobscheduler.cpp
View file

@ -19,13 +19,9 @@ TODO:
- arithmetic interface
- propagation queue:
- register theory variables for catching when jobs are bound to resources
- register bounds on start times to propagate energy constraints
- more general registration mechanism for arithmetic theory.
- csp_cmds
- use predicates for add_ feature set? Closed world.
set up environment in one swoop.
- interact with opt
- interact with opt
- jobs without resources
- complain or add dummy resource? At which level.
@ -37,6 +33,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
@ -86,6 +83,13 @@ 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;
rational r;
@ -96,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 {
@ -113,15 +119,57 @@ namespace smt {
throw default_exception(strm.str());
}
void theory_jobscheduler::new_eq_eh(theory_var v1, theory_var v2) {
enode* e1 = get_enode(v1);
enode* e2 = get_enode(v2);
enode* root = e1->get_root();
unsigned r;
if (u.is_resource(root->get_owner(), r)) {
enode* next = e1;
do {
unsigned j;
if (u.is_job2resource(next->get_owner(), j) && !m_jobs[j].m_is_bound) {
m_bound_jobs.push_back(j);
m_jobs[j].m_is_bound = true;
}
next = next->get_next();
}
while (e1 != next);
}
}
void theory_jobscheduler::new_diseq_eh(theory_var v1, theory_var v2) {
}
void theory_jobscheduler::push_scope_eh() {
scope s;
s.m_bound_jobs_lim = m_bound_jobs.size();
s.m_bound_qhead = m_bound_qhead;
m_scopes.push_back(s);
}
void theory_jobscheduler::pop_scope_eh(unsigned num_scopes) {
unsigned new_lvl = m_scopes.size() - num_scopes;
scope const& s = m_scopes[new_lvl];
for (unsigned i = s.m_bound_jobs_lim; i < m_bound_jobs.size(); ++i) {
unsigned j = m_bound_jobs[i];
m_jobs[j].m_is_bound = false;
}
m_bound_jobs.shrink(s.m_bound_jobs_lim);
m_bound_qhead = s.m_bound_qhead;
m_scopes.shrink(new_lvl);
}
final_check_status theory_jobscheduler::final_check_eh() {
TRACE("csp", tout << "\n";);
bool blocked = false;
for (unsigned j = 0; j < m_jobs.size(); ++j) {
if (split_job2resource(j)) {
return FC_CONTINUE;
}
}
for (unsigned r = 0; r < m_resources.size(); ++r) {
if (constrain_resource_energy(r)) {
blocked = true;
@ -138,7 +186,7 @@ namespace smt {
}
bool theory_jobscheduler::can_propagate() {
return false;
return m_bound_qhead < m_bound_jobs.size();
}
literal theory_jobscheduler::mk_literal(expr * e) {
@ -227,6 +275,9 @@ namespace smt {
/**
* r = resource(j) & start(j) >= slb => end(j) >= ect(j, r, slb)
*
* note: not used so far
* note: subsumed by constrain_end_time_interval used in final-check
*/
void theory_jobscheduler::propagate_end_time(unsigned j, unsigned r) {
time_t slb = est(j);
@ -263,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<res_available>& 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;
@ -317,9 +371,6 @@ namespace smt {
return true;
}
void theory_jobscheduler::propagate_resource_energy(unsigned r) {
}
/**
* Ensure that job overlaps don't exceed available energy
@ -386,23 +437,52 @@ namespace smt {
}
void theory_jobscheduler::propagate() {
return;
for (unsigned j = 0; j < m_jobs.size(); ++j) {
while (m_bound_qhead < m_bound_jobs.size()) {
unsigned j = m_bound_jobs[m_bound_qhead++];
unsigned r = 0;
job_info const& ji = m_jobs[j];
unsigned r = resource(j);
propagate_end_time(j, r);
VERIFY(u.is_resource(ji.m_job2resource->get_root()->get_owner(), r));
TRACE("csp", tout << "job: " << j << " resource: " << r << "\n";);
propagate_job2resource(j, r);
}
for (unsigned r = 0; r < m_resources.size(); ++r) {
// TBD: check energy constraints on resources.
}
void theory_jobscheduler::propagate_job2resource(unsigned j, unsigned r) {
job_info const& ji = m_jobs[j];
res_info const& ri = m_resources[r];
job_resource const& jr = get_job_resource(j, r);
literal eq = mk_eq_lit(ji.m_job2resource, ri.m_resource);
assert_last_end_time(j, r, jr, eq);
assert_last_start_time(j, r, eq);
assert_first_start_time(j, r, eq);
vector<res_available> const& available = ri.m_available;
// 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, next, eq);
}
i = next;
}
}
theory_jobscheduler::theory_jobscheduler(ast_manager& m):
theory(m.get_family_id("csp")), m(m), u(m), a(m) {
theory(m.get_family_id("csp")),
m(m),
u(m),
a(m),
m_bound_qhead(0) {
}
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 {
@ -413,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 {
@ -548,7 +629,7 @@ namespace smt {
app_ref start(u.mk_start(j), m);
app_ref end(u.mk_end(j), m);
app_ref res(u.mk_job2resource(j), m);
if (!ctx.e_internalized(job)) ctx.internalize(job, false);
if (!ctx.e_internalized(job)) ctx.internalize(job, false);
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);
@ -563,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);
@ -574,37 +656,42 @@ 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));
}
/*
* Initialze the state based on the set of jobs and resources added.
* For each job j, with possible resources r1, ..., r_n assert
* resource(j) = r_1 || resource(j) = r_2 || ... || resource(j) = r_n
* For each job and resource r with deadline end(j,r) assert
* resource(j) = r => end(j) <= end(j,r)
*
* Ensure that the availability slots for each resource is sorted by time.
*
* For each resource j:
* est(j) <= start(j) <= end(j) <= lct(j)
*
* possible strengthenings:
* - start(j) <= lst(j)
* - start(j) + min_completion_time(j) <= end(j)
* - start(j) + max_completion_time(j) >= end(j)
*
* makespan constraints?
*
*/
void theory_jobscheduler::add_done() {
TRACE("csp", tout << "add-done begin\n";);
context & ctx = get_context();
// sort availability intervals
for (unsigned r = 0; r < m_resources.size(); ++r) {
res_info& ri = m_resources[r];
for (res_info& ri : m_resources) {
vector<res_available>& available = ri.m_available;
res_available::compare cmp;
std::sort(available.begin(), available.end(), cmp);
}
expr_ref fml(m);
literal lit, l1, l2, l3;
literal lit;
for (unsigned j = 0; j < m_jobs.size(); ++j) {
job_info const& ji = m_jobs[j];
literal_vector disj;
for (job_info const& ji : m_jobs) {
if (ji.m_resources.empty()) {
throw default_exception("every job should be associated with at least one resource");
}
@ -614,23 +701,24 @@ namespace smt {
ctx.mk_th_axiom(get_id(), 1, &lit);
time_t start_lb = std::numeric_limits<time_t>::max();
time_t end_ub = 0;
time_t runtime_lb = std::numeric_limits<time_t>::max();
time_t end_ub = 0, runtime_ub = 0;
for (job_resource const& jr : ji.m_resources) {
// resource(j) = r => end(j) <= end(j, r)
// resource(j) = r => start(j) <= lst(j, r, end(j, r))
unsigned r = jr.m_resource_id;
res_info const& ri = m_resources[r];
enode* j2r = m_jobs[j].m_job2resource;
literal eq = mk_eq_lit(j2r, ri.m_resource);
assert_last_end_time(j, r, jr, eq);
assert_last_start_time(j, r, eq);
disj.push_back(eq);
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);
}
runtime_lb = std::min(runtime_lb, jr.m_capacity);
// TBD: more accurate estimates for runtime_lb based on gaps
// TBD: correct estimate of runtime_ub taking gaps into account.
}
// resource(j) = r1 || ... || resource(j) = r_n
ctx.mk_th_axiom(get_id(), disj.size(), disj.c_ptr());
// start(j) >= start_lb
lit = mk_ge(ji.m_start, start_lb);
@ -639,45 +727,22 @@ namespace smt {
// end(j) <= end_ub
lit = mk_le(ji.m_end, end_ub);
ctx.mk_th_axiom(get_id(), 1, &lit);
}
for (unsigned r = 0; r < m_resources.size(); ++r) {
res_info& ri = m_resources[r];
vector<res_available>& available = ri.m_available;
if (available.empty()) continue;
enode* res = m_resources[r].m_resource;
for (unsigned j : ri.m_jobs) {
// resource(j) == r => start(j) >= available[0].m_start;
enode* j2r = m_jobs[j].m_job2resource;
assert_first_start_time(j, r, mk_eq_lit(j2r, res));
}
for (unsigned i = 0; i + 1 < available.size(); ++i) {
if (available[i].m_end > available[i + 1].m_start) {
throw default_exception("availability intervals should be disjoint");
}
for (unsigned j : ri.m_jobs) {
// jobs start within an interval.
// resource(j) == r => start(j) <= available[i].m_end || start(j) >= available[i + 1].m_start;
enode* j2r = m_jobs[j].m_job2resource;
literal eq = mk_eq_lit(j2r, res);
assert_job_not_in_gap(j, r, i, eq);
// if job is not pre-emptable, start and end have to align within contiguous interval.
// resource(j) == r => end(j) <= available[i].m_end || start(j) >= available[i + 1].m_start
if (!m_jobs[j].m_is_preemptable && available[i].m_end + 1 < available[i+1].m_start) {
assert_job_non_preemptable(j, r, i, eq);
}
}
}
}
// start(j) + runtime_lb <= end(j)
// end(j) <= start(j) + runtime_ub
}
TRACE("csp", tout << "add-done end\n";);
}
// resource(j) = r => end(j) <= end(j, r)
void theory_jobscheduler::assert_last_end_time(unsigned j, unsigned r, job_resource const& jr, literal eq) {
job_info const& ji = m_jobs[j];
literal l2 = mk_le(ji.m_end, jr.m_end);
get_context().mk_th_axiom(get_id(), ~eq, l2);
}
// resource(j) = r => start(j) <= lst(j, r, end(j, r))
void theory_jobscheduler::assert_last_start_time(unsigned j, unsigned r, literal eq) {
context& ctx = get_context();
time_t t;
@ -690,27 +755,70 @@ 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<res_available>& 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);
}
void theory_jobscheduler::assert_job_not_in_gap(unsigned j, unsigned r, unsigned idx, literal eq) {
// 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, unsigned idx1, literal eq) {
job_resource const& jr = get_job_resource(j, r);
vector<res_available>& 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);
}
void theory_jobscheduler::assert_job_non_preemptable(unsigned j, unsigned r, unsigned idx, literal eq) {
// 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, unsigned idx1, literal eq) {
vector<res_available>& 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);
}
}
/**
* bind a job to one of the resources it can run on.
*/
bool theory_jobscheduler::split_job2resource(unsigned j) {
job_info const& ji = m_jobs[j];
context& ctx = get_context();
if (ji.m_is_bound) return false;
auto const& jrs = ji.m_resources;
for (job_resource const& jr : jrs) {
unsigned r = jr.m_resource_id;
res_info const& ri = m_resources[r];
enode* e1 = ji.m_job2resource;
enode* e2 = ri.m_resource;
if (ctx.is_diseq(e1, e2))
continue;
literal eq = mk_eq_lit(e1, e2);
if (ctx.get_assignment(eq) != l_false) {
ctx.mark_as_relevant(eq);
if (assume_eq(e1, e2)) {
return true;
}
}
}
literal_vector lits;
for (job_resource const& jr : jrs) {
unsigned r = jr.m_resource_id;
res_info const& ri = m_resources[r];
enode* e1 = ji.m_job2resource;
enode* e2 = ri.m_resource;
lits.push_back(mk_eq_lit(e1, e2));
}
ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
return true;
}
/**
* check that each job is run on some resource according to
@ -757,17 +865,21 @@ namespace smt {
return ji.m_resources[ji.m_resource2index[r]];
}
/**
* find idx, if any, such that t is within the time interval of available[idx]
*/
bool theory_jobscheduler::resource_available(unsigned r, time_t t, unsigned& idx) {
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) {
@ -781,7 +893,6 @@ namespace smt {
return false;
}
/**
* compute earliest completion time for job j on resource r starting at time start.
*/
@ -799,20 +910,14 @@ 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;
time_t delta = solve_for_capacity(load_pct, j_load_pct, start, end);
TRACE("csp", tout << "delta: " << delta << " capacity: " << cap << " load " << load_pct << " jload: " << j_load_pct << " start: " << start << " end " << end << "\n";);
TRACE("csp", tout << "delta: " << delta << " capacity: " << cap << " load "
<< load_pct << " jload: " << j_load_pct << " start: " << start << " end " << end << "\n";);
if (delta > cap) {
//
// solve for end:
// cap = load * (end - start + 1)
// <=>
// cap / load = (end - start + 1)
// <=>
// end = cap / load + start - 1
//
end = solve_for_end(load_pct, j_load_pct, start, cap);
cap = 0;
}
@ -826,6 +931,9 @@ namespace smt {
return std::numeric_limits<time_t>::max();
}
/**
* find end, such that cap = (load / job_load_pct) * (end - start + 1)
*/
time_t theory_jobscheduler::solve_for_end(unsigned load_pct, unsigned job_load_pct, time_t start, time_t cap) {
SASSERT(load_pct > 0);
SASSERT(job_load_pct > 0);
@ -840,6 +948,9 @@ namespace smt {
return (load * (start - 1) + cap * job_load_pct) / load;
}
/**
* find start, such that cap = (load / job_load_pct) * (end - start + 1)
*/
time_t theory_jobscheduler::solve_for_start(unsigned load_pct, unsigned job_load_pct, time_t end, time_t cap) {
SASSERT(load_pct > 0);
SASSERT(job_load_pct > 0);
@ -854,6 +965,9 @@ namespace smt {
return (load * (end + 1) - cap * job_load_pct) / load;
}
/**
* find cap, such that cap = (load / job_load_pct) * (end - start + 1)
*/
time_t theory_jobscheduler::solve_for_capacity(unsigned load_pct, unsigned job_load_pct, time_t start, time_t end) {
SASSERT(job_load_pct > 0);
unsigned load = std::min(load_pct, job_load_pct);
@ -870,6 +984,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;
@ -882,12 +997,58 @@ namespace smt {
cap -= delta;
}
if (cap == 0) {
std::cout << "start " << start << "\n";
return true;
}
}
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;
}
};

30
src/smt/theory_jobscheduler.h
View file

@ -31,7 +31,7 @@ namespace smt {
class theory_jobscheduler : public theory {
public:
typedef map<symbol, double, symbol_hash_proc, symbol_eq_proc> properties;
typedef svector<symbol> properties;
protected:
struct job_resource {
@ -64,7 +64,8 @@ namespace smt {
enode* m_start;
enode* m_end;
enode* m_job2resource;
job_info(): m_is_preemptable(false), m_job(nullptr), m_start(nullptr), m_end(nullptr), m_job2resource(nullptr) {}
bool m_is_bound;
job_info(): m_is_preemptable(false), m_job(nullptr), m_start(nullptr), m_end(nullptr), m_job2resource(nullptr), m_is_bound(false) {}
};
struct res_available {
@ -90,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;
@ -98,6 +100,13 @@ namespace smt {
arith_util a;
vector<job_info> m_jobs;
vector<res_info> m_resources;
unsigned_vector m_bound_jobs;
unsigned m_bound_qhead;
struct scope {
unsigned m_bound_jobs_lim;
unsigned m_bound_qhead;
};
svector<scope> m_scopes;
protected:
@ -109,9 +118,9 @@ namespace smt {
void assign_eh(bool_var v, bool is_true) override {}
void new_eq_eh(theory_var v1, theory_var v2) override {}
void new_eq_eh(theory_var v1, theory_var v2) override;
void new_diseq_eh(theory_var v1, theory_var v2) override {}
void new_diseq_eh(theory_var v1, theory_var v2) override;
void push_scope_eh() override;
@ -166,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);
@ -179,17 +192,18 @@ namespace smt {
// propagation
void propagate_end_time(unsigned j, unsigned r);
void propagate_resource_energy(unsigned r);
void propagate_job2resource(unsigned j, unsigned r);
// final check constraints
bool constrain_end_time_interval(unsigned j, unsigned r);
bool constrain_resource_energy(unsigned r);
bool split_job2resource(unsigned j);
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);

7
src/util/uint_set.h
View file

@ -269,10 +269,9 @@ public:
void remove(unsigned v) {
if (contains(v)) {
m_in_set[v] = false;
unsigned i = 0;
for (i = 0; i < m_set.size() && m_set[i] != v; ++i)
;
SASSERT(i < m_set.size());
unsigned i = m_set.size();
for (; i > 0 && m_set[--i] != v; ) ;
SASSERT(m_set[i] == v);
m_set[i] = m_set.back();
m_set.pop_back();
}