Improvements to matching heuristics (#389)

* refactor b heuristic

* fix r heuristic

* add o heuristic

matching/src/main/scala/org/kframework/backend/llvm/matching/Heuristics.scala

@@ -131,14 +131,18 @@ object DHeuristic extends Heuristic {
 object BHeuristic extends Heuristic {
   val needsMatrix: Boolean = false
 
-  def computeScoreForKey(c: AbstractColumn, key: Option[Pattern[Option[Occurrence]]]): Double = {
+  def bf(c: AbstractColumn, key: Option[Pattern[Option[Occurrence]]]): Int = {
     val sigma = c.column.signatureForKey(key)
     if (c.column.category.hasIncompleteSignature(sigma, c.column.fringe)) {
-      -sigma.size-1
+      sigma.size+1
     } else {
-      -sigma.size
+      sigma.size
     }
   }
+
+  def computeScoreForKey(c: AbstractColumn, key: Option[Pattern[Option[Occurrence]]]): Double = {
+    -bf(c, key)
+  }
 }
 
 @NamedHeuristic(name='a')
@@ -191,7 +195,7 @@ object RHeuristic extends Heuristic {
     val signature = c.column.signatureForKey(key)
     for (con <- signature) {
       for (i <- c.column.patterns.indices) {
-        if (c.column.patterns(i).isSpecialized(con, false, c.column.fringe, c.column.clauses(i), c.column.maxPriority)) {
+        if (c.column.patterns(i).isSpecialized(con, false, c.column.fringe, c.column.clauses(i), c.column.maxPriorityForKey(key))) {
           result += 1.0
         }
       }
@@ -268,6 +272,25 @@ object QHeuristic extends Heuristic {
   }
 }
 
+/**
+ * One branch heuristic. Essentially, o is to b as f is to q. Where b measures
+ * the total number of branches resulting from choosing a particular column,
+ * and picks the column with the least branches, o only measures whether
+ * choosing a particular column has a branching factor of 1, ie, no branching.
+ * As a result, you can use the 'o' heuristic before the 'q' heuristic as
+ * a way of reducing the cost of generating the decision tree at the expense
+ * of greater path length.
+ */
+@NamedHeuristic(name='o')
+object OHeuristic extends Heuristic {
+  val needsMatrix: Boolean = false
+
+  def computeScoreForKey(c: AbstractColumn, key: Option[Pattern[Option[Occurrence]]]): Double = {
+    //-c.column.bf
+    if (BHeuristic.bf(c, key) == 1) 1 else 0
+  }
+}
+
 sealed trait PseudoHeuristic extends Heuristic {
   val needsMatrix: Boolean = false
 

matching/src/main/scala/org/kframework/backend/llvm/matching/Matrix.scala

@@ -136,7 +136,9 @@ class Column(val fringe: Fringe, val patterns: IndexedSeq[Pattern[String]], val
     signatureForKey(bestKey)
   }
 
-  def isChoice: Boolean = fringe.sortInfo.isCollection && bestKey == None
+  def isChoice: Boolean = isChoiceForKey(bestKey)
+
+  def isChoiceForKey(key: Option[Pattern[Option[Occurrence]]]) = fringe.sortInfo.isCollection && key == None
 
   private def asListP(p: Pattern[String]): Seq[ListP[String]] = {
     p match {
@@ -182,8 +184,10 @@ class Column(val fringe: Fringe, val patterns: IndexedSeq[Pattern[String]], val
     }
   }
 
-  def maxPriority: Int = {
-    if (isChoice) {
+  def maxPriority: Int = maxPriorityForKey(bestKey)
+
+  def maxPriorityForKey(key: Option[Pattern[Option[Occurrence]]]) = {
+    if (isChoiceForKey(key)) {
       clauses(0).action.priority
     } else {
       Int.MaxValue