content: /**
   * 
   */
  package kodkod.examples.tptp;
  
  import static kodkod.ast.Expression.UNIV;
  
  import java.util.ArrayList;
  import java.util.List;
  
  import kodkod.ast.Decls;
  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.TupleFactory;
  import kodkod.instance.TupleSet;
  import kodkod.instance.Universe;
  
  /**
   * A KK encoding of NUM378+1.020.015.p from http://www.cs.miami.edu/~tptp/
   * 
   * @author Emina Torlak
   */
  public final class NUM378 {
  	private final Relation succ, sum;
  	
  	/**
  	 * Constructs a new instance of NUM378.
  	 */
  	public NUM378() {
  		succ = Relation.binary("succ");
  		sum = Relation.ternary("sum");
  	}
  	
  	/**
  	 * Returns the expression y.(x.sum)
  	 * @return y.(x.sum)
  	 */
  	final Expression sum(Expression x, Expression y) {
  		return y.join(x.join(sum));
  	}
  	
  	/**
  	 * Returns the successor of x.
  	 * @return x.succ
  	 */
  	final Expression succ(Expression x) {
  		return x.join(succ);
  	}
  	
  	/**
  	 * Returns the predecessor of x.
  	 * @return succ.x
  	 */
  	final Expression pred(Expression x) {
  		return succ.join(x);
  	}
  	
  	/**
  	 * Returns the declarations.
  	 * @return one a && one b && one c
  	 */
  	public final Formula decls() { 
  		final Variable x = Variable.unary("X");
  		final Variable y = Variable.unary("Y");
  		return succ.function(UNIV, UNIV).
  			and(sum(x,y).one().forAll(x.oneOf(UNIV).and(y.oneOf(UNIV))));
  	}
  	
  	private final Variable[] vars(String name, int size) {
  		final Variable[] vars = new Variable[size];
  		for(int i = 0; i < size; i++) {
  			vars[i] = Variable.unary(name + i);
  		}
  		return vars;
  	}
  	
  	private final Decls decls(Variable[] vars) {
  		Decls d = vars[0].oneOf(UNIV);
  		for(int i = 1; i < vars.length; i++) {
  			d = d.and(vars[i].oneOf(UNIV));
  		}
  		return d;
  	}
  	
  	/**
  	 * Returns the try_satisfy_this axiom.
  	 * @return try_satisfy_this
  	 */
  	public final Formula inequalities() {
  		final Variable[] x = vars("X",16);
  		final Variable[] y = vars("Y",16);
  		final Variable[] npx = vars("NPX",15);
  		final Variable[] nsx = vars("NSX",15);
  		final Variable[] npy = vars("NPY",15);
  		final Variable[] nsy = vars("NSY",15);
  		
  		Expression s21 = succ;
  		for(int i = 1; i < 21; i++) {
  			s21 = s21.join(succ);
  		}
  		
  		Formula f = Formula.TRUE;
  		
  		for(int i = 0; i < 15; i++) {
  			Formula f0 = npx[i].eq(s21.join(x[i]));
  			Formula f1 = nsx[i].eq(x[i].join(s21));
  			Formula f2 = npy[i].eq(s21.join(y[i]));
  			Formula f3 = nsy[i].eq(y[i].join(s21));
  			f = f.and(f0).and(f1).and(f2).and(f3);
  		}
  		
  		for(int i = 1; i < 16; i++) {
  			Formula f0 = x[i].eq(sum(sum(pred(x[i-1]),succ(y[i-1])),sum(pred(y[i-1]),succ(x[i-1]))));
  			Formula f1 = y[i].eq(sum(pred(nsx[i-1]),sum(succ(npx[i-1]),sum(pred(nsy[i-1]),succ(npy[i-1])))));
  			f = f.and(f0).and(f1);
  		}
  		
  		Formula g = Formula.FALSE;
  		for(int i = 12; i < 16; i++) {
  			g = g.or(x[i].eq(y[i]).not());
  		}
  
  		return f.and(g).
  			forSome(decls(x).and(decls(y)).and(decls(npx)).and(decls(nsx)).and(decls(npy)).and(decls(nsy)));
  	}
  	
  	/**
  	 * Returns the conjunction of the axioms and the hypothesis.
  	 * @return axioms() && inequalities()
  	 */
  	public final Formula checkInequalities() { 
  		return decls().and(inequalities());
  	}
  	
  	/**
  	 * Returns bounds for the problem.
  	 * @return bounds for the problem.
  	 */
  	public final Bounds bounds() {
  		final int n = 21;
  		final List<String> atoms = new ArrayList<String>(n);
  		atoms.add("goal");
  		for(int i = 0; i < n; i++)
  			atoms.add("n"+i);
  		final Universe u = new Universe(atoms);
  		final Bounds bound = new Bounds(u);
  		final TupleFactory f = u.factory();
  		
  		final TupleSet succBound = f.noneOf(2);
  		for(int i = 0; i < n; i++) {
  			succBound.add(f.tuple("n"+i,"n"+((i+1)%n)));
  		}
  		bound.boundExactly(succ, succBound);
  		
  		final TupleSet sumBound = f.noneOf(3);
  		for(int i = 0; i < n; i++) {
  			for(int j = 0; j < n; j++) {
  				sumBound.add(f.tuple("n"+i, "n"+j, "n"+((i+j)%n)));
  			}
  		}
  		bound.boundExactly(sum, sumBound);
  		return bound;
  	}
  	
  	private static void usage() {
  		System.out.println("java examples.tptp.NUM378");
  		System.exit(1);
  	}
  	
  	/**
  	 * Usage: java examples.tptp.NUM378
  	 */
  	public static void main(String[] args) {
  	
  		try {
  	
  			final NUM378 model = new NUM378();
  			final Solver solver = new Solver();
  			solver.options().setSolver(SATFactory.DEFAULT);
  			final Formula f = model.decls().and(model.inequalities());
  			final Bounds b = model.bounds();
  //			System.out.println(f);
  //			System.out.println(b);
  			final Solution sol = solver.solve(f, b);
  			System.out.println(sol.outcome());
  			System.out.println(sol.stats());
  		} catch (NumberFormatException nfe) {
  			usage();
  		}
  	}
  	
  }
  