Merge pull request #33 from coti/master

Use z3 to get feasible points

orio/main/tuner/search/randomsimple/randomsimple.py

@@ -14,7 +14,6 @@ def __init__(self, params):
         orio.main.tuner.search.search.Search.__init__(self, params)
 
         self.__readAlgoArgs()
-        #        self.have_z3 = False
 
         if self.time_limit <= 0 and self.total_runs <= 0:
             err((
@@ -24,9 +23,10 @@ def __init__(self, params):
     def searchBestCoord(self, startCoord=None):
 
         info('\n----- begin random search -----')
-        print("Total runs:", self.total_runs)
-        print("Time limit:", self.time_limit)
 
+        info( "Total runs: %d" % self.total_runs )
+        info( "Time limit: %d" % self.time_limit )
+
         bestperfcost = self.MAXFLOAT
         bestcoord = None
         runs = 0
@@ -42,25 +42,28 @@ def searchBestCoord(self, startCoord=None):
             # get a random point
             coord = self.getRandomCoord()
 
-            # if not self.have_z3 and not self.checkValidity( coord ) or coord in visited:
-            if not self.checkValidity(coord) or coord in visited:
-                print("invalid point")
+            if coord == None:
+                debug( "No points left in the parameter space", obj=self, level=3 )
+                break
+            if not self.checkValidity( coord ) or coord in visited:
+                debug( "invalid point", obj=self, level=3 )
                 continue
             try:
-                print("coord:", coord, "run", runs)
-                perf_costs = self.getPerfCost(coord)
-                if bestperfcost > sum(perf_costs):
-                    info("Point %s gives a better perf: %s -- %s" % (coord, sum(perf_costs), bestperfcost))
-                    bestperfcost = sum(perf_costs)
+                debug( "coord: %s run %s" % (coord, runs ), obj=self, level=3 )
+                perf_costs = self.getPerfCost( coord )
+                if bestperfcost > sum( perf_costs ):
+                    info( "Point %s gives a better perf: %s -- %s" % (coord, sum( perf_costs ), bestperfcost ) )
+                    bestperfcost = sum( perf_costs )
                     bestcoord = coord
             except Exception as e:
                 info('FAILED: %s %s' % (e.__class__.__name__, e))
             runs += 1
-            # if not self.have_z3:
-            visited.append(coord)
-            # else:
-            #    point = self.coordToPerfParams( coord )
-            #    self.addPoint( point )
+
+            if not self.use_z3:
+                visited.append( coord )
+            else:
+                point = self.coordToPerfParams( coord )
+                self.z3solver.addPoint( point )
 
         search_time = time.time() - start_time
         return bestcoord, bestperfcost, search_time, runs
@@ -82,3 +85,4 @@ def __readAlgoArgs(self):
             else:
                 err('orio.main.tuner.search.randomsimple: unrecognized %s algorithm-specific argument: "%s"' %
                     (self.__class__.__name__, vname))
+

orio/main/tuner/search/search.py

@@ -5,7 +5,6 @@
 from orio.main.util.globals import *
 from functools import reduce
 
-
 class Search:
     '''The search engine used to explore the search space '''
 
@@ -75,12 +74,27 @@ def __init__(self, params):
         self.input_params = params.get('input_params')
 
         self.timing_code = ''
-        
+
         self.verbose = Globals().verbose
         self.perf_cost_records = {}
         self.transform_time={}
         self.best_coord_info="None"
 
+        # TODO pass it as an option
+        #        if 'use_z3' in params.keys():
+        try:
+            import z3_search
+            _use_z3 = True
+        except Exception as e:
+            _use_z3 = False
+
+        if _use_z3:
+            self.use_z3 = True
+            self.z3solver = z3_search.Z3search( self.total_dims, self.axis_names, self.axis_val_ranges, self.dim_uplimits, self.params['ptdriver'].tinfo.pparam_constraints, self )
+        else:
+            self.use_z3 = False
+            self.z3solver = None
+
     #----------------------------------------------------------
 
     def searchBestCoord(self):
@@ -165,7 +179,17 @@ def coordToPerfParams(self, coord):
         perf_params = {}
         for i in range(0, self.total_dims):
             ipoint = coord[i]
-            perf_params[self.axis_names[i]] = self.axis_val_ranges[i][ipoint]
+            # If the point is not in the definition domain, take the nearest feasible value (z3)
+            if ipoint < len( self.axis_val_ranges[i] ):
+                perf_params[self.axis_names[i]] = self.axis_val_ranges[i][ipoint]
+            else:
+                if ipoint > self.axis_val_ranges[-1]:
+                    perf_params[self.axis_names[i]] = self.axis_val_ranges[i][-1]
+                else:
+                    perf_params[self.axis_names[i]] = self.axis_val_ranges[i][0]
+
+            # BN old version: perf_params[self.axis_names[i]] = self.axis_val_ranges[i][ipoint]
+
         return perf_params
 
     #----------------------------------------------------------
@@ -464,7 +488,13 @@ def getRandomCoord(self):
             iuplimit = self.dim_uplimits[i]
             ipoint = self.getRandomInt(0, iuplimit-1)
             random_coord.append(ipoint)
-        return random_coord
+        if self.use_z3:
+            point = self.z3solver.getNearestFeasible( random_coord )
+            if None == point:
+                return None
+            return self.z3solver.perfParamTabToCoord( point )
+        else:
+            return random_coord
 
 
     def getInitCoord(self):
@@ -475,9 +505,11 @@ def getInitCoord(self):
             #iuplimit = self.dim_uplimits[i]
             #ipoint = self.getRandomInt(0, iuplimit-1)
             random_coord.append(0)
-        return random_coord
-
-
+        if self.use_z3:
+            point = self.z3solver.getNearestFeasible( random_coord )
+            return self.z3solver.perfParamTabToCoord( point )
+        else:
+            return random_coord
 
     #----------------------------------------------------------
 

orio/main/tuner/search/simplex/simplex.py

@@ -57,6 +57,8 @@ def __init__(self, params):
         self.x0 = [0] * self.total_dims
         self.sim_size = max(self.dim_uplimits)
 
+#        _have_z3 = False
+
         # read all algorithm-specific arguments
         self.__readAlgoArgs()
 
@@ -430,7 +432,8 @@ def __readAlgoArgs(self):
                 err('man.tuner.search.simplex.simplex: unrecognized %s algorithm-specific argument: "%s"' %
                        (self.__class__.__name__, vname))
 
-
+    #-----------------------------------------------------
+
     #-----------------------------------------------------
 
     def __checkSearchSpace(self):
@@ -539,32 +542,68 @@ def __initRandomSimplex(self, simplex_records):
 
     #-----------------------------------------------------
 
+    # Get a centroid. If we are using z3, get a *feasible* centroid
+    # Get the nearest feasible point to the center
     def __getCentroid(self, coords):
-        '''Return a centroid coordinate'''
+        # Get a centroid
         total_coords = len(coords)
         centroid = coords[0]
         for c in coords[1:]:
             centroid = self.addCoords(centroid, c)
         centroid = self.mulCoords((1.0/total_coords), centroid)
-        return centroid
 
+        if self.use_z3:
+            # Get the nearest feasible point
+            point = self.z3solver.getNearestFeasible( centroid )
+            return self.z3solver.perfParamTabToCoord( point ) 
+        else:
+            return centroid
+
+    #-----------------------------------------------------
+
     def __getReflection(self, coord, centroid):
         '''Return a reflection coordinate'''
         sub_coord = self.subCoords(centroid, coord)
-        return [self.addCoords(centroid, self.mulCoords(x, sub_coord)) for x in self.refl_coefs]
-
+
+        point = map(lambda x: self.addCoords(centroid, self.mulCoords(x, sub_coord)),
+                    self.refl_coefs)
+        if self.use_z3:
+            # Get the nearest feasible point
+            return [ self.z3solver.perfParamTabToCoord( self.z3solver.getNearestFeasible( p ) ) for p in point ]
+       	else:
+            return list(point)
+
     def __getExpansion(self, coord, centroid):
         '''Return an expansion coordinate'''
         sub_coord = self.subCoords(coord, centroid)
-        return [self.addCoords(centroid, self.mulCoords(x, sub_coord)) for x in self.exp_coefs]
+        point = map(lambda x: self.addCoords(centroid, self.mulCoords(x, sub_coord)),
+                   self.exp_coefs)
+        if self.use_z3:
+            # Get the nearest feasible point
+            return [ self.z3solver.perfParamTabToCoord( self.z3solver.getNearestFeasible( p ) ) for p in point ]
+       	else:
+            return list(point)
 
     def __getContraction(self, coord, centroid):
         '''Return a contraction coordinate'''
         sub_coord = self.subCoords(coord, centroid)
-        return [self.addCoords(centroid, self.mulCoords(x, sub_coord)) for x in self.cont_coefs]
+
+        point = map(lambda x: self.addCoords(centroid, self.mulCoords(x, sub_coord)),
+                   self.cont_coefs)
+        if self.use_z3:
+            # Get the nearest feasible point
+            return [ self.z3solver.perfParamTabToCoord( self.z3solver.getNearestFeasible( p ) ) for p in point ]
+       	else:
+            return list(point)
 
     def __getShrinkage(self, coord, rest_coords):
         '''Return a shrinkage simplex'''
-        return [self.addCoords(coord, self.mulCoords(self.shri_coef,
-                                                                  self.subCoords(x, coord))) for x in rest_coords]
-
+        point = map(lambda x: self.addCoords(coord, self.mulCoords(self.shri_coef,
+                                                                  self.subCoords(x, coord))),
+                   rest_coords)
+        if self.use_z3:
+            # Get the nearest feasible point
+            return [ self.z3solver.perfParamTabToCoord( self.z3solver.getNearestFeasible( p ) ) for p in point ]
+       	else:
+            return list(point)
+