// rule behaviors - a rule mutates a History
History {
	// applicability tests:

	// true iff current state is M || F || N and
	// for some literal k, unsat(M!k, F) >= unsat(N, F)
	// and var(k) not in M
	public boolean canUnitPropagate() {{
		return getUPLiteral() != null;
	}}

   // find a literal that UP rule can be applied to
	private Literal getUPLiteral() {{
		State currentState = getLastState();

      // get all vars in F and not in M
		Set possibleVars = currentState.get_formula().vars();
		possibleVars.removeAll(currentState.get_partial().vars());

		// try +/- on each variable until one passes the unsat test
		Iterator<Variable> iVars = possibleVars.iterator();
		while (iVars.hasNext()) {
			Variable v = iVars.next();
			Literal vLit= new T();
			vLit.set_var(v);
			if (upTest(vLit, currentState))
				return vLit;
			else if (upTest(vLit.not(), currentState))
				return vLit.not();
		}

		return null; // if no literal passed the unsat test
	}}

   // true iff unsat (M!k, F) >= unsat(N, F)
	// or if !k in resolvent (<=> unsat(k,R) > 0)
	private boolean upTest(Literal l, State s) {{
		Assignment a = s.get_partial().copy().extend(l.not());
		Enumeration e = s.get_resolvent().elements();
		while (e.hasMoreElements()) 
			if (l.not().equals(e.nextElement()))
				return true;
		return s.get_resolvent().contains(l.not()) ||
		  s.get_formula().unsat(a) >= 
		  s.get_formula().unsat(s.get_best());
	}}

	public boolean canUpdate() {{
		// test unsats
		State s = getLastState();
		if (s.get_formula().unsat(s.get_partial()) <
			s.get_formula().unsat(s.get_best())) {
			return s.get_formula().vars().equals(s.get_partial().vars());
		} else
			return false;
	}}

   // true iff current partial assignment is incomplete
	public boolean canDecide() {{
		State s = getLastState();
		return !s.get_partial().isComplete(s.get_formula());
	}}

	public boolean canRestart() {{
		return true;
	}}

	public boolean canFinale() {{
		// test unsat
		State s = getLastState();
		if (s.get_formula().unsat(s.get_best()) == 0.0) {
			return s.get_formula().vars().equals(s.get_partial().vars());
		} else
			return false;
	}}

	public boolean canSSR() {{
		State s = getLastState();
		return !getDecisionLiterals().isEmpty() &&
		   s.get_formula().unsat(s.get_partial()) >= 
		   s.get_formula().unsat(s.get_best());
	}}

   // apply the UP rule, return false if can't apply
	public boolean unitPropagate() {{
		if (!canUnitPropagate())
			return false;
		// find literal, add to current state copy, append to history
		Literal l = getUPLiteral();
		State s = getLastState().copy();
		s.set_partial(s.get_partial().extend(l));
		TState ts = new TState();
		ts.set_transition(new UnitPropagation());
		ts.set_state(s);

		transitions.addElement(ts);
		return true;
	}}

  (@ private static Random rgen = new Random(); @)
  (@ private InputGen appmean; @)
  (@ static final double biasUpdateOdds = 1.0; @)

   // apply the decide rule
	public void decide() {{
		State s = getLastState().copy();
		if (appmean == null) {
			// if this is the first decide, do initial appmean stuff
			appmean = new InputGen();
			s.set_bias(appmean.initial(calcPairs(
			s.get_formula(), s.get_partial())).getMaxBias());
		} else if (rgen.nextDouble() <= biasUpdateOdds) {
			s.set_bias(appmean.update(calcPairs(
			s.get_formula(), s.get_partial())).getMaxBias());
		}

	   Set vars = s.get_formula().vars();
	   vars.removeAll(s.get_partial().vars());
		Iterator<Variable> iVar = vars.iterator();
		Variable v = iVar.next(); // there has to be >= 1 variable

		double r = rgen.nextDouble();
		Literal l = (r < s.get_bias()) ? new T() : new F();
		l.set_var(v);
		s.set_partial(s.get_partial().extend(l));
		
		TState ts = new TState();
		Decide t = new Decide();
		t.set_d_literal(l);
		ts.set_transition(t);
		ts.set_state(s);
		transitions.addElement(ts);
	}}

   // apply the restart rule
	public void restart() {{
		State s = getLastState().copy();
		s.set_partial(Assignment.parse(""));

		TState ts = new TState();
		ts.set_transition(new Restart());
		ts.set_state(s);
		transitions.addElement(ts);
	}}

	// apply the finale rule
	public void finale() {{
		State s = getLastState().copy();

		TState ts = new TState();
		ts.set_transition(new Finale());
		ts.set_state(s);
		transitions.addElement(ts);
	}}

	// apply the update rule
	public void update() {{
		State s = getLastState().copy();
		s.set_best(s.get_partial().copy());

		TState ts = new TState();
		ts.set_transition(new Update());
		ts.set_state(s);
		transitions.addElement(ts);
	}}

   // apply the SSR rule
	public void SSR() {{
		Set lits = getDecisionLiterals();

		State s = getLastState().copy();
		Iterator<Literal> ix = (Iterator<Literal>)lits.iterator();
		while (ix.hasNext())
			s.get_resolvent().push(ix.next());

		TState ts = new TState();
		ts.set_transition(new SSR());
		ts.set_state(s);
		transitions.addElement(ts);
	}}

   // get all decision literals from most recent restart to now
	private Set getDecisionLiterals() via TState to {State, Decide} {
		init (@ return_val = new HashSet(); @)
		before State (@ 
		  if (host.get_partial().isEmpty()) {
			  return_val.clear();
		  }
		@)
		before Decide (@ 
		  return_val.add(host.get_d_literal());
		@)
	}

  (@
  // calculates the pairs for f and pa
  private Set<Pair> calcPairs(CSP f, Assignment pa) {
    // count up occurances of relations
    Map<Relation, Integer> relationCounts = new HashMap<Relation, Integer>();
    CSP reduced = f.reduce(pa);

    Enumeration<Constraint> ic = reduced.get_constraints().elements();
    int totalRelations = 0;
    while (ic.hasMoreElements()) {
      totalRelations++;
      Relation r = ic.nextElement().get_relation();
      if (relationCounts.containsKey(r))
        relationCounts.put(r, relationCounts.get(r) + 1);
      else
        relationCounts.put(r, 1);
    }

    // generate a set of pairs from the relationCounts table
    Set<Pair> pairs = new HashSet<Pair>();
    Iterator<Relation> ir = relationCounts.keySet().iterator();
    while (ir.hasNext()) {
      Relation r = ir.next();
      double fraction = ((double)relationCounts.get(r)) / totalRelations;
      pairs.add(new Pair(fraction, r.get_relationNumber()));
    }

    return pairs;
  }
  @)
}