public abstract class Expression<E> extends AbstractPrintable {
  
  
  public static final int QUOTE_IDENTIFIERS = 1;
  public static final int INCLUDE_VARIABLE_TYPE = 2;
  public static final int INCLUDE_BOUND_DECL_TYPE = 4;
  public static final int SIMPLE_PROP_OPERATORS = 8;
  
  public static final int DEFAULT_FLAGS = QUOTE_IDENTIFIERS | INCLUDE_BOUND_DECL_TYPE;
  
  public static final int JAVA_COMPAT_FLAGS = SIMPLE_PROP_OPERATORS;
  
  public static boolean quoteIdentifiers(int printFlags) {
    return (printFlags & QUOTE_IDENTIFIERS) == QUOTE_IDENTIFIERS;
  }
  
  public static boolean includeVariableType(int printFlags) {
    return (printFlags & INCLUDE_VARIABLE_TYPE) == INCLUDE_VARIABLE_TYPE;
  }
  
  public static boolean includeBoundDeclType(int printFlags) {
    return (printFlags & INCLUDE_BOUND_DECL_TYPE) == INCLUDE_BOUND_DECL_TYPE;
  }
  
  public static Expression<?>[] NO_CHILDREN = new Expression[0];
  
    
  /**
   * evaluates using the provided values for symbolic variables
   * 
   * @param values
   * @return 
   */
  public abstract E evaluate(Valuation values);  
  
  /**
   * collect all symbolic variables
   * 
   * @param names 
   */
  public abstract void collectFreeVariables(Collection<? super Variable<?>> variables);
  
  public abstract <R,D> R accept(ExpressionVisitor<R, D> visitor, D data);
  
  
  public abstract Type<E> getType();
  
  public Class<E> getResultType() {
    return getType().getCanonicalClass();
  }
  
  
  public abstract Expression<?>[] getChildren();
  public abstract Expression<?> duplicate(Expression<?>[] newChildren);
  
  @SuppressWarnings("unchecked")
  public <F> Expression<F> as(Type<F> type) {
    Type<E> thisType = getType();
    if(!thisType.equals(type))
      return null;
    return (Expression<F>)this;
  }
  
  public <F> Expression<F> requireAs(Type<F> type) {
    Expression<F> exp = as(type);
    if(exp == null)
      throw new IllegalArgumentException("Expected type " + type + ", is " + getType());
    return exp;
  }
  
  public abstract void print(Appendable a, int flags) throws IOException;

  /**A malformed Expression might contain a null value.
  This method should only be used in debug environment
   * @throws java.io.IOExceptions*/
  public abstract void printMalformedExpression(Appendable a, int flags)
          throws IOException;

  public String toString(int flags) {
    StringBuilder sb = new StringBuilder();
    try {
      print(sb, flags);
      return sb.toString();
    }
    catch(IOException ex) {
      throw new RuntimeException("Unexpected IOException writing to StringBuilder");
    }
  }
  
  @Override
  public final void print(Appendable a) throws IOException {
    print(a, DEFAULT_FLAGS);
  }
  
  public final void printMalformedExpression(Appendable a) throws IOException {
    printMalformedExpression(a, DEFAULT_FLAGS);
  }

  
  // LEGACY API
  
  /**
   * replace terms according to replace
   * 
   * @param replace
   * @return 
   */
  @Deprecated
  @SuppressWarnings("rawtypes")
  public Expression replaceTerms(Map<Expression,Expression> replacements) {
    Expression<?> rep = replacements.get(this);
    if(rep != null)
      return rep;
    Expression<?>[] children = getChildren();
    
    boolean changed = false;
    for(int i = 0; i < children.length; i++) {
      Expression<?> old = children[i];
      Expression<?> newExp = old.replaceTerms(replacements);
      if(old != newExp)
        changed = true;
      children[i] = newExp;
    }
    
    if(!changed)
      return this;
    
    return duplicate(children);
  }
  
  @Deprecated
  @SuppressWarnings("rawtypes")
  public void getVariables(Set<Variable> variables) {
    collectFreeVariables(variables);
  }
  
} public class Variable<E> extends Expression<E> {

  public static <E> Variable<E> create(Type<E> type, String name) {
    return new Variable<E>(type, name);
  }
  
  public static <E> Variable<E> createAnonymous(Type<E> type) {
    return new Variable<E>(type);
  }
  
  private final Type<E> type;
  
  private final String name;

  
  public Variable(Type<E> type) {
    this(type, null);
  }
  
  public Variable(Type<E> type, String name) {
    this.type = type;
    this.name = name;
  }

  @Override
  public E evaluate(Valuation values) {
    return values.getValue(this);
  }

  @Override
  public void collectFreeVariables(Collection<? super Variable<?>> variables) {
    variables.add(this);
  }
  
  @Override
  public boolean equals(Object obj) {
    if(obj == this) {
      return true;
    }
    if (obj == null) {
      return false;
    }
    // Special case: Anonymous variables are only equal to their INSTANCE
    if(name == null) {
      return false;
    }
    
    if(obj.getClass() != Variable.class) {
      return false;
    }
    final Variable<?> other = (Variable<?>) obj;
    
    if(!this.type.equals(other.type))
      return false;
    
    return this.name.equals(other.name);
  }

  @Override
  public int hashCode() {
    if(name == null) // Identity-based equals/hashCode semantics for anonymous variables
      return super.hashCode(); 
    
    int hash = 7;
    hash = 47 * hash + (this.type != null ? this.type.hashCode() : 0);
    hash = 47 * hash + (this.name != null ? this.name.hashCode() : 0);
    return hash;
  }

  
  public String getName() {
    return this.name;
  }

  @Override
  public Expression<?>[] getChildren() {
    return NO_CHILDREN;
  }

  @Override
  public Expression<E> duplicate(Expression<?>[] newChildren) {
    assert newChildren.length == 0;
    return this;
  }

  @Override
  public Type<E> getType() {
    return type;
  }

  @Override
  public void print(Appendable a, int flags) throws IOException {
    boolean qid = quoteIdentifiers(flags);
    if(qid)
      a.append('\'');
    a.append(name);
    if(qid)
      a.append('\'');
    if(includeVariableType(flags)) {
      a.append(':');
      a.append(type.getName());
    }
  }

  @Override
  public void printMalformedExpression(Appendable a, int flags)
          throws IOException{
    boolean qid = quoteIdentifiers(flags);
    if(qid)
      a.append('\'');
    if(name == null){
      a.append("null");
    }else {
      a.append(name);
    }
    if(qid)
      a.append('\'');
    if(includeVariableType(flags)) {
      a.append(':');
      if(type == null){
        a.append("null");
      } else {
        a.append(type.getName());
      }
    }
  }

  @Override
  public <R, D> R accept(ExpressionVisitor<R, D> visitor, D data) {
    return visitor.visit(this, data);
  }

  public void printTyped(Appendable a) throws IOException {
    print(a, DEFAULT_FLAGS | INCLUDE_VARIABLE_TYPE);
  }
  
  
  
  
  
  // LEGACY API
  
  @Deprecated
  public Variable(Class<E> clazz, String name) {
    this(ObjectConstraints.getPrimitiveType(clazz), name);
  }
  
} public class Constant<E> extends AbstractExpression<E> {
  
  public static <E> Constant<E> create(Type<E> type, E value) {
    return new Constant<E>(type, value);
  }
  
  public static <E> Constant<E> createParsed(Type<E> type, String txt) {
    return new Constant<E>(type, type.parse(txt));
  }
  
  public static <E> Constant<E> createCasted(Type<E> type, Object value) {
    return new Constant<E>(type, type.cast(value));
  }

  private final Type<E> type;
  private final E value;
  
  public Constant(Type<E> type, E value) {
    this.type = type;
    this.value = value;
  }  


  @Override
  public E evaluate(Valuation values) {
    return this.value;
  }


  @Override
  public void collectFreeVariables(Collection<? super Variable<?>> variables) {
    // do nothing
  }

  @Override
  public boolean equals(Object obj) {
    if (obj == null) {
      return false;
    }
    if (getClass() != obj.getClass()) {
      return false;
    }
    final Constant<?> other = (Constant<?>) obj;
    if (this.type != other.type && (this.type == null || !this.type.equals(other.type))) {
      return false;
    }
    if ((this.value == null) ? (other.value != null) : !this.value.equals(other.value)) {
      return false;
    }
    return true;
  }

  @Override
  public int hashCode() {
    int hash = 7;
    hash = 47 * hash + (this.type != null ? this.type.hashCode() : 0);
    hash = 47 * hash + (this.value != null ? this.value.hashCode() : 0);
    return hash;
  }
  
  
  @Override
  public Type<E> getType() {
    return this.type;
  }    

  public E getValue() {
    return this.value;
  }


  @Override
  public Expression<?>[] getChildren() {
    return NO_CHILDREN;
  }


  @Override
  public Expression<E> duplicate(Expression<?>[] newChildren) {
    assert newChildren.length == 0;
    return this;
  }


  @Override
  public void print(Appendable a, int flags) throws IOException {
    a.append(String.valueOf(value));
  }

  @Override
  public void printMalformedExpression(Appendable a, int flags) 
          throws IOException {
    if(value == null){
      a.append("null");
    } else {
      a.append(String.valueOf(value));
    }
  }
  @Override
  public <R, D> R accept(ExpressionVisitor<R, D> visitor, D data) {
    return visitor.visit(this, data);
  }

  
  // LEGACY API
  
  @Deprecated
  public Constant(Class<E> clazz, E value) {
    this(ObjectConstraints.getPrimitiveType(clazz), value);
  }
} public class IfThenElse<E> extends AbstractExpression<E> {

    private final Type<E> type;
    
    private final Expression<Boolean> ifCond;
    private final Expression<E> thenExpr;    
    private final Expression<E> elseExpr;

    public IfThenElse(Type<E> type, Expression<Boolean> ifCond, Expression<E> thenExpr, Expression<E> elseExpr) {
        this.type = type;
        this.ifCond = ifCond;
        this.thenExpr = thenExpr;
        this.elseExpr = elseExpr;
    }
    
    public IfThenElse(Expression<Boolean> ifCond, Expression<E> thenExpr, Expression<E> elseExpr) {
        assert thenExpr.getType().equals(elseExpr.getType());
        this.type = thenExpr.getType();
        this.ifCond = ifCond;
        this.thenExpr = thenExpr;
        this.elseExpr = elseExpr;
    }
    
    @Override
    public E evaluate(Valuation values) {
        return ifCond.evaluate(values) ? thenExpr.evaluate(values) : elseExpr.evaluate(values);
    }

    @Override
    public void collectFreeVariables(Collection<? super Variable<?>> variables) {
        ifCond.collectFreeVariables(variables);
        thenExpr.collectFreeVariables(variables);
        elseExpr.collectFreeVariables(variables);
    }

    @Override
    public <R, D> R accept(ExpressionVisitor<R, D> visitor, D data) {
        return visitor.visit(this, data);
    }

    @Override
    public Type<E> getType() {
        return type;
    }

    @Override
    public Expression<?>[] getChildren() {
        return new Expression[] {ifCond, thenExpr, elseExpr};
    }

    @Override
    public Expression<?> duplicate(Expression<?>[] newChildren) {
        assert newChildren.length == 3;
        Expression newIf = newChildren[0];
        Expression newThen = newChildren[1];
        Expression newElse = newChildren[2];

        if(ifCond == newIf && thenExpr == newThen && elseExpr == newElse) {
          return this;
        }
        return new IfThenElse<>(this.type, ifCond, thenExpr, elseExpr);
    }

    @Override
    public void print(Appendable a, int flags) throws IOException {
        a.append("if (");
        ifCond.print(a, flags);
        a.append(") then (");
        thenExpr.print(a, flags);
        a.append(") else (");
        elseExpr.print(a, flags);
        a.append(")");
    }

    @Override
    public void printMalformedExpression(Appendable a, int flags) throws IOException{
      a.append("if (");
      if(ifCond == null){
        a.append("null");
      } else {
        ifCond.printMalformedExpression(a, flags);
      }
      a.append(") then (");
      if(thenExpr == null){
        a.append("null");
      } else{
        thenExpr.print(a, flags);
      }
      a.append(") else (");
      if(elseExpr == null){
        a.append("null");
      }else {
        elseExpr.print(a, flags);
      }
      a.append(")");
    }

    @Override
    public int hashCode() {
        int hash = 3;
        hash = 53 * hash + Objects.hashCode(this.ifCond);
        hash = 53 * hash + Objects.hashCode(this.thenExpr);
        hash = 53 * hash + Objects.hashCode(this.elseExpr);
        return hash;
    }

    @Override
    public boolean equals(Object obj) {
        if (obj == null) {
            return false;
        }
        if (getClass() != obj.getClass()) {
            return false;
        }
        final IfThenElse<?> other = (IfThenElse<?>) obj;
        if (!Objects.equals(this.ifCond, other.ifCond)) {
            return false;
        }
        if (!Objects.equals(this.thenExpr, other.thenExpr)) {
            return false;
        }
        if (!Objects.equals(this.elseExpr, other.elseExpr)) {
            return false;
        }
        return true;
    }

    public Expression<Boolean> getIf() {
        return ifCond;
    }

    public Expression<E> getThen() {
        return thenExpr;
    }

    public Expression<E> getElse() {
        return elseExpr;
    }
} public class QuantifierExpression extends AbstractBoolExpression {

  private final Quantifier quantifier;
  private final List<? extends Variable<?>> boundVariables;
  private final Expression<Boolean> body;

  public QuantifierExpression(Quantifier quantifier, List<? extends Variable<?>> boundVariables, Expression<Boolean> body) {
    this.quantifier = quantifier;
    this.boundVariables = new ArrayList<Variable<?>>(boundVariables);
    this.body = body;
  }

  public Quantifier getQuantifier() {
    return quantifier;
  }

  public List<? extends Variable<?>> getBoundVariables() {
    return Collections.unmodifiableList(boundVariables);
  }

  public Expression<Boolean> getBody() {
    return body;
  }

  @Override
  public boolean equals(Object obj) {
    if (obj == null) {
      return false;
    }
    if (getClass() != obj.getClass()) {
      return false;
    }
    final QuantifierExpression other = (QuantifierExpression) obj;

    if (this.quantifier != other.quantifier) {
      return false;
    }

    if (this.boundVariables != other.boundVariables && (this.boundVariables == null || !this.boundVariables.equals(other.boundVariables))) {
      return false;
    }

    if (this.body != other.body && (this.body == null || !this.body.equals(other.body))) {
      return false;
    }

    return true;
  }

  @Override
  public int hashCode() {
    int hash = 3;
    hash = 43 * hash + quantifier.hashCode();
    hash = 43 * hash + boundVariables.hashCode();
    hash = 43 * hash + body.hashCode();
    return hash;
  }

  @Override
  public void print(Appendable a, int flags) throws IOException {
    a.append('(').append(quantifier.toString()).append(" (");
    boolean first = true;
    int varDeclFlags = flags;
    if (includeBoundDeclType(flags)) {
      varDeclFlags |= INCLUDE_VARIABLE_TYPE;
    }

    for (Variable<?> var : boundVariables) {
      if (first) {
        first = false;
      } else {
        a.append(", ");
      }
      var.print(a, varDeclFlags);
    }
    a.append("): ");
    body.print(a, flags);
    a.append(')');
  }

  @Override
  public void printMalformedExpression(Appendable a, int flags) 
          throws IOException{
    a.append('(').append(quantifier.toString()).append(" (");
    boolean first = true;
    int varDeclFlags = flags;
    if (includeBoundDeclType(flags)) {
      varDeclFlags |= INCLUDE_VARIABLE_TYPE;
    }

    for (Variable<?> var : boundVariables) {
      if (first) {
        first = false;
      } else {
        a.append(", ");
      }
      if(var != null){
        var.print(a, varDeclFlags);
      }else{
        a.append("null");
      }
    }
    a.append("): ");
    if(body != null){
      body.print(a, flags);
    }else{
      a.append("null");
    }
    a.append(')');
  }

  @Override
  public Boolean evaluate(Valuation values) {
    throw new UnsupportedOperationException("Evaluation not supported for quantifiers");
  }

  @Override
  public void collectFreeVariables(Collection<? super Variable<?>> variables) {
    // Omit bound variables 
    // List of bound variables that DO NOT appear in the outer scope
    List<Variable<?>> boundOnly = new ArrayList<Variable<?>>();
    for (Variable<?> v : boundVariables) {
      if (!variables.contains(v)) {
        boundOnly.add(v);
      }
    }
    body.collectFreeVariables(variables);
    variables.removeAll(boundOnly);
  }

  @Override
  public Expression<?>[] getChildren() {
    return new Expression[]{body};
  }

  @Override
  public Expression<Boolean> duplicate(
          Expression<?>[] newChildren) {
    assert newChildren.length == 1;

    Expression<?> newBody = newChildren[0];
    if (body == newBody) {
      return this;
    }
    return new QuantifierExpression(this.quantifier, boundVariables, newBody.as(BuiltinTypes.BOOL));
  }

  @Override
  public <R, D> R accept(ExpressionVisitor<R, D> visitor, D data) {
    return visitor.visit(this, data);
  }

} public class UnaryMinus<E> extends AbstractExpression<E> {

  public static <E> UnaryMinus<E> create(
      Expression<E> negated) {
    return new UnaryMinus<E>(negated);
  }
  
  private final Expression<E> negated;

  public UnaryMinus(Expression<E> negated) {
    this.negated = negated;
  }
  
  public Expression<E> getNegated() {
    return this.negated;
  }
  
  @Override
  public E evaluate(Valuation values) {
    E num = negated.evaluate(values);
    NumericType<E> type = (NumericType<E>)getType();
    return type.negate(num);
  }    
    
  
  @Override
  public void collectFreeVariables(Collection<? super Variable<?>> variables) {
    this.negated.collectFreeVariables(variables);
  }

  
  @Override
  public int hashCode() {
    final int prime = 31;
    int result = 1;
    result = prime * result + negated.hashCode();
    return result;
  }

  @Override
  public boolean equals(Object obj) {
    if (this == obj)
      return true;
    if (obj == null)
      return false;
    if (getClass() != obj.getClass())
      return false;
    UnaryMinus<?> other = (UnaryMinus<?>) obj;
    return negated.equals(other.negated);
  }

  public Type<E> getType() {
    return negated.getType();
  }

  @Override
  public Expression<?>[] getChildren() {
    return new Expression[]{negated};
  }

  @Override
  public Expression<?> duplicate(Expression<?>[] newChildren) {
    assert newChildren.length == 1;
    
    if(negated == newChildren[0])
      return this;
    
    return UnaryMinus.create(newChildren[0]);
  }

  @Override
  public void print(Appendable a, int flags) throws IOException {
    a.append("-(");
    negated.print(a, flags);
    a.append(')');
  }

  @Override
  public void printMalformedExpression(Appendable a, int flags) throws IOException{
    a.append("-(");
    if(negated == null){
      a.append("null");
    } else {
      negated.print(a, flags);
    }
    a.append(')');
  }

  @Override
  public <R, D> R accept(ExpressionVisitor<R, D> visitor, D data) {
    return visitor.visit(this, data);
  }
} public class Function<T> extends AbstractPrintable {
  
  private final String name;
  private final Type<T> returnType;
  private final Type<?>[] paramTypes;

  @SafeVarargs
  public Function(String name, Type<T> returnType, Type<?> ...paramTypes) {
    this.name = name;
    this.returnType = returnType;
    this.paramTypes = paramTypes;
  }
  
  
  public String getName() {
    return name;
  }
  
  public Type<T> getReturnType() {
    return returnType;
  }
  
  public Type<?>[] getParamTypes() {
    return paramTypes;
  }
  
  public FunctionExpression<T> toExpression(Expression<?> ...args) {
	  return new FunctionExpression<>(this, args);
  }
  
  public T evaluate(Object... args) {
	  throw new UnsupportedOperationException("Semantics for function '" + name + "' undefined");
  }
  
  public int getArity() {
	  return paramTypes.length;
  }


  @Override
  public void print(Appendable a) throws IOException {
    a.append(name).append('(');
    Joiner.on(',').appendTo(a, paramTypes);
    a.append("):").append(returnType.toString());
  }

} public class FunctionExpression<T> extends AbstractExpression<T> {
  
  private final Function<T> function;
  private final Expression<?>[] args;
  
  
  public FunctionExpression(Function<T> function, Expression<?> ...args) {
	  if(function.getArity() != args.length) {
		  throw new IllegalArgumentException("Cannot invoke function " + function.getName() + " of arity "
				  + function.getArity() + " with " + args.length + " arguments");
		  
		  // TODO parameter type check?
	  }
    this.function = function;
    this.args = args;
  }
  
  
  @Override
  public T evaluate(Valuation values) {
	  Object[] argValues = new Object[args.length];
	  for(int i = 0; i < args.length; i++) {
		  argValues[i] = args[i].evaluate(values);
	  }
	  return function.evaluate(argValues);
  }
  
  @Override
  public void collectFreeVariables(Collection<? super Variable<?>> variables) {
    for(Expression<?> a : args)
      a.collectFreeVariables(variables);
  }
  
  @Override
  public <R, D> R accept(ExpressionVisitor<R, D> visitor, D data) {
    return visitor.visit(this, data);
  }
  
  @Override
  public Type<T> getType() {
    return function.getReturnType();
  }
  
  @Override
  public Expression<?>[] getChildren() {
    return args.clone();
  }
  
  @Override
  public Expression<?> duplicate(Expression<?>[] newChildren) {
    Type<?>[] ptypes = function.getParamTypes();
    assert ptypes.length == newChildren.length;
    
    for(int i = 0; i < ptypes.length; i++) {
      assert ptypes[i].equals(newChildren[i].getType());
    }
    
    return new FunctionExpression<>(function, newChildren);
  }
  
  @Override
  public void print(Appendable a, int flags) throws IOException {
    boolean qid = Expression.quoteIdentifiers(flags);
    if(qid)
      a.append('\'');
    a.append(function.getName());
    if(qid)
      a.append('\'');
    a.append('(');
    boolean first = true;
    for(Expression<?> arg : args) {
      if(first)
        first = false;
      else
        a.append(',');
      arg.print(a, flags);
    }
    a.append(')');
  }

  @Override
  public void printMalformedExpression(Appendable a, int flags) throws IOException {
    boolean qid = Expression.quoteIdentifiers(flags);
    if(qid)
      a.append('\'');
    if(function == null){
      a.append("null");
    } else {
      a.append(function.getName());
    }
    if(qid)
      a.append('\'');
    a.append('(');
    boolean first = true;
    for(Expression<?> arg : args) {
      if(first)
        first = false;
      else
        a.append(',');
      if(arg != null){
        a.append("null");
      } else {
        arg.print(a, flags);
      }
    }
    a.append(')');
  }

  /* (non-Javadoc)
   * @see java.lang.Object#hashCode()
   */
  @Override
  public int hashCode() {
    final int prime = 31;
    int result = 1;
    result = prime * result + Arrays.hashCode(args);
    result = prime * result + ((function == null) ? 0 : function.hashCode());
    return result;
  }


  /* (non-Javadoc)
   * @see java.lang.Object#equals(java.lang.Object)
   */
  @Override
  public boolean equals(Object obj) {
    if (this == obj)
      return true;
    if (obj == null)
      return false;
    if (getClass() != obj.getClass())
      return false;
    FunctionExpression<?> other = (FunctionExpression<?>) obj;
    if (!Arrays.equals(args, other.args))
      return false;
    if (function == null) {
      if (other.function != null)
        return false;
    } else if (!function.equals(other.function))
      return false;
    return true;
  }

    public Function<T> getFunction() {
        return function;
    }

    public Expression<?>[] getArgs() {
        return args;
    }
} public abstract class BinaryDoubleFunction extends Function<Double> {

	public BinaryDoubleFunction(String name) {
		super(name, BuiltinTypes.DOUBLE, BuiltinTypes.DOUBLE, BuiltinTypes.DOUBLE);
	}

	@Override
	public Double evaluate(Object... args) {
		if(args.length != 2) {
			throw new IllegalArgumentException("Error evaluating function '" + getName()
					+ "': incorrect number of arguments: expected 1, got " + args.length);
		}
		
		Object arg1 = args[0];
		if(!(arg1 instanceof Number)) {
			throw new IllegalArgumentException("Error evaluating function '" + getName()
					+ "': expected numeric argument, got type " + arg1.getClass());
		}
		
		Object arg2 = args[1];
		if(!(arg2 instanceof Number)) {
			throw new IllegalArgumentException("Error evaluating function '" + getName()
					+ "': expected numeric argument, got type " + arg2.getClass());
		}

                Number narg1 = (Number)arg1;
                Number narg2 = (Number)arg2;
		
		return doEvaluate(narg1.doubleValue(), narg2.doubleValue());
	}

	
	protected abstract double doEvaluate(double v1, double v2);
     
} public abstract class MathFunctions {
	
	public static UnaryDoubleFunction COS = new UnaryDoubleFunction("cos") {
		@Override
		protected double doEvaluate(double value) {
			return Math.cos(value);
		}
	};
	
	public static UnaryDoubleFunction SIN = new UnaryDoubleFunction("sin") {
		@Override
		protected double doEvaluate(double value) {
			return Math.sin(value);
		}
	};
	
	public static UnaryDoubleFunction TAN = new UnaryDoubleFunction("tan") {
		@Override
		protected double doEvaluate(double value) {
			return Math.tan(value);
		}
	};
	
	public static UnaryDoubleFunction ACOS = new UnaryDoubleFunction("acos") {
		@Override
		protected double doEvaluate(double value) {
			return Math.acos(value);
		}
	};
	
	public static UnaryDoubleFunction ASIN = new UnaryDoubleFunction("asin") {
		@Override
		protected double doEvaluate(double value) {
			return Math.asin(value);
		}
	};
	
	public static UnaryDoubleFunction ATAN = new UnaryDoubleFunction("atan") {
		@Override
		protected double doEvaluate(double value) {
			return Math.atan(value);
		}
	};

	public static UnaryDoubleFunction LOG = new UnaryDoubleFunction("log") {
		@Override
		protected double doEvaluate(double value) {
			return Math.log(value);
		}
	};

	public static UnaryDoubleFunction EXP = new UnaryDoubleFunction("exp") {
		@Override
		protected double doEvaluate(double value) {
			return Math.exp(value);
		}
	};

	public static UnaryDoubleFunction SQRT = new UnaryDoubleFunction("sqrt") {
		@Override
		protected double doEvaluate(double value) {
			return Math.sqrt(value);
		}
	};
	
	public static UnaryDoubleFunction LOG10 = new UnaryDoubleFunction("log10") {
	  @Override
	  protected double doEvaluate(double value) {
	    return Math.log10(value);
	  }
	};

	public static UnaryDoubleLongFunction ROUND = new UnaryDoubleLongFunction("round") {
	  @Override
	  protected long doEvaluate(double value) {
	    return Math.round(value);
	  }
	};

	public static BinaryDoubleFunction ATAN2 = new BinaryDoubleFunction("atan2") {
	  @Override
		protected double doEvaluate(double v1, double v2) {
			return Math.atan2(v1, v2);
		}
	};        

	public static BinaryDoubleFunction POW = new BinaryDoubleFunction("pow") {
		@Override
		protected double doEvaluate(double v1, double v2) {
			return Math.pow(v1, v2);
		}
	};   
        
	public static UnaryIntegerFunction IABS = new UnaryIntegerFunction("abs") {
		@Override
		protected int doEvaluate(int v1) {
			return Math.abs(v1);
		}
	};          
} public class PropertyBuilder {
 
    private PropertyBuilder() {        
    }
    
    /* ***************************************************************************
     *
     * CONSTANTS
     *
     */
//    final static Constant ZERO = Constant.create(BuiltinTypes.DOUBLE, 0.0);
//    final static Constant ONE = Constant.create(BuiltinTypes.DOUBLE, 1.0);
//    final static Constant MINUS_ONE = Constant.create(BuiltinTypes.DOUBLE, -1.0);
//
//    final static Constant MINUS_PI_0_5 = Constant.create(BuiltinTypes.DOUBLE, Math.PI / -2.0);
//    final static Constant PI_0_5 = Constant.create(BuiltinTypes.DOUBLE, Math.PI / 2.0);
//    final static Constant PI = Constant.create(BuiltinTypes.DOUBLE, Math.PI);
//    final static Constant PI_1_5 = Constant.create(BuiltinTypes.DOUBLE, Math.PI * 1.5);
//    final static Constant PI_2_0 = Constant.create(BuiltinTypes.DOUBLE, Math.PI * 2.0);
//
//    final static Constant E = Constant.create(BuiltinTypes.DOUBLE, Math.E);

    /* ***************************************************************************
     *
     * LINEAR INTERPOLATION
     *
     */
    public static QuantifierExpression linearInterpolation(
            Function func, double[] dVals, double[] fVals) {

        assert dVals.length == fVals.length;
        assert dVals.length > 2;

        Variable x = var(BuiltinTypes.DOUBLE);
        FunctionExpression fe = fexpr(func, x);
        IfThenElse ite = linearInterpolation(x, dVals, fVals);
        Expression<Boolean> equal = eq(fe, ite);
        return forall(equal, x);
    }

    public static QuantifierExpression linearInterpolation(
            Function func, IfThenElse ite, Variable x) {

        FunctionExpression fe = fexpr(func, x);
        Expression<Boolean> equal = eq(fe, ite);
        return forall(equal, x);
    }
    
    public static IfThenElse linearInterpolation(
            Expression x, double[] dVals, double[] fVals) {
        
        Expression[] itp = new Expression[dVals.length - 1];
        for (int i = 0; i < itp.length; i++) {
            itp[i] = interpolate(x, fVals[i], fVals[i + 1], dVals[i], dVals[i + 1]);
        }

        IfThenElse ite = ite(bounds(x, dVals[dVals.length - 3], dVals[dVals.length - 2], false, false),
                itp[itp.length - 2], itp[itp.length - 1]);

        for (int i = 3; i < dVals.length; i++) {

            ite = ite(bounds(x, dVals[dVals.length - i - 1], dVals[dVals.length - i], false, false),
                    itp[itp.length - i], ite);
        }

        return ite; 
    }
    
    public static Expression interpolate(
            Expression x, double min, double max, double lower, double upper) {

        Constant minC = new Constant(BuiltinTypes.DOUBLE, min);
        Constant lowerC = new Constant(BuiltinTypes.DOUBLE, lower);
        
        Constant ratio = new Constant(BuiltinTypes.DOUBLE,  (max - min) / (upper - lower));
        return plus(minC, mul(ratio, minus(x, lowerC)));
    }       
    
    /* ***************************************************************************
     *
     * FUNCTIONS
     *
     */

    public static Expression<Boolean> bounds(Function func, Constant lower, Constant upper, boolean open) {
        Variable i[] = new Variable[func.getArity()];
        for (int j=0; j<i.length; j++) {
            i[j] = var(BuiltinTypes.DOUBLE);
        }
        FunctionExpression fe = fexpr(func, i);
        Expression<Boolean> lBound = open ? lt(lower, fe) : lte(lower, fe);
        Expression<Boolean> uBound = open ? gt(upper, fe) : gte(upper, fe);
        return forall(and(lBound, uBound), i);
    }

    public static Expression<Boolean> bounds(Expression x, double lower, double upper, boolean openLower, boolean openUpper) {
        Constant cl = new Constant(BuiltinTypes.DOUBLE, lower);
        Constant cu = new Constant(BuiltinTypes.DOUBLE, upper);

        Expression<Boolean> lBound = openLower ? lt(cl, x) : lte(cl, x);
        Expression<Boolean> uBound = openUpper ? lt(x, cu) : lte(x, cu);
        return and(lBound, uBound);
    }

    public static Expression<Boolean> lbound(Function func, Constant lower, boolean open) {
        Variable i = var(BuiltinTypes.DOUBLE);
        FunctionExpression fe = fexpr(func, i);
        Expression<Boolean> lBound = open ? lt(lower, fe) : lte(lower, fe);
        return forall(lBound, i);
    }    
    
    public static Expression<Boolean> ubound(Function func, Constant upper, boolean open) {
        Variable i = var(BuiltinTypes.DOUBLE);
        FunctionExpression fe = fexpr(func, i);
        Expression<Boolean> lBound = open ? gt(upper, fe) : gte(upper, fe);
        return forall(lBound, i);
    }  
    
    /* ***************************************************************************
     *
     * BASIC HELPERS
     *
     */
    public static FunctionExpression fexpr(Function f, Expression... args) {
        return new FunctionExpression(f, args);
    }

    public static <T extends Number> NumericBooleanExpression gt(
            Expression<T> left, Expression<T> right) {
        return nbe(left, NumericComparator.GT, right);
    }

    public static <T extends Number> NumericBooleanExpression gte(
            Expression<T> left, Expression<T> right) {
        return nbe(left, NumericComparator.GE, right);
    }

    public static <T extends Number> NumericBooleanExpression lt(
            Expression<T> left, Expression<T> right) {
        return nbe(left, NumericComparator.LT, right);
    }

    public static <T extends Number> NumericBooleanExpression lte(
            Expression<T> left, Expression<T> right) {
        return nbe(left, NumericComparator.LE, right);
    }

    public static <T extends Number> NumericBooleanExpression eq(
            Expression<T> left, Expression<T> right) {
        return nbe(left, NumericComparator.EQ, right);
    }

    public static <T extends Number> NumericBooleanExpression neq(
            Expression<T> left, Expression<T> right) {
        return nbe(left, NumericComparator.NE, right);
    }

    public static QuantifierExpression forall(Expression<Boolean> expr, Variable<?>... vars) {
        return new QuantifierExpression(Quantifier.FORALL, Arrays.asList(vars), expr);
    }

    public static PropositionalCompound follows(Expression<Boolean> ante, Expression<Boolean> claim) {
        return new PropositionalCompound(ante, LogicalOperator.IMPLY, claim);
    }

    public static <T extends Number> NumericBooleanExpression nbe(
            Expression<T> left, NumericComparator c, Expression<T> right) {
        return new NumericBooleanExpression(left, c, right);
    }


    public static <E> IfThenElse<E> ite(Expression<Boolean> ifCond, Expression<E> thenExpr, Expression<E> elseExpr) {
        return new IfThenElse<>(ifCond, thenExpr, elseExpr);
    }

    public static <E> NumericCompound plus(Expression<E> left, Expression<E> right) {
        return new NumericCompound<>(left, NumericOperator.PLUS, right);
    }

    public static <E> NumericCompound minus(Expression<E> left, Expression<E> right) {
        return new NumericCompound<>(left, NumericOperator.MINUS, right);
    }

    public static <E> NumericCompound mul(Expression<E> left, Expression<E> right) {
        return new NumericCompound<>(left, NumericOperator.MUL, right);
    }

    public static <E> NumericCompound div(Expression<E> left, Expression<E> right) {
        return new NumericCompound<>(left, NumericOperator.DIV, right);
    }

    
    /* ***************************************************************************
     *
     * TERMINALS
     *
     */

    private static int id = 0;
    
    public static synchronized Variable<?> var(Type t) {
        return new Variable(t, "__axiom_" + id++);
    }    

    public static Variable<?> doubleVar() {
        return var(BuiltinTypes.DOUBLE);
    }    

    public static Constant constant(double val) {
        return new Constant(BuiltinTypes.DOUBLE, val);
    }     

    /* ***************************************************************************
     *
     * INTERVALS
     *
     */
    
    public static double[] interval(double min, double max, int elements) {
        double[] d = new double[elements];
        double width = max - min;
        double step = width / ((double) (elements - 1));
        double val = min;
        for (int i=0; i<elements; i++) {
            d[i] = val;
            val += step;
        }
        return d;
    }
    
    /* ***************************************************************************
     *
     * OTHER
     *
     */
    
    public static Expression<Boolean>[] array(Expression<Boolean> ... args) {
        return args;
    }
} public abstract class BuiltinTypes {
  
  public static final class SInt8Type extends ConcreteBVIntegerType<Byte> {
    SInt8Type() {
      super("sint8", Byte.class, Byte.valueOf((byte)0), 8, true, BigInteger.valueOf(Byte.MIN_VALUE), BigInteger.valueOf(Byte.MAX_VALUE), SINT16, new String[]{"byte"}, byte.class);
    }

    @Override
    public Byte parse(String string) {
      return new BigInteger(string).byteValue();
    }

    @Override
    public int compare(Byte left, Byte right) {
      return left.compareTo(right);
    }

    @Override
    public Byte negate(Byte num) {
      return (byte)-num;
    }

    @Override
    public Byte shiftLeft(Byte value, Byte shiftAmt) {
      return (byte)(value << shiftAmt);
    }

    @Override
    public Byte shiftRight(Byte value, Byte shiftAmt) {
      return (byte)(value >> shiftAmt);
    }

    @Override
    public Byte shiftRightUnsigned(Byte value, Byte shiftAmt) {
      return (byte)(value >>> shiftAmt);
    }

    @Override
    public Byte not(Byte value) {
      return (byte)~value;
    }

    @Override
    public Byte and(Byte left, Byte right) {
      return (byte)(left & right);
    }

    @Override
    public Byte or(Byte left, Byte right) {
      return (byte)(left | right);
    }

    @Override
    public Byte xor(Byte left, Byte right) {
      return (byte)(left ^ right);
    }

    @Override
    public Byte plus(Byte left, Byte right) {
      return (byte)(left + right);
    }

    @Override
    public Byte minus(Byte left, Byte right) {
      return (byte)(left - right);
    }

    @Override
    public Byte mul(Byte left, Byte right) {
      return (byte)(left * right);
    }

    @Override
    public Byte div(Byte left, Byte right) {
      return (byte)(left / right);
    }

    @Override
    public Byte mod(Byte left, Byte right) {
      return (byte)(left % right);
    }

    @Override
    public BigInteger integerValue(Byte value) {
      return BigInteger.valueOf(value.intValue());
    }

    @Override
    public Byte cast(Object other) {
      if(other instanceof Number)
        return ((Number)other).byteValue();
      throw new ClassCastException();
    }
    
    @Override
    @SuppressWarnings("unchecked")
    protected <O> CastOperation<? super O, ? extends Byte> castFrom(
        Type<O> other) {
      if(Number.class.isAssignableFrom(other.getCanonicalClass()))
        return (CastOperation<? super O,? extends Byte>)NumericCastOperation.TO_SINT8;
      return null;
    }
  }

  public static final class SInt16Type extends ConcreteBVIntegerType<Short> {
    SInt16Type() {
      super("sint16", Short.class, (short)0, 16, true, BigInteger.valueOf(Short.MIN_VALUE), BigInteger.valueOf(Short.MAX_VALUE), SINT32, new String[]{"short"}, short.class);
    }

    @Override
    public Short parse(String string) {
      return new BigInteger(string).shortValue();
    }

    @Override
    public int compare(Short left, Short right) {
      return left.compareTo(right);
    }

    @Override
    public Short negate(Short num) {
      return (short)-num;
    }

    @Override
    public Short shiftLeft(Short value, Short shiftAmt) {
      return (short)(value << shiftAmt);
    }

    @Override
    public Short shiftRight(Short value, Short shiftAmt) {
      return (short)(value >> shiftAmt);
    }

    @Override
    public Short shiftRightUnsigned(Short value, Short shiftAmt) {
      return (short)(value >>> shiftAmt);
    }

    @Override
    public Short plus(Short left, Short right) {
      return (short)(left + right);
    }

    @Override
    public Short minus(Short left, Short right) {
      return (short)(left - right);
    }

    @Override
    public Short mul(Short left, Short right) {
      return (short)(left * right);
    }

    @Override
    public Short div(Short left, Short right) {
      return (short)(left / right);
    }

    @Override
    public Short mod(Short left, Short right) {
      return (short)(left % right);
    }

    @Override
    public Short not(Short value) {
      return (short)~value;
    }

    @Override
    public Short and(Short left, Short right) {
      return (short)(left & right);
    }

    @Override
    public Short or(Short left, Short right) {
      return (short)(left | right);
    }

    @Override
    public Short xor(Short left, Short right) {
      return (short)(left ^ right);
    }

    @Override
    public BigInteger integerValue(Short value) {
      return BigInteger.valueOf(value.longValue());
    }

    @Override
    public Short cast(Object other) {
      if(other instanceof Number)
        return ((Number)other).shortValue();
      throw new ClassCastException();
    }
    
    @Override
    @SuppressWarnings("unchecked")
    protected <O> CastOperation<? super O, ? extends Short> castFrom(
        Type<O> other) {
      if(Number.class.isAssignableFrom(other.getCanonicalClass()))
        return (CastOperation<? super O,? extends Short>)NumericCastOperation.TO_SINT16;
      return null;
    }
  }
  
  public static final class UInt16Type extends ConcreteBVIntegerType<Character> {
    UInt16Type() {
      super("uint16", Character.class, Character.valueOf('\0'), 16, false, BigInteger.valueOf(Character.MIN_VALUE), BigInteger.valueOf(Character.MAX_VALUE), SINT32, new String[]{"char"}, char.class);
    }

    @Override
    public Character shiftLeft(Character value, Character shiftAmt) {
      return (char)(value << shiftAmt);
    }

    @Override
    public Character shiftRight(Character value, Character shiftAmt) {
      return (char)(value >> shiftAmt);
    }

    @Override
    public Character shiftRightUnsigned(Character value, Character shiftAmt) {
      return (char)(value >>> shiftAmt);
    }

    @Override
    public Character not(Character value) {
      return (char)~value;
    }

    @Override
    public Character and(Character left, Character right) {
      return (char)(left & right);
    }

    @Override
    public Character or(Character left, Character right) {
      return (char)(left | right);
    }

    @Override
    public Character xor(Character left, Character right) {
      return (char)(left ^ right);
    }

    @Override
    public BigInteger integerValue(Character value) {
      return BigInteger.valueOf(value);
    }

    @Override
    public int compare(Character left, Character right) {
      return left - right;
    }

    @Override
    public Character plus(Character left, Character right) {
      return (char)(left + right);
    }

    @Override
    public Character minus(Character left, Character right) {
      return (char)(left - right);
    }

    @Override
    public Character mul(Character left, Character right) {
      return (char)(left * right);
    }

    @Override
    public Character div(Character left, Character right) {
      return (char)(left / right);
    }

    @Override
    public Character mod(Character left, Character right) {
      return (char)(left % right);
    }

    @Override
    public Character negate(Character num) {
      return (char)-num;
    }

    @Override
    public Character cast(Object other) {
      if(other instanceof Number)
        return (char)((Number)other).intValue();
      if(other instanceof Character)
        return ((Character)other).charValue();
      throw new ClassCastException("Cannot cast from " + other.getClass().getName() + " to char");
    }

    @Override
    public Character parse(String string) {
      BigInteger bi = new BigInteger(string);
      return (char)bi.intValue();
    }
  }

  public static final class SInt32Type extends ConcreteBVIntegerType<Integer> {
    SInt32Type() {
      super("sint32", Integer.class, 0, 32, true, BigInteger.valueOf(Integer.MIN_VALUE), BigInteger.valueOf(Integer.MAX_VALUE), SINT64, new String[]{"int"}, int.class); 
    }

    @Override
    public Integer parse(String string) {
      return new BigInteger(string).intValue();
    }

    @Override
    public int compare(Integer left, Integer right) {
      return left.compareTo(right);
    }

    @Override
    public Integer negate(Integer num) {
      return -num;
    }

    @Override
    public Integer shiftLeft(Integer value, Integer shiftAmt) {
      return value << shiftAmt;
    }

    @Override
    public Integer shiftRight(Integer value, Integer shiftAmt) {
      return value >> shiftAmt;
    }

    @Override
    public Integer shiftRightUnsigned(Integer value, Integer shiftAmt) {
      return value >>> shiftAmt;
    }

    @Override
    public Integer plus(Integer left, Integer right) {
      return left + right;
    }

    @Override
    public Integer minus(Integer left, Integer right) {
      return left - right;
    }

    @Override
    public Integer mul(Integer left, Integer right) {
      return left * right;
    }

    @Override
    public Integer div(Integer left, Integer right) {
      return left / right;
    }

    @Override
    public Integer mod(Integer left, Integer right) {
      return left % right;
    }

    @Override
    public Integer not(Integer value) {
      return ~value;
    }

    @Override
    public Integer and(Integer left, Integer right) {
      return left & right;
    }

    @Override
    public Integer or(Integer left, Integer right) {
      return left | right;
    }

    @Override
    public Integer xor(Integer left, Integer right) {
      return left ^ right;
    }

    @Override
    public BigInteger integerValue(Integer value) {
      return BigInteger.valueOf(value.longValue());
    }

    @Override
    public Integer cast(Object other) {
      if(other instanceof Number)
        return ((Number)other).intValue();
      throw new ClassCastException();
    }
    
    @Override
    @SuppressWarnings("unchecked")
    protected <O> CastOperation<? super O, ? extends Integer> castFrom(
        Type<O> other) {
      if(Number.class.isAssignableFrom(other.getCanonicalClass()))
        return (CastOperation<? super O,? extends Integer>)NumericCastOperation.TO_SINT32;
      return null;
    }
  }

  public static final class SInt64Type extends ConcreteBVIntegerType<Long> {
    SInt64Type() {
      super("sint64", Long.class, 0L, 64, true, BigInteger.valueOf(Long.MIN_VALUE), BigInteger.valueOf(Long.MAX_VALUE), INTEGER, new String[]{"long"}, long.class);
    }

    @Override
    public Long parse(String string) {
      return new BigInteger(string).longValue();
    }

    @Override
    public int compare(Long left, Long right) {
      return left.compareTo(right);
    }

    @Override
    public Long negate(Long num) {
      return -num;
    }

    @Override
    public Long shiftLeft(Long value, Long shiftAmt) {
      return value << shiftAmt;
    }

    @Override
    public Long shiftRight(Long value, Long shiftAmt) {
      return value >> shiftAmt;
    }

    @Override
    public Long shiftRightUnsigned(Long value, Long shiftAmt) {
      return value >>> shiftAmt;
    }

    @Override
    public Long plus(Long left, Long right) {
      return left + right;
    }

    @Override
    public Long minus(Long left, Long right) {
      return left - right;
    }

    @Override
    public Long mul(Long left, Long right) {
      return left * right;
    }

    @Override
    public Long div(Long left, Long right) {
      return left / right;
    }

    @Override
    public Long mod(Long left, Long right) {
      return left % right;
    }

    @Override
    public Long not(Long value) {
      return ~value;
    }

    @Override
    public Long and(Long left, Long right) {
      return left & right;
    }

    @Override
    public Long or(Long left, Long right) {
      return left | right;
    }

    @Override
    public Long xor(Long left, Long right) {
      return left ^ right;
    }

    @Override
    public BigInteger integerValue(Long value) {
      return BigInteger.valueOf(value.longValue());
    }

    @Override
    public Long cast(Object other) {
      if(other instanceof Number)
        return ((Number)other).longValue();
      throw new ClassCastException();
    }
    
    @Override
    @SuppressWarnings("unchecked")
    protected <O> CastOperation<? super O, ? extends Long> castFrom(
        Type<O> other) {
      if(Number.class.isAssignableFrom(other.getCanonicalClass()))
        return (CastOperation<? super O,? extends Long>)NumericCastOperation.TO_SINT64;
      return null;
    }
  }

  public static final class FloatType extends ConcreteFloatingPointType<Float> {
    FloatType() {
      super("float", Float.class, 0.0f, true, 23, BigDecimal.valueOf(-Float.MAX_VALUE), BigDecimal.valueOf(Float.MAX_VALUE), DOUBLE, new String[]{"float32"}, float.class);
    }

    @Override
    public Float parse(String string) {
      return new BigDecimal(string).floatValue();
    }

    @Override
    public int compare(Float left, Float right) {
      return left.compareTo(right);
    }

    @Override
    public Float negate(Float num) {
      return -num;
    }

    @Override
    public Float plus(Float left, Float right) {
      return left + right;
    }

    @Override
    public Float minus(Float left, Float right) {
      return left - right;
    }

    @Override
    public Float mul(Float left, Float right) {
      return left * right;
    }

    @Override
    public Float div(Float left, Float right) {
      return left / right;
    }

    @Override
    public Float mod(Float left, Float right) {
      return left % right;
    }


    @Override
    public BigDecimal decimalValue(Float value) {
      return BigDecimal.valueOf(value.doubleValue());
    }

    @Override
    public Float cast(Object other) {
      if(other instanceof Number)
        return ((Number)other).floatValue();
      throw new ClassCastException();
    }
    
    @Override
    @SuppressWarnings("unchecked")
    protected <O> CastOperation<? super O, ? extends Float> castFrom(
        Type<O> other) {
      if(Number.class.isAssignableFrom(other.getCanonicalClass()))
        return (CastOperation<? super O,? extends Float>)NumericCastOperation.TO_FLOAT;
      return null;
    }
  }

  public static final class DoubleType extends ConcreteFloatingPointType<Double> {
    DoubleType() {
      super("double", Double.class, 0.0, true, 52, BigDecimal.valueOf(-Double.MAX_VALUE), BigDecimal.valueOf(Double.MAX_VALUE), DECIMAL, new String[]{"float64"}, double.class);
    }

    @Override
    public Double parse(String string) {
      return new BigDecimal(string).doubleValue();
    }

    @Override
    public int compare(Double left, Double right) {
      return left.compareTo(right);
    }

    @Override
    public Double negate(Double num) {
      return -num;
    }

    @Override
    public Double plus(Double left, Double right) {
      return left + right;
    }

    @Override
    public Double minus(Double left, Double right) {
      return left - right;
    }

    @Override
    public Double mul(Double left, Double right) {
      return left * right;
    }

    @Override
    public Double div(Double left, Double right) {
      return left / right;
    }

    @Override
    public Double mod(Double left, Double right) {
      return left % right;
    }

    @Override
    public BigDecimal decimalValue(Double value) {
      return BigDecimal.valueOf(value.doubleValue());
    }

    @Override
    public Double cast(Object other) {
      if(other instanceof Number)
        return ((Number)other).doubleValue();
      throw new ClassCastException();
    }
    
    @Override
    @SuppressWarnings("unchecked")
    protected <O> CastOperation<? super O, ? extends Double> castFrom(
        Type<O> other) {
      if(Number.class.isAssignableFrom(other.getCanonicalClass()))
        return (CastOperation<? super O,? extends Double>)NumericCastOperation.TO_DOUBLE;
      return null;
    }
  }

  public static final class BigIntegerType extends ConcreteIntegerType<BigInteger> {
    BigIntegerType() {
      super("integer", BigInteger.class, BigInteger.ZERO, true, null, null, DECIMAL, new String[]{"BigInteger"});
    }

    @Override
    public BigInteger parse(String string) {
      return new BigInteger(string);
    }

    @Override
    public int compare(BigInteger left, BigInteger right) {
      return left.compareTo(right);
    }

    @Override
    public BigInteger negate(BigInteger num) {
      return num.negate();
    }

    @Override
    public BigInteger plus(BigInteger left, BigInteger right) {
      return left.add(right);
    }

    @Override
    public BigInteger minus(BigInteger left, BigInteger right) {
      return left.add(right);
    }

    @Override
    public BigInteger mul(BigInteger left, BigInteger right) {
      return left.multiply(right);
    }

    @Override
    public BigInteger div(BigInteger left, BigInteger right) {
      return left.divide(right);
    }

    @Override
    public BigInteger mod(BigInteger left, BigInteger right) {
      return left.remainder(right);
    }

    @Override
    public BigInteger integerValue(BigInteger value) {
      return value;
    }

    @Override
    public BigInteger cast(Object other) {
      if(other instanceof BigInteger)
        return (BigInteger)other;
      if(other instanceof BigDecimal)
        return ((BigDecimal)other).toBigInteger();
      if(other instanceof Number)
        return BigInteger.valueOf(((Number)other).longValue());
      throw new ClassCastException();
    }
    
    @Override
    @SuppressWarnings("unchecked")
    protected <O> CastOperation<? super O, ? extends BigInteger> castFrom(
        Type<O> other) {
      if(Number.class.isAssignableFrom(other.getCanonicalClass()))
        return (CastOperation<? super O,? extends BigInteger>)NumericCastOperation.TO_INTEGER;
      return null;
    }
  }

  public static final class BigDecimalType extends ConcreteRealType<BigDecimal> {
    BigDecimalType() {
      super("decimal", BigDecimal.class, BigDecimal.ZERO, true, null, null, null, new String[]{"BigDecimal"});
    }

    @Override
    public BigDecimal parse(String string) {
      return new BigDecimal(string);
    }

    @Override
    public int compare(BigDecimal left, BigDecimal right) {
      return left.compareTo(right);
    }

    @Override
    public BigDecimal negate(BigDecimal num) {
      return num.negate();
    }

    @Override
    public BigDecimal plus(BigDecimal left, BigDecimal right) {
      return left.add(right);
    }

    @Override
    public BigDecimal minus(BigDecimal left, BigDecimal right) {
      return left.subtract(right);
    }

    @Override
    public BigDecimal mul(BigDecimal left, BigDecimal right) {
      return left.multiply(right);
    }

    @Override
    public BigDecimal div(BigDecimal left, BigDecimal right) {
      return left.divide(right);
    }

    @Override
    public BigDecimal mod(BigDecimal left, BigDecimal right) {
      return left.remainder(right);
    }

    @Override
    public BigDecimal decimalValue(BigDecimal value) {
      return value;
    }

    @Override
    public BigDecimal cast(Object other) {
      if(other instanceof BigDecimal)
        return (BigDecimal)other;
      if(other instanceof BigInteger)
        return new BigDecimal((BigInteger)other);
      if(other instanceof Number)
        return BigDecimal.valueOf(((Number)other).doubleValue());
      throw new ClassCastException();
    }
    
    @Override
    @SuppressWarnings("unchecked")
    protected <O> CastOperation<? super O, ? extends BigDecimal> castFrom(
        Type<O> other) {
      if(Number.class.isAssignableFrom(other.getCanonicalClass()))
        return (CastOperation<? super O,? extends BigDecimal>)NumericCastOperation.TO_DECIMAL;
      return null;
    }
  }

  public static final class BoolType extends ConcreteType<Boolean> {
    BoolType() {
      super("bool", Boolean.class, false, null, new String[]{"boolean"}, boolean.class);
    }

    @Override
    public Boolean parse(String string) {
      return Boolean.parseBoolean(string);
    }

    @Override
    public Boolean cast(Object other) {
      if(other instanceof Boolean)
        return (Boolean)other;
      throw new ClassCastException();
    }
  }

  public static final BoolType BOOL = new BoolType();
  public static final BigDecimalType DECIMAL = new BigDecimalType();
  public static final BigIntegerType INTEGER = new BigIntegerType();
  public static final DoubleType DOUBLE = new DoubleType();
  public static final FloatType FLOAT = new FloatType();
  public static final SInt64Type SINT64 = new SInt64Type();
  public static final SInt32Type SINT32 = new SInt32Type();
  public static final SInt16Type SINT16 = new SInt16Type();
  public static final UInt16Type UINT16 = new UInt16Type(); 
  public static final SInt8Type SINT8 = new SInt8Type();
  
  static final Type<?>[] BUILTIN_TYPES = new Type<?>[]{
    BOOL,
    DECIMAL,
    INTEGER,
    DOUBLE,
    FLOAT,
    SINT64,
    SINT32,
    SINT16,
    UINT16,
    SINT8
  };

  private BuiltinTypes() {}

} public class ExpressionUtil {
  
  public static final Constant<Boolean> FALSE = Constant.create(BuiltinTypes.BOOL, Boolean.FALSE);
  public static final Constant<Boolean> TRUE = Constant.create(BuiltinTypes.BOOL, Boolean.TRUE);
  
  public static Constant<Boolean> boolConst(boolean val) {
    return val ? TRUE : FALSE;
  }
  
  
  public static boolean isConstant(Expression<?> expr, Object value) {
    if(!(expr instanceof Constant))
      return false;
    Constant<?> cnst = (Constant<?>)expr;
    return Objects.equals(cnst.getValue(), value);
  }
  
  public static boolean isBoolConst(Expression<?> expr, boolean value) {
    return isConstant(expr, Boolean.valueOf(value));
  }
  
  public static boolean isTrue(Expression<?> expr) {
    return isBoolConst(expr, true);
  }
  
  public static boolean isFalse(Expression<?> expr) {
    return isBoolConst(expr, false); 
  }

  
  public static boolean containsVars(Expression<?> e) {
    return ContainsVarsVisitor.getInstance().apply(e);
  }
  
  public static <E> Expression<E> simplify(Expression<E> e) {
    return ExpressionSimplificationVisitor.getInstance().simplify(e);
  }
  
  
  public static <E> Expression<E> stripPrefix(Expression<E> e, String prefix) {
    return StripPrefixVisitor.INSTANCE.apply(e, prefix);
  }
  
  public static <E> Expression<E> addPrefix(Expression<E> e, String prefix) {
    return AddPrefixVisitor.INSTANCE.apply(e, prefix);
  }
  
  public static Set<Variable<?>> freeVariables(Expression<?> e) {
    Set<Variable<?>> vars = new HashSet<Variable<?>>();
    e.collectFreeVariables(vars);
    return vars;
  }

  public static Valuation stripPrefix(Valuation v, String prefix) {
    Valuation ret = new Valuation();
    for(ValuationEntry<?> e : v) 
      stripEntryPrefix(e, prefix, ret);
    return ret;
  }
  
  private static <E> void stripEntryPrefix(ValuationEntry<E> entry, String prefix, Valuation target) {
    Variable<E> var = entry.getVariable();
    String name = var.getName();
    if(name.startsWith(prefix))
      var = Variable.create(var.getType(), name.substring(prefix.length()));
    target.setValue(var, entry.getValue());
  }
  
  public static Expression<Boolean> combine(LogicalOperator op, Expression<Boolean> def, Iterable<? extends Expression<Boolean>> expressions) {
    Iterator<? extends Expression<Boolean>> it = expressions.iterator();
    
    
    if(!it.hasNext())
      return def;
    
    Expression<Boolean> curr = it.next();

    while(it.hasNext()) {
      Expression<Boolean> next = it.next();
      curr = new PropositionalCompound(curr, op, next);
    }
    
    return curr;
  }
  
  @SafeVarargs
  public static Expression<Boolean> or(Expression<Boolean> ...expressions) {
    return or(Arrays.asList(expressions));
  }
  
  public static Expression<Boolean> or(Iterable<? extends Expression<Boolean>> expressions) {
    return combine(LogicalOperator.OR, FALSE, expressions);
  }
  
  @SafeVarargs
  public static Expression<Boolean> and(Expression<Boolean> ...expressions) {
    return and(Arrays.asList(expressions));
  }
  
  public static Expression<Boolean> and(Iterable<? extends Expression<Boolean>> expressions) {
    return combine(LogicalOperator.AND, TRUE, expressions);
  }
  
  public static <T> Expression<T> restrict(Expression<T> expr, Predicate<? super Variable<?>> pred) {
    return ExpressionRestrictionVisitor.getInstance().apply(expr, pred);
  }
  
  public static <T> Expression<T> transformVars(Expression<T> expr, Function<? super Variable<?>,? extends Expression<?>> transform) {
    return TransformVarVisitor.getInstance().apply(expr, transform);
  }
  
  public static <T> Expression<T> renameVars(Expression<T> expr, Function<String,String> rename) {
    return RenameVarVisitor.getInstance().apply(expr, rename);
  }
  
  
  public static String toParseableString(Expression<?> expression) {
    Set<Variable<?>> freeVars = freeVariables(expression);
    
    if(freeVars.isEmpty())
      return expression.toString();
    
    StringBuilder sb = new StringBuilder();
    
    sb.append("declare ");
    
    try {
      boolean first = true;
      for(Variable<?> var : freeVars) {
        if(first)
          first = false;
        else
          sb.append(", ");
        var.printTyped(sb);
      }
      sb.append(" in ");
      expression.print(sb);
      
      return sb.toString();
    }
    catch(IOException ex) {
      throw new RuntimeException("Unexpected IOException while writing to a StringBuilder");
    }
  }
  
  
  public static Expression<Boolean> valuationToExpression(Valuation val) {
    Expression<Boolean> result = null;
    for(ValuationEntry<?> e : val) {
      result = addValuationEntryExpression(e, result);
    }
    return result;
  }
  
  private static <T> Expression<Boolean> addValuationEntryExpression(ValuationEntry<T> e, Expression<Boolean> expr) {
    Variable<T> var = e.getVariable();
    Type<T> type = var.getType();
    T value = e.getValue();
    Expression<Boolean> newExpr;
    if(BuiltinTypes.BOOL.equals(type)) {
      Expression<Boolean> bvar = var.as(BuiltinTypes.BOOL);
      if((Boolean)value) {
        newExpr = bvar;
      }
      else {
        newExpr = new Negation(bvar);
      }
    }
    else {
      Constant<T> cnst = Constant.create(type, value);
      newExpr = new NumericBooleanExpression(var, NumericComparator.EQ, cnst);
    }
    return (expr == null) ? newExpr : ExpressionUtil.and(newExpr, expr);
  }
  
  public static int nestingDepth(Expression<?> expr) {
    return NestingDepthVisitor.getInstance().apply(expr);
  }
  
  public static Valuation combineValuations(Iterable<? extends Valuation> vals) {
    Valuation ret = new Valuation();
    
    for(Valuation v : vals) {
      ret.putAll(v);
    }
    
    return ret;
  }
  
  public static Valuation combineValuations(Valuation ...vals) {
    return combineValuations(Arrays.asList(vals));
  }
  
  public static <T> Expression<T> partialEvaluate(Expression<T> expr, Valuation val) {
    return simplify(partialEvaluate(expr, val));
  }
  
  
  // LEGACY API
  
  @Deprecated
  @SuppressWarnings({"rawtypes","unchecked"})
  public static Set<Variable> getVariables(Expression e) {
    return (Set<Variable>)(Set)freeVariables(e); // This may not look like it's safe, but it is..
  }
  
  @Deprecated
  public static Expression<Boolean> combine(Iterable<? extends Expression<Boolean>> expressions, LogicalOperator op) {
    return combine(op, null, expressions);
  }
} @SafeVarargs
public static Expression<Boolean> and(Expression<Boolean> ...expressions) {
  return and(Arrays.asList(expressions));
}
import static gov.nasa.jpf.constraints.util.ExpressionUtil.and;
import gov.nasa.jpf.constraints.api.Expression;
import gov.nasa.jpf.constraints.api.Variable;
import gov.nasa.jpf.constraints.expressions.Constant;
import gov.nasa.jpf.constraints.expressions.IfThenElse;
import gov.nasa.jpf.constraints.expressions.QuantifierExpression;
import gov.nasa.jpf.constraints.expressions.UnaryMinus;
import gov.nasa.jpf.constraints.expressions.functions.Function;
import gov.nasa.jpf.constraints.expressions.functions.FunctionExpression;
import gov.nasa.jpf.constraints.expressions.functions.math.BinaryDoubleFunction;
import gov.nasa.jpf.constraints.expressions.functions.math.MathFunctions;
import static gov.nasa.jpf.constraints.expressions.functions.math.axioms.PropertyBuilder.*;
import gov.nasa.jpf.constraints.types.BuiltinTypes;
import gov.nasa.jpf.constraints.util.ExpressionUtil;
/*
 * Copyright (C) 2015, United States Government, as represented by the 
 * Administrator of the National Aeronautics and Space Administration.
 * All rights reserved.
 *
 * The PSYCO: A Predicate-based Symbolic Compositional Reasoning environment 
 * platform is licensed under the Apache License, Version 2.0 (the "License"); you 
 * may not use this file except in compliance with the License. You may obtain a 
 * copy of the License at http://www.apache.org/licenses/LICENSE-2.0. 
 *
 * Unless required by applicable law or agreed to in writing, software distributed 
 * under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR 
 * CONDITIONS OF ANY KIND, either express or implied. See the License for the 
 * specific language governing permissions and limitations under the License.
 */


package gov.nasa.jpf.constraints.expressions.functions.math.axioms;


public class Atan2Properties implements FunctionProperties {

    public static final Function ATAN2_LOOKUP = new BinaryDoubleFunction("atan2_lookup") {
        @Override
        protected double doEvaluate(double v1, double v2) {
            throw new UnsupportedOperationException("Not supported yet."); 
        }
    };

    public static final Function ATAN2_Y_POS = new BinaryDoubleFunction("atan2_y_pos") {
        @Override
        protected double doEvaluate(double v1, double v2) {
            throw new UnsupportedOperationException("Not supported yet."); 
        }
    };    
    
    private final int lookupSize;
    
    private final SqrtProperties sqrt;

    public Atan2Properties(int lookupSize, SqrtProperties sqrt) {
        this.lookupSize = lookupSize;
        this.sqrt = sqrt;
    }
    
    
    private Expression<Boolean> bounds(Expression x, double lower, double upper, 
            boolean openLower, boolean openUpper, Expression scale) {
        Constant cl = new Constant(BuiltinTypes.DOUBLE, lower);