package fr.lifl.stc.stan.implicitFlow.data;

import java.util.Vector;

/**
 * 
 * @author dorina
 *
 */
public class Minterm {
	
	/**
	 * contains BooleanVariables ordered after <code>line</code>
	 */
	Vector<BooleanVariable> terms;
	
	/**
	 * 
	 *
	 */
	public Minterm(){
		terms = new Vector<BooleanVariable>();
	}
	
	/**
	 * 
	 * @param b
	 */
	public Minterm(BooleanVariable b){
		this();
		terms.add(b);
	}
	
	public Minterm(Minterm m) {
		terms = new Vector<BooleanVariable>();
		for(int i=0; i < m.size(); i++){
			this.terms.add(m.terms.elementAt(i));
		}
	}
	
	/**
	 * 
	 * @return
	 */
	public int size(){
		return terms.size();
	}
	
	/**
	 * 
	 * @return
	 */
	public boolean isTrue(){
		if(size() != 1)
			return false;
		BooleanVariable b = terms.elementAt(0);
		return b == BooleanVariable.condition_true;
	}
	
	/**
	 * 
	 * @return
	 */
	public boolean isFalse(){
		if(size() != 1)
			return false;
		BooleanVariable b = terms.elementAt(0);
		return b == BooleanVariable.condition_false;
	}
	
	/**
	 * 
	 */
	public boolean equals(Object obj){
		if(!(obj instanceof Minterm))
			return false;
		
		Minterm m = (Minterm)obj;
		
		if(this.size() != m.size())
			return false;
		for(int i=0; i < this.size(); i++){
			if(! this.terms.elementAt(i).equals(m.terms.elementAt(i)))
				return false;
		}
		return true;
	}
	
	/**
	 * 
	 * @param m
	 * @return <code>true</code> if <code>this</code> is greater or equal than <code>m</code>
	 */
	public boolean greaterOrEqualTo(Minterm m){
		if(this.size()<m.size())
			return false;
		
		for(int i = 0; i < m.size(); i++) {
			if(! this.terms.contains(m.terms.elementAt(i)))
				return false;
		}
		
		return true;
	}
	
	void and(Minterm m){
		for(int i = 0; i < m.size(); i++) {
			this.add((BooleanVariable)m.terms.elementAt(i));
		}
	}
	
	/**
	 * adds a booleanVariable to the minterm
	 */
	private void add(BooleanVariable b){		
		//check if this is constant
		if(this.isFalse())
			return;
		if(this.isTrue()){
			this.terms.clear();
			this.terms.add(b);
			return;
		}
		
		//check if b is constant
		if(b.getType() == BooleanVariable.CONSTANT_TYPE) {
			if(b.getLine()==BooleanVariable.TRUE_TYPE)
				return;
			if(b.getLine()==BooleanVariable.FALSE_TYPE){
				this.terms.clear();
				this.terms.add(b);
				return;
			}
		}
		
		//test if it already exists (or its negation)
		for(int i = 0; i < size(); i++) {
			BooleanVariable tmp = terms.elementAt(i);
			if(tmp == b)
				return;
			if(tmp.getNegation() == b) {
				//eliminer tmp
				
				delete(tmp);
				return;
			}
		}
		insert(b);
	}
	
	/**
	 * 	insert the boolean variable in order to keep the order 
	 */
	private void insert(BooleanVariable b){
		
		int i = 0;
		for(; i < terms.size(); i++) {
			if( b.compareTo(terms.elementAt(i)) == -1 )
				break;
		}
		terms.add(i,b);
		/*
		 int i = 0;
		 do {
		 tmp = (BooleanVariable)terms.elementAt(i);
		 i++;
		 }while(tmp.getLine() > line && i <= size());
		 
		 i--;
		 terms.add(i, b);
		 */
	}
	
	public void insertOnTop(BooleanVariable b){
		this.terms.add(0, b);
	}
	
	/**
	 * 
	 * @param b
	 */
	private void delete(BooleanVariable b){
		terms.removeElement(b);
		if(terms.size() == 0)
			terms.add(BooleanVariable.condition_true);
	}
	
	public boolean contains(BooleanVariable b){
		return this.terms.contains(b);
	}
	
	public String toString(){
		String s = "[ ";//size = "+this.terms.size()+" ";
		
		for(int i = 0; i < terms.size(); i++) {
			s += terms.elementAt(i);
			if( i < terms.size()-1)
				s += "&";
		}		
		s += "]";
		return s;
	}
}