Add changes from theory-of-heaps-translation-thesis-version

uuverifiers · Jun 17, 2024 · 481819f · 481819f
1 parent b081923
commit 481819f
Show file tree

Hide file tree

Showing 3 changed files with 25 additions and 6 deletions.
diff --git a/src/tricera/Main.scala b/src/tricera/Main.scala
@@ -678,7 +678,7 @@ class Main (args: Array[String]) {
                     printlnDebug(postClauses.toString)
 
                     acslProcessedSolution = addClauses(
-                      postClauses,ctx.prePred.pred, acslProcessedSolution)
+                      postClauses,ctx.postPred.pred, acslProcessedSolution)
                   }
 
                   val printHeapExprProcessors = Seq(

diff --git a/src/tricera/concurrency/CCReader.scala b/src/tricera/concurrency/CCReader.scala
@@ -696,7 +696,7 @@ class CCReader private (prog              : Program,
 
   if (modelHeap) {
     GlobalVars addVar heapVar
-    GlobalVars.inits += CCTerm(heap.emptyHeap(), CCHeap(heap), None)
+    GlobalVars.inits += CCTerm(heapTerm, CCHeap(heap), None)
     variableHints += List()
   }
 

diff --git a/src/tricera/postprocessor/ADTExploder.scala b/src/tricera/postprocessor/ADTExploder.scala
@@ -64,6 +64,23 @@ object ADTExploder extends SolutionProcessor
                            subres: Seq[IExpression]) : IExpression = {
 
       import IExpression._
+      def checkExplodable(originalEq : IEquation, ctorFun : IFunction,
+                       lhsIsCtor : Boolean) : Boolean = {
+        val newEq = originalEq update subres
+        val (newFunApp, selectorTerms, newRootTerm) =
+          if (lhsIsCtor) {
+            val Eq(newFunApp@IFunApp(_, selectorTerms), newRootTerm) = newEq
+            (newFunApp, selectorTerms, newRootTerm)
+          } else {
+            val Eq(newRootTerm, newFunApp@IFunApp(_, selectorTerms)) = newEq
+            (newFunApp, selectorTerms, newRootTerm)
+          }
+        val adtTerm = getADTTerm(newFunApp).get
+        val adt = adtTerm.adtSort.adtTheory
+        val ctorIndex = adt.constructors.indexOf(ctorFun)
+        ctorIndex != -1
+      }
+
       def explodeADTSelectors (originalEq : IEquation, ctorFun : IFunction,
                                lhsIsCtor : Boolean) = {
         val newEq = originalEq update subres
@@ -85,10 +102,12 @@ object ADTExploder extends SolutionProcessor
       }
 
       t match {
-        case e@Eq(funApp@IFunApp(fun, _), _) if getADTTerm(funApp).nonEmpty =>
-          explodeADTSelectors(e.asInstanceOf[IEquation], fun, lhsIsCtor = true)
-        case e@Eq(_, funApp@IFunApp(fun, _)) if getADTTerm(funApp).nonEmpty =>
-          explodeADTSelectors(e.asInstanceOf[IEquation], fun, lhsIsCtor = false)
+        case e@Eq(funApp@IFunApp(fun, _), _) if getADTTerm(funApp).nonEmpty &&
+              checkExplodable(e.asInstanceOf[IEquation], fun, lhsIsCtor = true) =>
+                explodeADTSelectors(e.asInstanceOf[IEquation], fun, lhsIsCtor = true)
+        case e@Eq(_, funApp@IFunApp(fun, _)) if getADTTerm(funApp).nonEmpty &&
+              checkExplodable(e.asInstanceOf[IEquation], fun, lhsIsCtor = false) =>
+                explodeADTSelectors(e.asInstanceOf[IEquation], fun, lhsIsCtor = false)
         case t@IFunApp(f,_) =>
           val newApp = t update subres
           (for (theory <- TheoryRegistry lookupSymbol f;