quantifying over expr_vector index

Question

In the expr_vector example from example.cpp, can we quantify over the expr_vector index. For example, if we have the following code fragment :

expr_vector steps(c); 
expr b = c.bool_val(true); 
for(unsigned i = 0; i<N ; i++ ) 
{  expr step = c.int_const(...)

  if( i == 0 ) b = b && step == 0 ; 
  else b = b && step == steps[i-1] + 1 ; 
  steps.push_back(step); 
}

can we express something like

expr choice = c.int_const("choice); 
b = b && 0 <= choice && choice < N; 
b = b && steps[choice] > 5 ; 

Answer 1

No, this is not possible, expr_vectors are just like normal vectors with fixed size and explicit indexing. That said, it may be possible to express your problem by the use of arrays (see e.g., the Arrays section in the tutorial); this may come at the cost of performance however, because depending on the different combinations of theories a different decision procedure may have to be selected.