import java.security.KeyStore.Entry;
import java.util.*;
import java.io.*;

public class Planner {
 ArrayList<Operator> operators;
 static ArrayList<String> preInstantiations;
 static ArrayList<String> preGoals;
 ArrayList<String> allGoals ;
 Random rand;
 ArrayList<Operator> plan;

 int count;
 int max = 20;
 public static void main(String argv[]){
  (new Planner()).start();
 }

 Planner(){
  rand = new Random();
  preInstantiations = new ArrayList<String>();
  preGoals = new ArrayList<String>();
  allGoals = new ArrayList<String>();
 }

 public void start(){
  initOperators("operator.txt");
  staticPrioritySet();
  ArrayList<String> goalList     = initGoalList();
  ArrayList<String> initialState = initInitialState();
  allGoals = initGoalList();
  
  HashMap<String,String> theBinding = new HashMap<String,String>();
  plan = new ArrayList<Operator>();
  
  //ループ上限は20~1000まで
  while(max < 1000){
	  count = 0;
	  if(planning((ArrayList<String>)goalList.clone(),
			  (ArrayList<String>)initialState.clone(),
			  (HashMap<String,String>)theBinding.clone())){

		  System.out.println("***** This is a plan! *****");
		  for(int i = 0 ; i < plan.size() ; i++){
			  Operator op = (Operator)plan.get(i);	    
			  System.out.println((op.instantiate(theBinding)).name);
		  }
		  break;
	  }else{
		  System.out.println(false+"\n");
		  //ゴールリストをシャッフル
		  int randInt1 = Math.abs(rand.nextInt()) % goalList.size();
		  String goal =  goalList.get(randInt1);
		  goalList.remove(goal);
		  goalList.add(goal);
		  int randInt2 = Math.abs(rand.nextInt()) % goalList.size();
		  goal =  goalList.get(randInt2);
		  goalList.remove(goal);
		  goalList.add(goal);
		  preInstantiations.clear();
		  preGoals.clear();
		  plan.clear();
		  max++;
	  }
  }
  }

 /*
  * ゴールリストに対するプランニングを行うメソッド
  * 
  * @param	ゴールリストを表す theGoalList,
  * 		ワーキングメモリを表す theCurrentState,
  * 		変数束縛情報を表す theBinding
  * @return theGoalListに対するプランニングが成功すれば true ,失敗すれば false
  */
 private boolean planning(ArrayList<String> theGoalList,
                          ArrayList<String> theCurrentState,
                          HashMap<String,String> theBinding)
 {
	 //ループの上限が設定してある
	 if(count++ > max) return false;
	 
	 System.out.println("*** GOALS ***" + theGoalList);
	 
	 //ゴールリストがワーキングメモリにすべて含まれている場合のみ成功とみなす
	 if(theCurrentState.containsAll(theGoalList)) return true;
  
	 if(theGoalList.size() == 1){
		 String aGoal = (String)theGoalList.get(0);
		 theGoalList.remove(0);
		 
		 //同じゴールを設定しないことにする
		 if(preGoals.contains(aGoal)) return false;
		 
		 preGoals.add(aGoal);
		 System.out.println(aGoal + preGoals);
		 if(planningAGoal(aGoal,theGoalList,theCurrentState,theBinding) != -1){
			 //一度成功した場合過去のゴールの情報を捨てる
			 preGoals.clear();
			 return true;
		 } else {
			  return false;
		 }
	  
	 } else {
		 String aGoal = (String)theGoalList.get(0);
		 theGoalList.remove(0);
   
		 //同じゴールを設定しないことにする
		 if(preGoals.contains(aGoal)) {
			 System.out.println(aGoal + " contains "+ preGoals);
			  return false;
		 }
		 
		 System.out.println(aGoal + preGoals);
		 preGoals.add(aGoal);
		 // Store original binding
		 HashMap<String,String> orgBinding = new HashMap<String,String>();
		 for(Iterator e = theBinding.keySet().iterator() ; e.hasNext();){
			 String key = (String)e.next();
			 String value = (String)theBinding.get(key);
			  orgBinding.put(key,value);
		 }
		 ArrayList<String> orgState = new ArrayList<String>();
		 for(int i = 0; i < theCurrentState.size() ; i++){
			 orgState.add(theCurrentState.get(i));
		 }

		 int tmpPoint = planningAGoal(aGoal,theGoalList,theCurrentState,theBinding);
		 
		 if(tmpPoint != -1){
			 //ワーキングメモリにゴールリストが含まれている場合のみを成功とみなす
			 if(theCurrentState.containsAll(theGoalList)){
				 //探索木を折り返す
				 preGoals.clear();
				return true;
			 } else {
				 //他のゴール条件にオペレータを適応する余地が残っている
				 preGoals.remove(aGoal);
				 
				 /*
				  * ここがデバックのポイント
				  */
				 
				 //全ゴールに対して変数束縛を行う
				 /*
				  * 先ほどプランニングに用いたゴールを再びリストの尾に戻す
				  * これはのちのプランニングでワーキングメモリが書きかえられる可能性があるため、
				  * 真の成功条件で終了するまで保持し続ける必要があるから
				  */
				 theGoalList.add(aGoal);
				 for(int i = 0; i < theGoalList.size(); ++i){
					 String st = theGoalList.get(0);
					 theGoalList.remove(0);
					 st = instantiateString(st,theBinding);
					 theGoalList.add(st);
				 }
				 
				 //再帰的にプランニングを続行
				 if(planning(theGoalList,theCurrentState,theBinding)){
					 preGoals.clear();
					 return true;
				 } else {
					 return false;
				 }
			 }
		 } else {
			 theBinding.clear();
			 for(Iterator e=orgBinding.keySet().iterator();e.hasNext();){
				 String key = (String)e.next();
				 String value = (String)orgBinding.get(key);
				 theBinding.put(key,value);
			 }
			 theCurrentState.clear();
			 for(int i = 0 ; i < orgState.size() ; i++){
				 theCurrentState.add(orgState.get(i));
			 }
			 return false;
		 }
	 }
 }

 /*
  * ゴールリストの1要素に対してプランニングを行うメソッド
  * 
  * @param	現ゴールリストの1つ目の要素 theGoal,その他の要素のリスト otherGoals,
  * 		現在の変数束縛情報 theBinding
  * @return	ワーキングメモリの要素とtheGoalがマッチした場合 0 ,
  * 		再帰的にプランニングを行いtheGoalが達成された場合 1 ,
  * 		失敗した場合 -1 
  *	返り値の0,1の違いはなくなったので気にしないでいい
  */
 private int planningAGoal(
		 String theGoal,
		 ArrayList<String> otherGoals,
		 ArrayList<String> theCurrentState,
		 HashMap<String,String> theBinding)
 {	 
	 System.out.println("preGoal :"+preGoals);
	 System.out.println("preIns :"+preInstantiations);
	 System.out.println("**"+theGoal);
	 int size = theCurrentState.size();
	 //ワーキングメモリとのマッチング
	 for(int i =  0; i < size ; i++){
		 String aState = (String)theCurrentState.get(i);
		 if((new Unifier()).unify(theGoal,aState,theBinding)){
			 System.out.println(theGoal+" <=> "+aState);
			 System.out.println(theBinding);
			 return 1;
 	  }
	 }

	 HashMap<Operator,HashMap<String,String>> conflictSet = new HashMap<Operator,HashMap<String,String>>();
	 // 現在のCurrent state, Binding, planをbackup
	 HashMap<String,String> orgBinding = new HashMap<String,String>();
	 for(Iterator e = theBinding.keySet().iterator() ; e.hasNext();){
		 String key = (String)e.next();
		 String value = (String)theBinding.get(key);
		 orgBinding.put(key,value);
	 }
	 ArrayList<String> orgState = new ArrayList<String>();
	 for(int j = 0; j < theCurrentState.size() ; j++){
		 orgState.add(theCurrentState.get(j));
	 }
	 ArrayList<Operator> orgPlan = new ArrayList<Operator>();
	 for(int j = 0; j < plan.size() ; j++){
		 orgPlan.add(plan.get(j));
	 }
	 
	 //競合集合を見つける
	 for(int i = 0 ; i < operators.size() ; i++){
		 Operator anOperator = rename((Operator)operators.get(i));
		 ArrayList<String> addList = anOperator.getAddList();
	   
		 for(int j = 0 ; j < addList.size() ; j++){
			 HashMap<String,String> tmpBinding = (HashMap<String, String>) theBinding.clone();
			 if((new Unifier()).unify(theGoal,
					 (String)addList.get(j),
					 tmpBinding)){
				 conflictSet.put(anOperator,tmpBinding);
			 }
		   }
	 }
	 if(conflictSet.size() == 0) return -1;
	 
	 ArrayList<String> theGoals = new ArrayList<String>();
	 theGoals.add(theGoal);
	 theGoals.addAll(otherGoals);

	 //競合解消
	 ArrayList<HashMap> newConflictSetList =
		 resolveConflict(theCurrentState,theGoals,conflictSet);
	 
	 //優先度順にオペレータを試す
	 for(int i = 0 ; i < newConflictSetList.size(); ++i){
		 HashMap<Operator,HashMap<String,String>> newConflictSet = 
			 (HashMap<Operator,HashMap<String,String>>)newConflictSetList.get(i);
		 for(Iterator e = newConflictSet.keySet().iterator() ; e.hasNext();){
			 Operator newOperator = (Operator)e.next();
			 HashMap<String,String> newBinding = newConflictSet.get(newOperator);
	  
			 newOperator = newOperator.instantiate(newBinding);
			 ArrayList<String> newGoals = newOperator.getIfList();
			 allGoals.remove(theGoal);
			 allGoals.addAll(newGoals);
			 
			 //使用したインスタンシエーションを保存
			 preInstantiations.add(newOperator.name);
			 
			 System.out.println("newOp:"+newOperator.name);
			 System.out.println("newBind:"+newBinding);
			 if(planning(newGoals,theCurrentState,newBinding)){
				 newOperator = newOperator.instantiate(newBinding);
				 System.out.println(newOperator.name);
				 System.out.println(newBinding.toString()+theBinding.toString());
				 preInstantiations.add(newOperator.name);
				 plan.add(newOperator);
				 theCurrentState =
			  newOperator.applyState(theCurrentState);
				 //theBinding.clear();
				 //theBinding = newBinding;
				 
				 //新しい変数束縛情報をこのメソッドの呼び出し元に反映させるための処理
				 copyMap(newBinding,theBinding);
		
				 System.out.println(theBinding);
				 return 0;
			 } else {
				 // 失敗したら元に戻す．
				 //preInstantiations,preGoalsも復元
				 preInstantiations.remove(newOperator.name);
				 preGoals.remove(theGoal);
				 allGoals.removeAll(newGoals);
				 allGoals.add(theGoal);
				 
				 System.out.println("失敗 :"+newOperator.name+"\nGoal :"+theGoal);
				 theBinding.clear();
				 for(Iterator e1=orgBinding.keySet().iterator();e1.hasNext();){
					 String key = (String)e1.next();
					 String value = (String)orgBinding.get(key);
					 theBinding.put(key,value);
				 }
				 theCurrentState.clear();
				 for(int k = 0 ; k < orgState.size() ; k++){
					 theCurrentState.add(orgState.get(k));
				 }
				 plan.clear();
				 for(int k = 0 ; k < orgPlan.size() ; k++){
					 plan.add(orgPlan.get(k));
				 }
			 }
		 }
	 }		
	 return -1;
 }
    
 /*
  * map1 copy to map2 
  */
 private void copyMap(HashMap map1 ,HashMap map2){
	 map2.clear();
	 map2.putAll(map1);
 }
 
 /*
  * 競合解消を行うメソッド
  * 
  * @param	現在のワーキングメモリを表す theCurrentState, ゴールリストを表す theGoalList 、競合集合を表す conflictSet
  * @return 優先度順にソートされた<インスタンシエーション、変数束縛情報>のエントリを持つ ArrayList
  */
 	private ArrayList<HashMap> resolveConflict(
 			ArrayList<String> theCurrentState,
 			ArrayList<String> theGoalList,
 			HashMap<Operator,HashMap<String,String>> conflictSet){
 		ArrayList<HashMap> result = new ArrayList<HashMap>();
 		HashMap<Operator,HashMap<String,String>> dynamic = dynamicPrioritySet(theCurrentState,theGoalList,conflictSet);
 		Vector<Operator> opList = new Vector<Operator>();
 		for(Iterator ite = dynamic.keySet().iterator(); ite.hasNext();){
 			Operator instantiation = (Operator)ite.next();
 			int i = 0;
 			while(true){
 				//動的な優先度でソートする
 				if(opList.size() <= i){
 					opList.insertElementAt(instantiation, i);
 					break;
 				}
 				if(instantiation.getPriority() > opList.elementAt(i).getPriority()){
 					opList.insertElementAt(instantiation, i);
 					break;
 				} else if(instantiation.getPriority() == opList.elementAt(i).getPriority()){
 					//動的な優先度が同じ場合、静的な優先度でソートする
 					Operator op1 = null;
 					Operator op2 = null;
 					for(int j = 0; j< operators.size(); ++j){
 						if((new Unifier()).unify(operators.get(j).name,instantiation.name)){
 							op1 = operators.get(j);
 						}
 						if((new Unifier()).unify(operators.get(j).name,opList.elementAt(i).name)){
 							op2 = operators.get(j);
					 }
 					}
 					if(op1.getPriority() >= op2.getPriority()){
 						opList.insertElementAt(instantiation, i);
 						break;
 					}
 				}
 				++i;
 			}
 		}
 		for(int i = 0; i < opList.size(); ++i){
 			HashMap tmpMap = new HashMap();
 			//System.out.println(opList.get(i).name +" - "+ opList.get(i).getPriority());
 			tmpMap.put(opList.get(i),dynamic.get(opList.get(i)));
 			result.add(tmpMap);
 		}
 		return result;
 	}
 
 /*
  * オペレータごとに静的な優先度を設定する
  */
 private void staticPrioritySet(){
	 //静的な優先度 = オペレータのIFリスト長 - ADDリスト長 - DELETEリスト長
	 for(int i = 0; i < operators.size(); ++i){
		 Operator anOperator = operators.get(i);
		 int priority = (anOperator).getIfList().size()   
		 	- (anOperator).getAddList().size()
		 	- (anOperator).getDeleteList().size();
		 operators.get(i).setPriority(priority);
	 }
 }
 
 /*
  * インスタンシエーションに動的な優先度を設定する
  * 
  * @param	現在のワーキングメモリ theCurrentState ,
  * 		現在のゴール状態のリスト theGoalList ,
  * 		競合集合中のオペレータのリストとそれぞれの束縛情報のエントリをもつ theConflictSet	
  * @return	インスタンシエーションとそれぞれの束縛情報のエントリを持つマップ 
  */
 private HashMap<Operator,HashMap<String,String>> dynamicPrioritySet(
		 ArrayList<String> theCurrentState,
		 ArrayList<String> theGoalList, 
		 HashMap<Operator,HashMap<String,String>> theConflictSet){
	 
	 HashMap<Operator,HashMap<String,String>> result = new HashMap<Operator,HashMap<String,String>>();
	System.out.println(allGoals);
	 for(Iterator ite = theConflictSet.keySet().iterator(); ite.hasNext();){
		 Operator anOperator = (Operator)ite.next();
		 HashMap<String,String> theBinding = (HashMap<String,String>)theConflictSet.get(anOperator);
		 Operator theInstantiation = anOperator.instantiate(theBinding);
		
		 //過去に使用したインスタンシエーションを削除する
		// if(!preInstantiations.contains(theInstantiation.name)){	
		 int contribution = 0;
		 ArrayList<String> theIfList = theInstantiation.getIfList();
		 ArrayList<String> theAddList = theInstantiation.getAddList();
		 ArrayList<String> theDeleteList = theInstantiation.getDeleteList();
		
		 for(int i = 0; i < theCurrentState.size(); ++i){
			 for(int j = 0; j < theIfList.size(); ++j){
				 if((new Unifier()).unify(theCurrentState.get(i),theIfList.get(j))){
					contribution++; 
				 }
			 }
		 }
		 
		 for(int j = 0; j < allGoals.size(); ++j){
			 for(int k = 0; k < theAddList.size(); ++k){
				 if((new Unifier()).unify(allGoals.get(j),theAddList.get(k))){
					 contribution++;
				 }
			 }
			 for(int l = 0; l < theDeleteList.size(); ++l){
				 if((new Unifier()).unify(allGoals.get(j),theDeleteList.get(l))){
		 			contribution--;
				 }
			 }
		 }
		 theInstantiation.setPriority(contribution);
		 System.out.println(theInstantiation.name + " -> " + theInstantiation.getPriority());
		 result.put(theInstantiation, theBinding);
		// }
	 }
	 return result;
 }
 
 private String instantiateString(String thePattern, HashMap<String,String> theBinding){
     String result = new String();
     StringTokenizer st = new StringTokenizer(thePattern);
     for(int i = 0 ; i < st.countTokens();){
         String tmp = st.nextToken();
         if(var(tmp)){
		String newString = (String)theBinding.get(tmp);
		if(newString == null){
		    result = result + " " + tmp;
		} else {
		    result = result + " " + newString;
		}
         } else {
             result = result + " " + tmp;
         }
     }
     return result.trim();
 }

 private boolean var(String str1){
     // 先頭が ? なら変数
     return str1.startsWith("?");
 }
 
 int uniqueNum = 0;
 private Operator rename(Operator theOperator){
  Operator newOperator = theOperator.getRenamedOperator(uniqueNum);
  uniqueNum = uniqueNum + 1;
  return newOperator;
 }

 private ArrayList<String> initGoalList(){
  ArrayList<String> goalList = new ArrayList<String>();
  goalList.add("A on B");
  goalList.add("B on C");
  return goalList;
 }
    
 private ArrayList<String> initInitialState(){
	 ArrayList<String> initialState = new ArrayList<String>();
	 initialState.add("C on B");
	 initialState.add("B on A");
  initialState.add("ontable A");
  initialState.add("clear C");

  initialState.add("handEmpty");

  return initialState;
 }
    
 /* 
  * ファイルからオペレータを読み込むメソッド
  * ファイルの書き方の例は
  *
  * NAME	RULE
  * IF		pattern1
  * 		patten2
  * ADD	addition
  * DELETE	remove
  * 
  * @param	ファイル名
  * @ret	読み込み成功時は0,Exception時は-1,読み込み途中で失敗した場合は途中までの行数
 */
 private int initOperators(String filename) {
 operators = new ArrayList<Operator>();
//	 operators = new LinkedList<Operator>();
  try{
  BufferedReader bf = new BufferedReader(new FileReader(filename));
  
  String line = bf.readLine();
  int count = 0;
  int errorLine = 1;
  //System.out.println(errorLine +":"+line);
  while(true) {
	  if(line == null){
		  return errorLine;
	  }
	  String name = null;
	  ArrayList<String> theIfList = new ArrayList<String>();
	  ArrayList<String> theAddList = new ArrayList<String>();
	  ArrayList<String> theDeleteList = new ArrayList<String>();
	  
	  while(!line.startsWith("NAME")){
		  line = bf.readLine();
		  errorLine++;
		  System.out.println(errorLine +":"+line);
		  if(line == null){
			  return errorLine;
		  }
	  }
	  name = (line.replace("NAME", "").trim());
	  line = bf.readLine();
	  errorLine++;
	  //System.out.println(errorLine +":1"+line);
	  if(line == null){
		  return errorLine;
	  }
	  line = line.trim();
	  
	  while(!line.startsWith("IF")){
		  line = bf.readLine();
		  errorLine++;
		  //System.out.println(errorLine +":"+line);
		  if(line == null){
			  return errorLine;
		  }
	  }
	  line = (line.replace("IF", "")).trim();
	  while(line != null && ! line.startsWith("ADD") && ! line.startsWith("DELETE")){
		  if(line.length() != 0){
			  theIfList.add(line);
		  }
		  line = bf.readLine();
		  errorLine++;
		  //System.out.println(errorLine +":"+line);
		  if(line != null){
			  line = line.trim();
		  }
	  }
	  
	  if(line != null && line.startsWith("ADD")){
		  line = (line.replace("ADD", "")).trim();
		  while(line != null && ! line.startsWith("DELETE") && ! line.startsWith("NAME")){
			  if(line.length() != 0){
				  theAddList.add(line);
			  }
			  line = bf.readLine();
			  errorLine++;
			  //System.out.println(errorLine +":"+line);
			  if(line != null){
				  line = line.trim();
			  }
		  }
	  }
	  
	  if(line != null && line.startsWith("DELETE")){
		  line = (line.replace("DELETE", "")).trim();
		  while(line != null && ! line.startsWith("NAME")){
			  if(line.length() != 0){
				  theDeleteList.add(line);
			  }
			  line = bf.readLine();
			  errorLine++;
			  //System.out.println(errorLine +":"+line);
			  if(line != null){
				  line = line.trim();
			  }
		  }
	  }
	  
	  if(name != null &&
			  theIfList != null &&
			  (theAddList.size() != 0 ||
			  theDeleteList.size() != 0	)){
		  operators.add(new Operator(name,theIfList,theAddList,theDeleteList));
		  //operators.offer(new Operator(name,theIfList,theAddList,theDeleteList));
		  if(line == null){
			  break;
		  } 
	  } else {
		  bf.close();
		  //ERROR
		  return errorLine;
	  }
  }
  bf.close(); // Reader を閉じる
  return 0;
  
  } catch (FileNotFoundException e){
	  e.printStackTrace();
	  return -1;
  } catch (IOException e){
	  e.printStackTrace();
	  return -1;
  }
 }

}

class Operator{
    String name;
    ArrayList<String> ifList;
    ArrayList<String> addList;
    ArrayList<String> deleteList;
    int priority;
    
    Operator(String theName,
    		ArrayList<String> theIfList,ArrayList<String> theAddList,ArrayList<String> theDeleteList){
	name       = theName;
	ifList     = theIfList;
	addList    = theAddList;
	deleteList = theDeleteList;
    }


    /*
     * このオペレータオブジェクトの優先度のセットする
     */
    public void setPriority(int p){
    	this.priority = p;
    }
    
    /*
     * このオペレータの優先度を返す
     */
    public int getPriority(){
    	return this.priority;
    }
    
    public ArrayList<String> getAddList(){
	return addList;
    }

    public ArrayList<String> getDeleteList(){
	return deleteList;
    }

    public ArrayList<String> getIfList(){
	return ifList;
    }

    public String toString(){
	String result =
	    "NAME: "+name + "\n" +
	    "IF :"+ifList + "\n" +
	    "ADD:"+addList + "\n" +
	    "DELETE:"+deleteList;
	return result;
    }

    public ArrayList<String> applyState(ArrayList<String> theState){
	for(int i = 0 ; i < addList.size() ; i++){
	    theState.add(addList.get(i));
	}
	for(int i = 0 ; i < deleteList.size() ; i++){
	    theState.remove(deleteList.get(i));
	}
	return theState;
    }
    

    public Operator getRenamedOperator(int uniqueNum){
    	ArrayList<String> vars = new ArrayList<String>();
	// IfListの変数を集める
	for(int i = 0 ; i < ifList.size() ; i++){
	    String anIf = (String)ifList.get(i);
	    vars = getVars(anIf,vars);
	}
	// addListの変数を集める
	for(int i = 0 ; i < addList.size() ; i++){
	    String anAdd = (String)addList.get(i);
	    vars = getVars(anAdd,vars);
	}
	// deleteListの変数を集める
	for(int i = 0 ; i < deleteList.size() ; i++){
	    String aDelete = (String)deleteList.get(i);
	    vars = getVars(aDelete,vars);
	}
	Hashtable renamedVarsTable = makeRenamedVarsTable(vars,uniqueNum);
	
	// 新しいIfListを作る
	ArrayList<String> newIfList = new ArrayList<String>();
	for(int i = 0 ; i < ifList.size() ; i++){
	    String newAnIf =
		renameVars((String)ifList.get(i),
			   renamedVarsTable);
	    newIfList.add(newAnIf);
	}
	// 新しいaddListを作る
	ArrayList<String> newAddList = new ArrayList<String>();
	for(int i = 0 ; i < addList.size() ; i++){
	    String newAnAdd =
		renameVars((String)addList.get(i),
			   renamedVarsTable);
	    newAddList.add(newAnAdd);
	}
	// 新しいdeleteListを作る
	ArrayList<String> newDeleteList = new ArrayList<String>();
	for(int i = 0 ; i < deleteList.size() ; i++){
	    String newADelete =
		renameVars((String)deleteList.get(i),
			   renamedVarsTable);
	    newDeleteList.add(newADelete);
	}
	// 新しいnameを作る
	String newName = renameVars(name,renamedVarsTable);
	
	return new Operator(newName,newIfList,newAddList,newDeleteList);
    }

    private ArrayList<String> getVars(String thePattern,ArrayList<String> vars){
	StringTokenizer st = new StringTokenizer(thePattern);
	for(int i = 0 ; i < st.countTokens();){
	    String tmp = st.nextToken();
	    if(var(tmp)){
		vars.add(tmp);
	    }
	}
	return vars;
    }

    private Hashtable makeRenamedVarsTable(ArrayList<String> vars,int uniqueNum){
	Hashtable result = new Hashtable();
	for(int i = 0 ; i < vars.size() ; i++){
	    String newVar =
		(String)vars.get(i) + uniqueNum;
	    result.put((String)vars.get(i),newVar);
	}
	return result;
    }
    
    private String renameVars(String thePattern,
			      Hashtable renamedVarsTable){
	String result = new String();
	StringTokenizer st = new StringTokenizer(thePattern);
	for(int i = 0 ; i < st.countTokens();){
	    String tmp = st.nextToken();
	    if(var(tmp)){
		result = result + " " +
		    (String)renamedVarsTable.get(tmp);
	    } else {
		result = result + " " + tmp;
	    }
	}
	return result.trim();
    }

    
    public Operator instantiate(HashMap<String,String> theBinding){
	// name を具体化
	String newName =
	    instantiateString(name,theBinding);
	// ifList    を具体化
	ArrayList<String> newIfList = new ArrayList<String>();
	for(int i = 0 ; i < ifList.size() ; i++){
	    String newIf = 
		instantiateString((String)ifList.get(i),theBinding);
	    newIfList.add(newIf);
	}
	// addList   を具体化
	ArrayList<String> newAddList = new ArrayList<String>();
	for(int i = 0 ; i < addList.size() ; i++){
	    String newAdd =
		instantiateString((String)addList.get(i),theBinding);
	    newAddList.add(newAdd);
	}
	// deleteListを具体化
	ArrayList<String> newDeleteList = new ArrayList<String>();
	for(int i = 0 ; i < deleteList.size() ; i++){
	    String newDelete =
		instantiateString((String)deleteList.get(i),theBinding);
	    newDeleteList.add(newDelete);
	}
	return new Operator(newName,newIfList,newAddList,newDeleteList);
    }

    private String instantiateString(String thePattern, HashMap<String,String> theBinding){
        String result = new String();
        StringTokenizer st = new StringTokenizer(thePattern);
        for(int i = 0 ; i < st.countTokens();){
            String tmp = st.nextToken();
            if(var(tmp)){
		String newString = (String)theBinding.get(tmp);
		if(newString == null){
		    result = result + " " + tmp;
		} else {
		    result = result + " " + newString;
		}
            } else {
                result = result + " " + tmp;
            }
        }
        return result.trim();
    }

    private boolean var(String str1){
        // 先頭が ? なら変数
        return str1.startsWith("?");
    }
}
class Unifier {
    StringTokenizer st1;
    String buffer1[];    
    StringTokenizer st2;
    String buffer2[];
    HashMap<String,String> vars;
    
    Unifier(){
	vars = new HashMap<String,String>();
    }

    public boolean unify(String string1,String string2,HashMap<String,String> theBindings){
	HashMap<String,String> orgBindings = new HashMap<String,String>();
	for(Iterator<String> i = theBindings.keySet().iterator(); i.hasNext();){
	    String key = i.next();
	    String value = theBindings.get(key);
	    orgBindings.put(key,value);
	}
	this.vars = theBindings; ////これがポインタ代入なら理解できる
	if(unify(string1,string2)){
	    ////更新しなくていいのか？
		return true;
	} else {
	    // 失敗したら元に戻す．
	    theBindings.clear();
	    for(Iterator<String> i = orgBindings.keySet().iterator(); i.hasNext();){
		String key = i.next();
		String value = orgBindings.get(key);
		theBindings.put(key,value);
	    }
	    return false;
	}
    }

    public boolean unify(String string1,String string2){
	// 同じなら成功
	if(string1.equals(string2)) return true;
	
	// 各々トークンに分ける
	st1 = new StringTokenizer(string1);
	st2 = new StringTokenizer(string2);
	
	// 数が異なったら失敗
	if(st1.countTokens() != st2.countTokens()) return false;
	
	// 定数同士
	int length = st1.countTokens();
	buffer1 = new String[length];
	buffer2 = new String[length];
	for(int i = 0 ; i < length; i++){
	    buffer1[i] = st1.nextToken();
	    buffer2[i] = st2.nextToken();
	}

	// 初期値としてバインディングが与えられていたら
	if(this.vars.size() != 0){
	    for(Iterator<String> i = vars.keySet().iterator(); i.hasNext();){
		String key = i.next();
		String value = vars.get(key);
		replaceBuffer(key,value);
	    }
	}

	for(int i = 0 ; i < length ; i++){
	    if(!tokenMatching(buffer1[i],buffer2[i])){
		return false;
	    }
	}

	return true;
    }

    boolean tokenMatching(String token1,String token2){
	if(token1.equals(token2)) return true;
	if( var(token1) && !var(token2)) return varMatching(token1,token2);
	if(!var(token1) &&  var(token2)) return varMatching(token2,token1);
	if( var(token1) &&  var(token2)) return varMatching(token1,token2);
	return false;
    }

    boolean varMatching(String vartoken,String token){
	if(vars.containsKey(vartoken)){
	    if(token.equals(vars.get(vartoken))){
		return true;
	    } else {
		return false;
	    }
	} else {
	    replaceBuffer(vartoken,token);
	    if(vars.containsValue(vartoken)){
		replaceBindings(vartoken,token);
	    }
	    vars.put(vartoken,token);
	}
	return true;
    }

    void replaceBuffer(String preString,String postString){
	for(int i = 0 ; i < buffer1.length ; i++){
	    if(preString.equals(buffer1[i])){
		buffer1[i] = postString;
	    }
	    if(preString.equals(buffer2[i])){
		buffer2[i] = postString;
	    }
	}
    }
    
    void replaceBindings(String preString,String postString){
	for(Iterator<String> i = vars.keySet().iterator(); i.hasNext();){
	    String key = i.next();
	    if(preString.equals(vars.get(key))){
		vars.put(key,postString);
	    }
	}
    }
    
    boolean var(String str1){
	// 先頭が ? なら変数
	return str1.startsWith("?");
    }