package v1 import scala.util.parsing.combinator.syntactical.StandardTokenParsers import scala.util.parsing.input._ import scala.util.parsing.syntax._ import java.io._ object NelsonSAT 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(formulas, _) => try { println("Initial set of formulas:\n "+formulas) // we create nodes in our graph and give them unique equivalence classes val terms=gatherTerms(formulas).removeDuplicates; //println("The terms in the formula are:\n"+ terms.toString) var nodes=initEqClasses(terms,0) //println("Nodes(terms with eq classes) are:\n "+nodes) //we add terms and formulas that model the list properties //more pricisely that cons(car(a),cdr(a))=a, car(cons(a,b))=a, cdr(cons(a,b))=b var (newNodes,newFormulas)=addTerms(nodes,nodes,formulas) //println("Formulas after list constraints:\n "+newFormulas) //println("Nodes after list constraints:\n "+newNodes) //We merge the equivalence classes based on the //Congruence Closure on Graph Relations algorithm newNodes=mergeAll(newFormulas,newNodes) //println("nodes after congruence closure:\n "+newNodes) //search through the dis-equalities to find contradictions if(refute(newFormulas,newNodes)) println("satisfiable") else println("unsatisfiable") } catch { case tperror => println(tperror.toString) } case e => println(e) } } //gathers all terms from our set of formulas def gatherTerms(f:List[Formula]):List[Term]=f match { case Equals(a,b)::ftail =>a::b::(innerTerms(a):::innerTerms(b):::gatherTerms(ftail)) case NotEquals(a,b)::ftail=>a::b::(innerTerms(a):::innerTerms(b):::gatherTerms(ftail)) case Nil=>Nil } //gathers all the terms inside a term def innerTerms(t:Term):List[Term]=t match{ case Cons(a,b)=>a::b::innerTerms(a):::innerTerms(b) case Car(a)=>a::innerTerms(a) case Cdr(a)=>a::innerTerms(a) case Null() =>List(Null()) case Var(m) =>List(Var(m)) } //gives a unique equivalence class to each term def initEqClasses(l:List[Term],i:Int):List[(Term,String)]=l match { case h::t=>(h,i.toString)::initEqClasses(t,i+1) case Nil =>Nil } //adds the terms that model the list properties to the graph def addTerms(listNodes:List[(Term,String)],l:List[(Term,String)],formulas:List[Formula]):(List[(Term,String)],List[Formula])=listNodes match { case (Car(a),clcar)::rest=>{ val cla=classOf(a,l) val clconsold=classOf(Cons(Car(a),Cdr(a)),l) if(clconsold.equals("noclass")) addTerms(rest, (Cons(Car(a),Cdr(a)),cla)::l, Equals(Cons(Car(a),Cdr(a)),a)::formulas) else if(!clconsold.equals(cla)) addTerms(rest, changeClass(Cons(Car(a),Cdr(a)),cla,l), Equals(Cons(Car(a),Cdr(a)),a)::formulas) else addTerms(rest, l, Equals(Cons(Car(a),Cdr(a)),a)::formulas) } case (Cdr(a),clcdr)::rest=>{ val cla=classOf(a,l) val clconsold=classOf(Cons(Car(a),Cdr(a)),l) if(clconsold.equals("noclass")) addTerms(rest, (Cons(Car(a),Cdr(a)),cla)::l, Equals(Cons(Car(a),Cdr(a)),a)::formulas) else if(!clconsold.equals(cla)) addTerms(rest, changeClass(Cons(Car(a),Cdr(a)),cla,l), Equals(Cons(Car(a),Cdr(a)),a)::formulas) else addTerms(rest, l, Equals(Cons(Car(a),Cdr(a)),a)::formulas) } case (Cons(a,b),clab)::rest=>{ val cla=classOf(a,l) val clb=classOf(b,l) val clcar=classOf(Car(Cons(a,b)),l) val clcdr=classOf(Cdr(Cons(a,b)),l) var newListOfNodes=l if (!clcar.equals(cla)) if(clcar.equals("noclass")) newListOfNodes=(Car(Cons(a,b)),cla)::newListOfNodes else newListOfNodes=changeClass(Car(Cons(a,b)),cla,l) if (!clcar.equals(cla)) if (!clcdr.equals(clb)) if(clcdr.equals("noclass")) newListOfNodes=(Cdr(Cons(a,b)),clb)::newListOfNodes else newListOfNodes=changeClass(Cdr(Cons(a,b)),clb,l) //println(cla+"/"+clb+"/"+clcar+"/"+clcdr+"/"+newNodes) addTerms(rest, newListOfNodes, Equals(Car(Cons(a,b)),a)::Equals(Cdr(Cons(a,b)),b)::formulas) } case a::rest=>addTerms(rest,l,formulas) case Nil=>(l,formulas.removeDuplicates) } //calls the merge procedure for each pair of terms (a,b) where a=b is present in our set of formulas def mergeAll(f:List[Formula],l:List[(Term,String)]):List[(Term,String)]= f match { case Equals(a,b)::rest=>mergeAll(rest,merge(a,b,l)) case NotEquals(a,b)::rest=>mergeAll(rest,l) case Nil=>l } //modifies the equivalence class of a term t to clas c def changeClass(t:Term,c:String,l:List[(Term,String)]):List[(Term,String)]=l match{ case (term,clas)::rest=>if(areEqual(term,t)) (term,c)::changeClass(t,c,rest) else (term,clas)::changeClass(t,c,rest) case Nil=>Nil } //gets the equivalence class of term t def classOf(t:Term,l:List[(Term,String)]):String=l match { case (a,cl)::rest=>if(t.equals(a)) cl else classOf(t,rest) case Nil=>return "noclass" } //main congruence closure method described in the paper def merge(u:Term,v:Term,l:List[(Term,String)]):List[(Term,String)]= { val clu=classOf(u,l) val clv=classOf(v,l) val Pu=getPredsOfAll(u::getAllEquiv(clu,l),l) val Pv=getPredsOfAll(v::getAllEquiv(clv,l),l) var lnew=union(l,clu,clv) Pu.foreach(x=> { Pv.foreach( y=>{ val clx=classOf(x,lnew) val cly=classOf(y,lnew) if(!clx.equals(cly) && areCongruent((x,y),lnew)) lnew=merge(x,y,lnew) } ) } ) lnew } //gets the union of predecessors of each term from list l def getPredsOfAll(l:List[Term],lall:List[(Term,String)]):List[Term]=l match { case a::b=>Preds(a,lall).union(getPredsOfAll(b,lall)) case Nil=>Nil } //gets all predecessors of a term in terms of application of uninterpreted function def Preds(t:Term,lall:List[(Term,String)]):List[Term]=lall match { case (Cons(a,b),s)::rest =>if (areEqual((a,t)) ||areEqual((b,t))) Cons(a,b)::Preds(t,rest) else Preds(t,rest) case (Car(a),s)::rest =>if (areEqual((a,t))) Car(a)::Preds(t,rest) else Preds(t,rest) case (Cdr(a),s)::rest =>if (areEqual((a,t))) Cdr(a)::Preds(t,rest) else Preds(t,rest) case _::rest=>Preds(t,rest) case Nil=>Nil } //gets all the terms from equivalence class c1 def getAllEquiv(cl:String,l:List[(Term,String)]):List[Term]=l match { case (t,c)::rest=>if (cl.equals(cl)) t::getAllEquiv(cl,rest) else getAllEquiv(cl,rest) case Nil=>Nil } //checks if two terms have the same equivalence class def areCongruent(t:(Term,Term),l:List[(Term,String)]):Boolean=t match {case (Car(a),Car(b))=>classOf(a,l).equals(classOf(b,l)) case (Cdr(a),Cdr(b))=>classOf(a,l).equals(classOf(b,l)) case (Cons(a,b),Cons(c,d))=>classOf(a,l).equals(classOf(c,l))&&classOf(b,l).equals(classOf(d,l)) case _ =>false } //checks if two terms are identical def areEqual(t:(Term,Term)):Boolean=t match{ case (Cons(a,b),Cons(c,d))=>areEqual((a,c)) && areEqual((b,d)) case (Car(a),Car(b))=>areEqual((a,b)) case (Cdr(a),Cdr(b))=>areEqual((a,b)) case (Var(a),Var(b))=>a.equals(b) case _ => false } //unifies two equivalence classes c1 and c2 def union(l:List[(Term,String)],c1:String,c2:String):List[(Term,String)]=l match { case (t,cl)::rest=>if(cl.equals(c2)) (t,c1)::union(rest,c1,c2) else (t,cl)::union(rest,c1,c2) case Nil=>Nil } // tries to find contradictions based on equivalence classes of terms def refute(f:List[Formula],l:List[(Term,String)]):Boolean = f match{ case NotEquals(a,b)::rest=>if(classOf(a,l).equals(classOf(b,l))) false else refute(rest,l) case Equals(a,b)::rest=>refute(rest,l) case Nil=>true } }