From 3ac8daafd11c4710b35394cba8d184b0273c0a90 Mon Sep 17 00:00:00 2001
From: nella <simontupy64@gmail.com>
Date: Mon, 27 Jul 2026 10:00:16 +0200
Subject: [PATCH]  Add reusable SatEffortBudget helper to qcsat.

---
 kernel/qcsat.cc | 21 +++++++++++++++++++++
 kernel/qcsat.h  | 33 +++++++++++++++++++++++++++++++++
 2 files changed, 54 insertions(+)

diff --git a/kernel/qcsat.cc b/kernel/qcsat.cc
index c9d00efa1..f996a963a 100644
--- a/kernel/qcsat.cc
+++ b/kernel/qcsat.cc
@@ -100,3 +100,24 @@ int QuickConeSat::cell_complexity(RTLIL::Cell *cell)
 	// Unknown cell.
 	return 5;
 }
+
+void SatEffortBudget::charge_import(QuickConeSat &qcsat, int64_t &cells_charged)
+{
+	if (enabled())
+		remaining -= (GetSize(qcsat.imported_cells) - cells_charged) * import_cell_cost;
+	cells_charged = GetSize(qcsat.imported_cells);
+}
+
+SatEffortBudget::Result SatEffortBudget::solve(QuickConeSat &qcsat, int64_t cap, const std::vector<int> &modelExprs,
+		std::vector<bool> &modelVals, const std::vector<int> &assumptions)
+{
+	if (enabled())
+		cap = (cap > 0) ? std::min(cap, remaining) : remaining;
+	qcsat.ez->setSolverPropLimit(cap);
+	bool sat = qcsat.ez->solve(modelExprs, modelVals, assumptions);
+	if (enabled())
+		remaining -= qcsat.ez->getSolverProps();
+	if (!sat && qcsat.ez->getSolverPropLimitStatus())
+		return Result::LimitReached;
+	return sat ? Result::Sat : Result::Unsat;
+}
diff --git a/kernel/qcsat.h b/kernel/qcsat.h
index e4d3c3c5d..d0b717c8f 100644
--- a/kernel/qcsat.h
+++ b/kernel/qcsat.h
@@ -71,6 +71,39 @@ struct QuickConeSat {
 	static int cell_complexity(RTLIL::Cell *cell);
 };
 
+// A deterministic effort budget for SAT-based optimizations, measured in solver
+// propagation steps (see ezSAT::getSolverProps). The budget is held once per unit
+// of work (typically a module) and reused across many QuickConeSat instances: a
+// pass that rebuilds the solver in batches keeps a single SatEffortBudget and
+// spends from it in every batch, rather than resetting the budget per solver.
+// Spending the budget only skips optimizations, and it never affects correctness,
+// because a skipped proof just leaves a candidate un-optimized.
+struct SatEffortBudget {
+	enum class Result { Sat, Unsat, LimitReached };
+
+	// Effort charged per imported cell
+	static constexpr int64_t import_cell_cost = 100;
+
+	// starting budget (0 = unlimited)
+	int64_t total = 0;
+	int64_t remaining = 0;
+
+	SatEffortBudget() {}
+	explicit SatEffortBudget(int64_t total) : total(total), remaining(total) {}
+
+	bool enabled() const { return total > 0; }
+
+	// True once the budget is used up
+	bool spent() const { return enabled() && remaining <= 0; }
+
+	// Charge for the cells imported into qcsat since the previous call (pricing the cells pulled in)
+	// cells_charged records how many of qcsat's imported cells are already paid for
+	void charge_import(QuickConeSat &qcsat, int64_t &cells_charged);
+
+	Result solve(QuickConeSat &qcsat, int64_t cap, const std::vector<int> &modelExprs,
+			std::vector<bool> &modelVals, const std::vector<int> &assumptions);
+};
+
 YOSYS_NAMESPACE_END
 
 #endif