/*
 * SATinstance.java
 *
 * Created on March 10, 2006, 4:09 PM
 *
 * To change this template, choose Tools | Template Manager
 * and open the template in the editor.
 */

package cz.pcland.sat;
import cz.pcland.ga.BinaryIndividual;
import cz.pcland.ga.GenerationInfo;
import cz.pcland.ga.Population;
import cz.pcland.gavisualization.Operations;
import java.util.*;
import java.awt.event.*;
//import java.io.*;
import cz.pcland.sat.tokens.*;
import java.awt.geom.*;
import java.awt.*;
import cz.pcland.io.*;
/**
 *
 * @author petr
 */


public class SATInstance implements Loadable{
    private String SATString = "";
    private int strPointer = 0;
    
    public int clausesCount;
    public int varsCount;
    public int[][] clauses;
    public boolean canSatisfy = false;
    public boolean checked = false;
    
    public GenerationInfo gi = null; //stores info from the lastgeneration
    public Vector infoData = null;  //stores all generations info
    public Population population; //stores population in last generation
    
    public void loadFromString(String str) {
        if(str == null || str == "") return;
        SATString = "";
        append(str);
        parse();
    }
    
    
    public void parse(){
        Lexan lexan = new Lexan(SATString);
        BaseToken token;
        int clausOrder = 0;
        
        while(!((token = lexan.readToken()) instanceof TokenEOF)){
            
            if(token instanceof TokenClausesEnd) {
                token = lexan.readToken(); //eol
                token = lexan.readToken(); //0
                if(token instanceof TokenNum && (((TokenNum)token).getValue() == 0))  {
                    break;
                }else {
                    System.out.println("end your file with \n % \n 0");
                }
            }
            
            if(token instanceof TokenParams){
                if((token = lexan.readToken()) instanceof TokenWord){
                    //System.out.println(((TokenWord)token).getValue());
                    if((((TokenWord)token).getValue().equals("cnf"))) {
                        
                        if((token = lexan.readToken()) instanceof TokenNum){
                            varsCount = ((TokenNum)token).getValue();
                        }else System.out.println("Parse error !");
                        
                        if((token = lexan.readToken()) instanceof TokenNum){
                            clausesCount = ((TokenNum)token).getValue();
                            clauses = new int[clausesCount][3];
                        }else System.out.println("Parse error !");
                        
                    }else {
                        System.out.println("Awaited CNF token !");
                    }
                }else {
                    System.out.println("Parse error !");
                }
                
                if(!((token = lexan.readToken()) instanceof TokenEOL)){
                    System.out.println("Awaited and of line !");
                }
            }
            
            if(token instanceof TokenNum || token instanceof TokenNegatedNum){
                    int a, b, c;
                    if(token instanceof TokenNum) a = ((TokenNum)token).getValue(); else a = -((TokenNegatedNum)token).getValue();
                    token = lexan.readToken();
                    if(token instanceof TokenNum) b = ((TokenNum)token).getValue(); else b = -((TokenNegatedNum)token).getValue();
                    token = lexan.readToken();
                    if(token instanceof TokenNum) c = ((TokenNum)token).getValue(); else c = -((TokenNegatedNum)token).getValue();
                    clauses[clausOrder][0] = a;
                    clauses[clausOrder][1] = b;
                    clauses[clausOrder][2] = c;
                    clausOrder++;
                
                    token = lexan.readToken();
                    int zero = -1;
                    if(token instanceof TokenNum) zero = ((TokenNum)token).getValue();
                    if(zero != 0) System.out.println("Bad format of file, zero expected !");
                
                    if(!((token = lexan.readToken()) instanceof TokenEOL)){
                        System.out.println("Awaited and of line !");
                    }
            }
        }
        
    }
    
    String getBoolean(boolean b){
        if(b)return "1"; else return "0";
    }
    
    public String toString(){
        
        String str = "";
        for(int i=0;i<clausesCount;i++){
            str += "(" + clauses[i][0] + "|" + clauses[i][1] + "|" + clauses[i][2] + ")";
            if(i < clausesCount - 1) str += "&";
        }
        return "clausesCount=" + clausesCount + ", varsCount=" + varsCount + ", str=" + str;
    }
    
    public boolean canSatisfyClause(int i, BinaryIndividual individual){
        if(isVarTrue( individual.getString(), clauses[i][0]) ||
                isVarTrue( individual.getString(), clauses[i][1]) ||
                isVarTrue( individual.getString(), clauses[i][2])
                )return true; else return false;
    }
    
    public boolean isVarTrue(boolean[] bits, int varNum){
        boolean result = bits[Math.abs(varNum)-1];
        if(varNum < 0) result = !result;
        return result;
    }
    
    public String getEvaluatedInstance(BinaryIndividual individual){
        
        String str = "";
        for(int i=0;i<clausesCount;i++){
            String m1 = clauses[i][0] < 0 ? "-" : ""; 
            String m2 = clauses[i][1] < 0 ? "-" : ""; 
            String m3 = clauses[i][2] < 0 ? "-" : ""; 
            Color clr=canSatisfyClause(i, individual) ? Color.GREEN : Color.RED;
            str +=  Operations.getColoredText(clr ,"( "+ m1 + getBoolean(individual.getString()[Math.abs(clauses[i][0])-1]) + " | " + m2 + getBoolean(individual.getString()[Math.abs(clauses[i][1])-1]) + " | " + m3 + getBoolean(individual.getString()[Math.abs(clauses[i][2])-1])+ " )" ) ;
            if(i < clausesCount - 1) str += "&";
        }
        return str;
    }
    
    public String getString(){
        return this.SATString;
    }
    
    public void append(String str){
        SATString +=  str;
    }
    /** Creates a new instance of SATinstance */
    public SATInstance() {
        
    }
    
}
