option to disable additional ADT/heap arguments

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

Hide file tree

Showing 2 changed files with 8 additions and 3 deletions.
diff --git a/src/lazabs/Main.scala b/src/lazabs/Main.scala
@@ -103,6 +103,7 @@ class GlobalParameters extends Cloneable {
     CCReader.ArithmeticMode.Mathematical
   var arrayRemoval = false
   var arrayQuantification : Option[Int] = None
+  var expandADTArguments = true
   var princess = false
   var staticAccelerate = false
   var dynamicAccelerate = false
@@ -189,6 +190,7 @@ class GlobalParameters extends Cloneable {
     that.finiteDomainPredBound = this.finiteDomainPredBound
     that.arithmeticMode = this.arithmeticMode
     that.arrayRemoval = this.arrayRemoval
+    that.expandADTArguments = this.expandADTArguments
     that.princess = this.princess
     that.staticAccelerate = this.staticAccelerate
     that.dynamicAccelerate = this.dynamicAccelerate

diff --git a/src/lazabs/horn/preprocessor/DefaultPreprocessor.scala b/src/lazabs/horn/preprocessor/DefaultPreprocessor.scala
@@ -57,9 +57,12 @@ class DefaultPreprocessor extends HornPreprocessor {
          new ClauseInliner)
 
   def extendingStages : List[HornPreprocessor] =
-    List(new HeapSizeArgumentExtender,
-         new SizeArgumentExtender,
-         new CtorTypeExtender)
+    if (GlobalParameters.get.expandADTArguments)
+      List(new HeapSizeArgumentExtender,
+           new SizeArgumentExtender,
+           new CtorTypeExtender)
+    else
+      List()
 
   def postStages : List[HornPreprocessor] =
     List(new ClauseShortener) ++