content: /*
   * Kodkod -- Copyright (c) 2005-present, Emina Torlak 
   * Pardinus -- Copyright (c) 2013-present, Nuno Macedo, INESC TEC
   * 
   * Permission is hereby granted, free of charge, to any person obtaining a copy
   * of this software and associated documentation files (the "Software"), to deal
   * in the Software without restriction, including without limitation the rights
   * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
   * copies of the Software, and to permit persons to whom the Software is
   * furnished to do so, subject to the following conditions:
   * 
   * The above copyright notice and this permission notice shall be included in
   * all copies or substantial portions of the Software.
   * 
   * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
   * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
   * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
   * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
   * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
   * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
   * SOFTWARE.
   */
  package kodkod.ast;
  
  import static kodkod.ast.operator.ExprCastOperator.CARDINALITY;
  import static kodkod.ast.operator.ExprCastOperator.SUM;
  import static kodkod.ast.operator.ExprCompOperator.EQUALS;
  import static kodkod.ast.operator.ExprCompOperator.SUBSET;
  import static kodkod.ast.operator.ExprOperator.CLOSURE;
  import static kodkod.ast.operator.ExprOperator.DIFFERENCE;
  import static kodkod.ast.operator.ExprOperator.INTERSECTION;
  import static kodkod.ast.operator.ExprOperator.JOIN;
  import static kodkod.ast.operator.ExprOperator.OVERRIDE;
  import static kodkod.ast.operator.ExprOperator.PRODUCT;
  import static kodkod.ast.operator.ExprOperator.REFLEXIVE_CLOSURE;
  import static kodkod.ast.operator.ExprOperator.TRANSPOSE;
  import static kodkod.ast.operator.ExprOperator.UNION;
  import static kodkod.ast.operator.Multiplicity.LONE;
  import static kodkod.ast.operator.Multiplicity.NO;
  import static kodkod.ast.operator.Multiplicity.ONE;
  import static kodkod.ast.operator.Multiplicity.SOME;
  import static kodkod.ast.operator.TemporalOperator.PRIME;
  
  import java.util.Arrays;
  import java.util.Collection;
  import java.util.Iterator;
  
  import kodkod.ast.operator.ExprCastOperator;
  import kodkod.ast.operator.ExprCompOperator;
  import kodkod.ast.operator.ExprOperator;
  import kodkod.ast.operator.Multiplicity;
  import kodkod.ast.operator.TemporalOperator;
  import kodkod.ast.visitor.ReturnVisitor;
  import kodkod.util.collections.Containers;
  
  /** 
   * A relational expression.  Unless otherwise noted,
   * all methods in this class throw a NullPointerException when given
   * null arguments.
   * 
   * @specfield arity: int
   * @invariant arity > 0
   *
   * @author Emina Torlak 
   * @modified Eduardo Pessoa, Nuno Macedo // [HASLab] temporal model finding
   */
  public abstract class Expression extends Node {
  	
  	/** The universal relation:  contains all atoms in a {@link kodkod.instance.Universe universe of discourse}. */
  	public static final Expression UNIV = new ConstantExpression("univ", 1);
  	
  	/** The identity relation: maps all atoms in a {@link kodkod.instance.Universe universe of discourse} to themselves. */
  	public static final Expression IDEN = new ConstantExpression("iden", 2);
  	
  	/** The empty relation: contains no atoms. */
  	public static final Expression NONE = new ConstantExpression("none", 1);
  	
  	/** The integer relation: contains all atoms {@link kodkod.instance.Bounds bound} to integers */
  	public static final Expression INTS = new ConstantExpression("ints", 1);
  	
      /**
       * Constructs a leaf expression
       * @ensures no this.children'
       */
      Expression() { }
  
      /**
       * Returns the join of this and the specified expression.  The effect
       * of this method is the same as calling this.compose(JOIN, expr).
       * @return this.compose(JOIN, expr)
       */
      public final Expression join(Expression expr) {
          return compose(JOIN,expr);
      }
      
      /**
       * Returns the product of this and the specified expression.  The effect
       * of this method is the same as calling this.compose(PRODUCT, expr).
       * @return this.compose(PRODUCT, expr)
       */
      public final Expression product(Expression expr) {
          return compose(PRODUCT,expr);
      }
      
      /**
       * Returns the union of this and the specified expression.  The effect
       * of this method is the same as calling this.compose(UNION, expr).
       * @return this.compose(UNION, expr)
       */
      public final Expression union(Expression expr) {
      	return compose(UNION,expr);
      }
      
      /**
       * Returns the difference of this and the specified expression.  The effect
       * of this method is the same as calling this.compose(DIFFERENCE, expr).
       * @return this.compose(DIFFERENCE, expr)
       */
      public final Expression difference(Expression expr) {
      	return compose(DIFFERENCE,expr);
      }
      
      /**
       * Returns the intersection of this and the specified expression.  The effect
       * of this method is the same as calling this.compose(INTERSECTION, expr).
       * @return this.compose(INTERSECTION, expr)
       */
      public final Expression intersection(Expression expr) {
      	return compose(INTERSECTION,expr);
      }
      
      /**
       * Returns the relational override of this with the specified expression.  The effect
       * of this method is the same as calling this.compose(OVERRIDE, expr).
       * @return this.compose(OVERRIDE, expr)
       */
      public final Expression override(Expression expr) {
      	return compose(OVERRIDE,expr);
      }
      
      /**
       * Returns the composition of this and the specified expression, using the
       * given binary operator.
       * @requires op in ExprOperator.BINARY
       * @return {e: Expression | e.left = this and e.right = expr and e.op = this }
       */
      public final Expression compose(ExprOperator op, Expression expr) {
      	return new BinaryExpression(this, op, expr);
      }
      
      /**
       * Returns the union of the given expressions.  The effect of this method is the
       * same as calling compose(UNION, exprs).
       * @return compose(UNION, exprs)
       */
      public static Expression union(Expression...exprs) { 
      	return compose(UNION, exprs);
      }
      
      /**
       * Returns the union of the given expressions.  The effect of this method is the
       * same as calling compose(UNION, exprs).
       * @return compose(UNION, exprs)
       */
      public static Expression union(Collection<? extends Expression> exprs) { 
      	return compose(UNION, exprs);
      }
         
      /**
       * Returns the intersection of the given expressions.  The effect of this method is the
       * same as calling compose(INTERSECTION, exprs).
       * @return compose(INTERSECTION, exprs)
       */
      public static Expression intersection(Expression...exprs) { 
      	return compose(INTERSECTION, exprs);
      }
      
      /**
       * Returns the intersection of the given expressions.  The effect of this method is the
       * same as calling compose(INTERSECTION, exprs).
       * @return compose(INTERSECTION, exprs)
       */
      public static Expression intersection(Collection<? extends Expression> exprs) { 
      	return compose(INTERSECTION, exprs);
      }
      
      /**
       * Returns the product of the given expressions.  The effect of this method is the
       * same as calling compose(PRODUCT, exprs).
       * @return compose(PRODUCT, exprs)
       */
      public static Expression product(Expression...exprs) { 
      	return compose(PRODUCT, exprs);
      }
      
      /**
       * Returns the product of the given expressions.  The effect of this method is the
       * same as calling compose(PRODUCT, exprs).
       * @return compose(PRODUCT, exprs)
       */
      public static Expression product(Collection<? extends Expression> exprs) { 
      	return compose(PRODUCT, exprs);
      }
      
      /**
       * Returns the override of the given expressions.  The effect of this method is the
       * same as calling compose(OVERRIDE, exprs).
       * @return compose(OVERRIDE, exprs)
       */
      public static Expression override(Expression...exprs) { 
      	return compose(OVERRIDE, exprs);
      }
      
      /**
       * Returns the override of the given expressions.  The effect of this method is the
       * same as calling compose(OVERRIDE, exprs).
       * @return compose(OVERRIDE, exprs)
       */
      public static Expression override(Collection<? extends Expression> exprs) { 
      	return compose(OVERRIDE, exprs);
      }
      
      /**
       * Returns the composition of the given expressions using the given operator. 
       * @requires exprs.length = 2 => op.binary(), exprs.length > 2 => op.nary()
       * @return exprs.length=1 => exprs[0] else {e: Expression | e.children = exprs and e.op = this }
       */
      public static Expression compose(ExprOperator op, Expression...exprs) { 
      	switch(exprs.length) { 
      	case 0 : 	throw new IllegalArgumentException("Expected at least one argument: " + Arrays.toString(exprs));
      	case 1 : 	return exprs[0];
      	case 2 : 	return new BinaryExpression(exprs[0], op, exprs[1]);
      	default : 	return new NaryExpression(op, Containers.copy(exprs, new Expression[exprs.length]));
      	}
      }
      
      /**
       * Returns the composition of the given expressions using the given operator. 
       * @requires exprs.size() = 2 => op.binary(), exprs.size() > 2 => op.nary()
       * @return exprs.size()=1 => exprs.iterator().next() else {e: Expression | e.children = exprs.toArray() and e.op = this }
       */
      public static Expression compose(ExprOperator op, Collection<? extends Expression> exprs) { 
      	switch(exprs.size()) { 
      	case 0 : 	throw new IllegalArgumentException("Expected at least one argument: " + exprs);
      	case 1 : 	return exprs.iterator().next();
      	case 2 :
      		final Iterator<? extends Expression> itr = exprs.iterator();
      		return new BinaryExpression(itr.next(), op, itr.next());
      	default : 			
      		return new NaryExpression(op, exprs.toArray(new Expression[exprs.size()]));
      	}
      }
      
      
      
      /**
       * Returns the transpose of this.  The effect of this method is the same
       * as calling this.apply(TRANSPOSE).
       * @return this.apply(TRANSPOSE)
       */
      public final Expression transpose() {
          return apply(TRANSPOSE);
      }
      
      /**
       * Returns the transitive closure of this.  The effect of this  method is the same
       * as calling this.apply(CLOSURE).
       * @return this.apply(CLOSURE)
       */
      public final Expression closure() {
          return apply(CLOSURE);
      }
      
      /**
       * Returns the reflexive transitive closure of this.  The effect of this 
       * method is the same
       * as calling this.apply(REFLEXIVE_CLOSURE).
       * @return this.apply(REFLEXIVE_CLOSURE)
       */
      public final Expression reflexiveClosure() {
      	return apply(REFLEXIVE_CLOSURE);
      }
      
      /**
       * Returns the primed version of this.  The effect of this 
       * method is the same
       * as calling this.apply(PRIME).
       * @return this.apply(PRIME)
       */
      public final Expression prime() {
      	return apply(PRIME);
      }
      
      /**
       * Returns the expression that results from applying the given unary operator
       * to this.  
       * @requires op.unary()
       * @return {e: Expression | e.expression = this && e.op = this }
       * @throws IllegalArgumentException  this.arity != 2
       */
      public final Expression apply(ExprOperator op) {
      	return new UnaryExpression(op, this);
      }
  
      /**
       * Returns the expression that results from applying the given unary temporal operator
       * to this.  
       * @requires op.unary()
       * @return {e: Expression | e.expression = this && e.op = this }
       * @throws IllegalArgumentException  this.arity != 1
       */
      // [HASLab]
      public final Expression apply(TemporalOperator op) {
      	return new TempExpression(op, this);
      }
  
      /**
       * Returns the projection of this expression onto the specified columns.
       * @return {e: Expression | e = project(this, columns) }
       * @throws IllegalArgumentException  columns.length < 1
       */
      public final Expression project(IntExpression... columns) {
      	return new ProjectExpression(this, columns);
      }
      
      /**
       * Returns the cardinality of this expression.  The effect of this method is the
       * same as calling this.apply(CARDINALITY).  
       * @return this.apply(CARDINALITY)
       */
      public final IntExpression count() {
      	return apply(CARDINALITY);
      }
      
      /**
       * Returns the sum of the integer atoms in this expression.  The effect of this method is the
       * same as calling this.apply(SUM).  
       * @return this.apply(SUM)
       */
      public final IntExpression sum() {
      	return apply(SUM);
      }
      
      /**
       * Returns the cast of this expression to an integer expression,
       * that represents either the cardinality of this expression (if op is CARDINALITY)
       * or the sum of the integer atoms it contains (if op is SUM).
       * @return {e: IntExpression | e.op = op && e.expression = this} 
       */
      public final IntExpression apply(ExprCastOperator op) { 
      	return new ExprToIntCast(this, op);
      }
      
      /**
       * Returns the formula 'this = expr'. The effect of this method is the same 
       * as calling this.compare(EQUALS, expr).
       * @return this.compare(EQUALS, expr)
       */
      public final Formula eq(Expression expr) {
      	return compare(EQUALS, expr);
      }
      
      /**
       * Returns the formula 'this in expr'.  The effect of this method is the same 
       * as calling this.compare(SUBSET, expr).
       * @return this.compare(SUBSET, expr)
       */
      public final Formula in(Expression expr) {
      	return compare(SUBSET, expr);
      }
      
      /**
       * Returns the formula that represents the comparison of this and the
       * given expression using the given comparison operator.
       * @return {f: Formula | f.left = this && f.right = expr  && f.op = op}
       */
      public final Formula compare(ExprCompOperator op, Expression expr) {
      	return new ComparisonFormula(this, op, expr);
      }
      
      /**
       * Returns the formula 'some this'.  The effect of this method is the same as calling
       * this.apply(SOME).
       * @return this.apply(SOME)
       */
      public final Formula some() {
          return apply(SOME);
      }
      
      /**
       * Returns the formula 'no this'.  The effect of this method is the same as calling
       * this.apply(NO).
       * @return this.apply(NO)
       */
      public final Formula no() {
          return apply(NO);
      }
      
      /**
       * Returns the formula 'one this'.  The effect of this method is the same as calling
       * this.apply(ONE).
       * @return this.apply(ONE)
       */
      public final Formula one() {
          return apply(ONE);
      }
      
      /**
       * Returns the formula 'lone this'.  The effect of this method is the same as calling
       * this.apply(LONE).
       * @return this.apply(LONE)
       */
      public final Formula lone() {
          return apply(LONE);
      }
      
      /**
       * Returns the formula that results from applying the specified multiplicity to
       * this expression.  The SET multiplicity is not allowed.
       * @return {f: Formula | f.multiplicity = mult && f.expression = this}
       * @throws IllegalArgumentException  mult = SET
       */
      public final Formula apply(Multiplicity mult) {
      	return new MultiplicityFormula(mult, this);
      }
      
      /**
       * Returns the arity of this expression.
       * @return this.arity
       */
      public abstract int arity();
          
      /**
       * Accepts the given visitor and returns the result.
       * @see kodkod.ast.Node#accept(kodkod.ast.visitor.ReturnVisitor)
       */
      public abstract <E, F, D, I> E accept(ReturnVisitor<E, F, D, I> visitor);
   }
  