/*
 * Copyright 2009 Wishnu Prasetya.
 *
 * This file is part of T2.
 * T2 is free software; you can redistribute it and/or modify it under
 * the terms of the GNU General Public License (GPL) as published by the
 * Free Software Foundation; either version 3 of the License, or any
 * later version.
 * 
 * T2 is distributed in the hope that it will be useful, but WITHOUT ANY
 * WARRANTY; without even the implied warranty of MERCHANTABILITY or
 * FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License
 * for more details.
 *
 * A copy of the GNU General Public License can be found in T2 distribution.
 * If it is missing, see http://www.gnu.org/licenses.
 */

package Sequenic.T2ext.CoverageEngine;

import java.lang.reflect.Method;
import java.util.* ;
import java.io.*;
import java.util.concurrent.*;

import Sequenic.T2.BaseDomainSmall;
import Sequenic.T2.Pool;
import Sequenic.T2.Seq.*;
import Sequenic.T2ext.Analyzer.*;
import Sequenic.T2ext.Instrumenter.*;

/**
 * This engine refines SemiExhaustiveEngine. The main algorithm remains
 * the same; it just differs in:
 * 
 *     <ol>
 *     <li>How the base trace is prepared.
 *     <li>Parameters selection.
 *     <li>How it constructs the domains for the parameters.
 *     </ol>
 * 
 * <p>When preparing the base trace, we do as in SemiExhaustiveEngine.
 * Then we minimize the variations in the REF. Let REF j be parameter in
 * the base-trace, and that this is represents a reference to an object
 * of type C. We will try to find a REF i of class D which is a subclass 
 * of C, and such that i<j. This REF i corresponds to a previously 
 * created object, of compatible type. It is then type-safe to replace
 * "j" in REF j with "i"; and we will do so. By doing so it is as if we
 * try to focus and maximize side effects on a subset of the object pool.
 * 
 * <p>Parameters will be selected in principle as in SemiExhaustedEngine;
 * however because this class is not complete yet, currently only integer,
 * boolean, and string CONST-parameters are included.
 * 
 * <p>Domains construction. This engine inspect the set of constants used
 * along the target paths. Based on these domains are constructed.
 *
 * @author Wishnu Prasetya
 *
 */

public class Engine_10 extends SemiExhaustiveEngine {
	
	
	public Engine_10() { super() ; }
	
	
	public Engine_10(T2TraceFileCoverageResult covReport_, 
			T2TraceFileCoverageAnalyzer t2covAnalyzer_,
			LinkedList<Node> targetpath_){
		super(covReport_, t2covAnalyzer_, targetpath_) ;
	}
	
	@Override
	protected void prepareBaseTrace(){
		super.prepareBaseTrace() ;
		
		T2TraceInspection traceInspection2 = new T2TraceInspection(basetrace,
				t2covAnalyzer.getC(),
				t2covAnalyzer.getPool(),
				t2covAnalyzer.getClassinvs()) ;	
		
		List<MkValStep> allparams = traceInspection2.getParams(0,basetrace.trace.size()+1,false) ;
		// Get the REF-parameters, sort in reverse order. This makes
		// sure that REF with bigger indices will appear first in the
		// list.
		List<REF> REFparams = new LinkedList<REF>() ;
		int i = allparams.size() ;
		while (0<i) {
			i-- ;
			MkValStep P = allparams.get(i) ;
			if (P instanceof REF) REFparams.add((REF) P) ;
		}
		
		int N = REFparams.size() ;
		System.out.println(">>> #REF params: " + N) ;
		for (i=0; i<N; i++) {
			REF R1 = REFparams.get(i) ;
			// Determine the class of R1:
			Class C1 = null ;
			for (Pair<Integer,Class> ic : traceInspection2.REFtype_table) {
				if (ic.fst == R1.index) {
					C1 = ic.snd ;
					break ;
				}
			}
			assert C1 != null ;
			// Find a smaller index i that can replace the index of R1,
			// then change the index of  R1 with this i:
			for (Pair<Integer,Class> ic : traceInspection2.REFtype_table) {
				if (C1.isAssignableFrom(ic.snd)) {
					R1.index = ic.fst ;
					break ;
				}
			}
		}
		
	}
	
	
	/**
	 * In principle we use the same parameters frame as the one defined by
	 * the SemiExhaustiveEngine. But currently we'll restrict it further to
	 * only include Bool, Integer, and String.
	 */
	@Override
	protected void setupParamsFrame() {
		super.setupParamsFrame() ;
		List<MkValStep> toDelete = new LinkedList<MkValStep>() ;
		for (MkValStep P : paramsFrame) {
			Class C = SemiExhaustiveEngine.typeOfCONST((CONST) P) ;
			if ((C != Integer.class) && (C != Integer.TYPE) 
					&& (C != Boolean.class) && (C != Boolean.TYPE)
					&& (C != String.class))
				toDelete.add(P) ;
		}
		paramsFrame.removeAll(toDelete) ;		
	}
	
	@Override
	protected void setupDomains() {
		domainTable = new HashMap<MkValStep, List>() ;
		setupDomainsWorker() ;
		for (MkValStep P : paramsFrame) {
			CONST CONST = (CONST) P ;
			Class C = typeOfCONST(CONST) ;
			 
			if (C == Integer.class || C == Integer.TYPE) { domainTable.put(P,IntegerDomain) ; }
			if (C == Boolean.class || C == Boolean.TYPE) {
				List domain = new ArrayList<Integer>(2) ;
				domain.add(new Boolean(true)) ;
				domain.add(new Boolean(false)) ;
				domainTable.put(P,domain) ;
			}
			if (C == String.class) { domainTable.put(P,StringDomain) ; }
		}
	}
	
	/**
	 * The domain of all integer parameters. 
	 */
	List<Integer> IntegerDomain ;
	
	/**
	 * The domain of string parameters. 
	 */
	List<String> StringDomain ;
	
	/**
	 * This construct the domains, based on the constants used in
	 * along the target path.
	 */
	private void setupDomainsWorker() {
		System.out.println();
		// Use set to prevent duplicates!
		Set<Integer> intConsts = new HashSet<Integer>() ;
		Set<String> stringConsts = new HashSet<String>() ;
		for (Node N : targetpath) {
			for (Object x : N.getConstants()) {
				if (x instanceof Integer) {
					Integer x_ = (Integer) x ;
					// Add x, x-1, and x+1 to our constant-pool
					intConsts.add(x_) ;
					if (x_ > Integer.MIN_VALUE) intConsts.add(x_ - 1) ;
					if (x_ < Integer.MAX_VALUE) intConsts.add(x_ + 1) ;	
					System.out.println(">>> adding: " + (x_-1) + ", " + x_ + ", " + (x_+1)) ;
				}
				if (x instanceof String) stringConsts.add((String) x) ;
			}
		}
		// Aren't these already in the base domain?
		// Yes; but we will have to construct new domains here.
		intConsts.add(-1) ;
		intConsts.add(0) ;
		intConsts.add(1) ;
		stringConsts.add("") ;
		stringConsts.add((String) null) ;
		// Ok now convert them to lists:
		IntegerDomain = new ArrayList<Integer>(intConsts) ;
		StringDomain = new ArrayList<String>(stringConsts) ;
	}
	
}