better criteria for when ADT arguments should be expanded

uuverifiers · Oct 29, 2021 · 074084a · 074084a
1 parent 0f2557b
commit 074084a
Show file tree

Hide file tree

Showing 3 changed files with 37 additions and 7 deletions.
diff --git a/src/lazabs/horn/preprocessor/ArgumentExpander.scala b/src/lazabs/horn/preprocessor/ArgumentExpander.scala
@@ -56,6 +56,11 @@ abstract class ArgumentExpander extends HornPreprocessor {
    */
   def isExpandableSort(s : Sort) : Boolean
 
+  /**
+   * Set up the preprocessor for the given set of clauses.
+   */
+  def setup(clauses : Clauses) : Unit = {}
+
   override def isApplicable(clauses : Clauses) : Boolean =
     (HornClauses allPredicates clauses) exists {
       p => predArgumentSorts(p) exists isExpandableSort
@@ -80,6 +85,8 @@ abstract class ArgumentExpander extends HornPreprocessor {
 
   def process(clauses : Clauses, hints : VerificationHints)
              : (Clauses, VerificationHints, BackTranslator) = {
+    setup(clauses)
+
     val predicates =
       HornClauses allPredicates clauses
     val newPreds =

diff --git a/src/lazabs/horn/preprocessor/CtorTypeExtender.scala b/src/lazabs/horn/preprocessor/CtorTypeExtender.scala
@@ -31,11 +31,11 @@ package lazabs.horn.preprocessor
 
 import ap.parser._
 import IExpression.{Predicate, Sort, and}
-import ap.theories.ADT
+import ap.theories.{ADT, Theory}
 import ap.types.MonoSortedPredicate
 
 import scala.collection.mutable.{HashMap => MHashMap, ArrayBuffer,
-                                 LinkedHashMap}
+                                 LinkedHashMap, HashSet => MHashSet}
 
 object CtorTypeExtender {
 
@@ -127,6 +127,7 @@ object CtorTypeExtender {
 class CtorTypeExtender extends ArgumentExpander {
 
   import IExpression._
+  import HornPreprocessor.Clauses
 
   val name = "adding constructor id arguments"
 
@@ -141,10 +142,22 @@ class CtorTypeExtender extends ArgumentExpander {
   def expand(pred : Predicate, argNum : Int, sort : Sort)
            : Option[(Seq[(ITerm, Sort, String)], Option[ITerm])] = {
     val adtSort = sort.asInstanceOf[ADT.ADTProxySort]
-    val idfun = adtSort.adtTheory.ctorIds(adtSort.sortNum)
-    Some((List((idfun(v(0)), idfun.resSort, "ctor_id")), None))
+    if (usedTheories contains adtSort.adtTheory) {
+      val idfun = adtSort.adtTheory.ctorIds(adtSort.sortNum)
+      Some((List((idfun(v(0)), idfun.resSort, "ctor_id")), None))
+    } else {
+      None
+    }
+  }
+
+  override def setup(clauses : Clauses) : Unit = {
+    usedTheories.clear
+    for (clause <- clauses)
+      usedTheories ++= clause.theories
   }
 
+  private val usedTheories = new MHashSet[Theory]
+
   def isExpandableSort(s : Sort) : Boolean = s.isInstanceOf[ADT.ADTProxySort]
 
 }
diff --git a/src/lazabs/horn/preprocessor/SizeArgumentExtender.scala b/src/lazabs/horn/preprocessor/SizeArgumentExtender.scala
@@ -31,11 +31,11 @@ package lazabs.horn.preprocessor
 
 import ap.parser._
 import IExpression.{Predicate, Sort, and}
-import ap.theories.ADT
+import ap.theories.{ADT, Theory}
 import ap.types.MonoSortedPredicate
 
 import scala.collection.mutable.{HashMap => MHashMap, ArrayBuffer,
-                                 LinkedHashMap}
+                                 LinkedHashMap, HashSet => MHashSet}
 
 /**
  * Preprocessor that adds explicit size arguments for each predicate
@@ -44,13 +44,15 @@ import scala.collection.mutable.{HashMap => MHashMap, ArrayBuffer,
 class SizeArgumentExtender extends ArgumentExpander {
 
   import IExpression._
+  import HornPreprocessor.Clauses
 
   val name = "adding size arguments"
 
   def expand(pred : Predicate, argNum : Int, sort : Sort)
            : Option[(Seq[(ITerm, Sort, String)], Option[ITerm])] = {
     val adtSort = sort.asInstanceOf[ADT.ADTProxySort]
-    if (adtSort.adtTheory.termSize != null &&
+    if ((usedTheories contains adtSort.adtTheory) &&
+          adtSort.adtTheory.termSize != null &&
           recursiveADTSorts.getOrElseUpdate(adtSort, isRecursive(adtSort))) {
       val sizefun = adtSort.adtTheory.termSize(adtSort.sortNum)
       Some((List((sizefun(v(0)), Sort.Nat, "adt_size")), None))
@@ -81,6 +83,14 @@ class SizeArgumentExtender extends ArgumentExpander {
       }
     }
 
+  override def setup(clauses : Clauses) : Unit = {
+    usedTheories.clear
+    for (clause <- clauses)
+      usedTheories ++= clause.theories
+  }
+
+  private val usedTheories = new MHashSet[Theory]
+
   def isExpandableSort(s : Sort) : Boolean = s.isInstanceOf[ADT.ADTProxySort]
 
 }