Skip to content

Commit

Permalink
Rewriting system.
Browse files Browse the repository at this point in the history
  • Loading branch information
@robby-phd
robby-phd committed Mar 8, 2024
1 parent 676f98f commit 228e497
Show file tree
Hide file tree
Showing 2 changed files with 53 additions and 33 deletions.
35 changes: 21 additions & 14 deletions shared/src/main/scala/org/sireum/logika/RewritingSystem.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -198,13 +198,20 @@ object RewritingSystem {
val provenClaims: HashSMap[AST.ProofAst.StepId, AST.CoreExp.Base],
val patterns: ISZ[Rewriter.Pattern.Claim],
val methodPatterns: MethodPatternMap,
val fromStepOpt: Option[(AST.CoreExp.Base, AST.ProofAst.StepId)],
val shouldTrace: B,
val shouldTraceEval: B,
var labeledOnly: B,
var inLabel: B,
var done: B,
var trace: ISZ[Trace]) {
val unfoldingMap: MBox[UnfoldingNumMap] = MBox(HashSMap.empty)
@memoize def provenClaimStepIdMapEval: HashSMap[AST.CoreExp.Base, AST.ProofAst.StepId] = {
fromStepOpt match {
case Some((e, fromStepId)) => return provenClaimStepIdMap - (e, fromStepId)
case _ => return provenClaimStepIdMap
}
}
@memoize def provenClaimStepIdMap: HashSMap[AST.CoreExp.Base, AST.ProofAst.StepId] = {
@strictpure def conjuncts(e: AST.CoreExp.Base): ISZ[AST.CoreExp.Base] = {
e match {
Expand Down Expand Up @@ -411,6 +418,16 @@ object RewritingSystem {
case _ => return Some(o(exp = r))
}
case _ =>
if (r0.isEmpty && labeledOnly) {
evalBase(th, EvalConfig.all, cache, methodPatterns, unfoldingMap, 1,
provenClaimStepIdMapEval, o, F, shouldTraceEval) match {
case Some((r1, t)) =>
trace = trace ++ t
done = T
return Some(r1)
case _ =>
}
}
}
if (hasChanged || r0.nonEmpty)
Some(o(exp = r0.getOrElse(o.exp)))
Expand Down Expand Up @@ -492,14 +509,14 @@ object RewritingSystem {
if (patterns2.isEmpty) {
o
} else {
Rewriter(maxCores, th, HashSMap.empty, patterns2, methodPatterns, F, F, F, F, F, ISZ()).
Rewriter(maxCores, th, HashSMap.empty, patterns2, methodPatterns, fromStepOpt, F, F, F, F, F, ISZ()).
transformCoreExpBase(cache, o).getOrElse(o)
}
}
}
val (o3Opt, t): (Option[AST.CoreExp.Base], ISZ[Trace]) =
evalBase(th, EvalConfig.allButEquivSubst, cache, methodPatterns, unfoldingMap, 1,
provenClaimStepIdMap, o2, F, shouldTraceEval) match {
evalBase(th, EvalConfig.all, cache, methodPatterns, unfoldingMap, 1,
provenClaimStepIdMapEval, o2, F, shouldTraceEval) match {
case Some((o3o, t)) => (Some(o3o), t)
case _ => (None(), ISZ())
}
Expand Down Expand Up @@ -545,7 +562,7 @@ object RewritingSystem {
(for (k <- 0 until apcs.size; apc <- toCondEquiv(th, apcs(k)._2)) yield
r2l(Rewriter.Pattern.Claim(pattern.name :+ s"Assumption$k", F, isPermutative(apc), HashSSet.empty, apc))) ++
patterns
val o2 = Rewriter(maxCores, th, HashSMap.empty, patterns2, methodPatterns, F, F, F, F, F, ISZ()).
val o2 = Rewriter(maxCores, th, HashSMap.empty, patterns2, methodPatterns, fromStepOpt, F, F, F, F, F, ISZ()).
transformCoreExpBase(cache, o).getOrElse(o)
val m = unifyExp(T, th, pattern.localPatternSet, from, o2, map, pas, sm, ems)
if (ems.value.isEmpty) {
Expand Down Expand Up @@ -586,16 +603,6 @@ object RewritingSystem {
tryPattern()
i = i + 1
}
if (rOpt.isEmpty) {
evalBase(th, EvalConfig.allButEquivSubst, cache, methodPatterns, unfoldingMap, 1,
provenClaimStepIdMap, o, F, shouldTraceEval) match {
case Some((r2, t)) =>
trace = trace ++ t
rOpt = Some(r2)
done = T
case _ =>
}
}
return rOpt
}
}
Expand Down
51 changes: 32 additions & 19 deletions shared/src/main/scala/org/sireum/logika/plugin/RewritePlugin.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -84,26 +84,27 @@ import org.sireum.logika.{Logika, RewritingSystem, Smt2, State, StepProofContext
}
(r1, r2)
}
val (fromOpt, fromClaim): (Option[AST.ProofAst.StepId], AST.Exp) = if (isRSimpl || isSimpl) {
(None(), AST.Exp.LitB(T, step.just.id.attr))
} else {
val from: AST.ProofAst.StepId =
AST.Util.toStepIds(ISZ(justArgs(if (isEval) 0 else 1)), Logika.kind, reporter) match {
case Some(s) => s(0)
case _ => return err
val (fromOpt, fromClaim, fromCoreClaim): (Option[AST.ProofAst.StepId], AST.Exp, AST.CoreExp.Base) =
if (isRSimpl || isSimpl) {
(None(), AST.Exp.LitB(T, step.just.id.attr), AST.CoreExp.LitB(T))
} else {
val from: AST.ProofAst.StepId =
AST.Util.toStepIds(ISZ(justArgs(if (isEval) 0 else 1)), Logika.kind, reporter) match {
case Some(s) => s(0)
case _ => return err
}
spcMap.get(from) match {
case Some(spc: StepProofContext.Regular) => (Some(from), spc.exp, spc.coreExpClaim)
case _ =>
reporter.error(from.posOpt, Logika.kind, s"Expecting a regular proof step")
return err
}
spcMap.get(from) match {
case Some(spc: StepProofContext.Regular) => (Some(from), spc.exp)
case _ =>
reporter.error(from.posOpt, Logika.kind, s"Expecting a regular proof step")
return err
}
}
var provenClaims = HashSMap.empty[AST.ProofAst.StepId, AST.CoreExp.Base]
if (step.just.hasWitness) {
for (w <- step.just.witnesses) {
spcMap.get(w) match {
case Some(spc: StepProofContext.Regular) if isEval ___>: (w != fromOpt.get) =>
case Some(spc: StepProofContext.Regular) =>
provenClaims = provenClaims + w ~> spc.coreExpClaim
case Some(_) =>
reporter.error(w.posOpt, Logika.kind, s"Expecting a regular proof step for $w")
Expand All @@ -114,7 +115,7 @@ import org.sireum.logika.{Logika, RewritingSystem, Smt2, State, StepProofContext
} else {
for (spc <- spcMap.values) {
spc match {
case spc: StepProofContext.Regular if !spc.stepNo.isPremise && (isEval ___>: (spc.stepNo != fromOpt.get)) =>
case spc: StepProofContext.Regular if !spc.stepNo.isPremise =>
provenClaims = provenClaims + spc.stepNo ~> spc.coreExpClaim
case _ =>
}
Expand All @@ -128,15 +129,17 @@ import org.sireum.logika.{Logika, RewritingSystem, Smt2, State, StepProofContext
else None()

val rwPc = Rewriter(if (logika.config.rwPar) logika.config.parCores else 1, logika.th,
provenClaims, patterns, methodPatterns, logika.config.rwTrace, logika.config.rwEvalTrace, F, F, F, ISZ())
provenClaims, patterns, methodPatterns,
if (fromOpt.isEmpty) None() else Some((fromCoreClaim, fromOpt.get)),
logika.config.rwTrace, logika.config.rwEvalTrace, F, F, F, ISZ())
val stepClaim = RewritingSystem.translateExp(logika.th, F, step.claim)

if (logika.config.rwEvalTrace) {
rwPc.trace = rwPc.trace :+ RewritingSystem.Trace.Begin("simplifying", stepClaim)
}

val stepClaimEv: AST.CoreExp.Base = RewritingSystem.evalBase(logika.th, RewritingSystem.EvalConfig.all, cache,
rwPc.methodPatterns, MBox(HashSMap.empty), logika.config.rwMax, rwPc.provenClaimStepIdMap, stepClaim, T,
rwPc.methodPatterns, MBox(HashSMap.empty), logika.config.rwMax, rwPc.provenClaimStepIdMapEval, stepClaim, T,
logika.config.rwEvalTrace) match {
case Some((e, t)) =>
rwPc.trace = t
Expand Down Expand Up @@ -172,7 +175,6 @@ import org.sireum.logika.{Logika, RewritingSystem, Smt2, State, StepProofContext
} else {
val simplTrace = rwPc.trace
rwPc.trace = ISZ()
val fromCoreClaim = RewritingSystem.translateExp(logika.th, F, fromClaim)
@strictpure def simplTraceOpt: Option[ST] = if (stepClaim == stepClaimEv) None() else Some(
st"""and/or after simplifying the step claim to:
| ${stepClaimEv.prettyST}"""
Expand All @@ -184,7 +186,7 @@ import org.sireum.logika.{Logika, RewritingSystem, Smt2, State, StepProofContext
rwPc.trace = rwPc.trace :+ RewritingSystem.Trace.Begin("evaluating", fromCoreClaim)
}
rwClaim = RewritingSystem.evalBase(logika.th, RewritingSystem.EvalConfig.all, cache, rwPc.methodPatterns,
MBox(HashSMap.empty), logika.config.rwMax, rwPc.provenClaimStepIdMap, rwClaim, T, logika.config.rwEvalTrace) match {
MBox(HashSMap.empty), logika.config.rwMax, rwPc.provenClaimStepIdMapEval, rwClaim, T, logika.config.rwEvalTrace) match {
case Some((c, t)) =>
rwPc.trace = rwPc.trace ++ t
c
Expand All @@ -199,6 +201,7 @@ import org.sireum.logika.{Logika, RewritingSystem, Smt2, State, StepProofContext
val ld = RewritingSystem.LabeledDetector(F)
ld.transformCoreExpBase(rwClaim)
rwPc.labeledOnly = ld.found
var changed = F
while (!done && i < logika.config.rwMax && rwClaim != stepClaim) {
rwPc.done = F
if (logika.config.rwTrace) {
Expand All @@ -207,6 +210,7 @@ import org.sireum.logika.{Logika, RewritingSystem, Smt2, State, StepProofContext
rwClaim = rwPc.transformCoreExpBase(cache, rwClaim) match {
case Some(c) =>
rwPc.trace = rwPc.trace :+ RewritingSystem.Trace.Done(rwClaim, c)
changed = T
c
case _ =>
done = T
Expand All @@ -215,6 +219,15 @@ import org.sireum.logika.{Logika, RewritingSystem, Smt2, State, StepProofContext
i = i + 1
}
rwClaim = RewritingSystem.LabeledRemover().transformCoreExpBase(rwClaim).getOrElse(rwClaim)
if (!rwPc.labeledOnly && !changed) {
rwClaim = RewritingSystem.evalBase(logika.th, RewritingSystem.EvalConfig.all, cache, rwPc.methodPatterns,
rwPc.unfoldingMap, 1, rwPc.provenClaimStepIdMapEval, rwClaim, T, T) match {
case Some((r, t)) =>
rwPc.trace = rwPc.trace ++ t
r
case _ => rwClaim
}
}
}
@strictpure def fromCoreClaimST: Option[ST] = if (fromOpt.isEmpty) None() else Some(
st"""After ${if (isEval) "evaluating" else "rewriting"}${if (fromOpt.isEmpty) st"" else st" ${fromOpt.get}"}:
Expand Down

0 comments on commit 228e497

Please sign in to comment.