@@ -254,17 +254,6 @@ static Process& getSolver() {
254
254
// VlRandomizer:: Methods
255
255
256
256
void VlRandomVar::emit (std::ostream& s) const { s << m_name; }
257
- void VlRandomConst::emit (std::ostream& s) const {
258
- s << " #b" ;
259
- for (int i = 0 ; i < m_width; i++) s << (VL_BITISSET_Q (m_val, m_width - i - 1 ) ? ' 1' : ' 0' );
260
- }
261
- void VlRandomBinOp::emit (std::ostream& s) const {
262
- s << ' (' << m_op << ' ' ;
263
- m_lhs->emit (s);
264
- s << ' ' ;
265
- m_rhs->emit (s);
266
- s << ' )' ;
267
- }
268
257
void VlRandomExtract::emit (std::ostream& s) const {
269
258
s << " ((_ extract " << m_idx << ' ' << m_idx << " ) " ;
270
259
m_expr->emit (s);
@@ -307,27 +296,28 @@ bool VlRandomVar::set(std::string&& val) const {
307
296
return true ;
308
297
}
309
298
310
- std::shared_ptr<const VlRandomExpr> VlRandomizer::randomConstraint (VlRNG& rngr, int bits) {
311
- unsigned long long hash = VL_RANDOM_RNG_I (rngr) & ((1 << bits) - 1 );
312
- std::shared_ptr<const VlRandomExpr> concat = nullptr ;
313
- std::vector<std::shared_ptr<const VlRandomExpr>> varbits;
299
+ void VlRandomizer::randomConstraint (std::ostream& os, VlRNG& rngr, int bits) {
300
+ IData hash = VL_RANDOM_RNG_I (rngr) & ((1 << bits) - 1 );
301
+ std::vector<std::unique_ptr<const VlRandomExpr>> varbits;
314
302
for (const auto & var : m_vars) {
315
303
for (int i = 0 ; i < var.second ->width (); i++)
316
- varbits.emplace_back (std::make_shared <const VlRandomExtract>(var.second , i));
304
+ varbits.emplace_back (std::make_unique <const VlRandomExtract>(var.second , i));
317
305
}
306
+ os << " (= #b" ;
307
+ for (int i = bits - 1 ; i >= 0 ; i--) os << (VL_BITISSET_I (hash, i) ? ' 1' : ' 0' );
308
+ if (bits > 1 ) os << " (concat" ;
318
309
for (int i = 0 ; i < bits; i++) {
319
- std::shared_ptr< const VlRandomExpr> bit = nullptr ;
310
+ os << " (bvxor " ;
320
311
for (unsigned j = 0 ; j * 2 < varbits.size (); j++) {
321
312
unsigned idx = j + VL_RANDOM_RNG_I (rngr) % (varbits.size () - j);
322
- auto sel = varbits[idx];
323
313
std::swap (varbits[idx], varbits[j]);
324
- bit = bit == nullptr ? sel : std::make_shared<const VlRandomBinOp>(" bvxor" , bit, sel);
314
+ os << ' ' ;
315
+ varbits[j]->emit (os);
325
316
}
326
- concat = concat == nullptr ? bit
327
- : std::make_shared<const VlRandomBinOp>(" concat" , concat, bit);
317
+ os << ' )' ;
328
318
}
329
- return std::make_shared< const VlRandomBinOp>(
330
- " = " , concat, std::make_shared< const VlRandomConst>(hash, bits)) ;
319
+ if (bits > 1 ) os << ' ) ' ;
320
+ os << ' ) ' ;
331
321
}
332
322
333
323
bool VlRandomizer::next (VlRNG& rngr) {
@@ -356,7 +346,7 @@ bool VlRandomizer::next(VlRNG& rngr) {
356
346
357
347
for (int i = 0 ; i < _VL_SOLVER_HASH_LEN_TOTAL && sat; i++) {
358
348
f << " (assert " ;
359
- randomConstraint (rngr, _VL_SOLVER_HASH_LEN)-> emit (f );
349
+ randomConstraint (f, rngr, _VL_SOLVER_HASH_LEN);
360
350
f << " )\n " ;
361
351
f << " \n (check-sat)\n " ;
362
352
sat = parseSolution (f);
0 commit comments