---

Expr.java

package gov.nasa.arc.ase.jpf.expr;

import java.util.StringTokenizer;
import gov.nasa.arc.ase.jpf.JPF;

//#ifdef BUCHI
public class Expr {
  SubExpr[] terms;

  public Expr() {
    terms = new SubExpr[0];
  }  
  public Expr(Expr e) {
    int l = e.terms.length;
    
    terms = new SubExpr[l];

    for(int i = 0; i < l; i++)
      terms[i] = e.terms[i];
  }  
  void backtrack(JPF jpf, int id) {
    terms[id].backtrack();
  }  
  boolean evaluate(JPF jpf, int id) {
    return terms[id].evaluate();
  }  
  void execute(JPF jpf, int id) {
    terms[id].execute();
  }  
  private void grow() {
    int l = terms.length;
    SubExpr[] nt = new SubExpr[l+1];
    System.arraycopy(terms, 0, nt, 0, l);
    terms = nt;
  }  
  private SubExpr id(SubExpr e) {
    for(int i = 0, l = terms.length; i < l; i++)
      if(terms[i].equals(e))
    return terms[i];
    put(e);

    return e;
  }  
  public SubExpr parse(String e) {
    if(e.equals("-")) return new True();

    return parseOr(e);
  }  
  private SubExpr parseAnd(String e) {
    String[] t = tokenize(e, "&");
    int l = t.length;

    if(l == 1) return parseNot(e);

    And s = new And(l);

    for(int i = 0; i < l; i++)
      s.set(i, parseNot(t[i]));

    return id(s);
  }  
  private SubExpr parseNot(String e) {
    e = e.trim();

    if(!e.startsWith("!")) return parseTerm(e);

    Not s = new Not(parseTerm(e.substring(1)));

    return id(s);
  }  
  private SubExpr parseOr(String e) {
    String[] t = tokenize(e, "|");
    int l = t.length;

    if(l == 1) return parseAnd(e);

    Or s = new Or(l);

    for(int i = 0; i < l; i++)
      s.set(i, parseAnd(t[i]));

    return id(s);
  }  
  private SubExpr parseTerm(String e) {
    return id(new Evaluate(e));
  }  
  private int put(SubExpr e) {
    int l = terms.length;
    grow();
    terms[l] = e;
    
    return l;
  }  
  private static String[] tokenize(String s, String d) {
    StringTokenizer st = new StringTokenizer(s, d);

    int ntokens = st.countTokens();
    String[] tokens = new String[ntokens];

    for(int i = 0; i < ntokens; i++)
      tokens[i] = st.nextToken();

    return tokens;
  }  
  String toString(int id) {
    return terms[id].toString();
  }  
}

---