Warn when vcgen was too slow.
Keep this temporarily so we can more easily spot & fix old vcgens
MODIFY
CMakeLists.txt
CMakeLists.txt
@@ -87,6 +87,7 @@ set(UTIL_SRCS
util/errors.cpp
util/file.cpp
util/sort.cpp
+ util/stopwatch.cpp
util/symexec.cpp
)

MODIFY
tools/transform.cpp
tools/transform.cpp
#include "smt/solver.h"
#include "util/config.h"
#include "util/errors.h"
+#include "util/stopwatch.h"
#include "util/symexec.h"
#include <algorithm>
+#include <iostream>
#include <map>
#include <set>
#include <sstream>
@@ -894,6 +896,7 @@ Errors TransformVerify::verify() const {
}
}
+ StopWatch symexec_watch;
calculateAndInitConstants(t);
State::resetGlobals();
State src_state(t.src, true), tgt_state(t.tgt, false);
@@ -907,6 +910,11 @@ Errors TransformVerify::verify() const {
return move(e);
}
+ symexec_watch.stop();
+ if (symexec_watch.seconds() > 5) {
+ cerr << "WARNING: slow vcgen! Took " << symexec_watch << '\n';
+ }
+
Errors errs;
if (check_each_var) {

ADD
util/stopwatch.cpp
+#include "util/stopwatch.h"
+#include <cassert>
+#include <iomanip>
+
+using namespace std;
+using namespace std::chrono;
+
+static auto now() {
+ return steady_clock::now();
+}
+
+namespace util {
+
+StopWatch::StopWatch() {
+ start = now();
+}
+
+void StopWatch::stop() {
+ assert(!stopped);
+ end = now();
+ assert((stopped = true));
+}
+
+float StopWatch::seconds() const {
+ assert(stopped);
+ return duration_cast<duration<float>>(end - start).count();
+}
+
+ostream& operator<<(ostream &os, const StopWatch &w) {
+ os << fixed << setprecision(2);
+ auto seconds = w.seconds();
+ if (seconds < 1)
+ return os << (seconds / 1000.0) << " ms";
+ return os << seconds << " s";
+}
+
+}

ADD
util/stopwatch.h
+#pragma once
+
+// Copyright (c) 2018-present The Alive2 Authors.
+// Distributed under the MIT license that can be found in the LICENSE file.
+
+#include <chrono>
+#include <ostream>
+
+namespace util {
+
+class StopWatch {
+ std::chrono::steady_clock::time_point start, end;
+#ifndef NDEBUG
+ bool stopped = false;
+#endif
+
+public:
+ StopWatch();
+ void stop();
+ float seconds() const;
+
+ friend std::ostream& operator<<(std::ostream &os, const StopWatch &w);
+};
+
+}

Warn when vcgen was too slow.
Keep this temporarily so we can more easily spot & fix old vcgens