From 885ec1ccddb0c5484cb2e884e1f5d8064b7a10c7 Mon Sep 17 00:00:00 2001 From: Robby Date: Mon, 12 Feb 2024 09:46:13 -0600 Subject: [PATCH] Rewriting system. --- .../main/scala/org/sireum/logika/RewritingSystem.scala | 9 ++++++++- .../scala/org/sireum/logika/plugin/RewritePlugin.scala | 2 +- 2 files changed, 9 insertions(+), 2 deletions(-) diff --git a/shared/src/main/scala/org/sireum/logika/RewritingSystem.scala b/shared/src/main/scala/org/sireum/logika/RewritingSystem.scala index 9deb5761..fbac7fc0 100644 --- 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 index b635d954..99d06150 100644 --- 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