Rewriting system.

sireum · Feb 21, 2024 · 357cdd6 · 357cdd6
1 parent 137b450
commit 357cdd6
Show file tree

Hide file tree

Showing 2 changed files with 43 additions and 28 deletions.
diff --git a/jvm/src/test/scala/org/sireum/logika/example/rewrite.sc b/jvm/src/test/scala/org/sireum/logika/example/rewrite.sc
@@ -47,7 +47,7 @@ import Rules._
       //@formatter:off
       1  (c ≡ d)              by Premise,
       2  ((d + 1) ≡ 3)        by Premise,
-      4  ((c + 1) ≡ 3)        by Rewrite(~RS(subst _), 2) and (1, 2) // and (...) is optional but it makes the search faster
+      3  ((c + 1) ≡ 3)        by Rewrite(~RS(subst _), 2) and (1, 2) // and (...) is optional but it makes the search faster
       //@formatter:on
     )
   )
@@ -75,10 +75,10 @@ import Rules._
   Deduce(
     //@formatter:off
     1  (EvalFoo(x = 4, y = 5).x == 4)   by Simpl,
-    3  (o(x = 4, y = 5).x == 4)         by Simpl,
-    5  (o(x = 4, y = 5).y == 5)         by Simpl,
-    7  (o(x = 4)(y = 1)(x = 5).x == 5)  by Simpl,
-    9  (o(x = 4)(x = 5).y == o.y)       by Simpl
+    2  (o(x = 4, y = 5).x == 4)         by Simpl,
+    3  (o(x = 4, y = 5).y == 5)         by Simpl,
+    4  (o(x = 4)(y = 1)(x = 5).x == 5)  by Simpl,
+    5  (o(x = 4)(x = 5).y == o.y)       by Simpl
     //@formatter:on
   )
 }
@@ -87,7 +87,7 @@ import Rules._
   Deduce(
     //@formatter:off
     1  ((1, 2)._1 == 1)   by Simpl,
-    3  ((1, 2)._2 == 2)   by Simpl
+    2  ((1, 2)._2 == 2)   by Simpl
     //@formatter:on
   )
 }
@@ -101,10 +101,10 @@ import Rules._
     1  (i != j)                             by Premise,
     2  (i == k)                             by Premise,
     3  (ISZ(1, 2, 3).size == 3)             by Simpl,
-    5  (ISZ[Z](1, 2, 3)(0 ~> 5).size == 3)  by Simpl,
-    7  (a(0 ~> t1).size == a.size)          by Simpl,
-    9  (a(i ~> t1)(j ~> t2)(i) == t1)       by Simpl,
-    11 (a(i ~> t1)(k ~> t2)(i) == t2)       by Simpl
+    4  (ISZ[Z](1, 2, 3)(0 ~> 5).size == 3)  by Simpl,
+    5  (a(0 ~> t1).size == a.size)          by Simpl,
+    6  (a(i ~> t1)(j ~> t2)(i) == t1)       by Simpl,
+    7  (a(i ~> t1)(k ~> t2)(i) == t2)       by Simpl
     //@formatter:on
   )
 }
@@ -130,3 +130,15 @@ import Rules._
     //@formatter:on
   )
 }
+
+@pure def evalTest(a: Z, b: Z): Unit = {
+  Contract(
+    Requires(a + b + (3 - 1) > 3)
+  )
+  Deduce(
+    //@formatter:off
+    1  (a + b + (3 - 1) > 3)                  by Premise,
+    2  (a + b + 2 > 3)                        by Eval(1)
+    //@formatter:on
+  )
+}
diff --git a/shared/src/main/scala/org/sireum/logika/plugin/RewritePlugin.scala b/shared/src/main/scala/org/sireum/logika/plugin/RewritePlugin.scala
@@ -84,11 +84,26 @@ import org.sireum.logika.{Logika, RewritingSystem, Smt2, State, StepProofContext
         }
         (r1, r2)
       }
+    val (fromOpt, fromClaim): (Option[AST.ProofAst.StepId], AST.Exp) = if (isRSimpl || isSimpl) {
+      (None(), AST.Exp.LitB(T, step.just.id.attr))
+    } else {
+      val from: AST.ProofAst.StepId =
+        AST.Util.toStepIds(ISZ(justArgs(if (isEval) 0 else 1)), Logika.kind, reporter) match {
+          case Some(s) => s(0)
+          case _ => return emptyResult
+        }
+      spcMap.get(from) match {
+        case Some(spc: StepProofContext.Regular) => (Some(from), spc.exp)
+        case _ =>
+          reporter.error(from.posOpt, Logika.kind, s"Expecting a regular proof step")
+          return emptyResult
+      }
+    }
     var provenClaims = HashSMap.empty[AST.ProofAst.StepId, AST.CoreExp.Base]
     if (step.just.hasWitness) {
       for (w <- step.just.witnesses) {
         spcMap.get(w) match {
-          case Some(spc: StepProofContext.Regular) =>
+          case Some(spc: StepProofContext.Regular) if isEval ___>: (w != fromOpt.get) =>
             provenClaims = provenClaims + w ~> spc.coreExpClaim
           case Some(_) =>
             reporter.error(w.posOpt, Logika.kind, s"Expecting a regular proof step for $w")
@@ -99,7 +114,10 @@ import org.sireum.logika.{Logika, RewritingSystem, Smt2, State, StepProofContext
     } else {
       for (spc <- spcMap.values) {
         spc match {
-          case spc: StepProofContext.Regular if !spc.stepNo.isPremise =>
+          case spc: StepProofContext.Regular if !spc.stepNo.isPremise && (isEval ___>: (spc.stepNo != fromOpt.get)) =>
+            println(fromOpt)
+            println(spc.stepNo)
+            println(isEval ___>: (spc.stepNo != fromOpt.get))
             provenClaims = provenClaims + spc.stepNo ~> spc.coreExpClaim
           case _ =>
         }
@@ -157,21 +175,6 @@ import org.sireum.logika.{Logika, RewritingSystem, Smt2, State, StepProofContext
     } else {
       val simplTrace = rwPc.trace
       rwPc.trace = ISZ()
-      val (fromOpt, fromClaim): (Option[ST], AST.Exp) = if (isRSimpl) {
-        (None(), AST.Exp.LitB(T, step.just.id.attr))
-      } else {
-        val from: AST.ProofAst.StepId =
-          AST.Util.toStepIds(ISZ(justArgs(if (isEval) 0 else 1)), Logika.kind, reporter) match {
-            case Some(s) => s(0)
-            case _ => return emptyResult
-          }
-        spcMap.get(from) match {
-          case Some(spc: StepProofContext.Regular) => (Some(st" $from"), spc.exp)
-          case _ =>
-            reporter.error(from.posOpt, Logika.kind, s"Expecting a regular proof step")
-            return emptyResult
-        }
-      }
       val fromCoreClaim = RewritingSystem.translateExp(logika.th, F, fromClaim)
       @strictpure def simplTraceOpt: Option[ST] = if (stepClaim == stepClaimEv) None() else Some(
         st"""and/or after simplifying the step claim to:
@@ -213,7 +216,7 @@ import org.sireum.logika.{Logika, RewritingSystem, Smt2, State, StepProofContext
         }
       }
       @strictpure def fromCoreClaimST: Option[ST] = if (fromOpt.isEmpty) None() else Some(
-        st"""After ${if (isEval) "evaluating" else "rewriting"}$fromOpt:
+        st"""After ${if (isEval) "evaluating" else "rewriting"}${if (fromOpt.isEmpty) st"" else st" ${fromOpt.get}"}:
             |  ${fromCoreClaim.prettyST}
             |"""
       )