package v1

import scala.util.parsing.combinator.syntactical.StandardTokenParsers
import scala.util.parsing.input._
import scala.util.parsing.syntax._
import java.io._
object SAT  extends StandardTokenParsers{
  
  
  lexical.delimiters ++= List("=",",","(",")", "->", "{", "}", "!=")
  lexical.reserved   ++= List("car", "cdr", "cons", "null")
   def myP : Parser[List[Formula]]= "{"~>rep1sep(Formula,",")<~"}" ^^ { case a=> a}
 def Formula: Parser[Formula] =(
   (Term <~"=") ~ Term ^^{ case t1 ~ t2 => Equals(t1,t2) }
   |(Term <~ "!=") ~ Term ^^{ case t1 ~ t2 => NotEquals(t1,t2) }
) 
 
def Term: Parser[Term] = (    
     ("car" ~ "(") ~> Term <~ ")"   ^^ { case t => Car(t) }
    | ("cdr" ~ "(")~>Term <~ ")"  ^^ { case  t => Cdr(t) }
    | (("cons"~"(") ~> Term <~",")~Term <~")" ^^ { case  t1 ~ t2 => Cons(t1,t2) }
    |"null" ^^ {case "null" =>Null() }
    | ident ^^ { case id => Var(id) }
    
    | failure("illegal start of simple term"))

//In order to check the intermediate steps of the algorithm
//please uncomment all the println commands

  def main(args: Array[String])  {
    
    val a0="{a=b}" //sat
    val a1="{cons(x,y)=z, car(w)=x, cdr(w)=y, z!=w}"//unsat
    val a2="{cons(x,y)=z, car(w)=x, cdr(w)!=y, z=w}"//unsat
    val a3="{cons(x,y)=z, car(w)=y}"//sat    
    val a4="{cons(z,cons(x,y))=t, w=cons(x,y), cons(z,w)=v, v=t, z!=car(v)}"//unsat
    val a5 ="{cons(cons(a,b),cons(c,d))!=cons(cons(a1,b1),cons(c1,d1)),a=a1,b=b1,c=c1,d=d1}"//unsat 
    val a6="{a=b,c=d,cons(a,c)!=cons(b,d)}"//unsat
    val a7="{x=y,z=t,car(cons(x,z))!=car(cons(y,t))}"//unsat 
    val a8="{a1=b1, b1=c1, cons(a1,d)!=cons(c1,d)}"//unsat   
   
    val tokens = new lexical.Scanner(StreamReader(new StringReader(a1)))
        
    phrase(myP)(tokens) match {
      case Success(t, _) =>
        try {
          if(satisfiable(t))
              println("satisfiable")
          else
              println("unsatisfiable") 
         
        
        } catch {
          case tperror => println(tperror.toString)
        }
      case e =>
        println(e)
    }
  }
  
    // main function which transforms the set of formulas to the normal form and decides satisfiability
  def satisfiable(t: List[Formula]) = {
    println("Initial Set:")
    println(t);
    var simplifiedT : List[Formula] = Nil
    t.foreach(f => f match {
      case Equals(t1,t2) => simplifiedT = Equals(simplify(t1),simplify(t2)) :: simplifiedT
      case NotEquals(t1,t2) => simplifiedT = NotEquals(simplify(t1),simplify(t2)) :: simplifiedT
    })
    //println("Simplfied Set:")
    //println(simplifiedT);
    
    //println("No Selector Set:")
    var n = replaceSelectors(simplifiedT)
    //println(n);
    downwards(n)
  }
  
  //reduces trivial terms
   def simplify(t: Term) : Term = t match{
    case Cdr(Cons(x,y)) => simplify(y)
    case Car(Cons(x,y)) => simplify(x)
    case Cons(x,y) => Cons(simplify(x),simplify(y))
    case t => t    
  }
  
   //replaces a variable x with term c inside term t
  def replaceInTerm(x : String, c : Term, t:Term) : Term= t match 
  {
    case Var(r)=>if(x.equals(r)) c
                 else Var(r)
    case Cons(a,b)=> Cons(replaceInTerm(x,c,a),replaceInTerm(x,c,b))
    case _=> t;
  }
  
  //replaces var x with term t in our set of formulas (substitution)
  def replace(x:String,c:Term,l: List[Formula]):(List[Formula])=l match{
    case Nil =>Nil
    case Equals(a,b)::t=>Equals(replaceInTerm(x,c,a),replaceInTerm(x,c,b))::replace(x,c,t) 
    case NotEquals(a,b)::t=>NotEquals(replaceInTerm(x,c,a),replaceInTerm(x,c,b))::replace(x,c,t)
  }
  
  //removes cons=var formulas
  def downConsVar(l: List[Formula],L: List[Formula]):(List[Formula],Boolean) =l match{
      case Equals(Var(x),Cons(a,b))::rest =>( replace(x,Cons(a,b),rest:::L),true)
      case Equals(Cons(a,b),Var(x))::rest => (replace(x,Cons(a,b),rest:::L),true)
      case h::rest=>downConsVar(rest,h::L)                    
      case Nil=>(L,false)
    }
      
  // removes cons=cons formulas
  def downConsCons(l: List[Formula],L: List[Formula]):(List[Formula],Boolean) =l match{
      case Equals(Cons(a,b),Cons(c,d))::rest =>(Equals(a,c)::Equals(b,d)::rest:::L,true)
      case NotEquals(Cons(a,b),Cons(c,d))::rest =>if(findContradict(NotEquals(a,c),rest:::L)) (NotEquals(a,c)::rest:::L,true)
                                                  else if(findContradict(NotEquals(b,d),rest:::L)) (rest:::L,true) 
                                                  else downConsCons(rest,NotEquals(Cons(a,b),Cons(c,d))::L)
      case a::b=>downConsCons(b,a::L)
      case Nil=>(L,false)
  }
  
  //checks to see if a formula contradicts another formula
  def contradicts (a: Formula,b: Formula ): Boolean =a match{
    case Equals(Var(x),Var(y))=> b match{
      case NotEquals(Var(z),Var(t))=> ((x.equals(z) && y.equals(t))||(x.equals(t) && y.equals(z)))
      case _ => false
    }
    case NotEquals(Var(x),Var(y))=> b match{
      case Equals(Var(z),Var(t))=> ((x.equals(z) && y.equals(t))||(x.equals(t) && y.equals(z)))
      case _ => false
    }
    case _=>false
  }
  
  //finds a contradiction to formula e in the list l
  def findContradict(e: Formula, l: List[Formula]): Boolean = l match{
    case h::t=>(contradicts(h,e) || findContradict(e,t))
    case Nil=> false
  }
  
  //procedure which applies the two down rules until neither can be applied anymore 
  def downwards(t: List[Formula]): Boolean = {
    var changed = true
    var newt = t
    while(changed){
      val (nt,ch) = downConsCons(newt,Nil)
      changed = ch
      if (!changed) {
        val (nt2,ch2) = downConsVar(nt,Nil)
        changed = ch2
        newt = nt2
        //if (changed) println("  ConsVar removal:\n" + newt)
      } else {
        //println("  ConsCons removal:\n" + nt)
        newt = nt
      }
      
    }
    val normalForm = removeVarVar(newt)
    //println("Normal form:\n" + normalForm)
    val c = contradiction(normalForm)
    c
  }
  
  //find contradictions in disequalities
  def contradiction(l: List[Formula]):Boolean =l match{
    
     case NotEquals(Cons(a,b),Cons(c,d))::rest => if (a.equals(c) && b.equals(d))  false
                                                      else	contradiction(rest)
     case NotEquals(Var(a),Var(b))::rest => if (a.equals(b)) false
                                                      else	contradiction(rest)
     case a::rest=>contradiction(rest)
     case Nil=>true
      
  }
  
  //substitutes variables by removing var=var formulas
  def removeVarVar(l: List[Formula]):List[Formula] = {
    //see if we have a Var=Var formula in the set
    
    val found = l.find(f => f match {
      case Equals(Var(a),Var(b)) => true
      case _ => false
    })
    found match {
      case None => l //done
      case Some(Equals(Var(a),Var(b))) => {
        var list:List[Formula] = Nil
        l.foreach(f => f match {
          case Equals(Var(a1),Var(b1)) => if (!(a.equals(a1) && b.equals(b1))) list = f::list
          case _ => list = f::list
        })
        
        //println("  Removing: " + a + "="+b)
        if (!a.equals(b)){
          val v =(Var(a),Var(b))
          var res:List[Formula] = Nil
          list.foreach(f => f match {
            case Equals(t1,t2) => res = Equals(subVinT(v,t1),subVinT(v,t2))::res
            case NotEquals(t1,t2) => res = NotEquals(subVinT(v,t1),subVinT(v,t2))::res
          })
          list = res
        }
        //println(list)
        removeVarVar(list)
      }
      case _ => l
    }
    
    
    
  }
  
  def sub(v:(Var,Var),f:Formula):Formula = f match{
    case Equals(a,b) => Equals(subVinT(v,a),subVinT(v,b))
    case NotEquals(a,b) => NotEquals(subVinT(v,a),subVinT(v,b))
  }
  
  def subVinT(v:(Var,Var),t:Term):Term = t match {
    case Car(t1) => Car(subVinT(v,t1))
    case Cdr(t1) => Cdr(subVinT(v,t1))
    case Cons(t1,t2) => Cons(subVinT(v,t1),subVinT(v,t2))
    case Var(a) => {
      if ((v._1.n).equals(a)) v._2
      else Var(a)
    }
    case a=>a
  }
  
  //collects all variable names
  def collectLiterals(t: Term):List[String]= {
    t match {
      case Car(l) => collectLiterals(l)
      case Cdr(l) => collectLiterals(l)
      case Var(n: String) => List(n)
      case Cons(Var(x),y) => x :: collectLiterals(y)
      case Cons(x,y) => collectLiterals(x).union(collectLiterals(y))
      case Null() => Nil
    }
  }
  
  //removes selectors from the list of formulas
  def replaceSelectors(t: List[Formula]): List[Formula] = {
    var literals : List[String] = Nil
    t.foreach(elem => {
      elem match {
        case Equals(t1,t2) => {
          val f = collectLiterals(t1)
          literals = literals.union(f.removeDuplicates)
          literals = literals.union(collectLiterals(t2).removeDuplicates)
        }
        case NotEquals(t1,t2) => {
          literals = literals.union(collectLiterals(t1).removeDuplicates)
          literals = literals.union(collectLiterals(t2).removeDuplicates)          
        }
      }      
    })
    
    var hasCons : List[String] = Nil
    t.foreach(e => {
      hasCons = varIsCons(e).union(hasCons)
    })
    hasCons.removeDuplicates
    
    var replace : List[String] = Nil
    t.foreach(e => {
      replace = getSelected(e).union(replace)
    })
    replace=replace.removeDuplicates
    
    var newCons : List[String]=replace--hasCons
    
    var newFormulas : List[Formula]=Nil;
    var oldFormulas : List[Formula]=t;
    newCons.foreach(e => {
      val c=createNewCons(e);
      oldFormulas=replaceSel(c,oldFormulas);
      newFormulas = c:: newFormulas
    })
    
    newFormulas:::oldFormulas

  }
  
  //replaces selectors in a term
  def replaceSelInTerm(a:String,l:String,r:String,t:Term):Term=t match{
    case Car(Var(v))=>if(v.equals(a)) Var(l)
                      else Car(Var(v))
    case Cdr(Var(v))=>if(v.equals(a)) Var(r)
                      else Cdr(Var(v))
    case Cons(t1,t2)=>Cons(replaceSelInTerm(a,l,r,t1),replaceSelInTerm(a,l,r,t2))
    case Car(t1)=>Car(replaceSelInTerm(a,l,r,t1))
    case Cdr(t1)=>Cdr(replaceSelInTerm(a,l,r,t1))
    case Var(v)=>Var(v)
    case Null() =>Null()
     
    
  } 
  
  //replaces selectors in all terms
  def replaceSel(f: Formula,l :List[Formula]):List[Formula]=f match{
    case Equals(Var(p),Cons(Var(lchild),Var(rchild)))=>l match{
      case Equals(a,b)::rest=>Equals(replaceSelInTerm(p,lchild,rchild,a),replaceSelInTerm(p,lchild,rchild,b))::replaceSel(f,rest) 
      case NotEquals(a,b)::rest=>NotEquals(replaceSelInTerm(p,lchild,rchild,a),replaceSelInTerm(p,lchild,rchild,b))::replaceSel(f,rest)
      case Nil => Nil
    }
    case _ => l
  }
  
  //creates new cons(wl,wr)=w formula that replaces the meaning of a slector on a variable
  def createNewCons(p: String): Formula= {
    val lchild: String = p + "l"
    val rchild: String = p + "r"
    Equals(Var(p),Cons(Var(lchild),Var(rchild)))
    }
  
  //finds all the variables in a formula that have selectors applied to them
  def getSelected(f: Formula): List[String] = f match {
    case Equals(t1,t2) => (getSelectorVars(t1).removeDuplicates).union(getSelectorVars(t2).removeDuplicates)
    case NotEquals(t1,t2) => (getSelectorVars(t1).removeDuplicates).union(getSelectorVars(t2).removeDuplicates)
  }
  def getSelectorVars(t : Term) : List[String] = t match {
    case Car(Var(l)) => l :: Nil
    case Car(t) => getSelectorVars(t)
    case Cdr(Var(l)) => l :: Nil
    case Cdr(t) => getSelectorVars(t)
    case Cons(t1,t2) =>  getSelectorVars(t1).union(getSelectorVars(t2))
    case _ => Nil
  }
  
  //checks if variable is a list or not
  def varIsCons(f: Formula): List[String] = f match {
    case Equals(Var(x),Cons(s,t)) => x :: Nil
    case Equals(Cons(c1,c2),Cons(c3,c4)) => varIsCons(Equals(c1,c3)).union(varIsCons(Equals(c2,c4)))
    case _ => Nil    
  }
  

  
}