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 15, 2024
1 parent 6ed64f9 commit d571cd6
Show file tree
Hide file tree
Showing 3 changed files with 64 additions and 57 deletions.
51 changes: 40 additions & 11 deletions jvm/src/test/scala/org/sireum/logika/example/list.sc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -99,7 +99,8 @@ object List {
3 ( update(map, key, value) ≡ Cons(p, update(next, key, value)) ) by RSimpl(RS(update _)), //Auto,
4 ( lookup(Cons(p, update(next, key, value)), key) ≡
lookup(update(next, key, value), key) ) by RSimpl(RS(lookup _)),
5 ( lookup(update(map, key, value), key) ≡ value ) by Rewrite(RS(lookupUpdateEq _), 4)
5 ( lookup(Cons(p, update(next, key, value)), key) ≡ value ) by Rewrite(RS(lookupUpdateEq _), 4),
6 ( lookup(update(next, key, value), key) ≡ value ) by Rewrite(RS(lookup _), 5)
//@formatter:on
)
return
Expand Down Expand Up @@ -147,16 +148,31 @@ object List {

//lookupUpdateNe(next, key1, key2, value)

Deduce(
//@formatter:off
1 ( key1 ≢ key2 ) by Premise,
2 ( map ≡ Cons(p, next) ) by Auto,
3 ( !(p._1 ≡ key1) ) by Premise,
4 ( update(map, key1, value) ≡ Cons(p, update(next, key1, value)) ) by RSimpl(RS(update _)),
5 ( lookup(update(next, key1, value), key2) ≡ lookup(next, key2) ) by RSimpl(RS(lookupUpdateNe _)),
6 ( lookup(update(map, key1, value), key2) ≡ lookup(map, key2) ) by RSimpl(RS(lookup _))
//@formatter:on
)
if (p._1 ≡ key2) {
Deduce(
//@formatter:off
1 ( key1 ≢ key2 ) by Premise,
2 ( map ≡ Cons(p, next) ) by Auto,
3 ( !(p._1 ≡ key1) ) by Premise,
7 ( p._1 ≡ key2 ) by Premise,
4 ( update(map, key1, value) ≡ Cons(p, update(next, key1, value)) ) by RSimpl(RS(update _)),
5 ( lookup(update(next, key1, value), key2) ≡ lookup(next, key2) ) by RSimpl(RS(lookupUpdateNe _)),
6 ( lookup(update(map, key1, value), key2) ≡ lookup(map, key2) ) by RSimpl(RS(lookup _))
//@formatter:on
)
} else {
Deduce(
//@formatter:off
1 ( key1 ≢ key2 ) by Premise,
2 ( map ≡ Cons(p, next) ) by Auto,
3 ( !(p._1 ≡ key1) ) by Premise,
7 ( !(p._1 ≡ key2) ) by Premise,
4 ( update(map, key1, value) ≡ Cons(p, update(next, key1, value)) ) by RSimpl(RS(update _)),
5 ( lookup(update(next, key1, value), key2) ≡ lookup(next, key2) ) by RSimpl(RS(lookupUpdateNe _)),
6 ( lookup(update(map, key1, value), key2) ≡ lookup(map, key2) ) by RSimpl(RS(lookup _))
//@formatter:on
)
}
return

}
Expand Down Expand Up @@ -272,6 +288,19 @@ object List {
//@formatter:on
)
}

@pure def singleQueueHead[T](q: Queue[T], a: T): Unit = {
Contract(
Requires(q.buffer ≡ Cons[T](a, Nil())),
Ensures(q.head ≡ a)
)
Deduce(
//@formatter:off
1 ( q.buffer ≡ List.Cons[T](a, List.Nil[T]()) ) by Premise,
2 ( q.head ≡ a ) by Simpl // Auto
//@formatter:on
)
}
}


Expand Down
45 changes: 10 additions & 35 deletions shared/src/main/scala/org/sireum/logika/RewritingSystem.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -235,11 +235,12 @@ object RewritingSystem {
val fromStepOpt: Option[(AST.CoreExp.Base, AST.ProofAst.StepId)],
val shouldTrace: B,
val shouldTraceEval: B,
val maxUnfolding: Z,
var labeledOnly: B,
var inLabel: B,
var done: B,
var trace: ISZ[Trace]) {
val unfoldingMap: MBox[UnfoldingNumMap] = MBox(HashSMap.empty)
@strictpure def 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)
Expand Down Expand Up @@ -455,7 +456,7 @@ object RewritingSystem {
}
case _ =>
if (r0.isEmpty && labeledOnly) {
evalBase(th, EvalConfig.all, cache, methodPatterns, unfoldingMap, 1,
evalBase(th, EvalConfig.all, cache, methodPatterns, unfoldingMap, 0,
provenClaimStepIdMapEval, o, F, shouldTraceEval) match {
case Some((r1, t)) =>
trace = trace ++ t
Expand Down Expand Up @@ -492,7 +493,7 @@ object RewritingSystem {
}
case _ => F
}
if (shouldUnfold) {
if (shouldUnfold && (!labeledOnly || inLabel)) {
evalBase(th, EvalConfig.none, cache, methodPatterns, unfoldingMap, 1, HashSMap.empty, o2, F, shouldTraceEval) match {
case Some((o3, t)) =>
trace = trace ++ t
Expand Down Expand Up @@ -545,13 +546,13 @@ object RewritingSystem {
if (patterns2.isEmpty) {
o
} else {
Rewriter(maxCores, th, HashSMap.empty, patterns2, methodPatterns, fromStepOpt, F, F, F, F, F, ISZ()).
transformCoreExpBase(cache, o).getOrElse(o)
Rewriter(maxCores, th, HashSMap.empty, patterns2, methodPatterns, fromStepOpt, F, F, maxUnfolding,
F, F, F, ISZ()).transformCoreExpBase(cache, o).getOrElse(o)
}
}
}
val (o3Opt, t): (Option[AST.CoreExp.Base], ISZ[Trace]) =
evalBase(th, EvalConfig.all, cache, methodPatterns, unfoldingMap, 1,
evalBase(th, EvalConfig.all, cache, methodPatterns, unfoldingMap, 0,
provenClaimStepIdMapEval, o2, F, shouldTraceEval) match {
case Some((o3o, t)) => (Some(o3o), t)
case _ => (None(), ISZ())
Expand Down Expand Up @@ -598,8 +599,8 @@ 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, fromStepOpt, F, F, F, F, F, ISZ()).
transformCoreExpBase(cache, o).getOrElse(o)
val o2 = Rewriter(maxCores, th, HashSMap.empty, patterns2, methodPatterns, fromStepOpt, F, F,
maxUnfolding, 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) {
unifyPendingApplications(T, th, pattern.localPatternSet, m, pas, sm, ems) match {
Expand Down Expand Up @@ -1768,11 +1769,7 @@ object RewritingSystem {
if (right < left) AST.CoreExp.Binary(right, AST.Exp.BinaryOp.InequivUni, left, AST.Typed.b)
else AST.CoreExp.Binary(left, AST.Exp.BinaryOp.InequivUni, right, AST.Typed.b)

var unfoldDisabled = F
def shouldUnfold(info: Info.Method): B = {
if (unfoldDisabled) {
return F
}
val r = !info.ast.hasContract && info.ast.isStrictPure &&
((info.ast.purity == AST.Purity.Abs) ->: methodPatterns.contains((info.name, info.isInObject)))
if (!r) {
Expand Down Expand Up @@ -1888,8 +1885,6 @@ object RewritingSystem {
}
case _ =>
}
val oldUnfoldDisabled = unfoldDisabled
unfoldDisabled = T
var done = rOpt.isEmpty
while (!done) {
rOpt match {
Expand All @@ -1903,7 +1898,6 @@ object RewritingSystem {
case _ => done = T
}
}
unfoldDisabled = oldUnfoldDisabled
return rOpt
}

Expand Down Expand Up @@ -2517,26 +2511,7 @@ object RewritingSystem {
}
return Some(r)
}
var tExp = e.tExp
var fExp = e.fExp
if (config.iteBranches) {
val oldUnfoldDisabled = unfoldDisabled
unfoldDisabled = T
evalBaseH(e.tExp) match {
case Some(t) =>
changed = T
tExp = t
case _ =>
}
evalBaseH(e.fExp) match {
case Some(f) =>
changed = T
fExp = f
case _ =>
}
unfoldDisabled = oldUnfoldDisabled
}
return if (changed) Some(e(cond = cond, tExp = tExp, fExp = fExp)) else None()
return if (changed) Some(e(cond = cond)) else None()
}

def evalApply(e: AST.CoreExp.Apply): Option[AST.CoreExp.Base] = {
Expand Down
25 changes: 14 additions & 11 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 @@ -135,7 +135,7 @@ import org.sireum.logika.{Logika, RewritingSystem, Smt2, State, StepProofContext
val rwPc = Rewriter(if (logika.config.rwPar) logika.config.parCores else 1, logika.th,
provenClaims, patterns, methodPatterns,
if (fromOpt.isEmpty) None() else Some((fromCoreClaim, fromOpt.get)),
logika.config.rwTrace, logika.config.rwEvalTrace, F, F, F, ISZ())
logika.config.rwTrace, logika.config.rwEvalTrace, logika.config.rwMax, F, F, F, ISZ())
if (logika.config.rwEvalTrace) {
rwPc.trace = rwPc.trace :+ RewritingSystem.Trace.Begin("simplifying", stepClaim)
}
Expand Down Expand Up @@ -204,7 +204,10 @@ import org.sireum.logika.{Logika, RewritingSystem, Smt2, State, StepProofContext
ld.transformCoreExpBase(rwClaim)
rwPc.labeledOnly = ld.found
var changed = F
while (!done && i < logika.config.rwMax && (if (isRSimpl) rwClaim != AST.CoreExp.True else rwClaim != stepClaim)) {
def continu: B = {
return if (isRSimpl) rwClaim != AST.CoreExp.True else rwClaim != stepClaim
}
while (!done && i < logika.config.rwMax && continu) {
rwPc.done = F
if (logika.config.rwTrace) {
rwPc.trace = rwPc.trace :+ RewritingSystem.Trace.Begin("rewriting", rwClaim)
Expand All @@ -218,18 +221,18 @@ import org.sireum.logika.{Logika, RewritingSystem, Smt2, State, StepProofContext
done = T
rwClaim
}
if (continu && !rwPc.labeledOnly) {
rwClaim = RewritingSystem.evalBase(logika.th, RewritingSystem.EvalConfig.all, cache, rwPc.methodPatterns,
MBox(HashSMap.empty), 0, rwPc.provenClaimStepIdMapEval, rwClaim, T, T) match {
case Some((r, t)) =>
rwPc.trace = rwPc.trace ++ t
r
case _ => rwClaim
}
}
i = i + 1
}
rwClaim = RewritingSystem.LabeledRemover().transformCoreExpBase(rwClaim).getOrElse(rwClaim)
if (!rwPc.labeledOnly) {
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 d571cd6

Please sign in to comment.