diff --git a/src/main/jastadd/hanoi/Constraints.jrag b/src/main/jastadd/hanoi/Constraints.jrag
index 94a087a30ca26a02b30d5dec5b31c9143bfe4d45..86e03df0bb2267f35c36ebff735b3737bce16af8 100644
--- a/src/main/jastadd/hanoi/Constraints.jrag
+++ b/src/main/jastadd/hanoi/Constraints.jrag
@@ -1,64 +1,139 @@
-import java.util.*;
-aspect Connectives{
-    uncache Connective.eval();
-    syn boolean Connective.eval();
-    eq Conjunction.eval(){
-        return this.getLeft().eval() && this.getRight().eval();
-    }
-    eq Disjunction.eval(){
-        return this.getLeft().eval() || this.getRight().eval();
-    }
-    eq Implication.eval(){
-        return (!this.getLeft().eval()) || this.getRight().eval();
-    }
-    eq Negation.eval()= !getConnective().eval();
-    eq Atom.eval(){
-        return this.getRelation().eval();
-    }
-    uncache Relation.eval();
-    syn boolean Relation.eval();
-    eq Subsetof.eval(){
-        Set left=new HashSet<>(); 
-        for(String element : this.getLeft().Set()){ 
-            left.add(element);
-        }
-        Set right=new HashSet<>(); 
-        for(String element : this.getRight().Set()){ 
-            right.add(element);
-        }
-        return right.containsAll(left);
-    }
-    eq Compare.eval(){
-        return (this.getLeft().eval() - this.getRight().eval())<0;
-    }
-    eq Equal.eval(){
-        return this.getLeft().eval() - this.getRight().eval()==0;
-    }
-    public double Term.eval(){
-        return 0;
-    }
-    public int Term.evalD(){
-        return 0;
-    }
-    public double Term1.eval(){//return the size of top disk
-        if(this.getRel().getNumDisk()>0){
-            //if the pillar is not empty, check if the top disk has size 1
-                return  this.getRel().getDisk(this.getRel().getNumDisk()-1).getSize();
-            }else{
-                return -1;//no disk, the number is invalid, return -1
-            }
-    }
-    public double Term2.eval(){
-        return this.getRel().moveSeq();
-    }
-    public double Term3.eval(){
-        return this.getRel().ID();
-    }
-    public double ConstantNum.eval(){
-        return this.getNum();
-    }
-    public String[] Term.Set(){
-        String[] str=new String[]{};
-        return str;
-    }
-}
+import java.util.*;
+aspect Connectives{
+    uncache Connective.eval();
+    syn boolean Connective.eval();
+    eq Conjunction.eval(){
+        return this.getLeft().eval() && this.getRight().eval();
+    }
+    eq Disjunction.eval(){
+        return this.getLeft().eval() || this.getRight().eval();
+    }
+    eq Implication.eval(){
+        return (!this.getLeft().eval()) || this.getRight().eval();
+    }
+    eq Negation.eval()= !getConnective().eval();
+    eq Atom.eval(){
+        return this.getRelation().eval();
+    }
+    uncache Relation.eval();
+    syn boolean Relation.eval();
+    eq Subsetof.eval(){
+        Set left=new HashSet<>(); 
+        for(String element : this.getLeft().Set()){ 
+            left.add(element);
+        }
+        Set right=new HashSet<>(); 
+        for(String element : this.getRight().Set()){ 
+            right.add(element);
+        }
+        return right.containsAll(left);
+    }
+    eq Compare.eval(){
+        return (this.getLeft().eval() - this.getRight().eval())<0;
+    }
+    eq Equal.eval(){
+        return this.getLeft().eval() - this.getRight().eval()==0;
+    }
+    uncache Term.eval();
+    syn int Term.eval();
+    eq Plus.eval(){
+        return this.getLeft().eval() + this.getRight().eval();
+    }
+    eq Minus.eval(){
+        return this.getLeft().eval() - this.getRight().eval();
+    }
+    eq Multi.eval(){
+        return this.getLeft().eval() * this.getRight().eval();
+    }
+    eq Divide.eval(){
+        return this.getLeft().eval() / this.getRight().eval();
+    }
+    eq Mod.eval(){
+        return this.getLeft().eval() % this.getRight().eval();
+    }
+    eq IfThenElse.eval(){
+        if(this.getIf().Satisfied()){
+           return this.getThen().eval();
+        }
+        return this.getElse().eval();
+    }
+    eq CompareFunction.eval(){
+        if(this.getLeft().eval() < this.getRight().eval()){
+            return 1;
+        }
+        return 0;
+    }
+    eq EqualFunction.eval(){
+        if(this.getLeft().eval() == this.getRight().eval()){
+            return 1;
+        }
+        return 0;
+    }
+    eq SubsetofFunction.eval(){
+        Set left=new HashSet<>(); 
+        for(String element : this.getLeft().Set()){ 
+            left.add(element);
+        }
+        Set right=new HashSet<>(); 
+        for(String element : this.getRight().Set()){ 
+            right.add(element);
+        }
+        if(right.containsAll(left)){
+            return 1;
+        }
+        return 0;
+    }
+    eq ConstantNum.eval(){
+        return this.getNum();
+    }
+    eq PillarID.eval(){
+        return this.getRel().ID();
+    }
+    eq TotalDiskAmount.eval(){
+        return this.getRel().AmountD();
+    }
+    eq DisksOnPillar.eval(){
+        return this.getRel().getNumDisk();
+    }
+    eq TopDiskSize.eval(){
+        return this.getRel().getDisk(this.getRel().getNumDisk()-1).getSize();
+    }
+//customerized terms
+    eq Term1.eval(){//return the size of top disk
+        if(this.getRel().getNumDisk()>0){
+            //if the pillar is not empty, check if the top disk has size 1
+                return  this.getRel().getDisk(this.getRel().getNumDisk()-1).getSize();
+            }else{
+                return -1;//no disk, the number is invalid, return -1
+            }
+    }
+    eq Term2.eval(){
+        return this.getRel().moveSeq();
+    }
+    eq Term3.eval(){
+        return this.getRel().ID();
+    }
+    uncache Condition.Satisfied();
+    syn boolean Condition.Satisfied();
+    eq CompareFunction.Satisfied(){
+        return this.getLeft().eval() < this.getRight().eval();
+    }
+    eq EqualFunction.Satisfied(){
+        return this.getLeft().eval() == this.getRight().eval();
+    }
+    eq SubsetofFunction.Satisfied(){
+        Set left=new HashSet<>(); 
+        for(String element : this.getLeft().Set()){ 
+            left.add(element);
+        }
+        Set right=new HashSet<>(); 
+        for(String element : this.getRight().Set()){ 
+            right.add(element);
+        }
+        return right.containsAll(left);
+    }
+    public String[] Term.Set(){
+        String[] str=new String[]{};
+        return str;
+    }
+}