Rewriting system.

sireum · Feb 12, 2024 · 885ec1c · 885ec1c
1 parent cf60c29
commit 885ec1c
Show file tree

Hide file tree

Showing 2 changed files with 9 additions and 2 deletions.
diff --git a/shared/src/main/scala/org/sireum/logika/RewritingSystem.scala b/shared/src/main/scala/org/sireum/logika/RewritingSystem.scala
@@ -199,7 +199,7 @@ object RewritingSystem {
                     case Either.Left(m2) =>
                       for (k <- 0 until apcs.size) {
                         for (apc <- toCondEquiv(th, apcs(k))) {
-                          patterns = patterns :+ Rewriter.Pattern(pattern.name :+ s"Assumption$k", F,
+                          patterns = patterns :+ Rewriter.Pattern(pattern.name :+ s"Assumption$k", pattern.rightToLeft,
                             isPermutative(apc), HashSSet.empty, apc)
                         }
                       }
@@ -326,6 +326,13 @@ object RewritingSystem {
               }
               return AST.CoreExp.LocalVarRef(isPattern, res.context, id, e.typedOpt.get)
             case res: AST.ResolvedInfo.Var if res.isInObject =>
+              if (res.owner == AST.Typed.sireumName) {
+                res.id match {
+                  case "T" => return AST.CoreExp.LitB(T)
+                  case "F" => return AST.CoreExp.LitB(F)
+                  case _ =>
+                }
+              }
               return AST.CoreExp.ObjectVarRef(res.owner, res.id, e.typedOpt.get)
             case res: AST.ResolvedInfo.Method => halt(s"TODO: $e")
             case _ => halt(s"Infeasible: $e")

diff --git a/shared/src/main/scala/org/sireum/logika/plugin/RewritePlugin.scala b/shared/src/main/scala/org/sireum/logika/plugin/RewritePlugin.scala
@@ -66,7 +66,7 @@ import org.sireum.logika.{Logika, RewritingSystem, Smt2, State, StepProofContext
       case _ => F
     }
     val just = step.just.asInstanceOf[AST.ProofAst.Step.Justification.Apply]
-    var patterns = RewritingSystem.retrievePatterns(logika.th, cache, just.args(0))
+    val patterns = RewritingSystem.retrievePatterns(logika.th, cache, just.args(0))
     val from: AST.ProofAst.StepId = AST.Util.toStepIds(ISZ(just.args(1)), Logika.kind, reporter) match {
       case Some(s) => s(0)
       case _ => return emptyResult