Support unique constraints (on 1D static arrays) (#6810) (#6878)

This commit is contained in:
Srinivasan Venkataramanan
2026-01-16 08:42:09 -05:00
committed by GitHub
parent 550cf4462d
commit 6fc9089a77
9 changed files with 234 additions and 21 deletions
+21 -1
View File
@@ -367,7 +367,26 @@ void VlRandomizer::randomConstraint(std::ostream& os, VlRNG& rngr, int bits) {
}
bool VlRandomizer::next(VlRNG& rngr) {
if (m_vars.empty()) return true;
if (m_vars.empty() && m_unique_arrays.empty()) return true;
for (const std::string& baseName : m_unique_arrays) {
const auto it = m_vars.find(baseName);
// Look up the actual size we stored earlier
// const uint32_t size = m_unique_array_sizes[baseName];
const uint32_t size = m_unique_array_sizes.at(baseName);
if (it != m_vars.end()) {
std::string distinctExpr = "(__Vbv (distinct";
for (uint32_t i = 0; i < size; ++i) {
char hexIdx[12];
sprintf(hexIdx, "#x%08x", i);
distinctExpr += " (select " + it->first + " " + hexIdx + ")";
}
distinctExpr += "))";
m_constraints.push_back(distinctExpr);
}
}
std::iostream& os = getSolver();
if (!os) return false;
@@ -384,6 +403,7 @@ bool VlRandomizer::next(VlRNG& rngr) {
var.second->emitType(os);
os << ")\n";
}
for (const std::string& constraint : m_constraints) {
os << "(assert (= #b1 " << constraint << "))\n";
}