More debugging

Author: uenoku

include/circt/Support/SatSolver.h

@@ -22,9 +22,11 @@
 #ifndef CIRCT_SUPPORT_SATSOLVER_H
 #define CIRCT_SUPPORT_SATSOLVER_H
 
+#include "llvm/ADT/ArrayRef.h"
 #include "llvm/ADT/STLFunctionalExtras.h"
 #include "llvm/ADT/SmallVector.h"
 #include "llvm/Support/Compiler.h"
+#include "llvm/Support/raw_ostream.h"
 #include <cassert>
 #include <cstdint>
 
@@ -207,6 +209,13 @@ class MiniSATSolver : public IncrementalSATSolverBase<MiniSATSolver> {
   /// Pre-allocate variables up to maxVar (1-indexed) without adding clauses.
   void reserveVars(int maxVar) { ensureVar(maxVar); }
 
+  /// Export current formula in DIMACS CNF format. Optionally includes
+  /// assumptions as unit clauses. Useful for debugging and creating reproducers.
+  /// Format: "p cnf <vars> <clauses>\n" followed by clauses (space-separated
+  /// literals terminated by 0).
+  void dumpDIMACS(llvm::raw_ostream &os,
+                  llvm::ArrayRef<int> assumptions = {}) const;
+
   /// Save current solver state. Must be at decision level 0 with no pending
   /// propagations. On rollback, variables/clauses added after bookmark are
   /// removed, watch lists are rebuilt from surviving clauses, and VSIDS

lib/Dialect/Synth/Transforms/FunctionalReduction.cpp

@@ -688,6 +688,10 @@ void FRAIGSolver<SATSolverT>::verifyCandidates() {
   LLVM_DEBUG(llvm::dbgs() << "FRAIG: Starting SAT verification with "
                           << equivClasses.size() << " equivalence classes\n");
 
+  // Check if user wants to dump all SAT queries
+  const char *dumpDir = std::getenv("FRAIG_DUMP_SAT");
+  bool dumpAll = (dumpDir != nullptr);
+
   // Global solver with bookmark/rollback (ABC-style):
   // - Pre-allocate variables for all values so they persist across rollbacks
   // - Learned clauses accumulate across equivalence classes (knowledge sharing)
@@ -729,6 +733,20 @@ void FRAIGSolver<SATSolverT>::verifyCandidates() {
 
       // Check 1: Can rep=1 and target=0?
       stats.numSATCalls++;
+
+      // Optionally dump SAT query for debugging
+      if (dumpAll) {
+        std::string filename = std::string(dumpDir) + "/sat_query_" +
+                               std::to_string(stats.numSATCalls) + "_check1.cnf";
+        std::error_code EC;
+        llvm::raw_fd_ostream out(filename, EC);
+        if (!EC) {
+          solver.dumpDIMACS(out, {repVar, -targetLit});
+          LLVM_DEBUG(llvm::dbgs()
+                     << "FRAIG: Dumped SAT query to " << filename << "\n");
+        }
+      }
+
       solver.assume(repVar);
       solver.assume(-targetLit);
       auto result1 = solver.solve(conflictLimit);
@@ -749,6 +767,20 @@ void FRAIGSolver<SATSolverT>::verifyCandidates() {
 
       // Check 2: Can rep=0 and target=1?
       stats.numSATCalls++;
+
+      // Optionally dump SAT query for debugging
+      if (dumpAll) {
+        std::string filename = std::string(dumpDir) + "/sat_query_" +
+                               std::to_string(stats.numSATCalls) + "_check2.cnf";
+        std::error_code EC;
+        llvm::raw_fd_ostream out(filename, EC);
+        if (!EC) {
+          solver.dumpDIMACS(out, {-repVar, targetLit});
+          LLVM_DEBUG(llvm::dbgs()
+                     << "FRAIG: Dumped SAT query to " << filename << "\n");
+        }
+      }
+
       solver.assume(-repVar);
       solver.assume(targetLit);
       auto result2 = solver.solve(conflictLimit);
@@ -940,6 +972,7 @@ class CadicalSATSolver : public IncrementalSATSolverBase<CadicalSATSolver> {
     LLVM_DEBUG(llvm::dbgs() << "Assuming: " << lit << "\n");
     solver->assume(lit);
     testSolver.assume(lit);
+    currentAssumptions.push_back(lit);
   }
 
   [[nodiscard]] Result solve(int64_t confLimit = -1) {
@@ -979,8 +1012,38 @@ class CadicalSATSolver : public IncrementalSATSolverBase<CadicalSATSolver> {
                            : (miniSatResult == MiniSATSolver::kUNSAT ? "UNSAT"
                                                                       : "UNKNOWN"))
                    << "\n";
+
+      // Dump DIMACS reproducer for debugging
+      static int mismatchCount = 0;
+      std::string filename =
+          "/tmp/cadical_mismatch_" + std::to_string(++mismatchCount) + ".cnf";
+      std::error_code EC;
+      llvm::raw_fd_ostream out(filename, EC);
+      if (!EC) {
+        dumpDIMACS(out, currentAssumptions);
+        llvm::errs() << "Dumped reproducer to " << filename << "\n";
+      } else {
+        llvm::errs() << "Failed to dump reproducer: " << EC.message() << "\n";
+      }
+
+      // Also dump MiniSAT's view
+      std::string miniFilename =
+          "/tmp/minisat_mismatch_" + std::to_string(mismatchCount) + ".cnf";
+      llvm::raw_fd_ostream miniOut(miniFilename, EC);
+      if (!EC) {
+        // Convert assumptions to proper format for dumpDIMACS
+        llvm::SmallVector<int> extAssumptions;
+        for (int lit : currentAssumptions) {
+          extAssumptions.push_back(lit);
+        }
+        testSolver.dumpDIMACS(miniOut, extAssumptions);
+        llvm::errs() << "Dumped MiniSAT view to " << miniFilename << "\n";
+      }
     }
 
+    // Clear assumptions for next solve
+    currentAssumptions.clear();
+
     return cadicalResult;
   }
 
@@ -1046,13 +1109,46 @@ class CadicalSATSolver : public IncrementalSATSolverBase<CadicalSATSolver> {
 
   [[nodiscard]] bool hasBookmark() const { return hasBookmark_; }
 
+  /// Export current formula in DIMACS CNF format for debugging.
+  void dumpDIMACS(llvm::raw_ostream &os,
+                  llvm::ArrayRef<int> assumptions = {}) const {
+    // Count total clauses
+    size_t totalClauses = clauses.size() + assumptions.size();
+
+    // DIMACS header (need to track maxVar)
+    int maxVar = 0;
+    for (const auto &clause : clauses) {
+      for (int lit : clause) {
+        maxVar = std::max(maxVar, std::abs(lit));
+      }
+    }
+    for (int lit : assumptions) {
+      maxVar = std::max(maxVar, std::abs(lit));
+    }
+
+    os << "p cnf " << maxVar << " " << totalClauses << "\n";
+
+    // All clauses
+    for (const auto &clause : clauses) {
+      for (int lit : clause)
+        os << lit << " ";
+      os << "0\n";
+    }
+
+    // Assumptions as unit clauses
+    for (int lit : assumptions) {
+      os << lit << " 0\n";
+    }
+  }
+
 private:
   CaDiCaL::Solver *solver;
   bool hasBookmark_ = false;
   llvm::SmallVector<llvm::SmallVector<int, 4>, 0> clauses; // All clauses added
   llvm::SmallVector<llvm::SmallVector<int, 4>, 0>
       bookmarkedClauses;                   // Clauses at bookmark
   llvm::SmallVector<int, 4> currentClause; // Current clause being built
+  llvm::SmallVector<int, 4> currentAssumptions; // Current assumptions
 
   MiniSATSolver testSolver;
 };

lib/Support/SatSolver.cpp

@@ -8,10 +8,13 @@
 
 #include "circt/Support/SatSolver.h"
 #include "llvm/ADT/STLExtras.h"
+#include "llvm/Support/Debug.h"
 #include "llvm/Support/raw_ostream.h"
 #include <algorithm>
 #include <cmath>
 
+#define DEBUG_TYPE "sat-solver"
+
 using namespace circt;
 
 //===----------------------------------------------------------------------===//
@@ -45,6 +48,46 @@ int MiniSATSolver::val(int v) const {
   return vars[v - 1].modelVal == kTrue ? v : -v;
 }
 
+void MiniSATSolver::dumpDIMACS(llvm::raw_ostream &os,
+                                llvm::ArrayRef<int> assumptions) const {
+  // Count total clauses: problem + learnt + binary + assumptions
+  size_t totalClauses = problemClauses.size() + learntClauses.size() +
+                        binaryClauses.size() + learntBinaryClauses.size() +
+                        assumptions.size();
+
+  // DIMACS header
+  os << "p cnf " << numVars << " " << totalClauses << "\n";
+
+  // Problem clauses (non-binary)
+  for (const auto &clause : problemClauses) {
+    for (int lit : clause.lits)
+      os << decodeLit(lit) << " ";
+    os << "0\n";
+  }
+
+  // Binary problem clauses
+  for (const auto &[lit0, lit1] : binaryClauses) {
+    os << decodeLit(lit0) << " " << decodeLit(lit1) << " 0\n";
+  }
+
+  // Learned clauses (optional - helps reproducibility)
+  for (const auto &clause : learntClauses) {
+    for (int lit : clause.lits)
+      os << decodeLit(lit) << " ";
+    os << "0\n";
+  }
+
+  // Binary learned clauses
+  for (const auto &[lit0, lit1] : learntBinaryClauses) {
+    os << decodeLit(lit0) << " " << decodeLit(lit1) << " 0\n";
+  }
+
+  // Assumptions as unit clauses
+  for (int lit : assumptions) {
+    os << lit << " 0\n";
+  }
+}
+
 //===----------------------------------------------------------------------===//
 // Variable management
 //===----------------------------------------------------------------------===//
@@ -135,7 +178,6 @@ void MiniSATSolver::backtrack(int level) {
                << " clearFrom=" << clearFrom << "\n";
 
   auto sf = [this](int x) { return vars[x].activity; };
-  bool found865 = false;
   for (int i = static_cast<int>(trail.size()) - 1; i >= clearFrom; i--) {
     int v = litVar(trail[i]);
     auto &var = vars[v];
@@ -643,7 +685,17 @@ MiniSATSolver::Result MiniSATSolver::search(int64_t confBudget) {
       int backLevel;
       analyze(confl, learntClause, backLevel);
       backtrack(std::max(backLevel, rootLevel));
-      recordLearnt(learntClause);
+      // Only record learned clauses if they don't involve assumption levels.
+      // Learned clauses containing literals from assumption levels (1..rootLevel)
+      // are contaminated and invalid for other assumption sets.
+      if (backLevel < rootLevel) {
+        // Don't learn - clause is tainted by assumptions
+        LLVM_DEBUG(llvm::dbgs() << "LEARN: Skipping tainted clause (backLevel="
+                                << backLevel << " < rootLevel=" << rootLevel
+                                << ")\n");
+      } else {
+        recordLearnt(learntClause);
+      }
       decayVarActivity();
       decayClauseActivity();
     } else {
@@ -719,13 +771,9 @@ MiniSATSolver::Result MiniSATSolver::solveImpl(int64_t confLimit) {
                    << " assign=" << static_cast<int>(vars[v].assign)
                    << " wantedLit=" << enc << "\n";
     }
-    llvm::errs() << "  After enqueue: trail.size=" << trail.size()
-                 << " var865.assign=" << static_cast<int>(vars[865].assign)
-                 << "\n";
+    llvm::errs() << "  After enqueue: trail.size=" << trail.size() << "\n";
     Conflict assumptionConfl = propagate();
-    llvm::errs() << "  After propagate: trail.size=" << trail.size()
-                 << " var865.assign=" << static_cast<int>(vars[865].assign)
-                 << "\n";
+    llvm::errs() << "  After propagate: trail.size=" << trail.size() << "\n";
     if (!enqueueOk || !assumptionConfl.isNone()) {
       llvm::errs() << "SOLVE: Assumption conflict! enqueueOk=" << enqueueOk
                    << " conflictNone=" << assumptionConfl.isNone() << "\n";