LEC: name the problem the solver is given, and the time it takes

src/sat/SATSolverWrapper.h

@@ -340,9 +340,19 @@ class SATSolverWrapper {
     addClauseRange(lits);
   }
 
+  // The problem as handed to the solver, for the log line that starts it:
+  // clauses added and the largest variable any of them uses.
+  size_t numClauses() const { return numClauses_; }
+  size_t numVariables() const { return numVariables_; }
+
  private:
   template <typename ClauseRange>
   void addClauseRange(const ClauseRange& lits) {
+    ++numClauses_;
+    for (int lit : lits) {
+      // external +-(var+2): a literal of magnitude v is variable v-1 counted from 1
+      numVariables_ = std::max(numVariables_, static_cast<size_t>(std::abs(lit)) - 1);
+    }
     if (solverType_ == KEPLER_FORMAL::Config::SolverType::GLUCOSE) {
       Glucose::vec<Glucose::Lit> clause;
       for (int lit : lits) {
@@ -1115,6 +1125,8 @@ class SATSolverWrapper {
   // LCOV_EXCL_STOP
 
 private:
+  size_t numClauses_ = 0;
+  size_t numVariables_ = 0;
   static CaDiCraig::CraigVarType cadicalCraigVariableType( // LCOV_EXCL_LINE
       CraigVariablePartition partition) {
     switch (partition) { // LCOV_EXCL_LINE

src/strategies/miter/MiterStrategy.cpp

@@ -1,6 +1,7 @@
 // Copyright 2024-2026 keplertech.io
 // SPDX-License-Identifier: Apache-2.0
 
+#include <chrono>
 #include "MiterStrategy.h"
 #include "BoolExpr.h"
 #include "BuildPrimaryOutputClauses.h"
@@ -1053,9 +1054,12 @@ bool MiterStrategy::run(bool compact) {
   solver.addClause({rootVar});
 
   // solve with no assumptions
-  logger->info("Starting solver");
+  logger->info("Starting solver: {} variables, {} clauses, {} outputs compared",
+               solver.numVariables(), solver.numClauses(), POs0.size());
+  const auto solveStart = std::chrono::steady_clock::now();
   bool sat = solver.solve();
-  logger->info("SAT solver finished: {}", sat ? "SAT" : "UNSAT");
+  logger->info("SAT solver finished: {} in {:.1f} s", sat ? "SAT" : "UNSAT",
+               std::chrono::duration<double>(std::chrono::steady_clock::now() - solveStart).count());
 
   if (sat) {
     logger->info("Miter found a difference -> moving to analyze individual POs");
@@ -1362,9 +1366,12 @@ bool MiterStrategy::runCompactPOs(const tbb::concurrent_vector<BoolExpr*>& POs0,
   int rootVar = tseitinEncode(solver, miter, node2var, varName2idx);
   solver.addClause({rootVar});
 
-  logger->info("Starting solver");
+  logger->info("Starting solver: {} variables, {} clauses, {} outputs compared",
+               solver.numVariables(), solver.numClauses(), POs0.size());
+  const auto solveStart = std::chrono::steady_clock::now();
   const bool sat = solver.solve();
-  logger->info("SAT solver finished: {}", sat ? "SAT" : "UNSAT");
+  logger->info("SAT solver finished: {} in {:.1f} s", sat ? "SAT" : "UNSAT",
+               std::chrono::duration<double>(std::chrono::steady_clock::now() - solveStart).count());
   logger->info("Circuits are {}", sat ? "DIFFERENT" : "IDENTICAL");
   if (sat) {
     logger->warn("Due to compact mode, per PO analysis is skipped.");

test/strategies/miter/KeplerFormalCliTests.cpp

@@ -12,6 +12,7 @@
 #include <fstream>
 #include <iterator>
 #include <memory>
+#include <regex>
 #include <sstream>
 #include <string>
 #include <utility>
@@ -1029,6 +1030,46 @@ TEST_F(KeplerFormalCliTests, InProcessDriverRejectsAnActiveNajaUniverse) {
   EXPECT_EQ(help.result.status, KEPLER_FORMAL::RunStatus::NoResult);
 }
 
+TEST_F(KeplerFormalCliTests, LecLogNamesTheSolverProblemAndItsTime) {
+  // An equivalent pair the miter cannot hash away, so the solver runs. Its
+  // start line names the problem it was given and its finish line the time:
+  // a long solve can then be told from a hang and compared with a smaller.
+  NamedLoggerGuard loggerGuard("kepler_formal_main_logger");
+  const auto fixture = createDesignFixture(
+      "v",
+      "module top(input a, input b, output y);\n"
+      "  assign y = a & b;\n"
+      "endmodule\n",
+      "module top(input a, input b, output y);\n"
+      "  assign y = ~(~a | ~b);\n"
+      "endmodule\n");
+  const auto log = fixture.tmpDir / "problem_size.log";
+  const auto cfg = writeTempConfig(
+      "format: verilog\n"
+      "verification: lec\n"
+      "input_paths:\n"
+      "  - " + fixture.design0Path.string() + "\n"
+      "  - " + fixture.design1Path.string() + "\n"
+      "log_file: " + log.string() + "\n");
+  const auto run = runStructuredWithConfigFile(cfg);
+  EXPECT_EQ(run.exitCode, EXIT_SUCCESS);
+  EXPECT_EQ(run.result.status, KEPLER_FORMAL::RunStatus::Equivalent);
+  std::ifstream in(log);
+  std::stringstream text;
+  text << in.rdbuf();
+  EXPECT_TRUE(std::regex_search(
+      text.str(),
+      std::regex("Starting solver: [0-9]+ variables, [0-9]+ clauses, "
+                 "[0-9]+ outputs compared")))
+      << text.str();
+  EXPECT_TRUE(std::regex_search(
+      text.str(),
+      std::regex("SAT solver finished: (SAT|UNSAT) in [0-9]+\\.[0-9] s")))
+      << text.str();
+  std::filesystem::remove(cfg);
+  std::filesystem::remove_all(fixture.tmpDir);
+}
+
 TEST_F(KeplerFormalCliTests, InProcessDriverReturnsStructuredLecResults) {
   SolverGuard solverGuard;
   ReportSkippedPOsGuard reportGuard;

test/strategies/miter/MiterTests.cpp

@@ -9,6 +9,7 @@
 #include <filesystem>
 #include <fstream>
 #include <functional>
+#include <regex>
 #include <set>
 #include <sstream>
 #include <string>
@@ -3209,6 +3210,96 @@ static int run_kepler_cli_with_args(const std::vector<std::string>& args) {
 #endif
 }
 
+// A scratch directory per test, and a shell run of kepler-formal in it with
+// stdout and stderr kept: the subprocess form of a CLI test.
+static std::filesystem::path cliScratchDir(const std::string& name) {
+  const auto dir = std::filesystem::temp_directory_path() /
+                   ("kepler_cli_" + name + "_" +
+                    std::to_string(std::chrono::steady_clock::now()
+                                       .time_since_epoch()
+                                       .count()));
+  std::filesystem::create_directories(dir);
+  return dir;
+}
+
+static void writeText(const std::filesystem::path& path, const std::string& text) {
+  std::ofstream out(path);
+  out << text;
+}
+
+static std::string readText(const std::filesystem::path& path) {
+  std::ifstream in(path);
+  std::stringstream text;
+  text << in.rdbuf();
+  return text.str();
+}
+
+// AND2, NAND2 and INV, enough for an equivalent pair the miter cannot hash
+// away: AND2 against NAND2 into INV.
+static const char* kTinyLiberty =
+    "library(tiny) {\n"
+    "  cell(AND2) {\n"
+    "    pin(A) { direction : input; }\n"
+    "    pin(B) { direction : input; }\n"
+    "    pin(Y) { direction : output; function : \"(A&B)\"; }\n"
+    "  }\n"
+    "  cell(NAND2) {\n"
+    "    pin(A) { direction : input; }\n"
+    "    pin(B) { direction : input; }\n"
+    "    pin(Y) { direction : output; function : \"!(A&B)\"; }\n"
+    "  }\n"
+    "  cell(INV) {\n"
+    "    pin(A) { direction : input; }\n"
+    "    pin(Y) { direction : output; function : \"!A\"; }\n"
+    "  }\n"
+    "}\n";
+
+// Runs kepler-formal in `dir`; its output goes to `dir`/kepler.out.
+static int runKeplerIn(const std::filesystem::path& dir,
+                       const std::vector<std::string>& args) {
+  std::string cmd = "cd '" + dir.string() + "' && '" + std::string(KEPLER_BIN) + "'";
+  for (const auto& a : args) {
+    cmd += " '" + a + "'";
+  }
+  cmd += " > kepler.out 2>&1";
+  const int rc = std::system(cmd.c_str());
+  return (rc != -1 && WIFEXITED(rc)) ? WEXITSTATUS(rc) : EXIT_FAILURE;
+}
+
+TEST(KeplerCliSubprocessTests, LecLogNamesTheSolverProblemAndItsTime) {
+  // An equivalent pair the miter cannot hash away, so the solver runs: its
+  // start line names the problem it was given, its finish line the time.
+  const auto dir = cliScratchDir("lec_problem_size");
+  writeText(dir / "tiny.lib", kTinyLiberty);
+  writeText(dir / "and.v",
+            "module top(input a, input b, output y);\n"
+            "  AND2 u (.A(a), .B(b), .Y(y));\n"
+            "endmodule\n");
+  writeText(dir / "nand_inv.v",
+            "module top(input a, input b, output y);\n"
+            "  wire n;\n"
+            "  NAND2 u0 (.A(a), .B(b), .Y(n));\n"
+            "  INV u1 (.A(n), .Y(y));\n"
+            "endmodule\n");
+  writeText(dir / "cfg.yaml",
+            "format: verilog\n"
+            "verification: lec\n"
+            "input_paths:\n  - and.v\n  - nand_inv.v\n"
+            "liberty_files:\n  - tiny.lib\n"
+            "log_file: miter.log\n");
+  ASSERT_EQ(runKeplerIn(dir, {"--config", "cfg.yaml"}), 0)
+      << readText(dir / "kepler.out");
+  const auto log = readText(dir / "miter.log");
+  EXPECT_TRUE(std::regex_search(
+      log, std::regex("Starting solver: [0-9]+ variables, [0-9]+ clauses, "
+                      "[0-9]+ outputs compared")))
+      << log;
+  EXPECT_TRUE(std::regex_search(
+      log, std::regex("SAT solver finished: UNSAT in [0-9]+\\.[0-9] s")))
+      << log;
+  std::filesystem::remove_all(dir);
+}
+
 TEST(KeplerCliSubprocessTests, BinaryExists) {
   std::filesystem::path p(KEPLER_BIN);
   bool exists = std::filesystem::exists(p);