content: /**
   * 
   */
  package kodkod.examples.tptp;
  import static kodkod.ast.Expression.UNIV;
  
  import java.util.ArrayList;
  import java.util.List;
  
  import kodkod.ast.Expression;
  import kodkod.ast.Formula;
  import kodkod.ast.Relation;
  import kodkod.ast.Variable;
  import kodkod.engine.Solution;
  import kodkod.engine.Solver;
  import kodkod.engine.satlab.SATFactory;
  import kodkod.instance.Bounds;
  import kodkod.instance.Universe;
  
  /**
   * A KK encoding of ALG212+1.p from http://www.cs.miami.edu/~tptp/
   * @author Emina Torlak
   */
  public final class ALG212 {
  	private final Relation f;
  	
  	/**
  	 * Constucts a new instance of ALG212.
  	 */
  	public ALG212() {
  		f = Relation.nary("f", 4);
  	}
  	
  	/**
  	 * Returns the declarations.
  	 * @return declarations.
  	 */
  	public final Formula decls() {
  		// all x,y,z: univ | one f[x][y][z] 
  		final Variable x = Variable.unary("x");
  		final Variable y = Variable.unary("y");
  		final Variable z = Variable.unary("z");
  		final Formula f0 = z.join(y.join(x.join(f))).one();
  		return f0.forAll(x.oneOf(UNIV).and(y.oneOf(UNIV)).and(z.oneOf(UNIV)));
  	}
  	
  	/**
  	 * Returns the majority axiom.
  	 * @return majority
  	 */
  	public final Formula majority() {
  		// all x, y: A | f[x][x][y] = x
  		final Variable x = Variable.unary("x");
  		final Variable y = Variable.unary("y");
  		return y.join(x.join(x.join(f))).eq(x).forAll(x.oneOf(UNIV).and(y.oneOf(UNIV)));
  	}
  	
  	/**
  	 * Returns the permute1 axiom.
  	 * @return permute1
  	 */
  	public final Formula permute1() {
  		// all x, y, z: A | f[x][y][z] = f[z][x][y]
  		final Variable x = Variable.unary("x");
  		final Variable y = Variable.unary("y");
  		final Variable z = Variable.unary("z");
  		final Formula f0 = z.join(y.join(x.join(f))).eq(y.join(x.join(z.join(f))));
  		return f0.forAll(x.oneOf(UNIV).and(y.oneOf(UNIV)).and(z.oneOf(UNIV)));
  	}
  	
  	/**
  	 * Returns the permute2 axiom.
  	 * @return permute2
  	 */
  	public final Formula permute2() {
  		// all x, y, z: A | f[x][y][z] = f[x][z][y]
  		final Variable x = Variable.unary("x");
  		final Variable y = Variable.unary("y");
  		final Variable z = Variable.unary("z");
  		final Formula f0 = z.join(y.join(x.join(f))).eq(y.join(z.join(x.join(f))));
  		return f0.forAll(x.oneOf(UNIV).and(y.oneOf(UNIV)).and(z.oneOf(UNIV)));
  	}
  	
  	/**
  	 * Returns the associativity axiom.
  	 * @return associativity
  	 */
  	public final Formula associativity() {
  		// all w, x, y, z: A | f[f[x][w][y]][w][z] = f[x][w][f[y][w][z]]
  		final Variable w = Variable.unary("w");
  		final Variable x = Variable.unary("x");
  		final Variable y = Variable.unary("y");
  		final Variable z = Variable.unary("z");
  		final Expression e0 = y.join(w.join(x.join(f)));
  		final Expression e1 = z.join(w.join(e0.join(f)));
  		final Expression e2 = z.join(w.join(y.join(f)));
  		final Expression e3 = e2.join(w.join(x.join(f)));
  		return e1.eq(e3).forAll(w.oneOf(UNIV).and(x.oneOf(UNIV)).and(y.oneOf(UNIV)).and(z.oneOf(UNIV)));
  	}
  	
  	/**
  	 * Returns the conjuction of all axioms.
  	 * @return axioms
  	 */
  	public final Formula axioms() { 
  		return decls().and(majority()).and(permute1()).and(permute2()).and(associativity());
  	}
  	
  	/**
  	 * Returns the dist_long conjecture.
  	 * @return dist_long
  	 */
  	public final Formula distLong() {
  		// all u, w, x, y, z: A | f[f[x][y][z]][u][w] = f[f[x][u][w]][f[y][u][w]][f[z][u][w]]
  		final Variable u = Variable.unary("u");
  		final Variable w = Variable.unary("w");
  		final Variable x = Variable.unary("x");
  		final Variable y = Variable.unary("y");
  		final Variable z = Variable.unary("z");
  		final Expression e0 =  z.join(y.join(x.join(f)));
  		final Expression e1 = w.join(u.join(e0.join(f)));
  		final Expression e2 = w.join(u.join(x.join(f)));
  		final Expression e3 = w.join(u.join(y.join(f)));
  		final Expression e4 = w.join(u.join(z.join(f)));
  		final Expression e5 = e4.join(e3.join(e2.join(f)));
  		return e1.eq(e5).
  		  forAll(u.oneOf(UNIV).and(w.oneOf(UNIV)).and(x.oneOf(UNIV)).and(y.oneOf(UNIV)).and(z.oneOf(UNIV)));
  	}
  	
  	/**
  	 * Returns the conjunction of the axioms and the negation of the hypothesis.
  	 * @return axioms() && !distLong()
  	 */
  	public final Formula checkDistLong() { 
  		return axioms().and(distLong().not());
  	}
  	
  	/**
  	 * Returns the bounds for the given scope.
  	 * @return bounds for the given scope
  	 */
  	public final Bounds bounds(int n) {
  		assert n > 0;
  		final List<String> atoms = new ArrayList<String>(n);
  		for(int i = 0; i < n; i++) atoms.add("a"+i);
  		final Universe u = new Universe(atoms);
  		final Bounds b = new Bounds(u);
  		b.bound(f, u.factory().allOf(4));
  		return b;
  	}
  	
  	private static void usage() {
  		System.out.println("java examples.tptp.ALG212 [univ size]");
  		System.exit(1);
  	}
  	
  	/**
  	 * Usage: java examples.tptp.ALG212 [univ size]
  	 */
  	public static void main(String[] args) {
  		if (args.length < 1)
  			usage();
  		
  		try {
  			final int n = Integer.parseInt(args[0]);
  			if (n < 1)
  				usage();
  			final ALG212 model = new ALG212();
  			final Solver solver = new Solver();
  			solver.options().setSolver(SATFactory.DEFAULT);
  //			solver.options().setSymmetryBreaking(n*n);
  //			solver.options().setFlatten(false);
  			final Formula f = model.checkDistLong();
  			final Bounds b = model.bounds(n);
  			System.out.println(f);
  			final Solution sol = solver.solve(f, b);
  			System.out.println(sol);
  		} catch (NumberFormatException nfe) {
  			usage();
  		}
  	}
  	
  }
  