private boolean executeQuantifier ( int index , Expr . Quantifier expr , CallStack frame ) { Tuple < Decl . Variable > vars = expr . getParameters ( ) ; if ( index == vars . size ( ) ) { // This is the base case where we evaluate the condition itself. RValue . Bool r = executeExpression ( BOOL_T , expr . getOperand ( ) , frame ) ; boolean q = ( expr instanceof Expr . UniversalQuantifier ) ; // If this evaluates to true, then we will continue executing the // quantifier. return r . boolValue ( ) == q ; } else { Decl . Variable var = vars . get ( index ) ; RValue . Array range = executeExpression ( ARRAY_T , var . getInitialiser ( ) , frame ) ; RValue [ ] elements = range . getElements ( ) ; for ( int i = 0 ; i != elements . length ; ++ i ) { frame . putLocal ( var . getName ( ) , elements [ i ] ) ; boolean r = executeQuantifier ( index + 1 , expr , frame ) ; if ( ! r ) { // early termination return r ; } } return true ; } }
Execute one range of the quantifier or the body if no ranges remain .