More refactoring, and fixed quant evals.

sireum · Feb 28, 2024 · fd0b887 · fd0b887
1 parent c501db6
commit fd0b887
Show file tree

Hide file tree

Showing 15 changed files with 149 additions and 176 deletions.
diff --git a/shared/src/main/scala/org/sireum/logika/Logika.scala b/shared/src/main/scala/org/sireum/logika/Logika.scala
diff --git a/shared/src/main/scala/org/sireum/logika/State.scala b/shared/src/main/scala/org/sireum/logika/State.scala
@@ -74,9 +74,11 @@ import org.sireum.message.Position
     return (newState, State.Value.sym(n, tipe, pos))
   }
 
-  @pure def unconstrainedClaims: State = {
+  @pure def unconstrainedClaims: (State, ISZ[(Z, Z)]) = {
     var r = ISZ[State.Claim]()
-    for (c <- claims) {
+    var r2 = ISZ[(Z, Z)]()
+    for (i <- 0 until claims.size) {
+      val c = claims(i)
       val add: B = c match {
         case _: State.Claim.Let.Id => T
         case _: State.Claim.Let.Name => T
@@ -87,10 +89,11 @@ import org.sireum.message.Position
       }
       if (add) {
         r = r :+ c
+        r2 = r2 :+ (i, r.size - 1)
       }
     }
     val thisL = this
-    return thisL(claims = r)
+    return (thisL(claims = r), r2)
   }
 
 }

diff --git a/shared/src/main/scala/org/sireum/logika/plugin/AdmitPlugin.scala b/shared/src/main/scala/org/sireum/logika/plugin/AdmitPlugin.scala
@@ -56,6 +56,6 @@ import org.sireum.logika.{Logika, Smt2, State, StepProofContext}
                       spcMap: HashSMap[AST.ProofAst.StepId, StepProofContext], state: State,
                       step: AST.ProofAst.Step.Regular, reporter: Logika.Reporter): State = {
     reporter.warn(step.claim.posOpt, Logika.kind, "Admitted claim")
-    return logika.evalRegularStepClaimRtCheck2(smt2, cache, F, state, step.claim, step.id.posOpt, reporter)
+    return logika.evalRegularStepClaimRtCheck(smt2, cache, F, state, step.claim, step.id.posOpt, reporter)
   }
 }
diff --git a/shared/src/main/scala/org/sireum/logika/plugin/AutoPlugin.scala b/shared/src/main/scala/org/sireum/logika/plugin/AutoPlugin.scala
@@ -329,14 +329,14 @@ object AutoPlugin {
                         |  ${(for (e <- pathConditions) yield e.prettyST, ";\n")}
                         |}""".render)
                 }
-                return logika.evalRegularStepClaimRtCheck2(smt2, cache, F, state, step.claim, step.id.posOpt, reporter)
+                return logika.evalRegularStepClaimRtCheck(smt2, cache, F, state, step.claim, step.id.posOpt, reporter)
               } else if (id == "Premise") {
                 AutoPlugin.detectOrIntro(logika.th, step.claim, pathConditions) match {
                   case Some(acceptMsg) =>
                     if (logika.config.detailedInfo) {
                       reporter.inform(pos, Logika.Reporter.Info.Kind.Verified, acceptMsg.render)
                     }
-                    return logika.evalRegularStepClaimRtCheck2(smt2, cache, F, state, step.claim, step.id.posOpt, reporter)
+                    return logika.evalRegularStepClaimRtCheck(smt2, cache, F, state, step.claim, step.id.posOpt, reporter)
                   case _ =>
                     reporter.error(posOpt, Logika.kind,
                       st"""The stated claim has not been proven before nor is a premise in the path conditions:
@@ -363,7 +363,8 @@ object AutoPlugin {
       val psmt2 = smt2.emptyCache(logika.config)
       val atMap = org.sireum.logika.Util.claimsToExps(logika.jescmPlugins._4, pos, logika.context.methodName,
         state.claims, logika.th, F, logika.config.atRewrite)._2
-      var s1 = state.unconstrainedClaims
+      val (suc, m) = state.unconstrainedClaims
+      var s1 = suc
       var ok = T
       for (arg <- just.witnesses if ok) {
         val stepNo = arg
@@ -389,7 +390,12 @@ object AutoPlugin {
           evalRegularStepClaimValue(psmt2, cache, s5, exp, step.id.posOpt, reporter)
       val r = checkValid(psmt2, s6, State.Claim.Prop(T, conclusion))
       smt2.combineWith(psmt2)
-      return if (r.ok) r(claims = state.claims ++ r.claims) else err
+      val sClaims = state.claims.toMS
+      for (p <- m) {
+        val (i, j) = p
+        sClaims(i) = r.claims(j)
+      }
+      return if (r.ok) r(claims = sClaims.toISZ[State.Claim] ++ ops.ISZOps(r.claims).slice(suc.claims.size, r.claims.size)) else err
     }
   }
 

diff --git a/shared/src/main/scala/org/sireum/logika/plugin/ClaimOfPlugin.scala b/shared/src/main/scala/org/sireum/logika/plugin/ClaimOfPlugin.scala
@@ -102,7 +102,7 @@ import org.sireum.logika.Logika.Reporter
       val substNormClaim = AST.Util.substExpSkipResolvedInfo(normClaim, sm)
       if (stepClaim == substNormClaim) {
         val claimPos = claim.posOpt.get
-        val s0 = logika.evalRegularStepClaimRtCheck2(smt2, cache, F, state, step.claim, step.id.posOpt, reporter)
+        val s0 = logika.evalRegularStepClaimRtCheck(smt2, cache, F, state, step.claim, step.id.posOpt, reporter)
         if (s0.ok && logika.config.detailedInfo) {
           reporter.inform(step.claim.posOpt.get, Reporter.Info.Kind.Verified,
             st"""Accepted by using $kind ${(name, ".")}'s claim at [${claimPos.beginLine}, ${claimPos.beginColumn}], i.e.:

diff --git a/shared/src/main/scala/org/sireum/logika/plugin/FoldUnfoldPlugin.scala b/shared/src/main/scala/org/sireum/logika/plugin/FoldUnfoldPlugin.scala
@@ -262,6 +262,6 @@ import FoldUnfoldPlugin._
             |""".render)
     }
 
-    return logika.evalRegularStepClaimRtCheck2(smt2, cache, F, state, step.claim, step.id.posOpt, reporter)
+    return logika.evalRegularStepClaimRtCheck(smt2, cache, F, state, step.claim, step.id.posOpt, reporter)
   }
 }
diff --git a/shared/src/main/scala/org/sireum/logika/plugin/InceptionPlugin.scala b/shared/src/main/scala/org/sireum/logika/plugin/InceptionPlugin.scala
@@ -302,7 +302,7 @@ import InceptionPlugin._
         reporter.error(step.claim.posOpt, Logika.kind, st"Could not derive the stated claim from $id's $conc${if (ensures.size > 1) "s" else ""}".render)
         return err
       }
-      val s0 = logika.evalRegularStepClaimRtCheck2(smt2, cache, F, state, step.claim, step.id.posOpt, reporter)
+      val s0 = logika.evalRegularStepClaimRtCheck(smt2, cache, F, state, step.claim, step.id.posOpt, reporter)
       if (s0.ok && logika.config.detailedInfo) {
         val (ePos, ensure, tensure) = ePosExpTExpOpt.get
         evidence = evidence :+

diff --git a/shared/src/main/scala/org/sireum/logika/plugin/LiftPlugin.scala b/shared/src/main/scala/org/sireum/logika/plugin/LiftPlugin.scala
@@ -139,7 +139,7 @@ import org.sireum.logika.{Logika, Smt2, State, StepProofContext}
       return err
     }
 
-    val s0 = logika.evalRegularStepClaimRtCheck2(smt2, cache, F, state, step.claim, step.id.posOpt, reporter)
+    val s0 = logika.evalRegularStepClaimRtCheck(smt2, cache, F, state, step.claim, step.id.posOpt, reporter)
     if (s0.ok && logika.config.detailedInfo) {
       val ipsSubst: ST = st"[${(for (pair <- ips.paramMap.entries) yield st"${pair._2.prettyST} / ${pair._1}", ", ")}]"
       reporter.inform(step.claim.posOpt.get, Logika.Reporter.Info.Kind.Verified,

diff --git a/shared/src/main/scala/org/sireum/logika/plugin/PredNatDedPlugin.scala b/shared/src/main/scala/org/sireum/logika/plugin/PredNatDedPlugin.scala
@@ -222,7 +222,7 @@ object PredNatDedPlugin {
           return err
         }
     }
-    val s0 = logika.evalRegularStepClaimRtCheck2(smt2, cache, F, state, step.claim, step.id.posOpt, reporter)
+    val s0 = logika.evalRegularStepClaimRtCheck(smt2, cache, F, state, step.claim, step.id.posOpt, reporter)
     if (s0.ok) {
       reporter.inform(step.claim.posOpt.get, Reporter.Info.Kind.Verified, acceptedMsg.render)
     }

diff --git a/shared/src/main/scala/org/sireum/logika/plugin/PropNatDedPlugin.scala b/shared/src/main/scala/org/sireum/logika/plugin/PropNatDedPlugin.scala
@@ -252,7 +252,7 @@ import org.sireum.logika.Logika.Reporter
           return err
         }
     }
-    val s0 = logika.evalRegularStepClaimRtCheck2(smt2, cache, F, state, step.claim, step.id.posOpt, reporter)
+    val s0 = logika.evalRegularStepClaimRtCheck(smt2, cache, F, state, step.claim, step.id.posOpt, reporter)
     if (s0.ok) {
       reporter.inform(step.claim.posOpt.get, Reporter.Info.Kind.Verified, acceptedMsg.render)
     }

diff --git a/shared/src/main/scala/org/sireum/logika/plugin/RewritePlugin.scala b/shared/src/main/scala/org/sireum/logika/plugin/RewritePlugin.scala
@@ -152,7 +152,7 @@ import org.sireum.logika.{Logika, RewritingSystem, Smt2, State, StepProofContext
             |
             |${traceOpt(rwPc.trace)}""".render)
       if (isSimpl) {
-        return logika.evalRegularStepClaimRtCheck2(smt2, cache, F, state, step.claim, step.id.posOpt, reporter)
+        return logika.evalRegularStepClaimRtCheck(smt2, cache, F, state, step.claim, step.id.posOpt, reporter)
       } else if (rwPc.methodPatterns.isEmpty) {
         reporter.warn(step.just.id.attr.posOpt, Logika.kind, "The claim can be discharged by using Simpl instead")
       } else if (rwPc.methodPatterns.nonEmpty && !isRSimpl) {
@@ -249,6 +249,6 @@ import org.sireum.logika.{Logika, RewritingSystem, Smt2, State, StepProofContext
         return err
       }
     }
-    return logika.evalRegularStepClaimRtCheck2(smt2, cache, F, state, step.claim, step.id.posOpt, reporter)
+    return logika.evalRegularStepClaimRtCheck(smt2, cache, F, state, step.claim, step.id.posOpt, reporter)
   }
 }
diff --git a/shared/src/main/scala/org/sireum/logika/plugin/SameDiffPlugin.scala b/shared/src/main/scala/org/sireum/logika/plugin/SameDiffPlugin.scala
@@ -87,10 +87,11 @@ import org.sireum.message.Position
     val logika2 = logika(plugins = SameDiffExpPlugin(posOpt, id, fromStepId, fromMap, step.id) +: logika.plugins)
 
     val s0: State = if (!just.hasWitness) {
-      logika2.evalRegularStepClaim2(smt2, cache, state, step.claim, step.id.posOpt, reporter)
+      logika2.evalRegularStepClaim(smt2, cache, state, step.claim, step.id.posOpt, reporter)
     } else {
       val psmt2 = smt2.emptyCache(logika.config)
-      var s1 = state.unconstrainedClaims
+      val (suc, m) = state.unconstrainedClaims
+      var s1 = suc
       var ok = T
       for (stepNo <- just.witnesses if ok) {
         spcMap.get(stepNo) match {
@@ -109,7 +110,13 @@ import org.sireum.message.Position
       if (!ok) {
         return err
       }
-      logika2.evalRegularStepClaim2(psmt2, cache, s1, step.claim, step.id.posOpt, reporter)
+      val sClaims = state.claims.toMS
+      for (p <- m) {
+        val (i, j) = p
+        sClaims(i) = s1.claims(j)
+      }
+      s1 = if (s1.ok) s1(claims = sClaims.toISZ[State.Claim] ++ ops.ISZOps(s1.claims).slice(suc.claims.size, s1.claims.size)) else err
+      logika2.evalRegularStepClaim(psmt2, cache, s1, step.claim, step.id.posOpt, reporter)
     }
     if (s0.ok && logika.config.detailedInfo) {
       val eqSTs: ISZ[ST] = for (num <- sortedNums) yield
@@ -137,7 +144,7 @@ import org.sireum.message.Position
             |""".render)
     }
 
-    return if (s0.ok) s0(claims = state.claims ++ s0.claims) else err
+    return if (s0.ok) s0 else err
   }
 }
 

diff --git a/shared/src/main/scala/org/sireum/logika/plugin/Smt2Plugin.scala b/shared/src/main/scala/org/sireum/logika/plugin/Smt2Plugin.scala
@@ -81,7 +81,8 @@ import org.sireum.logika.{Logika, Smt2, Smt2Config, Smt2Query, State, StepProofC
     val (s6, conclusion): (State, State.Value.Sym) = if (!just.hasWitness) {
       logikaSmt2.evalRegularStepClaimValue(smt2, cache, state, step.claim, step.id.posOpt, reporter)
     } else {
-      var s0 = state.unconstrainedClaims
+      val (suc, m) = state.unconstrainedClaims
+      var s0 = suc
       val atMap = org.sireum.logika.Util.claimsToExps(logikaSmt2.jescmPlugins._4, posOpt.get, logikaSmt2.context.methodName,
         state.claims, logikaSmt2.th, F, logikaSmt2.config.atRewrite)._2
       var ok = T
@@ -105,7 +106,13 @@ import org.sireum.logika.{Logika, Smt2, Smt2Config, Smt2Query, State, StepProofC
         return err
       }
       val (s4, exp) = logikaSmt2.rewriteAt(atMap, s0, step.claim, reporter)
-      logikaSmt2.evalRegularStepClaimValue(smt2, cache, s4, exp, step.id.posOpt, reporter)
+      val sClaims = state.claims.toMS
+      for (p <- m) {
+        val (i, j) = p
+        sClaims(i) = s4.claims(j)
+      }
+      val s5 = s4(claims = sClaims.toISZ[State.Claim] ++ ops.ISZOps(s4.claims).slice(suc.claims.size, s4.claims.size))
+      logikaSmt2.evalRegularStepClaimValue(smt2, cache, s5, exp, step.id.posOpt, reporter)
     }
 
     if (s6.ok) {
@@ -125,7 +132,7 @@ import org.sireum.logika.{Logika, Smt2, Smt2Config, Smt2Query, State, StepProofC
         case Smt2Query.Result.Kind.Error => error(s"Error occurred when deducing the claim of proof step ${step.id}")
       }
       val s7 = s6.addClaim(prop)
-      return if (status) if (just.hasWitness) s7(claims = state.claims ++ s7.claims) else s7 else err
+      return if (status) s7 else err
     } else {
       return err
     }

diff --git a/shared/src/main/scala/org/sireum/logika/plugin/SubstitutionPlugin.scala b/shared/src/main/scala/org/sireum/logika/plugin/SubstitutionPlugin.scala
@@ -102,7 +102,7 @@ import org.sireum.ops.ISZOps
                   reporter.error(step.claim.posOpt, Logika.kind, msg)
                   return err
                 } else {
-                  val s0 = logika.evalRegularStepClaimRtCheck2(smt2, cache, F, state, step.claim, step.id.posOpt, reporter)
+                  val s0 = logika.evalRegularStepClaimRtCheck(smt2, cache, F, state, step.claim, step.id.posOpt, reporter)
                   if (s0.ok && logika.config.detailedInfo) {
                     val msg =
                       st"""Accepted because:

diff --git a/shared/src/main/scala/org/sireum/logika/plugin/ValIntroElimPlugin.scala b/shared/src/main/scala/org/sireum/logika/plugin/ValIntroElimPlugin.scala
@@ -212,6 +212,6 @@ object ValIntroElimPlugin {
             |""".render)
     }
 
-    return logika.evalRegularStepClaimRtCheck2(smt2, cache, F, state, step.claim, step.id.posOpt, reporter)
+    return logika.evalRegularStepClaimRtCheck(smt2, cache, F, state, step.claim, step.id.posOpt, reporter)
   }
 }