import java.util.*;
import edu.neu.ccs.demeterf.*;
import edu.neu.ccs.demeter.*;
class Main {
  protected String s;
  public String get_s() { return s; }
  public void set_s(String new_s) { s = new_s; }
  public Main() { super(); }
  public Main(String s) {
    super();
    set_s(s);
  }
  public static Main parse(java.io.Reader in) throws ParseException { return new Parser(in)._Main(); }
  public static Main parse(java.io.InputStream in) throws ParseException { return new Parser(in)._Main(); }
  public static Main parse(String s) {
    try { return parse(new java.io.StringReader(s)); }
    catch (ParseException e) {
      throw new RuntimeException(e.toString());
    }
  }

		 public static void main(String args[]) throws Exception {
			 Formula csp = Formula.parse(System.in);

			 System.out.println("The given input is:");
			 csp.print();

			 Traversal travNumVar = new Traversal(new VarCounter());
			 // the second argument to traverse is tricky
			 // it is needed becuase we pass down the weight from ConcreteClause to literals
			 System.out.println("The number of variables is:"
					 + travNumVar.traverse(csp, 0));

			 Traversal travWeight = new Traversal(new TotalWeightCounter());
			 System.out.println("The total weight of this formula is:"
					 + travWeight.traverse(csp));

			 System.out.println("================================================");

		 }
	 
  void universal_trv0_bef(UniversalVisitor _v_) {
    ((UniversalVisitor) _v_).before(this);
  }

  void universal_trv0_aft(UniversalVisitor _v_) {
    ((UniversalVisitor) _v_).after(this);
  }

  void universal_trv0(UniversalVisitor _v_) {
    universal_trv0_bef(_v_);
    ((UniversalVisitor) _v_).before_s(this, s);
    ((UniversalVisitor) _v_).after_s(this, s);
    universal_trv0_aft(_v_);
  }

}