Main { 
{{
        static void print(String s){ System.out.print(s); }
        static void println(String s){ print(s+"\n"); }
        public static void main(String args[]) throws Exception {
            Formula csp = Formula.parse(System.in);
            
            println("The given input is:");
            csp.print();
            
            Traversal travNumVar = new Traversal(new VarCounter());

            // the second argument to traverse is tricky it is needed
            // because we pass down the weight from ConcreteClause to literals
            println("The number of variables is:"
                    + travNumVar.traverse(csp, 1));
            
            Traversal travWeight = new Traversal(new TotalWeightCounter());
            println("The total weight of this formula is:"
                    + travWeight.traverse(csp));
            
            println("================================================");
            println("The formula after traversal is:");
            csp.print();
            
            LiteralList assignment = new LiteralEmpty();
            for (int i = 1; i < 5; i++)
                assignment = new LiteralCons(Positive.parse(""+i), assignment);

            print("\nAssignment: ");assignment.print();

            println("\nReductions:");
            
            Formula result = csp;
            println("===============================");
            println("Before Reduction:");
            result.print();
            
            // Reduction Assignments
            int times = 0;
            while(assignment.hasMoreElements()){
                Literal red = assignment.nextElement();
                result = new Traversal(new CNFReducer()).traverse(result, red);
                assignment = assignment.rest();

                print("After reduction " + (++times)+ ", the formula is:");
                result.print();
                println("");
            }
         }
     }}
}

Formula {
    void print() to * (PrintVisitor);
    void display() to * (DisplayVisitor);
}

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

Literal {
    void print() to * (PrintVisitor);
{{
         public boolean sameVarAs(Literal lit) {
             return get_variable().sameVarAs(lit.get_variable());
         }
}} }
Variable { {{
         public boolean sameVarAs(Variable var) {
             return get_integer().equals(var.get_integer());
         }
}} }

Literal {
    {{
         public abstract boolean sameSignAs(Literal lit);
         boolean sameSignAs(Positive pos){ return false; }
         boolean sameSignAs(Negative neg){ return false; }
     }}
}

TrueLit{ public boolean sameSignAs(Literal lit){{ return false; }} }
FalseLit{ public boolean sameSignAs(Literal lit){{ return false; }} }

Positive { {{
         public boolean sameSignAs(Literal lit) {
             return lit.sameSignAs(this);
         }
         boolean sameSignAs(Positive pos){ return true; }
}} }

Negative { {{
         public boolean sameSignAs(Literal lit) {
             return lit.sameSignAs(this);
         }
         boolean sameSignAs(Negative neg){ return true; }
}} }

//================= List manipulation
// hasMoreElements
LiteralList {
    {{
         boolean hasMoreElements() {return false;}
         Literal nextElement(){ throw new RuntimeException("No Next Element"); }
         LiteralList rest(){ throw new RuntimeException("No Next Element"); }
    }}
}

LiteralCons {
    {{
         boolean hasMoreElements(){ return true; }
         Literal nextElement(){ return first; }
         LiteralList rest(){ return rest; }
    }}
}