update parser

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

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<builtin_name> & 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<symbol>& 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<symbol>& 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;
+}
+
 

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<symbol>& 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);

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;
         }