<commit_before>package examples;

import kodkod.ast.Formula;
import kodkod.ast.Relation;

/**
 * A toy implementation of the Kemeny rank aggregation function.
 * 
 * @author <NAME>
 */
public final class RankAggregation {
	private final Relation[] rankings;
	private final Relation kemeny, kfirst, klast, elts;
	
	/**
	 * Constructs a RankAggregation model for finding the Kemeny rank
	 * for the given number of rankings.
	 */
	public RankAggregation(int numRankings) {
		assert numRankings > 0;
		this.rankings = new Relation[numRankings];
		for(int i = 0; i < numRankings; i++)
			rankings[i] = Relation.binary("r"+i);
		this.kemeny = Relation.binary("kemeny");
		this.kfirst = Relation.unary("kfirst");
		this.klast = Relation.unary("klast");
		this.elts = Relation.unary("elts");
	}

	/**
	 * Returns a formula stating that the kemeny relation imposes a total
	 * on the universe.
	 * @return a formula stating that the kemeny relation imposes a total
	 * on the universe.
	 */
	public Formula declarations() {
		return kemeny.totalOrder(elts, kfirst, klast);
	}
	
	/**
	 * Returns a formula stating that the kemeny relation is locally minimal.
	 * @return a formula stating that the kemeny relation is locally minimal.
	 */
	public Formula locallyMinimal() {
		return null;
	}
	
}	<commit_msg>Incorporated bug fix to zchaff mincost<commit_after>package examples;

import java.util.ArrayList;
import java.util.Collections;
import java.util.List;
import java.util.Random;

import kodkod.ast.Expression;
import kodkod.ast.Formula;
import kodkod.ast.Relation;
import kodkod.ast.Variable;
import kodkod.engine.Cost;
import kodkod.engine.Solution;
import kodkod.engine.Solver;
import kodkod.engine.TimeoutException;
import kodkod.engine.satlab.SATFactory;
import kodkod.instance.Bounds;
import kodkod.instance.TupleFactory;
import kodkod.instance.TupleSet;
import kodkod.instance.Universe;

/**
 * A toy implementation of the Kemeny rank aggregation function.
 * 
 * @author <NAME>
 */
public final class RankAggregation {
	private final Relation[] rankings;
	private final Relation kemeny, cost, kfirst, klast, elts;
	
	/**
	 * Constructs a RankAggregation model for finding the Kemeny rank
	 * for the given number of rankings.
	 */
	public RankAggregation(int numRankings) {
		assert numRankings > 0;
		this.rankings = new Relation[numRankings];
		for(int i = 0; i < numRankings; i++)
			rankings[i] = Relation.binary("r"+i);
		this.kemeny = Relation.binary("kemeny");
		this.kfirst = Relation.unary("kfirst");
		this.klast = Relation.unary("klast");
		this.cost = Relation.binary("cost");
		this.elts = Relation.unary("elts");
	}

	/**
	 * Returns a formula stating that the kemeny relation imposes a total
	 * on the universe.
	 * @return a formula stating that the kemeny relation imposes a total
	 * on the universe.
	 */
	public Formula declarations() {
		return kemeny.totalOrder(elts, kfirst, klast);
	}
	
	/**
	 * Returns a formula defining the kemeny relation in terms of a cost function.
	 * @return a formula defining the kemeny relation in terms of a cost function.
	 */
	public Formula kemeny() {
		final Variable e = Variable.unary("e");
		Expression r = rankings[0].closure();
		for(int i = 1; i < rankings.length; i++) {
			r = r.union(rankings[i].closure());
		}
		return e.join(cost).eq(e.join(kemeny.closure()).intersection(r.join(e))).forAll(e.oneOf(elts));
	}
	
	/**
	 * Returns the cost function that needs to be minimized during solving.
	 * @return the cost function that needs to be minimized during solving.
	 */
	public Cost cost() {
		return new Cost() {

			public int edgeCost(Relation relation) {
				return relation==cost ? 2: 0;
			}
			
		};
	}
	
	/**
	 * Returns the conjunction of declarations() and kemeny().
	 * @return declarations() && kemeny()
	 */
	public Formula show() { 
		return declarations().and(kemeny());
	}
	
	/**
	 * Returns a bounds for a random universe of the given size.
	 * @requires usize > 1
	 * @return bounds for a random universe of the given size
	 */
	public Bounds bounds(int usize) {
		assert usize > 1;
		final List<String> atoms = new ArrayList<String>(usize);
		for(int i = 0; i < usize; i++) {
			atoms.add(String.valueOf(i));
		}
		final Universe u = new Universe(atoms);
		final TupleFactory f = u.factory();
		final Bounds b = new Bounds(u);
		
		b.boundExactly(elts, f.allOf(1));
		b.bound(kfirst, b.upperBound(elts));
		b.bound(klast, b.upperBound(elts));
		final TupleSet kbound = f.noneOf(2);
		for(int i = 0; i < usize; i ++) {
			for(int j = 0; j < usize; j++) {
				if (i!=j) {
					kbound.add(f.tuple(atoms.get(i), atoms.get(j)));
				}
			}
		}
		b.bound(kemeny, kbound);
		b.bound(cost, f.allOf(2));
		
//		final int rsize = (int)StrictMath.ceil(usize*.75);
		final long seed = System.currentTimeMillis();
		final Random rand = new Random(seed);
		System.out.println(seed);
		for(Relation r : rankings) {
			Collections.shuffle(atoms, rand);
			TupleSet rbound = f.noneOf(2);
			for(int i = 1; i < usize; i++) {
				rbound.add(f.tuple(atoms.get(i-1), atoms.get(i)));
			}
			b.boundExactly(r, rbound);
		}
		
		return b;
	}
	
	private static void usage() {
		System.out.println("Usage: java examples.RankAggregation [# entries] [# rankings]");
		System.exit(1);
	}
	
	/**
	 * Usage: java examples.RankAggregation [# entries] [# rankings]
	 */
	public static void main(String[] args) {
		if (args.length < 2) 
			usage();
		
		try {
			final RankAggregation model = new RankAggregation(Integer.parseInt(args[1]));
			final Solver solver = new Solver();
			solver.options().setSolver(SATFactory.ZChaffMincost);
			Formula f = model.show();
			Bounds b = model.bounds(Integer.parseInt(args[0]));
			System.out.println("solving...");
			Solution sol = solver.solve(f, b, model.cost());
			//System.out.println(f);
			//System.out.println(b);
			System.out.println(sol);
		} catch (TimeoutException e) {
			System.out.println("timed out.");
			e.printStackTrace();
		} catch (NumberFormatException nfe) {
			usage();
		}
	}
}	
{'fraction_non_alphanumeric': 0.13417679374063593, 'fraction_numerical': 0.00416181122024305, 'mean_word_length': 3.712156862745098, 'pattern_counts': {'":': 0, '<': 15, '<?xml version=': 0, '>': 11, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '2627400', 'n_tokens_mistral': 2243, 'n_tokens_neox': 2001, 'n_words': 558}