Tests {
	// test of reduce on a single constraint
	public static boolean constraintReduce() {{
		Constraint c = Constraint.parse("22 : 1 2 3 0");
		Constraint c2 = Constraint.parse("17: 1 2 3 0");
		Relation zero = new Relation();
		zero.set_relationNumber(0);
		Constraint c4 = Constraint.parse("255: 1 2 3 0");
		Assignment a1 = Assignment.parse("1");
		Assignment a2 = Assignment.parse("1 2");
		Assignment a3 = Assignment.parse("!1 !3 2");

		boolean result = true;
		result = result && c.reduce(a1).equals(c2);
		// since 0 relation can't be input...
		result = result && c.reduce(a2).get_relation().equals(zero);
		result = result && c.reduce(a3).equals(c4);

		return result;
	}}

   // quick test of looking up variables in an assignment
	public static boolean assignmentLookup() {{
		Assignment a = Assignment.parse("!1 3 2");
		boolean result = null != a.lookup(Variable.parse("3"));

		return result;
	}}

   // test of unsat function
	public static boolean unsat() {{
		boolean result = true;
		CSP aCSP = CSP.parse("p 3 2 22 : 1 2 3 0 1 : 1 2 3 0");
		Assignment best = Assignment.parse("1 2 3");
		Assignment pa = Assignment.parse("2");

		result = result && aCSP.unsat(best) == 1.0;
		result = result && aCSP.unsat(pa) == 0.5;

		return result;
	}}

   // tests both predicate and application of UP rule
	public static boolean unitPropagation() {{
		boolean result = true;
		String startStateString = "|| " + 
		   "p 3 2 18 : 1 2 3 0 2 : 1 2 3 0 || || 0.0 || 1 2 3";

		History h = History.parse(startStateString);

		result = result && h.unitPropagate();
		result = result && !h.canUnitPropagate();

    h = History.parse("1 !2 || p 3 2 18 : 1 2 3 0 2 : 1 2 3 0 || || 0.0 || 1 2 3");
    int upCount = 0;
    while (h.unitPropagate() && upCount++ < 10);

    result = result && (upCount == 1);

		return result;
	}}

   // tests both predicate and application of Decide rule
	public static boolean decide() {{
		boolean result = true;
		String startStateString = "|| " + 
		   "p 3 2 18 : 1 2 3 0 2 : 1 2 3 0 || || 0.0 || 1 2 3";

		History h = History.parse(startStateString);

		result = result && h.unitPropagate();
		result = result && !h.canUnitPropagate();
		result = result && h.canDecide();
		h.decide();
		result = result && h.unitPropagate();

		return result;
	}}

   // tests application of the update rule
	public static boolean update() {{
		boolean result = true;
		String startStateString = "|| " + 
		   "p 3 2 18 : 1 2 3 0 2 : 1 2 3 0 || || 0.0 || 1 2 3";

		History h = History.parse(startStateString);

    result = result && !h.canUpdate();
		result = result && h.unitPropagate();
		result = result && !h.canUnitPropagate();
		result = result && h.canDecide();
      result = result && !h.canUpdate();
		h.decide();
      result = result && !h.canUpdate();
		result = result && h.unitPropagate();

		result = result && h.canUpdate();
		h.update();

		return result;
	}}

   // tests application of the finale rule
	public static boolean finale() {{
		boolean result = true;
		String startStateString = "|| " + 
		   "p 3 2 18 : 1 2 3 0 2 : 1 2 3 0 || || 0.0 || 1 2 3";

		History h = History.parse(startStateString);

    // simplified rule applying loop
    int restarts = 0;
    boolean action = false;
    while (!h.canFinale() && restarts < 10) {
      action = false;
      while (h.unitPropagate()) {
        action = true;
      }
      if (h.canDecide()) {
        h.decide();
        action = true;
      }  
      if (h.canUpdate()) {
        h.update();
        action = true;
      }
      if (!action) {
        h.restart();
        restarts++;
      }
    }

		result = result && h.canFinale();
		h.finale();
    
    // make sure best unsat = 0.0
    State s = h.getLastState();
    result = result && (s.get_formula().unsat(s.get_best()) == 0.0);

		return result;
	}}

   // tests both predicate and application of SSR rule
	public static boolean ssr() {{
		boolean result = true;
		String startStateString = "|| " + 
		   "p 3 2 18 : 1 2 3 0 2 : 1 2 3 0 || || 0.0 || 1 2 3";

		History h = History.parse(startStateString);

		result = result && h.unitPropagate();
		result = result && !h.canUnitPropagate();
		result = result && h.canDecide();
		h.decide();
		result = result && h.unitPropagate();

		System.out.println("prior to 'ssr', history is ");
		h.print();
		h.SSR();

		return result;
	}}
}