Main {
  public static void main(String args[]) throws Exception {{
	  runTests();

    History h = new History(CSP.parse(System.in));
	 System.out.println("-------\nRunning .input test\n---------");
    solve(h);
    h.print();
    System.out.println();
  }}

  // find max solution starting from history h 
  private static void solve(History h) {{
	 boolean stuck = false;
	 
    while (!stuck && !h.canFinale()) {
		 stuck = true;
      while (h.unitPropagate())
			stuck = false;

      if (h.canDecide()) {
        h.decide();
		  stuck = false;
      }

		if (h.canSSR()) {
			h.SSR();
         h.restart();
			stuck = false;
      } else if (h.canUpdate()) {
        h.update();
         h.restart();
			stuck = false;
      }
    }

    if (h.canFinale())
      h.finale();
  }}

  private static void runTests() {{
	  //printTest("Assignment lookup test", Tests.assignmentLookup());
	  printTest("Constraint reduce test", Tests.constraintReduce());
	  printTest("unsat test", Tests.unsat());
	  printTest("UP rule test", Tests.unitPropagation());
	  printTest("Decide rule test", Tests.decide());
	  printTest("Update rule test", Tests.update());
	  printTest("Finale rule test", Tests.finale());
	  printTest("SSR rule test", Tests.ssr());
  }}

  // prints out a test name and its result
  private static void printTest(String testName, boolean result) {{
	  System.out.print(testName + ": ");
	  if (result)
		  System.out.println("PASSED");
	  else
		  System.out.println("FAILED");
  }}
}

CSP {
  void print() to * (PrintVisitor);
}