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?
@@ -202,7 +201,7 @@ def randomize(self, ri : RandInfo, bound_m : Dict[FieldModel,VariableBoundModel]
202201 # rs_i += 1
203202 if n_fields > max_fields or rs .order != - 1 :
204203 break
205-
204+
206205 for c in constraint_l :
207206 try :
208207 btor .Assume (c [1 ])
@@ -237,7 +236,7 @@ def randomize(self, ri : RandInfo, bound_m : Dict[FieldModel,VariableBoundModel]
237236 btor .Assert (c [1 ])
238237
239238 # If there are soft constraints, add these now
240- if len (soft_constraint_l ) > 0 :
239+ if len (soft_constraint_l ) > 0 :
241240 for c in soft_constraint_l :
242241 try :
243242 btor .Assume (c [1 ])
@@ -247,7 +246,7 @@ def randomize(self, ri : RandInfo, bound_m : Dict[FieldModel,VariableBoundModel]
247246 raise e
248247
249248 if self .solve_info is not None :
250- self .solve_info .n_sat_calls += 1
249+ self .solve_info .n_sat_calls += 1
251250 if btor .Sat () != btor .SAT :
252251 # All the soft constraints cannot be satisfied. We'll need to
253252 # add them incrementally
@@ -258,7 +257,7 @@ def randomize(self, ri : RandInfo, bound_m : Dict[FieldModel,VariableBoundModel]
258257 btor .Assume (c [1 ])
259258
260259 if self .solve_info is not None :
261- self .solve_info .n_sat_calls += 1
260+ self .solve_info .n_sat_calls += 1
262261 if btor .Sat () == btor .SAT :
263262 if self .debug > 0 :
264263 print ("Note: soft constraint %s (%d) passed" % (
@@ -275,7 +274,7 @@ def randomize(self, ri : RandInfo, bound_m : Dict[FieldModel,VariableBoundModel]
275274 for c in soft_constraint_l :
276275 btor .Assert (c [1 ])
277276
278- # Changes made to the randset are covered by the randomization_cache
277+ # Changes made to the randset are covered by the randomization_cache
279278 # Cache btor reference for use later
280279 if cache_enabled :
281280 self .btor_cache [rs_i ] = btor
@@ -588,13 +587,16 @@ def do_randomize(
588587 break
589588
590589 if cache_enabled :
591- # HACK Fill out field_l in FieldArrayModels so that look ups work
592- # This breaks deepcopy since it'll now have deepcopy references...
590+ # HACK Clear out field_l in FieldArrayModel from previous cache
593591 for fm in field_model_l :
594592 if hasattr (fm , 'field_l' ):
595593 for f in fm .field_l :
596- if hasattr (f , 'field_l' ):
597- f .latest_field_l = None
594+ if hasattr (f , 'field_l' ) and hasattr (f , 'old_field_l' ):
595+ # Revert to original value
596+ f .field_l = f .old_field_l
597+ elif hasattr (f , 'field_l' ):
598+ # Save off old, original value
599+ f .old_field_l = f .field_l
598600 # Save off original variables for FieldArrayModel hack after randomize
599601 (field_model_l_og , constraint_l_og ) = (field_model_l , constraint_l )
600602
@@ -608,6 +610,15 @@ def do_randomize(
608610 if ' dist { ' in call_hash :
609611 cache_enabled = False
610612 else :
613+ if call_hash not in Randomizer .randomize_call_count :
614+ Randomizer .randomize_call_count [call_hash ] = 0
615+ Randomizer .randomize_call_count [call_hash ] += 1
616+
617+ # Don't cache until this call_hash was seen N times
618+ if Randomizer .randomize_call_count [call_hash ] < 2 :
619+ cache_enabled = False
620+
621+ # Reset cache entry after N uses due to Boolector model growth
611622 if call_hash in Randomizer .randomize_cache :
612623 cache = Randomizer .randomize_cache [call_hash ]
613624 cache .r .btor_cache_uses -= 1
@@ -623,33 +634,30 @@ def do_randomize(
623634 if cache_enabled :
624635 (field_model_l , constraint_l ) = copy .deepcopy ((field_model_l , constraint_l ))
625636
626- if debug > 0 :
627- print ("Initial Model:" )
637+ if debug > 0 :
638+ print ("Initial Model:" )
628639 for fm in field_model_l :
629640 print (" " + ModelPrettyPrinter .print (fm ))
630641
631642 for c in constraint_l :
632643 clear_soft_priority .clear (c )
633644
634- # Collect all variables (pre-array) and establish bounds
645+ # Collect all variables (pre-array) and establish bounds
635646 bounds_v = VariableBoundVisitor ()
636647 bounds_v .process (field_model_l , constraint_l , False )
637648
638649 # TODO: need to handle inline constraints that impact arrays
639650 constraints_len = len (constraint_l )
640- # TODO dist are handled as soft constraints that caching doesn't recalculate...
641651 for fm in field_model_l :
642652 constraint_l .extend (ArrayConstraintBuilder .build (
643653 fm , bounds_v .bound_m ))
644654 # Now, handle dist constraints
645- # TODO Does this depend on the ArrayConstraintBuilder above?
646655 DistConstraintBuilder .build (randstate , fm )
647656
648657 for c in constraint_l :
649658 constraint_l .extend (ArrayConstraintBuilder .build (
650659 c , bounds_v .bound_m ))
651660 # Now, handle dist constraints
652- # TODO Does this depend on the ArrayConstraintBuilder above?
653661 DistConstraintBuilder .build (randstate , c )
654662
655663 # If we made changes during array remodeling,
@@ -658,7 +666,7 @@ def do_randomize(
658666 bounds_v .process (field_model_l , constraint_l )
659667
660668 if debug > 0 :
661- print ("Final Model:" )
669+ print ("Final Model:" )
662670 for fm in field_model_l :
663671 print (" " + ModelPrettyPrinter .print (fm ))
664672 for c in constraint_l :
@@ -672,36 +680,35 @@ def do_randomize(
672680 r = Randomizer (
673681 randstate ,
674682 solve_info = solve_info ,
675- debug = debug ,
676- lint = lint ,
683+ debug = debug ,
684+ lint = lint ,
677685 solve_fail_debug = solve_fail_debug )
678686# if Randomizer._rng is None:
679687# Randomizer._rng = random.Random(random.randrange(sys.maxsize))
680688 ri = RandInfoBuilder .build (field_model_l , constraint_l , Randomizer ._rng )
681689
682- # TODO Unecessary function refactor?
683690 Randomizer .try_randomize (srcinfo , field_model_l , solve_info , bounds_v , r , ri , cache_enabled )
684691
685- # Cache all interesting variables for later
692+ # Cache all interesting variables for later
686693 if cache_enabled :
687694 Randomizer .randomize_cache [call_hash ] = rand_cache_entry (bounds_v , ri , r , field_model_l , constraint_l )
688695
689- # HACK Fill out field_l in FieldArrayModels so that look ups work
690- # This breaks deepcopy since it'll now have deepcopy references...
696+ # HACK Fill out field_l in FieldArrayModels so that array lookups work in model
691697 if cache_enabled :
692698 field_model_l = Randomizer .randomize_cache [call_hash ].field_model_l
693699 for fm_new , fm_og in zip (field_model_l , field_model_l_og ):
694700 if hasattr (fm_og , 'field_l' ):
695701 for f_new , f_og in zip (fm_new .field_l , fm_og .field_l ):
696702 if hasattr (f_og , 'field_l' ):
697- f_og .latest_field_l = f_new .field_l
703+ f_og .field_l = f_new .field_l
704+
698705
699706
700707 @staticmethod
701708 def get_pretty_call_hash (randstate , field_model_l , constraint_l ):
702709 call_hash = ''
703710 call_hash += f'{ hex (id (randstate ))} \n '
704- if field_model_l is not None :
711+ if field_model_l is not None :
705712 for fm in field_model_l :
706713 # TODO This pretty print is an expensive call. Need a better way
707714 # to construct a unique ID/hash that doesn't depend on
@@ -715,15 +722,12 @@ def get_pretty_call_hash(randstate, field_model_l, constraint_l):
715722 if hasattr (fm , 'constraint_model_l' ):
716723 for cm in fm .constraint_model_l :
717724 call_hash += f'{ cm .name } -{ cm .enabled = } \n '
718- # TODO Is there a way to detect or quickly generate dist constraints?
719725
720- if constraint_l is not None :
721- # Each with constraint(block?) and its expressions
722- # TODO Is this missing anything? Dynamic expressions? Too aggressive?
726+ if constraint_l is not None :
727+ # Each with constraint(block?), its expressions, and enabled bit
723728 for cm in constraint_l :
724729 call_hash += ModelPrettyPrinter .print (cm , print_values = True )
725730 call_hash += f'{ cm .name } -{ cm .enabled = } \n '
726- # TODO Is there a way to detect or quickly generate dist constraints?
727731 return call_hash
728732
729733 @staticmethod
0 commit comments