From b6ebab90dbad34a0c830ac9d5c666209c5320d5d Mon Sep 17 00:00:00 2001 From: Robby Date: Mon, 2 Dec 2024 15:33:20 -0600 Subject: [PATCH] Fixed Auto justification issues. --- .../src/main/scala/org/sireum/logika/Logika.scala | 9 +++++++-- .../org/sireum/logika/plugin/AutoPlugin.scala | 15 +++++++-------- .../sireum/logika/plugin/PredNatDedPlugin.scala | 2 +- .../sireum/logika/plugin/PropNatDedPlugin.scala | 4 ++-- 4 files changed, 17 insertions(+), 13 deletions(-) diff --git a/shared/src/main/scala/org/sireum/logika/Logika.scala b/shared/src/main/scala/org/sireum/logika/Logika.scala index 936c98bb..66112ec5 100644 --- a/shared/src/main/scala/org/sireum/logika/Logika.scala +++ b/shared/src/main/scala/org/sireum/logika/Logika.scala @@ -1835,6 +1835,11 @@ import Util._ def evalSelect(exp: AST.Exp.Select): ISZ[(State, State.Value)] = { val pos = exp.id.attr.posOpt.get + exp.attr.resOpt.get match { + case res: AST.ResolvedInfo.Method if res.tpeOpt.isEmpty => + println("Here") + case _ => + } exp.attr.resOpt.get match { case res: AST.ResolvedInfo.BuiltIn if res.kind == AST.ResolvedInfo.BuiltIn.Kind.IsInstanceOf || res.kind == AST.ResolvedInfo.BuiltIn.Kind.AsInstanceOf => @@ -4878,7 +4883,7 @@ import Util._ if (s0.ok) { if (step.steps.size > 0) { m = stateMap._2 + stepNo ~> StepProofContext.SubProof(stepNo, - th.normalizeExp(step.steps(0).asInstanceOf[AST.ProofAst.Step.Assume].claim), extractClaims(step.steps), + step.steps(0).asInstanceOf[AST.ProofAst.Step.Assume].claim, extractClaims(step.steps), extractSpcs(1, step.steps)) } return (s0, m) @@ -4918,7 +4923,7 @@ import Util._ if (step.steps.nonEmpty && step.steps(0).isInstanceOf[AST.ProofAst.Step.Assume]) { return (s0, stateMap._2 + stepNo ~> StepProofContext.FreshAssumeSubProof(stepNo, step.context, step.params, - th.normalizeExp(step.steps(0).asInstanceOf[AST.ProofAst.Step.Assume].claim), + step.steps(0).asInstanceOf[AST.ProofAst.Step.Assume].claim, extractClaims(step.steps), extractSpcs(1, step.steps))) } else { return (s0, diff --git a/shared/src/main/scala/org/sireum/logika/plugin/AutoPlugin.scala b/shared/src/main/scala/org/sireum/logika/plugin/AutoPlugin.scala index d45dc9f5..26bd3038 100644 --- a/shared/src/main/scala/org/sireum/logika/plugin/AutoPlugin.scala +++ b/shared/src/main/scala/org/sireum/logika/plugin/AutoPlugin.scala @@ -356,7 +356,7 @@ object AutoPlugin { r = r + logika.th.normalizeExp(claim) ~> (spc.stepNo, T, claim) case spc: StepProofContext.SubProof => val claims: ISZ[AST.Exp] = for (p <- computeProvenClaims(spc.spcs).entries) yield p._2._3 - val claim = AST.Util.bigImply(F, ISZ(spc.assumption, AST.Util.bigAnd(claims, spc.stepNo.posOpt)), spc.stepNo.posOpt) + val claim = AST.Util.bigImply(T, ISZ(spc.assumption, AST.Util.bigAnd(claims, spc.stepNo.posOpt)), spc.stepNo.posOpt) r = r + logika.th.normalizeExp(claim) ~> (spc.stepNo, F, claim) case spc: StepProofContext.FreshSubProof => val claims: ISZ[AST.Exp] = for (p <- computeProvenClaims(spc.spcs).entries) yield p._2._3 @@ -376,7 +376,7 @@ object AutoPlugin { params = params :+ AST.Exp.Fun.Param(Some(p.id), p.tipeOpt, p.tipeOpt.get.typedOpt) } val claim = AST.Exp.QuantType(F, AST.Exp.Fun(spc.context, params, - AST.Stmt.Expr(AST.Util.bigImply(F, ISZ(spc.assumption, AST.Util.bigAnd(claims, spc.stepNo.posOpt)), + AST.Stmt.Expr(AST.Util.bigImply(T, ISZ(spc.assumption, AST.Util.bigAnd(claims, spc.stepNo.posOpt)), spc.stepNo.posOpt), tattr), tattr), AST.Attr(spc.stepNo.posOpt)) r = r + logika.th.normalizeExp(claim) ~> (spc.stepNo, F, claim) } @@ -465,8 +465,8 @@ object AutoPlugin { var s0 = state for (p <- provenClaims.entries) { if (!p._2._2) { - val (s1, exp) = l.rewriteAt(atMap, s0, p._1, reporter) - s0 = l.evalAssume(smt2, cache, T, "", s1, exp, p._1.posOpt, reporter)._1 + val (s1, exp) = l.rewriteAt(atMap, s0, p._2._3, reporter) + s0 = l.evalAssume(smt2, cache, T, "", s1, exp, p._2._3.posOpt, reporter)._1 } } val (s2, conclusion) = l.evalRegularStepClaimValue(smt2, cache, s0, step.claim, step.id.posOpt, reporter) @@ -478,8 +478,7 @@ object AutoPlugin { } return err } else { - val psmt2 = smt2.emptyCache(logika.config) - val (suc, m) = state.unconstrainedClaims + val (suc, _) = state.unconstrainedClaims var s1 = suc var ok = T val provenClaimMap = HashMap ++ (for (p <- provenClaims.entries) yield p._2._1 ~> p._2._3) @@ -498,9 +497,9 @@ object AutoPlugin { return err } val (s5, exp) = l.rewriteAt(atMap, s1, step.claim, reporter) - val (s6, conclusion) = l.evalRegularStepClaimValue(psmt2, cache, s5, exp, step.id.posOpt, reporter) + val (s6, conclusion) = l.evalRegularStepClaimValue(smt2, cache, s5, exp, step.id.posOpt, reporter) if (s6.ok) { - val r = checkValid(psmt2, s6, State.Claim.Prop(T, conclusion)) + val r = checkValid(smt2, s6, State.Claim.Prop(T, conclusion)) if (r.ok) { return state(claims = state.claims ++ ops.ISZOps(r.claims).slice(s1.claims.size, r.claims.size), nextFresh = r.nextFresh) } diff --git a/shared/src/main/scala/org/sireum/logika/plugin/PredNatDedPlugin.scala b/shared/src/main/scala/org/sireum/logika/plugin/PredNatDedPlugin.scala index 3eff1c3d..d4a35046 100644 --- a/shared/src/main/scala/org/sireum/logika/plugin/PredNatDedPlugin.scala +++ b/shared/src/main/scala/org/sireum/logika/plugin/PredNatDedPlugin.scala @@ -170,7 +170,7 @@ object PredNatDedPlugin { return err } val (params, assumption, subProof): (ISZ[AST.ProofAst.Step.Let.Param], AST.Exp, HashSet[AST.Exp]) = spcMap.get(subProofNo) match { - case Some(sp@StepProofContext.FreshAssumeSubProof(_, _, ps, ac, _, _)) => (ps, ac, HashSet ++ sp.claims) + case Some(sp@StepProofContext.FreshAssumeSubProof(_, _, ps, ac, _, _)) => (ps, logika.th.normalizeExp(ac), HashSet ++ sp.claims) case _ => reporter.error(subProofNo.posOpt, Logika.kind, s"Expecting a parameterized let sub-proof assume step") return err 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 6dd10b41..94d22f19 100644 --- a/shared/src/main/scala/org/sireum/logika/plugin/PropNatDedPlugin.scala +++ b/shared/src/main/scala/org/sireum/logika/plugin/PropNatDedPlugin.scala @@ -125,7 +125,7 @@ import org.sireum.logika.Logika.Reporter } val ISZ(subProofNo) = args val subProof: HashSet[AST.Exp] = spcMap.get(subProofNo) match { - case Some(sp: StepProofContext.SubProof) if sp.assumption == logika.th.normalizeExp(claim.left) => HashSet ++ sp.claims + sp.assumption + case Some(sp: StepProofContext.SubProof) if logika.th.normalizeExp(sp.assumption) == logika.th.normalizeExp(claim.left) => HashSet ++ sp.claims + sp.assumption case _ => reporter.error(subProofNo.posOpt, Logika.kind, s"Expecting a sub-proof step assuming the antecedent of step ${step.id}'s claim") return F @@ -215,7 +215,7 @@ import org.sireum.logika.Logika.Reporter } val ISZ(subProofNo) = args val subProof: ISZ[AST.Exp] = spcMap.get(subProofNo) match { - case Some(sp: StepProofContext.SubProof) if sp.assumption == logika.th.normalizeExp(claim.exp) => sp.claims + case Some(sp: StepProofContext.SubProof) if logika.th.normalizeExp(sp.assumption) == logika.th.normalizeExp(claim.exp) => sp.claims case _ => reporter.error(subProofNo.posOpt, Logika.kind, s"Expecting a sub-proof step assuming the operand of step ${step.id}'s claim") return err