Fixed Auto justification issues.

sireum · Dec 2, 2024 · b6ebab9 · b6ebab9
1 parent dcd8bc7
commit b6ebab9
Show file tree

Hide file tree

Showing 4 changed files with 17 additions and 13 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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