Skip to content

Commit

Permalink
Rewriting system.
Browse files Browse the repository at this point in the history
  • Loading branch information
robby-phd committed Feb 15, 2024
1 parent 548a779 commit b869c98
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions shared/src/main/scala/org/sireum/logika/RewritingSystem.scala
Original file line number Diff line number Diff line change
Expand Up @@ -1543,13 +1543,13 @@ object RewritingSystem {
if (args.size > params.size) {
val r = e(exp = body2, args = ops.ISZOps(args).slice(params.size, args.size))
if (shouldTrace) {
trace = trace :+ Trace.Eval(st"∀-instantiation ${q.prettyST}(${(for (arg <- ops.ISZOps(args).slice(0, params.size)) yield arg.prettyST, ", ")}) ≡ ${r.prettyST}", e, r)
trace = trace :+ Trace.Eval(st"∀-elimination ${q.prettyST}(${(for (arg <- ops.ISZOps(args).slice(0, params.size)) yield arg.prettyST, ", ")}) ≡ ${r.prettyST}", e, r)
}
return Some(r)
} else {
val r = body2
if (shouldTrace) {
trace = trace :+ Trace.Eval(st"∀-instantiation ${q.prettyST}(${(for (arg <- args) yield arg.prettyST, ", ")}) ≡ ${r.prettyST}", e, r)
trace = trace :+ Trace.Eval(st"∀-elimination ${q.prettyST}(${(for (arg <- args) yield arg.prettyST, ", ")}) ≡ ${r.prettyST}", e, r)
}
return Some(r)
}
Expand Down

0 comments on commit b869c98

Please sign in to comment.