add index option to 'eval' command for box objectives. Issue #955

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

src/ast/rewriter/seq_rewriter.cpp

@@ -12,6 +12,7 @@ Abstract:
 Author:
 
     Nikolaj Bjorner (nbjorner) 2015-12-5
+    Murphy Berzish 2017-02-21
 
 Notes:
 
@@ -514,30 +515,56 @@ br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& resu
     bool constantPos = m_autil.is_numeral(b, pos);
     bool constantLen = m_autil.is_numeral(c, len);
 
-    // case 1: pos<0 or len<0
+    // case 1: pos<0 or len<=0
     // rewrite to ""
-    if ( (constantPos && pos.is_neg()) || (constantLen && len.is_neg()) ) {
+    if ( (constantPos && pos.is_neg()) || (constantLen && !len.is_pos()) ) {
         result = m_util.str.mk_empty(m().get_sort(a));
         return BR_DONE;
     }
     // case 1.1: pos >= length(base)
     // rewrite to ""
-    if (constantBase && constantPos && pos.get_unsigned() >= s.length()) {
+    if (constantBase && constantPos && pos >= rational(s.length())) {
         result = m_util.str.mk_empty(m().get_sort(a));
         return BR_DONE;
     }
 
+    constantPos &= pos.is_unsigned();
+    constantLen &= len.is_unsigned();
+
     if (constantBase && constantPos && constantLen) {
         if (pos.get_unsigned() + len.get_unsigned() >= s.length()) {
             // case 2: pos+len goes past the end of the string
             unsigned _len = s.length() - pos.get_unsigned() + 1;
             result = m_util.str.mk_string(s.extract(pos.get_unsigned(), _len));
-            return BR_DONE;
         } else {
             // case 3: pos+len still within string
             result = m_util.str.mk_string(s.extract(pos.get_unsigned(), len.get_unsigned()));
-            return BR_DONE;
         }
+        return BR_DONE;
+    }
+
+    if (constantPos && constantLen) {
+        unsigned _pos = pos.get_unsigned();
+        unsigned _len = len.get_unsigned();
+        SASSERT(_len > 0);
+        expr_ref_vector as(m()), bs(m());
+        m_util.str.get_concat(a, as);
+        for (unsigned i = 0; i < as.size() && _len > 0; ++i) {
+            if (m_util.str.is_unit(as[i].get())) {
+                if (_pos == 0) {
+                    bs.push_back(as[i].get());
+                    --_len;
+                }
+                else {
+                    --_pos;
+                }
+            }              
+            else {
+                return BR_FAILED;
+            }
+        }
+        result = m_util.str.mk_concat(bs);
+        return BR_DONE;
     }
 
     return BR_FAILED;
@@ -640,10 +667,33 @@ br_status seq_rewriter::mk_seq_at(expr* a, expr* b, expr_ref& result) {
             result = m_util.str.mk_empty(m().get_sort(a));
             return BR_DONE;
         }
-        if (m_util.str.is_string(a, c) && r.is_unsigned() && r < rational(c.length())) {
+        if (m_util.str.is_string(a, c)) {
-            result = m_util.str.mk_string(c.extract(r.get_unsigned(), 1));
+            if (r.is_unsigned() && r < rational(c.length())) {
+                result = m_util.str.mk_string(c.extract(r.get_unsigned(), 1));
+            }
+            else {
+                result = m_util.str.mk_empty(m().get_sort(a));
+            }
             return BR_DONE;
-        } 
+        }
+        if (r.is_unsigned()) {
+            len = r.get_unsigned();
+            expr_ref_vector as(m());
+            m_util.str.get_concat(a, as);
+            for (unsigned i = 0; i < as.size(); ++i) {
+                if (m_util.str.is_unit(as[i].get())) {
+                    if (len == 0) {
+                        result = as[i].get();
+                        return BR_DONE;
+                    }
+                    --len;
+                }         
+                else {
+                    return BR_FAILED;
+                }
+            }
+        }
+        
     }
     return BR_FAILED;
 }

src/cmd_context/eval_cmd.cpp

@@ -38,6 +38,7 @@ public:
     virtual void init_pdescrs(cmd_context & ctx, param_descrs & p) {
         model_evaluator::get_param_descrs(p);
         insert_timeout(p);
+        p.insert("model_index", CPK_UINT, "(default: 0) index of model from box optimization objective");
     }
 
     virtual void prepare(cmd_context & ctx) { 
@@ -58,9 +59,15 @@ public:
         if (!ctx.is_model_available())
             throw cmd_exception("model is not available");
         model_ref md;
+        unsigned index = m_params.get_uint("model_index", 0);
         check_sat_result * last_result = ctx.get_check_sat_result();
         SASSERT(last_result);
-        last_result->get_model(md);
+        if (index == 0 || !ctx.get_opt()) {
+            last_result->get_model(md);
+        }
+        else {
+            ctx.get_opt()->get_box_model(md, index);
+        }
         expr_ref r(ctx.m());
         unsigned timeout = m_params.get_uint("timeout", UINT_MAX);
         unsigned rlimit  = m_params.get_uint("rlimit", 0);