// behaviors for assignments and helpers (literals etc.)
Assignment {
   traversal toAll(UniversalVisitor) { to *; }
   
   // deep copy the assignment
   public Assignment copy() {{
      CopyVisitor cv = new CopyVisitor(Assignment.class);
      toAll(cv);
      return (Assignment)cv.get_return_val();
   }}
   
   // extend the assignment with a new literal l
   // assumes that l is not in the assignment already
   public Assignment extend(Literal l) {{
      Assignment a = copy();
      a.get_literals().push(l);
      return a;
   }}

   // extends the assignment with new Literal l via mutation
   public void extendBang(Literal l) {{
     literals.push(l);
   }}
   
   // lookup the value of a variable in the assignment
   Literal lookup(Variable v) to Literal {
      before Literal (@
         if (host.get_var().equals(v))
            return_val = host;
      @)
   }

   // get a set of all variables used in the assignment
	Set vars() to Variable {
		init (@ return_val = new HashSet(); @)
		before Variable (@ return_val.add(host); @)
	}

   // true iff this is the empty assignment
	boolean isEmpty() {{
		return !literals.hasMoreElements();
	}}

	// checks whether assignment is complete w.r.t. a formula
	boolean isComplete(CSP aCSP) {{
		return aCSP.reduce(this).allComplete();
	}}
}

CSP {
	public boolean allComplete() to Relation {
		init (@ return_val = true; @)
		before Relation (@
		   return_val = return_val &&
			  (host.get_relationNumber() == 0 ||
			  host.get_relationNumber() == 255);
	  @)
	}
}

Literal {
   // convert the literal to integer representation
   public abstract int toInt();

	// get the negation of the literal
	public abstract Literal not();
}

T {
	public int toInt() {{ return 1; }}

	public String toString() {{ return var.toString(); }}

	public Literal not() {{
		Literal result = new F();
		result.set_var(var);
		return result;
	}}
}

F {
	public int toInt() {{ return 0; }}

	public String toString() {{ return "!" + var.toString(); }}

	public Literal not() {{
		Literal result = new T();
		result.set_var(var);
		return result;
	}}
}