1919#
2020# @author: ballance
2121
22-
2322import copy
2423from dataclasses import dataclass
24+ import random
2525import sys
2626import time
2727from typing import List , Dict
3131from vsc .constraints import constraint , soft
3232from vsc .model .bin_expr_type import BinExprType
3333from vsc .model .constraint_model import ConstraintModel
34- from vsc .model .constraint_override_model import ConstraintOverrideModel
35- from vsc .model .constraint_foreach_model import ConstraintForeachModel
3634from vsc .model .constraint_soft_model import ConstraintSoftModel
3735from vsc .model .expr_bin_model import ExprBinModel
3836from vsc .model .expr_fieldref_model import ExprFieldRefModel
@@ -72,6 +70,7 @@ class Randomizer(RandIF):
7270 EN_DEBUG = False
7371
7472 randomize_cache = {}
73+ randomize_call_count = {}
7574
7675 def __init__ (self , randstate , debug = 0 , lint = 0 , solve_fail_debug = 0 , solve_info = None ):
7776 self .randstate = randstate
@@ -141,18 +140,18 @@ def randomize(self, ri : RandInfo, bound_m : Dict[FieldModel,VariableBoundModel]
141140 idx = self .randstate .randint (0 , len (range_l )- 1 )
142141 uf .set_val (range_l [idx ][0 ])
143142
144- # TODO We want to re-randomize unconstrained variables when caching. Do we need to lock?
145143 # Lock so we don't overwrite
146- # uf.set_used_rand(False)
144+ if not cache_enabled :
145+ uf .set_used_rand (False )
147146
148147 rs_i = 0
149148 start_rs_i = 0
149+ # TODO What is going on with max_fields? It would probably
150+ # break this caching setup.
150151# max_fields = 20
151152 max_fields = 0
152153 while rs_i < len (ri .randsets ()):
153154 # If missing from cache, initialize/build btor and randset
154- # TODO What is going on with max_fields? It would break this
155- # caching setup.
156155 if not cache_enabled or rs_i not in self .btor_cache :
157156 btor = Boolector ()
158157 # TODO Is self.btor used anywhere?
@@ -203,7 +202,7 @@ def randomize(self, ri : RandInfo, bound_m : Dict[FieldModel,VariableBoundModel]
203202 # rs_i += 1
204203 if n_fields > max_fields or rs .order != - 1 :
205204 break
206-
205+
207206 for c in constraint_l :
208207 try :
209208 btor .Assume (c [1 ])
@@ -238,7 +237,7 @@ def randomize(self, ri : RandInfo, bound_m : Dict[FieldModel,VariableBoundModel]
238237 btor .Assert (c [1 ])
239238
240239 # If there are soft constraints, add these now
241- if len (soft_constraint_l ) > 0 :
240+ if len (soft_constraint_l ) > 0 :
242241 for c in soft_constraint_l :
243242 try :
244243 btor .Assume (c [1 ])
@@ -248,7 +247,7 @@ def randomize(self, ri : RandInfo, bound_m : Dict[FieldModel,VariableBoundModel]
248247 raise e
249248
250249 if self .solve_info is not None :
251- self .solve_info .n_sat_calls += 1
250+ self .solve_info .n_sat_calls += 1
252251 if btor .Sat () != btor .SAT :
253252 # All the soft constraints cannot be satisfied. We'll need to
254253 # add them incrementally
@@ -259,7 +258,7 @@ def randomize(self, ri : RandInfo, bound_m : Dict[FieldModel,VariableBoundModel]
259258 btor .Assume (c [1 ])
260259
261260 if self .solve_info is not None :
262- self .solve_info .n_sat_calls += 1
261+ self .solve_info .n_sat_calls += 1
263262 if btor .Sat () == btor .SAT :
264263 if self .debug > 0 :
265264 print ("Note: soft constraint %s (%d) passed" % (
@@ -276,7 +275,7 @@ def randomize(self, ri : RandInfo, bound_m : Dict[FieldModel,VariableBoundModel]
276275 for c in soft_constraint_l :
277276 btor .Assert (c [1 ])
278277
279- # Changes made to the randset are covered by the randomization_cache
278+ # Changes made to the randset are covered by the randomization_cache
280279 # Cache btor reference for use later
281280 if cache_enabled :
282281 self .btor_cache [rs_i ] = btor
@@ -589,13 +588,16 @@ def do_randomize(
589588 break
590589
591590 if cache_enabled :
592- # HACK Fill out field_l in FieldArrayModels so that look ups work
593- # This breaks deepcopy since it'll now have deepcopy references...
591+ # HACK Clear out field_l in FieldArrayModel from previous cache
594592 for fm in field_model_l :
595593 if hasattr (fm , 'field_l' ):
596594 for f in fm .field_l :
597- if hasattr (f , 'field_l' ):
598- f .latest_field_l = None
595+ if hasattr (f , 'field_l' ) and hasattr (f , 'old_field_l' ):
596+ # Revert to original value
597+ f .field_l = f .old_field_l
598+ elif hasattr (f , 'field_l' ):
599+ # Save off old, original value
600+ f .old_field_l = f .field_l
599601 # Save off original variables for FieldArrayModel hack after randomize
600602 (field_model_l_og , constraint_l_og ) = (field_model_l , constraint_l )
601603
@@ -609,6 +611,15 @@ def do_randomize(
609611 if ' dist { ' in call_hash :
610612 cache_enabled = False
611613 else :
614+ if call_hash not in Randomizer .randomize_call_count :
615+ Randomizer .randomize_call_count [call_hash ] = 0
616+ Randomizer .randomize_call_count [call_hash ] += 1
617+
618+ # Don't cache until this call_hash was seen N times
619+ if Randomizer .randomize_call_count [call_hash ] < 2 :
620+ cache_enabled = False
621+
622+ # Reset cache entry after N uses due to Boolector model growth
612623 if call_hash in Randomizer .randomize_cache :
613624 cache = Randomizer .randomize_cache [call_hash ]
614625 cache .r .btor_cache_uses -= 1
@@ -624,33 +635,30 @@ def do_randomize(
624635 if cache_enabled :
625636 (field_model_l , constraint_l ) = copy .deepcopy ((field_model_l , constraint_l ))
626637
627- if debug > 0 :
628- print ("Initial Model:" )
638+ if debug > 0 :
639+ print ("Initial Model:" )
629640 for fm in field_model_l :
630641 print (" " + ModelPrettyPrinter .print (fm ))
631642
632643 for c in constraint_l :
633644 clear_soft_priority .clear (c )
634645
635- # Collect all variables (pre-array) and establish bounds
646+ # Collect all variables (pre-array) and establish bounds
636647 bounds_v = VariableBoundVisitor ()
637648 bounds_v .process (field_model_l , constraint_l , False )
638649
639650 # TODO: need to handle inline constraints that impact arrays
640651 constraints_len = len (constraint_l )
641- # TODO dist are handled as soft constraints that caching doesn't recalculate...
642652 for fm in field_model_l :
643653 constraint_l .extend (ArrayConstraintBuilder .build (
644654 fm , bounds_v .bound_m ))
645655 # Now, handle dist constraints
646- # TODO Does this depend on the ArrayConstraintBuilder above?
647656 DistConstraintBuilder .build (randstate , fm )
648657
649658 for c in constraint_l :
650659 constraint_l .extend (ArrayConstraintBuilder .build (
651660 c , bounds_v .bound_m ))
652661 # Now, handle dist constraints
653- # TODO Does this depend on the ArrayConstraintBuilder above?
654662 DistConstraintBuilder .build (randstate , c )
655663
656664 # If we made changes during array remodeling,
@@ -659,7 +667,7 @@ def do_randomize(
659667 bounds_v .process (field_model_l , constraint_l )
660668
661669 if debug > 0 :
662- print ("Final Model:" )
670+ print ("Final Model:" )
663671 for fm in field_model_l :
664672 print (" " + ModelPrettyPrinter .print (fm ))
665673 for c in constraint_l :
@@ -673,36 +681,35 @@ def do_randomize(
673681 r = Randomizer (
674682 randstate ,
675683 solve_info = solve_info ,
676- debug = debug ,
677- lint = lint ,
684+ debug = debug ,
685+ lint = lint ,
678686 solve_fail_debug = solve_fail_debug )
679687# if Randomizer._rng is None:
680688# Randomizer._rng = random.Random(random.randrange(sys.maxsize))
681689 ri = RandInfoBuilder .build (field_model_l , constraint_l , Randomizer ._rng )
682690
683- # TODO Unecessary function refactor?
684691 Randomizer .try_randomize (srcinfo , field_model_l , solve_info , bounds_v , r , ri , cache_enabled )
685692
686- # Cache all interesting variables for later
693+ # Cache all interesting variables for later
687694 if cache_enabled :
688695 Randomizer .randomize_cache [call_hash ] = rand_cache_entry (bounds_v , ri , r , field_model_l , constraint_l )
689696
690- # HACK Fill out field_l in FieldArrayModels so that look ups work
691- # This breaks deepcopy since it'll now have deepcopy references...
697+ # HACK Fill out field_l in FieldArrayModels so that array lookups work in model
692698 if cache_enabled :
693699 field_model_l = Randomizer .randomize_cache [call_hash ].field_model_l
694700 for fm_new , fm_og in zip (field_model_l , field_model_l_og ):
695701 if hasattr (fm_og , 'field_l' ):
696702 for f_new , f_og in zip (fm_new .field_l , fm_og .field_l ):
697703 if hasattr (f_og , 'field_l' ):
698- f_og .latest_field_l = f_new .field_l
704+ f_og .field_l = f_new .field_l
705+
699706
700707
701708 @staticmethod
702709 def get_pretty_call_hash (randstate , field_model_l , constraint_l ):
703710 call_hash = ''
704711 call_hash += f'{ hex (id (randstate ))} \n '
705- if field_model_l is not None :
712+ if field_model_l is not None :
706713 for fm in field_model_l :
707714 # TODO This pretty print is an expensive call. Need a better way
708715 # to construct a unique ID/hash that doesn't depend on
@@ -716,15 +723,12 @@ def get_pretty_call_hash(randstate, field_model_l, constraint_l):
716723 if hasattr (fm , 'constraint_model_l' ):
717724 for cm in fm .constraint_model_l :
718725 call_hash += f'{ cm .name } -{ cm .enabled = } \n '
719- # TODO Is there a way to detect or quickly generate dist constraints?
720726
721- if constraint_l is not None :
722- # Each with constraint(block?) and its expressions
723- # TODO Is this missing anything? Dynamic expressions? Too aggressive?
727+ if constraint_l is not None :
728+ # Each with constraint(block?), its expressions, and enabled bit
724729 for cm in constraint_l :
725730 call_hash += ModelPrettyPrinter .print (cm , print_values = True )
726731 call_hash += f'{ cm .name } -{ cm .enabled = } \n '
727- # TODO Is there a way to detect or quickly generate dist constraints?
728732 return call_hash
729733
730734 @staticmethod
0 commit comments