From 77e43404703f2bc37f4b7579c7f56905d4ab2eca Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 14 Oct 2018 13:06:09 -0700 Subject: [PATCH] update parser Signed-off-by: Nikolaj Bjorner --- src/ast/csp_decl_plugin.cpp | 55 +++++++++++++++++++++++++++++++-- src/ast/csp_decl_plugin.h | 16 +++++++++- src/parsers/smt2/smt2parser.cpp | 6 ---- 3 files changed, 68 insertions(+), 9 deletions(-) diff --git a/src/ast/csp_decl_plugin.cpp b/src/ast/csp_decl_plugin.cpp index 27feadc6d..9cdd20376 100644 --- a/src/ast/csp_decl_plugin.cpp +++ b/src/ast/csp_decl_plugin.cpp @@ -119,7 +119,8 @@ func_decl * csp_decl_plugin::mk_func_decl( rng = m_alist_sort; break; case OP_JS_JOB_PREEMPTABLE: - if (arity != 1 || domain[0] != m_job_sort) m_manager->raise_exception("set-preemptable expects one argument, which is a job"); + if (arity != 1 || domain[0] != m_job_sort) + m_manager->raise_exception("set-preemptable expects one argument, which is a job"); name = symbol("set-preemptable"); rng = m_alist_sort; break; @@ -131,6 +132,22 @@ func_decl * csp_decl_plugin::mk_func_decl( name = symbol("js-properties"); rng = m_alist_sort; break; + case OP_JS_JOB_GOAL: + if (arity != 1 || domain[0] != m_job_sort) + m_manager->raise_exception("add-job-goal expects one argument, which is a job"); + if (num_parameters != 2 || !parameters[0].is_symbol() || !parameters[1].is_int()) + m_manager->raise_exception("add-job-goal expects one symbol and one integer parameter"); + name = symbol("add-job-goal"); + rng = m_alist_sort; + break; + case OP_JS_OBJECTIVE: + if (arity != 0) + m_manager->raise_exception("add-optimization-objective expects no arguments"); + if (num_parameters != 1 || !parameters[0].is_symbol()) + m_manager->raise_exception("add-optimization-objective expects one symbol parameter"); + name = symbol("add-optimization-objective"); + rng = m_alist_sort; + break; default: UNREACHABLE(); return nullptr; @@ -172,6 +189,8 @@ void csp_decl_plugin::get_op_names(svector & op_names, symbol cons 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)); + op_names.push_back(builtin_name("add-job-goal", OP_JS_JOB_GOAL)); + op_names.push_back(builtin_name("add-optimization-objective", OP_JS_OBJECTIVE)); } } @@ -309,7 +328,8 @@ bool csp_util::is_set_preemptable(expr* e, expr *& job) { } bool csp_util::is_js_properties(expr* e, svector& properties) { - if (!is_app_of(e, m_fid, OP_JS_PROPERTIES)) return false; + 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()); @@ -317,4 +337,35 @@ bool csp_util::is_js_properties(expr* e, svector& properties) { return true; } +bool csp_util::is_job_goal(expr* e, js_job_goal& goal, unsigned& level, expr*& job) { + if (!is_app_of(e, m_fid, OP_JS_JOB_GOAL)) + return false; + SASSERT(2 == to_app(e)->get_decl()->get_num_parameters()); + SASSERT(1 == to_app(e)->get_num_args()); + symbol g = to_app(e)->get_decl()->get_parameter(0).get_symbol(); + level = to_app(e)->get_decl()->get_parameter(1).get_int(); + if (g == ":earliest-end-time" || g == "earliest-end-time") + goal = JS_JOB_GOAL_EARLIEST_END_TIME; + else if (g == ":latest-start-time" || g == "latest-start-time") + goal = JS_JOB_GOAL_LATEST_START_TIME; + else + return false; + job = to_app(e)->get_arg(0); + return true; +} + +bool csp_util::is_objective(expr* e, js_optimization_objective& objective) { + if (!is_app_of(e, m_fid, OP_JS_OBJECTIVE)) + return false; + SASSERT(1 == to_app(e)->get_decl()->get_num_parameters()); + symbol obj = to_app(e)->get_decl()->get_parameter(0).get_symbol(); + if (obj == ":duration" || obj == "duration") + objective = JS_OBJECTIVE_DURATION; + else if (obj == ":priority" || obj == "priority") + objective = JS_OBJECTIVE_PRIORITY; + else + return false; + return true; +} + diff --git a/src/ast/csp_decl_plugin.h b/src/ast/csp_decl_plugin.h index 8d6ad56fa..05d6bfa7e 100644 --- a/src/ast/csp_decl_plugin.h +++ b/src/ast/csp_decl_plugin.h @@ -83,7 +83,19 @@ enum js_op_kind { 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. + OP_JS_PROPERTIES, // model declaration of a set of properties. Each property is a keyword. + OP_JS_JOB_GOAL, // job goal objective :earliest-end-time or :latest-start-time + OP_JS_OBJECTIVE // duration or completion-time +}; + +enum js_job_goal { + JS_JOB_GOAL_EARLIEST_END_TIME, + JS_JOB_GOAL_LATEST_START_TIME +}; + +enum js_optimization_objective { + JS_OBJECTIVE_DURATION, + JS_OBJECTIVE_PRIORITY }; class csp_decl_plugin : public decl_plugin { @@ -140,6 +152,8 @@ public: 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); + bool is_job_goal(expr* e, js_job_goal& goal, unsigned& level, expr*& job); + bool is_objective(expr* e, js_optimization_objective& objective); private: unsigned job2id(expr* j); diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp index d1b4847cc..fe7c048a9 100644 --- a/src/parsers/smt2/smt2parser.cpp +++ b/src/parsers/smt2/smt2parser.cpp @@ -625,8 +625,6 @@ namespace smt2 { args.push_back(u); next(); } - if (args.empty()) - throw parser_exception("invalid indexed sort, index expected"); sort * r = d->instantiate(pm(), args.size(), args.c_ptr()); if (r == nullptr) throw parser_exception("invalid sort application"); @@ -1520,7 +1518,6 @@ namespace smt2 { check_identifier("invalid indexed identifier, symbol expected"); symbol r = curr_id(); next(); - unsigned num_indices = 0; while (!curr_is_rparen()) { if (curr_is_int()) { if (!curr_numeral().is_unsigned()) { @@ -1545,10 +1542,7 @@ namespace smt2 { else { throw parser_exception("invalid indexed identifier, integer, identifier or '(' expected"); } - num_indices++; } - if (num_indices == 0) - throw parser_exception("invalid indexed identifier, index expected"); next(); return r; }