Updated comparator in regex to combinator in order to match the thesis.

src/main/scala/viper/silver/ast/utility/Rewriter/RegexStrategy.scala

@@ -10,61 +10,62 @@ import viper.silver.ast.QuantifiedExp
 
 /**
   * Extension of the Strategy context. Encapsulates all the required information for the rewriting
-  * @param aList List of all the ancestors
-  * @param c context information
+ *
+  * @param aList       List of all the ancestors
+  * @param c           context information
   * @param transformer current transformer
-  * @param upContext Function that describes how we update the context in case new context information comes in
-  * @param comp Function that evaluates which context to take in case a node is in two possible contexts at the same time (true = first param, false = second param)
+  * @param upContext   Function that describes how we update the context in case new context information comes in
+  * @param comb Function that evaluates which context to take in case a node is in two possible contexts at the same time (true = first param, false = second param)
   * @tparam N Type of all AST nodes
   * @tparam COLL Type of custom context
   */
-class RegexContext[N <: Rewritable, COLL](aList: Seq[N], val c: COLL, transformer: StrategyInterface[N], private val upContext: (COLL, COLL) => COLL, val comp: (COLL, COLL) => Boolean) extends ContextA[N](aList, transformer) {
+class RegexContext[N <: Rewritable, COLL](aList: Seq[N], val c: COLL, transformer: StrategyInterface[N], private val upContext: (COLL, COLL) => COLL, val comb: (COLL, COLL) => COLL) extends ContextA[N](aList, transformer) {
 
   // Add an ancestor
   override def addAncestor(n: N): RegexContext[N, COLL] = {
-    new RegexContext(ancestorList ++ Seq(n), c, transformer, upContext, comp)
+    new RegexContext(ancestorList ++ Seq(n), c, transformer, upContext, comb)
   }
 
   // Replace the current node
   override def replaceNode(n: N): RegexContext[N, COLL] = {
-    new RegexContext(ancestorList.dropRight(1) ++ Seq(n), c, transformer, upContext, comp)
+    new RegexContext(ancestorList.dropRight(1) ++ Seq(n), c, transformer, upContext, comb)
   }
 
   // Update the context with new information
   def update(con: COLL): RegexContext[N, COLL] = {
-    new RegexContext(ancestorList, upContext(c, con), transformer, upContext, comp)
+    new RegexContext(ancestorList, upContext(c, con), transformer, upContext, comb)
   }
 
   // Compare the context in order decide which one to take
-  def compare(other: RegexContext[N, COLL]): Boolean = {
-    comp(this.c, other.c)
+  def combinate(other: RegexContext[N, COLL]): RegexContext[N, COLL] = {
+    new RegexContext(aList, comb(this.c, other.c), transformer, upContext, comb)
   }
 }
 
 /**
   * A class that misses some information in order to be a full RegexContext. Provides methods to create a complete one
   * @param c Custom context
   * @param upContext Function that describes how we update the context in case new context information comes in
-  * @param comp Function that evaluates which context to take in case a node is in two possible contexts at the same time (true = first param, false = second param)
+  * @param comb Function that evaluates which context to take in case a node is in two possible contexts at the same time (true = first param, false = second param)
   * @tparam N Common supertype of every node in the tree
   * @tparam COLL Type of custom context
   */
-class PartialContextR[N <: Rewritable, COLL](val c: COLL, val upContext: (COLL, COLL) => COLL, val comp: (COLL, COLL) => Boolean) extends PartialContext[N, ContextA[N]] {
+class PartialContextR[N <: Rewritable, COLL](val c: COLL, val upContext: (COLL, COLL) => COLL, val comb: (COLL, COLL) => COLL) extends PartialContext[N, ContextA[N]] {
 
   /**
     * Complete the Partial context by providing the missing information for a RegexContext
     * @param anc List of ancestors
     * @param transformer current transformer
     * @return complete RegexContext object
     */
-  def get(anc: Seq[N], transformer: StrategyInterface[N]): RegexContext[N, COLL] = new RegexContext[N, COLL](anc, c, transformer, upContext, comp)
+  def get(anc: Seq[N], transformer: StrategyInterface[N]): RegexContext[N, COLL] = new RegexContext[N, COLL](anc, c, transformer, upContext, comb)
 
   /**
     * Provide the transformer for the real context
     * @param transformer current transformer
     * @return A complete Context object
     */
-  override def get(transformer: StrategyInterface[N]): RegexContext[N, COLL] = new RegexContext[N, COLL](Seq(), c, transformer, upContext, comp)
+  override def get(transformer: StrategyInterface[N]): RegexContext[N, COLL] = new RegexContext[N, COLL](Seq(), c, transformer, upContext, comb)
 }
 
 /**
@@ -118,7 +119,7 @@ class RegexStrategy[N <: Rewritable, COLL](a: TRegexAutomaton, p: PartialFunctio
           case 0 => map.append((node, context, matchingNodes.length))
           case 1 =>
             val tup = exactlyMatchingNodes.head // Got only 1 element
-            val better = (node, if (tup._1._2.compare(context)) tup._1._2 else context, tup._1._3)
+            val better:(N, CTXT, Int) = (node, tup._1._2.combinate(context), tup._1._3)
             map.remove(tup._2)
             map.append(better)
           case _ => println("Multiple entries for same node: " + node)
@@ -241,9 +242,8 @@ class RegexStrategy[N <: Rewritable, COLL](a: TRegexAutomaton, p: PartialFunctio
     val resultNodeO = replaceInfo match {
       case None => None
       case Some(elem) =>
-        val temp = p.applyOrElse((n, elem), (els:(N, CTXT)) => els._1)
-        if (temp eq n)
-          Some(temp)
+        if (p.isDefinedAt(n, elem))
+          Some(p(n, elem))
         else
           None
     }

src/main/scala/viper/silver/ast/utility/Rewriter/TRegex.scala

@@ -270,12 +270,12 @@ class Questionmark(m: Match) extends Match {
 /**
   * Helps in building a complete Regular expression strategy by allowing it to be filled incrementally with: 1. Regular expression 2. Rewriting function
   * @param accumulator Describes how we put the contexts together into one object
-  * @param comparator Imposes an ordering on the contexts => in case a node matches in two ways on two different contexts the bigger one is taken (true = first param, false = second param)
+  * @param combinator Imposes an ordering on the contexts => in case a node matches in two ways on two different contexts the bigger one is taken (true = first param, false = second param)
   * @param default The default context we start with
   * @tparam N Type of the AST
   * @tparam COLL Type of the context
   */
-class TreeRegexBuilder[N <: Rewritable, COLL](val accumulator: (COLL, COLL) => COLL, val comparator: (COLL, COLL) => Boolean, val default: COLL) {
+class TreeRegexBuilder[N <: Rewritable, COLL](val accumulator: (COLL, COLL) => COLL, val combinator: (COLL, COLL) => COLL, val default: COLL) {
 
   /**
     * Generates a TreeRegexBuilderWithMatch by adding the matching part to the mix
@@ -299,7 +299,7 @@ class TreeRegexBuilderWithMatch[N <: Rewritable, COLL](tbuilder: TreeRegexBuilde
     * @param p partial function used for rewriting
     * @return complete RegexStrategy
     */
-  def |->(p: PartialFunction[(N, RegexContext[N, COLL]), N]) = new RegexStrategy[N, COLL](regex.createAutomaton(), p, new PartialContextR(tbuilder.default, tbuilder.accumulator, tbuilder.comparator))
+  def |->(p: PartialFunction[(N, RegexContext[N, COLL]), N]) = new RegexStrategy[N, COLL](regex.createAutomaton(), p, new PartialContextR(tbuilder.default, tbuilder.accumulator, tbuilder.combinator))
 }
 
 /**
@@ -339,13 +339,13 @@ object TreeRegexBuilder {
   /**
     * Constructs a TreeRegexBuilder
     * @param accumulator Describes how we put the contexts together into one object
-    * @param comparator Imposes an ordering on the contexts => in case a node matches in two ways on two different contexts the bigger one is taken (true = first param, false = second param)
+    * @param combinator Imposes an ordering on the contexts => in case a node matches in two ways on two different contexts merge it together
     * @param default The default context we start with
     * @tparam N Type of the AST
     * @tparam COLL Type of the context
     * @return
     */
-  def context[N <: Rewritable, COLL](accumulator: (COLL, COLL) => COLL, comparator: (COLL, COLL) => Boolean, default: COLL) = new TreeRegexBuilder[N, COLL](accumulator, comparator, default)
+  def context[N <: Rewritable, COLL](accumulator: (COLL, COLL) => COLL, combinator: (COLL, COLL) => COLL, default: COLL) = new TreeRegexBuilder[N, COLL](accumulator, combinator, default)
 
   /**
     * Don't care about the custom context but want ancestor/sibling information

src/main/scala/viper/silver/ast/utility/ViperStrategy.scala

@@ -48,7 +48,7 @@ class SlimViperRegexStrategy[C](a: TRegexAutomaton, p: PartialFunction[Node, Nod
 }
 
 
-class ViperRegexBuilder[C](acc: (C, C) => C, comp: (C, C) => Boolean, dflt: C) extends TreeRegexBuilder[Node, C](acc, comp, dflt) {
+class ViperRegexBuilder[C](acc: (C, C) => C, comp: (C, C) => C, dflt: C) extends TreeRegexBuilder[Node, C](acc, comp, dflt) {
 
   /**
     * Generates a TreeRegexBuilderWithMatch by adding the matching part to the mix
@@ -62,7 +62,7 @@ class ViperRegexBuilder[C](acc: (C, C) => C, comp: (C, C) => Boolean, dflt: C) e
 
 class ViperRegexBuilderWithMatch[C](v: ViperRegexBuilder[C], m: Match) extends TreeRegexBuilderWithMatch[Node, C](v, m) {
 
-  override def |->(p: PartialFunction[(Node, RegexContext[Node, C]), Node]): ViperRegexStrategy[C] = new ViperRegexStrategy[C](m.createAutomaton(), p, new PartialContextR[Node, C](v.default, v.accumulator, v.comparator))
+  override def |->(p: PartialFunction[(Node, RegexContext[Node, C]), Node]): ViperRegexStrategy[C] = new ViperRegexStrategy[C](m.createAutomaton(), p, new PartialContextR[Node, C](v.default, v.accumulator, v.combinator))
 }
 
 
@@ -85,8 +85,8 @@ object ViperStrategy {
     new SlimViperRegexBuilder &> m |-> p
   }
 
-  def Regex[C](m: Match, p: PartialFunction[(Node, RegexContext[Node, C]), Node], default: C, acc: (C, C) => C, comp: (C, C) => Boolean) = {
-    new ViperRegexBuilder[C](acc, comp, default) &> m |-> p
+  def Regex[C](m: Match, p: PartialFunction[(Node, RegexContext[Node, C]), Node], default: C, acc: (C, C) => C, comb: (C, C) => C) = {
+    new ViperRegexBuilder[C](acc, comb, default) &> m |-> p
   }
 
   /**

src/test/scala/RegexTests.scala

@@ -25,17 +25,16 @@ class RegexTests extends FunSuite {
     val shared = FalseLit()()
     val sharedAST = And(Not(shared)(), shared)()
 
-    val t = TreeRegexBuilder.context[Node, Int](_ + _, _ > _, 0)
+    val t = TreeRegexBuilder.context[Node, Int](_ + _, math.max , 0)
     val strat = t &> c[Not](_ => 1) > n.r[FalseLit] |-> { case (FalseLit(), c) => if(c.c == 1) TrueLit()() else FalseLit()()}
 
     val res = strat.execute[Exp](sharedAST)
 
     // Check that both FalseLits were differently transformed
     res match {
-      case And(Not(t1), t2) => {
+      case And(Not(t1), t2) =>
         assert(t1 == TrueLit()())
         assert(t2 == FalseLit()())
-      }
       case _ => assert(false)
     }
   }
@@ -61,7 +60,6 @@ class RegexTests extends FunSuite {
       case (None, errors) => println("Problem with program: " + errors)
     }
 
-
     val res = time(strat.execute[Program](targetNode))
 
     assert(true)
@@ -98,7 +96,7 @@ class RegexTests extends FunSuite {
       }
 
       // Regular expression
-      val t = TreeRegexBuilder.context[Node, Seq[LocalVarDecl]]( _ ++ _ , _.size > _.size, Seq.empty[LocalVarDecl])
+      val t = TreeRegexBuilder.context[Node, Seq[LocalVarDecl]]( _ ++ _, (x,y) => (x ++ y).distinct, Seq.empty[LocalVarDecl])
       val strat = t &> c[QuantifiedExp]( _.variables).** >> n.r[Or] |-> { case (o:Or, c) => InhaleExhaleExp(CondExp(NonDet(c.c), o.left, o.right)(), c.noRec[Or](o))() }
 
       frontend.translate(ref) match {
@@ -120,7 +118,7 @@ class RegexTests extends FunSuite {
     val files = Seq("simple", "complex")
 
     // Regular expression
-    val t = TreeRegexBuilder.context[Node, Int](_ + _, _ > _, 0)
+    val t = TreeRegexBuilder.context[Node, Int](_ + _, math.max, 0)
     val strat = t &> iC[Method](_.body, _.name == "here") >> (n[Inhale] | n[Exhale]) >> (c[Or]( _ => 1 )  | c[And]( _ => 1)).* >> n.r[LocalVar]((v:LocalVar) => v.typ == Int && v.name.contains("x")) |-> { case (n:LocalVar, c) => IntLit(c.c)(n.pos, n.info, n.errT)}
 
     val frontend = new DummyFrontend