From 473f033786d0be238f1a3b2f55e0a9ee7fee2ebf Mon Sep 17 00:00:00 2001 From: Robby Date: Tue, 12 Sep 2023 11:59:06 -0500 Subject: [PATCH] Added OrE support for <= and >=. --- .../sireum/logika/plugin/PropNatDedPlugin.scala | 17 ++++++++++++++++- 1 file changed, 16 insertions(+), 1 deletion(-) diff --git a/shared/src/main/scala/org/sireum/logika/plugin/PropNatDedPlugin.scala b/shared/src/main/scala/org/sireum/logika/plugin/PropNatDedPlugin.scala index 0272dd09..0ba04ad5 100644 --- a/shared/src/main/scala/org/sireum/logika/plugin/PropNatDedPlugin.scala +++ b/shared/src/main/scala/org/sireum/logika/plugin/PropNatDedPlugin.scala @@ -132,7 +132,22 @@ import org.sireum.logika.Logika.Reporter case string"OrE" => val ISZ(orClaimNo, leftSubProofNo, rightSubProofNo) = args val orClaim: AST.Exp.Binary = spcMap.get(orClaimNo) match { - case Some(StepProofContext.Regular(_, exp: AST.Exp.Binary, _)) if isBuiltIn(exp, AST.ResolvedInfo.BuiltIn.Kind.BinaryOr) => exp + case Some(StepProofContext.Regular(_, exp: AST.Exp.Binary, _)) if isBuiltIn(exp, AST.ResolvedInfo.BuiltIn.Kind.BinaryOr) => + exp + case Some(StepProofContext.Regular(_, exp: AST.Exp.Binary, _)) if isBuiltIn(exp, AST.ResolvedInfo.BuiltIn.Kind.BinaryLe) => + AST.Exp.Binary( + exp(op = AST.Exp.BinaryOp.Lt, attr = exp.attr(resOpt = Some(AST.ResolvedInfo.BuiltIn(AST.ResolvedInfo.BuiltIn.Kind.BinaryLt)))), + AST.Exp.BinaryOp.Or, + exp(op = AST.Exp.BinaryOp.Eq, attr = exp.attr(resOpt = Some(AST.ResolvedInfo.BuiltIn(AST.ResolvedInfo.BuiltIn.Kind.BinaryEq)))), + AST.ResolvedAttr(exp.posOpt, Some(AST.ResolvedInfo.BuiltIn(AST.ResolvedInfo.BuiltIn.Kind.BinaryOr)), AST.Typed.bOpt) + ) + case Some(StepProofContext.Regular(_, exp: AST.Exp.Binary, _)) if isBuiltIn(exp, AST.ResolvedInfo.BuiltIn.Kind.BinaryGe) => + AST.Exp.Binary( + exp(op = AST.Exp.BinaryOp.Gt, attr = exp.attr(resOpt = Some(AST.ResolvedInfo.BuiltIn(AST.ResolvedInfo.BuiltIn.Kind.BinaryGt)))), + AST.Exp.BinaryOp.Or, + exp(op = AST.Exp.BinaryOp.Eq, attr = exp.attr(resOpt = Some(AST.ResolvedInfo.BuiltIn(AST.ResolvedInfo.BuiltIn.Kind.BinaryEq)))), + AST.ResolvedAttr(exp.posOpt, Some(AST.ResolvedInfo.BuiltIn(AST.ResolvedInfo.BuiltIn.Kind.BinaryOr)), AST.Typed.bOpt) + ) case _ => reporter.error(orClaimNo.posOpt, Logika.kind, s"Expecting a proof step with a disjunction binary expression claim") return emptyResult