Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Flush SMT logs and SMT profiling logs before (check-sat) #2962

Merged
merged 4 commits into from
Aug 23, 2024
Merged

Flush SMT logs and SMT profiling logs before (check-sat) #2962

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
db471f8
Flush SMT log before (check-sat)
thpani Aug 23, 2024
3c5f240
Flush SMT profiling info before (check-sat)
thpani Aug 23, 2024
ecec725
Update changelog
thpani Aug 23, 2024
a988030
Merge branch 'main' into th/flush-logs
konnov Aug 23, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions .unreleased/bug-fixes/2962-fix-trunc-smt-log
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
Fix truncation of SMT logs, see #2962
1 change: 1 addition & 0 deletions tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SymbStateRewriterImpl.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -565,6 +565,7 @@ class SymbStateRewriterImpl(
}

override def flushStatistics(): Unit = {
profilerListener.foreach { _.dumpToFile() }
statListener.locator.writeStats()
}

Expand Down
4 changes: 3 additions & 1 deletion tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/Z3SolverContext.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -486,6 +486,7 @@ class Z3SolverContext(val config: SolverConfig) extends SolverContext with LazyL

override def sat(): Boolean = {
log("(check-sat)")
flushLogs() // good time to flush
val status = z3solver.check()
log(s";; sat = ${status.name()}")
flushLogs() // good time to flush
Expand Down Expand Up @@ -513,11 +514,12 @@ class Z3SolverContext(val config: SolverConfig) extends SolverContext with LazyL
// temporarily, change the timeout
setTimeout(timeoutSec * 1000)
log("(check-sat)")
flushLogs() // good time to flush
val status = z3solver.check()
log(s";; sat = ${status.name()}")
flushLogs() // good time to flush
// return timeout to maximum
setTimeout(Int.MaxValue)
flushLogs() // good time to flush
status match {
case Status.SATISFIABLE => Some(true)
case Status.UNSATISFIABLE => Some(false)
Expand Down
1 change: 1 addition & 0 deletions tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/trex/TransitionExecutorImpl.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -318,6 +318,7 @@ class TransitionExecutorImpl[ExecCtxT](consts: Set[String], vars: Set[String], c
* timed out or reported *unknown*.
*/
override def sat(timeoutSec: Int): Option[Boolean] = {
ctx.rewriter.flushStatistics()
ctx.rewriter.solverContext.satOrTimeout(timeoutSec)
}

Expand Down
Loading