From 0f57b215d807e8b3532df197c76888995fb9fa3f Mon Sep 17 00:00:00 2001 From: Camille Coti Date: Mon, 14 Dec 2020 18:48:53 -0800 Subject: [PATCH 01/11] cleaned the randomsimple search module, using z3 to get feasible points --- .../tuner/search/randomsimple/__init__.py | 0 .../tuner/search/randomsimple/randomsimple.py | 191 +++++++++++++++++- 2 files changed, 185 insertions(+), 6 deletions(-) create mode 100644 orio/main/tuner/search/randomsimple/__init__.py diff --git a/orio/main/tuner/search/randomsimple/__init__.py b/orio/main/tuner/search/randomsimple/__init__.py new file mode 100644 index 00000000..e69de29b diff --git a/orio/main/tuner/search/randomsimple/randomsimple.py b/orio/main/tuner/search/randomsimple/randomsimple.py index 50f1e971..d76c1f7a 100644 --- a/orio/main/tuner/search/randomsimple/randomsimple.py +++ b/orio/main/tuner/search/randomsimple/randomsimple.py @@ -6,6 +6,12 @@ import orio.main.tuner.search.search from orio.main.util.globals import * +try: + import z3 + _have_z3 = True +except Exception as e: + _have_z3 = False + class Randomsimple(orio.main.tuner.search.search.Search): def __init__(self, params): @@ -13,7 +19,13 @@ def __init__(self, params): orio.main.tuner.search.search.Search.__init__(self, params) self.__readAlgoArgs() -# self.have_z3 = False + if _have_z3: + self.have_z3 = True + self.initZ3() + else: + self.have_z3 = False + self.solver = None + self.optim = None if self.time_limit <= 0 and self.total_runs <= 0: err(('orio.main.tuner.search.randomsimple.randomsimple: %s search requires either (both) the search time limit or (and) the ' + @@ -22,8 +34,8 @@ 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 + print( "Total runs:", self.total_runs ) + print( "Time limit:", self.time_limit ) bestperfcost = self.MAXFLOAT bestcoord = None @@ -40,10 +52,10 @@ def searchBestCoord(self, startCoord=None): coord = self.getRandomCoord() if not self.have_z3 and not self.checkValidity( coord ) or coord in visited: - print "invalid point" + print( "invalid point" ) continue try: - print "coord:", coord, "run", runs + 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 ) ) @@ -56,7 +68,7 @@ def searchBestCoord(self, startCoord=None): visited.append( coord ) else: point = self.coordToPerfParams( coord ) - self.addPoint( point ) + self.__addPoint( point ) search_time = time.time() - start_time return bestcoord, bestperfcost, search_time, runs @@ -77,3 +89,170 @@ def __readAlgoArgs(self): else: err('orio.main.tuner.search.randomsimple: unrecognized %s algorithm-specific argument: "%s"' % (self.__class__.__name__, vname)) + + def initZ3(self): + # Initialize the solver itself + self.variables = [] + self.solver = z3.Solver() + self.optim = z3.Optimize() + Globals.z3types = {} + Globals.z3variables = {} + + # find what we have on the axis + self.__addVariableNames( self.axis_names, self.axis_val_ranges ) + self.__addConstraints( self.params['ptdriver'].tinfo.pparam_constraints ) + + # In this function, either z3 finds a feasible point, or we ask the default function draw one. + def __getRandomPoint(self): + if not self.have_z3: + self.getRandomCoord() + else: + # if I have z3, get a *feasible* random coord + model = self._getRandomCoordZ3() + #model = self._getRandomCoordZ3Distance() + point = self._z3ToPoint( model ) + coord = self._perfParamTabToCoord( point ) + # If I could not find any feasible point, just return a random point + if None != coord: + return coord + + # Defines the variables, their type and, for numeric ones, their definition domain + def __addVariableNames( self, names, ranges ): + for idx, name in enumerate( names ): + values = ranges[idx] + if ( [ True, False ] == values ) or ( [ False, True ] == values ): #len( values ) == 2 and ( False in values or True in values ): + Globals.z3variables[name] = z3.Bool( name ) + self.__addDefinitionDomain( name, values ) + else: + try: + toto = int( values[0] ) + Globals.z3variables[name] = z3.Int( name ) + self.__addDefinitionDomain( name, values ) + except ValueError: + # if the parameter is non-numeric + # TODO we can add a case to handle floats + Globals.z3variables[name] = z3.Int( name ) + numvalues = self.__defineNonNumeric( name, values ) + self.__addDefinitionDomain( name, numvalues ) + self.variables.append( name ) # FIXME variables is axis_names + return + + # z3-specific routine: + # Defines a variable's definition domain + def __addDefinitionDomain( self, var, dom ): + # get the variables + for k,v in Globals.z3variables.iteritems( ): + locals()[k] = v + if len( dom ) == 0: + return + definition = z3.Or( [ eval( "(" + var + " == " + str( v ) + ")" ) for v in dom ] ) + # definition = z3.And( [ v >= 0, v < len( dom ) ] ) + + self.solver.add( definition ) + self.optim.add( definition ) + return + + # z3-specific routine: + # Add the constraints + def __addConstraints( self, constraints ): + # get the variables + for k,v in Globals.z3variables.iteritems( ): + locals()[k] = v + for vname, rhs in constraints: + # convert to constraint to prefix syntax + toto = eval( self.__infixToPrefix( rhs ) ) + self.solver.add( toto ) + self.optim.add( toto ) + return + + # z3-specific routine: + # in case a parameter is not numeric (ie, alphanumeric), we cannot store it + # as a regular value with constraints in z3. Hence, put the values in a list and + # use their index in the list instead. + def __defineNonNumeric( self, name, values ): + Globals.z3types[name] = list( values ) + return [ i for i in range( len( values ) ) ] + + # z3-specific routine: + # get the parameter corresponding to a numeric value + def __numericToNonNumeric( self, name, value, num ): + return Globals.z3types[name][num] + + # z3-specific routine: + # get the numeric value corresponding to a parameter + def __nonNumericToNumeric( self, name, value, param ): + return Globals.z3types[name].index( param ) + + # z3-specific routine: + # change constraint from infix notation (used in the input file) to prefix notation (used by z3) + def __infixToPrefix( self, expr ): + if "or" in expr or "and" in expr: + if "and" in expr: + operandsAND = expr.split( "and" ) + return "z3.And(" + ", ".join( [ infixToPrefix( op ) if "or" in op or "and" in op else op for op in operandsAND ] ) + " ) " + elif "or" in expr: + operandsOR = expr.split( "or" ) + return "z3.Or(" + ", ".join( [ infixToPrefix( op ) if "or" in op or "and" in op else op for op in operandsOR ] ) + " ) " + else: + return expr + else: + return expr + + # Add a forbidden point in the solver (and the optimizer) + # Input: a dictionary of performance parameters. + def __addPoint( self, point ): + # get the variables corresponding to the axis names + for name in self.axis_names: + locals()[name] = Globals.z3variables[name] + point2 = {} + # if there is a non-numeric value here, translate it + for idx, name in enumerate( point.keys() ): + # translate non-numeric values + if not self.z3IsNumeric( idx ): # non-numeric points -> coord to value + elem = Globals.z3types[name].index( point[name] ) + else: + elem = point[name] + point2[name] = elem + + # remove this point + for s in [ self.solver, self.optim ]: + s.add( z3.Or( [ locals()[name] != point2[name] for name in self.axis_names ] ) ) + + # Tests whether a z3 variable is numeric. Returns False for non-numeric ones. + def z3IsNumeric( self, dimensionNumber ): + return not self.axis_names[dimensionNumber] in Globals.z3types + + # Returns a *feasible* random point + def _getRandomCoordZ3( self ): + if self.solver.check() == z3.unsat: + return None + else: + model = self.solver.model() + return model + + # Converts a model (returned by z3) into a point. + # Returns a list + def z3ToPoint( self, point ): + res = [] + # get the variables corresponding to the axis names + for idx, i in enumerate( self.axis_names ): + locals()[i] = Globals.z3variables[i] + if i in Globals.z3types: # non-numeric points -> coord to value + value = Globals.z3types[i][point[locals()[i]].as_long()] + elif None == point[locals()[i]]: + info( "no value for %s, take %r (incomplete model)" % ( self.axis_names[idx], self.axis_val_ranges[idx][0] ) ) + value = self.axis_val_ranges[idx][ 0] + elif z3.is_int_value( point[locals()[i]] ): + value = point[locals()[i]].as_long() + elif z3.is_true( point[locals()[i]] ) or z3.is_false( point[locals()[i]] ): + value = z3.is_true( point[locals()[i]] ) + res.append( value ) + return res + + def perfParamTabToCoord( self, params ): + coord = [None]*self.total_dims + for i in range( self.total_dims ): + coord[i] = self.axis_val_ranges[i].index( params[i] ) + return coord + + From 82a04e12eeb2ced9ebd514ac95962a34259c5e35 Mon Sep 17 00:00:00 2001 From: Camille Coti Date: Mon, 21 Dec 2020 14:46:05 -0800 Subject: [PATCH 02/11] Use z3 to get feasible points in the Simplex (Nelder-Mead) search algo --- orio/main/tuner/search/simplex/simplex.py | 422 +++++++++++++++++++++- 1 file changed, 410 insertions(+), 12 deletions(-) diff --git a/orio/main/tuner/search/simplex/simplex.py b/orio/main/tuner/search/simplex/simplex.py index a768a03d..311f97b2 100644 --- a/orio/main/tuner/search/simplex/simplex.py +++ b/orio/main/tuner/search/simplex/simplex.py @@ -10,6 +10,12 @@ import orio.main.tuner.search.search from orio.main.util.globals import * +try: + import z3 + _have_z3 = True +except Exception as e: + _have_z3 = False + #----------------------------------------------------- class Simplex(orio.main.tuner.search.search.Search): @@ -56,8 +62,17 @@ 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() + if _have_z3: + self.have_z3 = True + self.initZ3() + else: + self.have_z3 = False + self.solver = None + self.optim = None # complain if both the search time limit and the total number of search runs are undefined if self.time_limit <= 0 and self.total_runs <= 0: @@ -430,7 +445,129 @@ def __readAlgoArgs(self): err('man.tuner.search.simplex.simplex: unrecognized %s algorithm-specific argument: "%s"' % (self.__class__.__name__, vname)) + #----------------------------------------------------- + + def initZ3(self): + # Initialize the solver itself + self.variables = [] + self.solver = z3.Solver() + self.optim = z3.Optimize() + Globals.z3types = {} + Globals.z3variables = {} + + # find what we have on the axis + self.__addVariableNames( self.axis_names, self.axis_val_ranges ) + self.__addConstraints( self.params['ptdriver'].tinfo.pparam_constraints ) + + # Defines the variables, their type and, for numeric ones, their definition domain + def __addVariableNames( self, names, ranges ): + for idx, name in enumerate( names ): + values = ranges[idx] + if ( [ True, False ] == values ) or ( [ False, True ] == values ): #len( values ) == 2 and ( False in values or True in values ): + Globals.z3variables[name] = z3.Bool( name ) + self.__addDefinitionDomain( name, values ) + else: + try: + toto = int( values[0] ) + Globals.z3variables[name] = z3.Int( name ) + self.__addDefinitionDomain( name, values ) + except ValueError: + # if the parameter is non-numeric + # TODO we can add a case to handle floats + Globals.z3variables[name] = z3.Int( name ) + numvalues = self.__defineNonNumeric( name, values ) + self.__addDefinitionDomain( name, numvalues ) + self.variables.append( name ) # FIXME variables is axis_names + return + + # z3-specific routine: + # Defines a variable's definition domain + def __addDefinitionDomain( self, var, dom ): + # get the variables + for k,v in Globals.z3variables.iteritems( ): + locals()[k] = v + if len( dom ) == 0: + return + definition = z3.Or( [ eval( "(" + var + " == " + str( v ) + ")" ) for v in dom ] ) + # definition = z3.And( [ v >= 0, v < len( dom ) ] ) + + self.solver.add( definition ) + self.optim.add( definition ) + return + + # z3-specific routine: + # Add the constraints + def __addConstraints( self, constraints ): + # get the variables + for k,v in Globals.z3variables.iteritems( ): + locals()[k] = v + for vname, rhs in constraints: + # convert to constraint to prefix syntax + toto = eval( self.__infixToPrefix( rhs ) ) + self.solver.add( toto ) + self.optim.add( toto ) + return + + # z3-specific routine: + # in case a parameter is not numeric (ie, alphanumeric), we cannot store it + # as a regular value with constraints in z3. Hence, put the values in a list and + # use their index in the list instead. + def __defineNonNumeric( self, name, values ): + Globals.z3types[name] = list( values ) + return [ i for i in range( len( values ) ) ] + + # z3-specific routine: + # get the parameter corresponding to a numeric value + def __numericToNonNumeric( self, name, value, num ): + return Globals.z3types[name][num] + + # z3-specific routine: + # get the numeric value corresponding to a parameter + def __nonNumericToNumeric( self, name, value, param ): + return Globals.z3types[name].index( param ) + + # Tests whether a z3 variable is numeric. Returns False for non-numeric ones. + def z3IsNumeric( self, dimensionNumber ): + return not self.axis_names[dimensionNumber] in Globals.z3types + + #----------------------------------------------------- + + # z3-specific routine: + # change constraint from infix notation (used in the input file) to prefix notation (used by z3) + def __infixToPrefix( self, expr ): + if "or" in expr or "and" in expr: + if "and" in expr: + operandsAND = expr.split( "and" ) + return "z3.And(" + ", ".join( [ infixToPrefix( op ) if "or" in op or "and" in op else op for op in operandsAND ] ) + " ) " + elif "or" in expr: + operandsOR = expr.split( "or" ) + return "z3.Or(" + ", ".join( [ infixToPrefix( op ) if "or" in op or "and" in op else op for op in operandsOR ] ) + " ) " + else: + return expr + else: + return expr + # Add a forbidden point in the solver (and the optimizer) + # Input: a dictionary of performance parameters. + def __addPoint( self, point ): + # get the variables corresponding to the axis names + for name in self.axis_names: + locals()[name] = Globals.z3variables[name] + point2 = {} + # if there is a non-numeric value here, translate it + for idx, name in enumerate( point.keys() ): + # translate non-numeric values + if not self.z3IsNumeric( idx ): # non-numeric points -> coord to value + elem = Globals.z3types[name].index( point[name] ) + else: + elem = point[name] + point2[name] = elem + + # remove this point + for s in [ self.solver, self.optim ]: + s.add( z3.Or( [ locals()[name] != point2[name] for name in self.axis_names ] ) ) + return + #----------------------------------------------------- def __checkSearchSpace(self): @@ -524,7 +661,10 @@ def __initRandomSimplex(self, simplex_records): # randomly pick (N+1) vertices to form a simplex, where N is the number of dimensions simplex = [] while True: - coord = self.getRandomCoord() + if self.have_z3: + coord = self.getRandomCoord_z3_distance() + else: + coord = self.getRandomCoord() if coord not in simplex: simplex.append(coord) if len(simplex) == self.__simplex_size: @@ -538,36 +678,294 @@ 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.have_z3: + # Get the nearest feasible point + point = self.__getNearestFeasible( centroid ) + return self.perfParamTabToCoord( point ) + else: + return centroid + + #----------------------------------------------------- + + # Returns a *feasible* random point + def getRandomCoord_z3( self ): + if self.solver.check() == z3.unsat: + return None + else: + model = self.solver.model() + return model + + # Getting a random point from an SMT solver is not a trivial question. + # This one gives a somehow random point, but the distribution is not uniform. + # TODO: David's idea involving SAT. + # TODO: non-constrained variables? + def getRandomCoord_z3_distance( self ): + if self.solver.check() == z3.unsat: + return None + else: + # Pick a random point in the solution space + rpc = [] + for i in range( self.total_dims ): + iuplimit = self.dim_uplimits[i] + ipoint = self.getRandomInt(0, iuplimit-1) + rpc.append(ipoint) + + # Get the nearest feasible point + point = self.__getNearestFeasible( rpc ) + return self.perfParamTabToCoord( point ) + + #----------------------------------------------------- + def __getReflection(self, coord, centroid): '''Return a reflection coordinate''' sub_coord = self.subCoords(centroid, coord) - return map(lambda x: self.addCoords(centroid, self.mulCoords(x, sub_coord)), - self.refl_coefs) + point = map(lambda x: self.addCoords(centroid, self.mulCoords(x, sub_coord)), + self.refl_coefs) + if self.have_z3: + p = self.__getNearestFeasible( point[0] ) + return [ self.perfParamTabToCoord( p ) ] + else: + return point def __getExpansion(self, coord, centroid): '''Return an expansion coordinate''' sub_coord = self.subCoords(coord, centroid) - return map(lambda x: self.addCoords(centroid, self.mulCoords(x, sub_coord)), - self.exp_coefs) + point = map(lambda x: self.addCoords(centroid, self.mulCoords(x, sub_coord)), + self.exp_coefs) + if self.have_z3: + return [ self.perfParamTabToCoord( self.__getNearestFeasible( point[0] ) )] + else: + return point def __getContraction(self, coord, centroid): '''Return a contraction coordinate''' sub_coord = self.subCoords(coord, centroid) - return map(lambda x: self.addCoords(centroid, self.mulCoords(x, sub_coord)), - self.cont_coefs) + point = map(lambda x: self.addCoords(centroid, self.mulCoords(x, sub_coord)), + self.cont_coefs) + if self.have_z3: + return [ self.perfParamTabToCoord( self.__getNearestFeasible( point[0] ) )] + else: + return point def __getShrinkage(self, coord, rest_coords): '''Return a shrinkage simplex''' - return map(lambda x: self.addCoords(coord, self.mulCoords(self.shri_coef, - self.subCoords(x, coord))), - rest_coords) + point = map(lambda x: self.addCoords(coord, self.mulCoords(self.shri_coef, + self.subCoords(x, coord))), + rest_coords) + if self.have_z3: + return [ self.perfParamTabToCoord( self.__getNearestFeasible( p ) ) for p in point ] + else: + return point + #----------------------------------------------------- + + # Defines the variables, their type and, for numeric ones, their definition domain + def __addVariableNames( self, names, ranges ): + for idx, name in enumerate( names ): + values = ranges[idx] + if ( [ True, False ] == values ) or ( [ False, True ] == values ): #len( values ) == 2 and ( False in values or True in values ): + Globals.z3variables[name] = z3.Bool( name ) + self.__addDefinitionDomain( name, values ) + else: + try: + toto = int( values[0] ) + Globals.z3variables[name] = z3.Int( name ) + self.__addDefinitionDomain( name, values ) + except ValueError: + # if the parameter is non-numeric + # TODO we can add a case to handle floats + Globals.z3variables[name] = z3.Int( name ) + numvalues = self.__defineNonNumeric( name, values ) + self.__addDefinitionDomain( name, numvalues ) + self.variables.append( name ) # FIXME variables is axis_names + return + + # z3-specific routine: + # Defines a variable's definition domain + def __addDefinitionDomain( self, var, dom ): + # get the variables + for k,v in Globals.z3variables.iteritems( ): + locals()[k] = v + if len( dom ) == 0: + return + definition = z3.Or( [ eval( "(" + var + " == " + str( v ) + ")" ) for v in dom ] ) + # definition = z3.And( [ v >= 0, v < len( dom ) ] ) + + self.solver.add( definition ) + self.optim.add( definition ) + return + + # z3-specific routine: + # Add the constraints + def __addConstraints( self, constraints ): + # get the variables + for k,v in Globals.z3variables.iteritems( ): + locals()[k] = v + for vname, rhs in constraints: + # convert to constraint to prefix syntax + toto = eval( self.__infixToPrefix( rhs ) ) + self.solver.add( toto ) + self.optim.add( toto ) + return + + # z3-specific routine: + # in case a parameter is not numeric (ie, alphanumeric), we cannot store it + # as a regular value with constraints in z3. Hence, put the values in a list and + # use their index in the list instead. + def __defineNonNumeric( self, name, values ): + Globals.z3types[name] = list( values ) + return [ i for i in range( len( values ) ) ] + + # z3-specific routine: + # get the parameter corresponding to a numeric value + def __numericToNonNumeric( self, name, value, num ): + return Globals.z3types[name][num] + + # z3-specific routine: + # get the numeric value corresponding to a parameter + def __nonNumericToNumeric( self, name, value, param ): + return Globals.z3types[name].index( param ) + + # z3-specific routine: + # change constraint from infix notation (used in the input file) to prefix notation (used by z3) + def __infixToPrefix( self, expr ): + if "or" in expr or "and" in expr: + if "and" in expr: + operandsAND = expr.split( "and" ) + return "z3.And(" + ", ".join( [ infixToPrefix( op ) if "or" in op or "and" in op else op for op in operandsAND ] ) + " ) " + elif "or" in expr: + operandsOR = expr.split( "or" ) + return "z3.Or(" + ", ".join( [ infixToPrefix( op ) if "or" in op or "and" in op else op for op in operandsOR ] ) + " ) " + else: + return expr + else: + return expr + + # Add a forbidden point in the solver (and the optimizer) + # Input: a dictionary of performance parameters. + def __addPoint( self, point ): + # get the variables corresponding to the axis names + for name in self.axis_names: + locals()[name] = Globals.z3variables[name] + point2 = {} + # if there is a non-numeric value here, translate it + for idx, name in enumerate( point.keys() ): + # translate non-numeric values + if not self.z3IsNumeric( idx ): # non-numeric points -> coord to value + elem = Globals.z3types[name].index( point[name] ) + else: + elem = point[name] + point2[name] = elem + + # remove this point + for s in [ self.solver, self.optim ]: + s.add( z3.Or( [ locals()[name] != point2[name] for name in self.axis_names ] ) ) + + # Tests whether a z3 variable is numeric. Returns False for non-numeric ones. + def z3IsNumeric( self, dimensionNumber ): + return not self.axis_names[dimensionNumber] in Globals.z3types + + def z3abs( self, x ): + return z3.If(x >= 0,x,-x) + + #----------------------------------------------------- + + # Converts a model (returned by z3) into a point. + # Returns a list + def z3ToPoint( self, point ): + res = [] + # get the variables corresponding to the axis names + for idx, i in enumerate( self.axis_names ): + locals()[i] = Globals.z3variables[i] + if i in Globals.z3types: # non-numeric points -> coord to value + value = Globals.z3types[i][point[locals()[i]].as_long()] + elif None == point[locals()[i]]: + info( "no value for %s, take %r (incomplete model)" % ( self.axis_names[idx], self.axis_val_ranges[idx][0] ) ) + value = self.axis_val_ranges[idx][ 0] + elif z3.is_int_value( point[locals()[i]] ): + value = point[locals()[i]].as_long() + elif z3.is_true( point[locals()[i]] ) or z3.is_false( point[locals()[i]] ): + value = z3.is_true( point[locals()[i]] ) + res.append( value ) + return res + + def coordToPerfParams(self, coord): + '''To convert the given coordinate to the corresponding performance parameters''' + # get the performance parameters that correspond the given coordinate + perf_params = {} + for i in range(0, self.total_dims): + ipoint = coord[i] + # If the point is not in the definition domain, take the nearest feasible value + 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] + # return the obtained performance parameters + return perf_params + + def perfParamToCoord( self, params ): + coord = [None]*self.total_dims + for i in range( self.total_dims ): + coord[i] = params[self.axis_names[i]] + if not self.z3IsNumeric( i ): + name = self.axis_names[i] + coord[i] = Globals.z3types[name].index( coord[i] ) + return coord + + def coordToTabOfPerfParams( self, coord ): + params = self.coordToPerfParams( coord ) + perftab = [] + for i, name in enumerate( self.axis_names ): + c = params[name] + if not self.z3IsNumeric( i ): + c = Globals.z3types[name].index( c ) + perftab.append( c ) + return perftab + + def perfParamTabToCoord( self, params ): + coord = [None]*self.total_dims + for i in range( self.total_dims ): + coord[i] = self.axis_val_ranges[i].index( params[i] ) + return coord + + + #----------------------------------------------------- + + # For a given point, returns the nearest feasible point + def __getNearestFeasible(self, coord ): + # get the variables corresponding to the axis names + for i in self.axis_names: + locals()[i] = Globals.z3variables[i] + + # Convert into parameters + rpp = self.coordToPerfParams( coord ) + for i, name in enumerate( self.axis_names ): + if not self.z3IsNumeric( i ): + rpp[name] = Globals.z3types[name].index( rpp[name] ) + + # create a new scope + self.optim.push() + + # Get a possible point that minimizes the 1-norm distance to this random point + # forget the booleans + self.optim.minimize( z3.Sum( [ self.z3abs( locals()[name] - rpp[name] )for name in self.axis_names if not z3.is_bool( locals()[name] ) ] ) ) + if z3.unsat == self.optim.check(): + return None + model = self.optim.model() + + # restore the state (exit the scope) + self.optim.pop() + return self.z3ToPoint( model ) From 839acb249e7ca2589f84dfed480699c69e83e81f Mon Sep 17 00:00:00 2001 From: Camille Coti Date: Mon, 21 Dec 2020 18:10:39 -0800 Subject: [PATCH 03/11] Put the z3-related functions in a separate file in order to minimize modifications --- orio/main/tuner/search/simplex/simplex.py | 397 ++------------------ orio/main/tuner/search/simplex/z3_search.py | 315 ++++++++++++++++ 2 files changed, 338 insertions(+), 374 deletions(-) create mode 100644 orio/main/tuner/search/simplex/z3_search.py diff --git a/orio/main/tuner/search/simplex/simplex.py b/orio/main/tuner/search/simplex/simplex.py index 311f97b2..e6cedf23 100644 --- a/orio/main/tuner/search/simplex/simplex.py +++ b/orio/main/tuner/search/simplex/simplex.py @@ -13,6 +13,8 @@ try: import z3 _have_z3 = True + import z3_search + except Exception as e: _have_z3 = False @@ -68,11 +70,10 @@ def __init__(self, params): self.__readAlgoArgs() if _have_z3: self.have_z3 = True - self.initZ3() + self.z3solver = z3_search.Z3search( self.total_dims, self.axis_names, self.axis_val_ranges, self.dim_uplimits, self.params['ptdriver'].tinfo.pparam_constraints ) else: self.have_z3 = False - self.solver = None - self.optim = None + self.z3solver = None # complain if both the search time limit and the total number of search runs are undefined if self.time_limit <= 0 and self.total_runs <= 0: @@ -201,10 +202,10 @@ def searchBestCoord(self, startCoord=None): second_worst_perf_cost = perf_costs[len(perf_costs)-2] # calculate centroid - centroid = self.__getCentroid(simplex[:len(simplex)-1]) + centroid = self.getCentroid(simplex[:len(simplex)-1]) # reflection - refl_coords = self.__getReflection(worst_coord, centroid) + refl_coords = self.getReflection(worst_coord, centroid) refl_perf_costs = map(self.getPerfCost, refl_coords) refl_perf_costs = map(lambda x: x[0] if len(x)==1 else sum(x[1:])/(len(x)-1), refl_perf_costs) @@ -226,7 +227,7 @@ def searchBestCoord(self, startCoord=None): elif refl_perf_cost < best_perf_cost: # expansion - exp_coords = self.__getExpansion(refl_coord, centroid) + exp_coords = self.getExpansion(refl_coord, centroid) exp_perf_costs = map(self.getPerfCost, exp_coords) exp_perf_costs = map(lambda x: x[0] if len(x)==1 else sum(x[1:])/(len(x)-1), exp_perf_costs) @@ -248,7 +249,7 @@ def searchBestCoord(self, startCoord=None): elif refl_perf_cost < worst_perf_cost: # outer contraction - cont_coords = self.__getContraction(refl_coord, centroid) + cont_coords = self.getContraction(refl_coord, centroid) cont_perf_costs = map(self.getPerfCost, cont_coords) cont_perf_costs = map(lambda x: x[0] if len(x)==1 else sum(x[1:])/(len(x)-1), cont_perf_costs) @@ -266,7 +267,7 @@ def searchBestCoord(self, startCoord=None): else: # inner contraction - cont_coords = self.__getContraction(worst_coord, centroid) + cont_coords = self.getContraction(worst_coord, centroid) cont_perf_costs = map(self.getPerfCost, cont_coords) cont_perf_costs = map(lambda x: x[0] if len(x)==1 else sum(x[1:])/(len(x)-1), cont_perf_costs) @@ -284,7 +285,7 @@ def searchBestCoord(self, startCoord=None): if next_coord == None and next_perf_cost == None: # shrinkage - simplex = self.__getShrinkage(best_coord, simplex) + simplex = self.getShrinkage(best_coord, simplex) perf_costs = map(self.getPerfCost, simplex) perf_costs = map(lambda x: x[0] if len(x)==1 else sum(x[1:])/(len(x)-1), perf_costs) @@ -447,127 +448,6 @@ def __readAlgoArgs(self): #----------------------------------------------------- - def initZ3(self): - # Initialize the solver itself - self.variables = [] - self.solver = z3.Solver() - self.optim = z3.Optimize() - Globals.z3types = {} - Globals.z3variables = {} - - # find what we have on the axis - self.__addVariableNames( self.axis_names, self.axis_val_ranges ) - self.__addConstraints( self.params['ptdriver'].tinfo.pparam_constraints ) - - # Defines the variables, their type and, for numeric ones, their definition domain - def __addVariableNames( self, names, ranges ): - for idx, name in enumerate( names ): - values = ranges[idx] - if ( [ True, False ] == values ) or ( [ False, True ] == values ): #len( values ) == 2 and ( False in values or True in values ): - Globals.z3variables[name] = z3.Bool( name ) - self.__addDefinitionDomain( name, values ) - else: - try: - toto = int( values[0] ) - Globals.z3variables[name] = z3.Int( name ) - self.__addDefinitionDomain( name, values ) - except ValueError: - # if the parameter is non-numeric - # TODO we can add a case to handle floats - Globals.z3variables[name] = z3.Int( name ) - numvalues = self.__defineNonNumeric( name, values ) - self.__addDefinitionDomain( name, numvalues ) - self.variables.append( name ) # FIXME variables is axis_names - return - - # z3-specific routine: - # Defines a variable's definition domain - def __addDefinitionDomain( self, var, dom ): - # get the variables - for k,v in Globals.z3variables.iteritems( ): - locals()[k] = v - if len( dom ) == 0: - return - definition = z3.Or( [ eval( "(" + var + " == " + str( v ) + ")" ) for v in dom ] ) - # definition = z3.And( [ v >= 0, v < len( dom ) ] ) - - self.solver.add( definition ) - self.optim.add( definition ) - return - - # z3-specific routine: - # Add the constraints - def __addConstraints( self, constraints ): - # get the variables - for k,v in Globals.z3variables.iteritems( ): - locals()[k] = v - for vname, rhs in constraints: - # convert to constraint to prefix syntax - toto = eval( self.__infixToPrefix( rhs ) ) - self.solver.add( toto ) - self.optim.add( toto ) - return - - # z3-specific routine: - # in case a parameter is not numeric (ie, alphanumeric), we cannot store it - # as a regular value with constraints in z3. Hence, put the values in a list and - # use their index in the list instead. - def __defineNonNumeric( self, name, values ): - Globals.z3types[name] = list( values ) - return [ i for i in range( len( values ) ) ] - - # z3-specific routine: - # get the parameter corresponding to a numeric value - def __numericToNonNumeric( self, name, value, num ): - return Globals.z3types[name][num] - - # z3-specific routine: - # get the numeric value corresponding to a parameter - def __nonNumericToNumeric( self, name, value, param ): - return Globals.z3types[name].index( param ) - - # Tests whether a z3 variable is numeric. Returns False for non-numeric ones. - def z3IsNumeric( self, dimensionNumber ): - return not self.axis_names[dimensionNumber] in Globals.z3types - - #----------------------------------------------------- - - # z3-specific routine: - # change constraint from infix notation (used in the input file) to prefix notation (used by z3) - def __infixToPrefix( self, expr ): - if "or" in expr or "and" in expr: - if "and" in expr: - operandsAND = expr.split( "and" ) - return "z3.And(" + ", ".join( [ infixToPrefix( op ) if "or" in op or "and" in op else op for op in operandsAND ] ) + " ) " - elif "or" in expr: - operandsOR = expr.split( "or" ) - return "z3.Or(" + ", ".join( [ infixToPrefix( op ) if "or" in op or "and" in op else op for op in operandsOR ] ) + " ) " - else: - return expr - else: - return expr - - # Add a forbidden point in the solver (and the optimizer) - # Input: a dictionary of performance parameters. - def __addPoint( self, point ): - # get the variables corresponding to the axis names - for name in self.axis_names: - locals()[name] = Globals.z3variables[name] - point2 = {} - # if there is a non-numeric value here, translate it - for idx, name in enumerate( point.keys() ): - # translate non-numeric values - if not self.z3IsNumeric( idx ): # non-numeric points -> coord to value - elem = Globals.z3types[name].index( point[name] ) - else: - elem = point[name] - point2[name] = elem - - # remove this point - for s in [ self.solver, self.optim ]: - s.add( z3.Or( [ locals()[name] != point2[name] for name in self.axis_names ] ) ) - return - #----------------------------------------------------- def __checkSearchSpace(self): @@ -662,7 +542,7 @@ def __initRandomSimplex(self, simplex_records): simplex = [] while True: if self.have_z3: - coord = self.getRandomCoord_z3_distance() + coord = self.z3solver.getRandomCoord_z3_distance() else: coord = self.getRandomCoord() if coord not in simplex: @@ -680,7 +560,7 @@ 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): + def getCentroid(self, coords): # Get a centroid total_coords = len(coords) centroid = coords[0] @@ -690,282 +570,51 @@ def __getCentroid(self, coords): if self.have_z3: # Get the nearest feasible point - point = self.__getNearestFeasible( centroid ) - return self.perfParamTabToCoord( point ) + point = self.z3solver.getNearestFeasible( centroid ) + return self.z3solver.perfParamTabToCoord( point ) else: return centroid #----------------------------------------------------- - - # Returns a *feasible* random point - def getRandomCoord_z3( self ): - if self.solver.check() == z3.unsat: - return None - else: - model = self.solver.model() - return model - - # Getting a random point from an SMT solver is not a trivial question. - # This one gives a somehow random point, but the distribution is not uniform. - # TODO: David's idea involving SAT. - # TODO: non-constrained variables? - def getRandomCoord_z3_distance( self ): - if self.solver.check() == z3.unsat: - return None - else: - # Pick a random point in the solution space - rpc = [] - for i in range( self.total_dims ): - iuplimit = self.dim_uplimits[i] - ipoint = self.getRandomInt(0, iuplimit-1) - rpc.append(ipoint) - - # Get the nearest feasible point - point = self.__getNearestFeasible( rpc ) - return self.perfParamTabToCoord( point ) - - #----------------------------------------------------- - def __getReflection(self, coord, centroid): + def getReflection(self, coord, centroid): '''Return a reflection coordinate''' sub_coord = self.subCoords(centroid, coord) point = map(lambda x: self.addCoords(centroid, self.mulCoords(x, sub_coord)), self.refl_coefs) if self.have_z3: - p = self.__getNearestFeasible( point[0] ) - return [ self.perfParamTabToCoord( p ) ] + p = self.z3solver.getNearestFeasible( point[0] ) + return [ self.z3solver.perfParamTabToCoord( p ) ] else: return point - def __getExpansion(self, coord, centroid): + def getExpansion(self, coord, centroid): '''Return an expansion coordinate''' sub_coord = self.subCoords(coord, centroid) point = map(lambda x: self.addCoords(centroid, self.mulCoords(x, sub_coord)), self.exp_coefs) if self.have_z3: - return [ self.perfParamTabToCoord( self.__getNearestFeasible( point[0] ) )] + return [ self.z3solver.perfParamTabToCoord( self.z3solver.getNearestFeasible( point[0] ) )] else: return point - def __getContraction(self, coord, centroid): + def getContraction(self, coord, centroid): '''Return a contraction coordinate''' sub_coord = self.subCoords(coord, centroid) point = map(lambda x: self.addCoords(centroid, self.mulCoords(x, sub_coord)), self.cont_coefs) if self.have_z3: - return [ self.perfParamTabToCoord( self.__getNearestFeasible( point[0] ) )] + return [ self.z3solver.perfParamTabToCoord( self.z3solver.getNearestFeasible( point[0] ) )] else: return point - def __getShrinkage(self, coord, rest_coords): + def getShrinkage(self, coord, rest_coords): '''Return a shrinkage simplex''' point = map(lambda x: self.addCoords(coord, self.mulCoords(self.shri_coef, self.subCoords(x, coord))), rest_coords) if self.have_z3: - return [ self.perfParamTabToCoord( self.__getNearestFeasible( p ) ) for p in point ] + return [ self.z3solver.perfParamTabToCoord( self.z3solver.getNearestFeasible( p ) ) for p in point ] else: return point - #----------------------------------------------------- - - # Defines the variables, their type and, for numeric ones, their definition domain - def __addVariableNames( self, names, ranges ): - for idx, name in enumerate( names ): - values = ranges[idx] - if ( [ True, False ] == values ) or ( [ False, True ] == values ): #len( values ) == 2 and ( False in values or True in values ): - Globals.z3variables[name] = z3.Bool( name ) - self.__addDefinitionDomain( name, values ) - else: - try: - toto = int( values[0] ) - Globals.z3variables[name] = z3.Int( name ) - self.__addDefinitionDomain( name, values ) - except ValueError: - # if the parameter is non-numeric - # TODO we can add a case to handle floats - Globals.z3variables[name] = z3.Int( name ) - numvalues = self.__defineNonNumeric( name, values ) - self.__addDefinitionDomain( name, numvalues ) - self.variables.append( name ) # FIXME variables is axis_names - return - - # z3-specific routine: - # Defines a variable's definition domain - def __addDefinitionDomain( self, var, dom ): - # get the variables - for k,v in Globals.z3variables.iteritems( ): - locals()[k] = v - if len( dom ) == 0: - return - definition = z3.Or( [ eval( "(" + var + " == " + str( v ) + ")" ) for v in dom ] ) - # definition = z3.And( [ v >= 0, v < len( dom ) ] ) - - self.solver.add( definition ) - self.optim.add( definition ) - return - - # z3-specific routine: - # Add the constraints - def __addConstraints( self, constraints ): - # get the variables - for k,v in Globals.z3variables.iteritems( ): - locals()[k] = v - for vname, rhs in constraints: - # convert to constraint to prefix syntax - toto = eval( self.__infixToPrefix( rhs ) ) - self.solver.add( toto ) - self.optim.add( toto ) - return - - # z3-specific routine: - # in case a parameter is not numeric (ie, alphanumeric), we cannot store it - # as a regular value with constraints in z3. Hence, put the values in a list and - # use their index in the list instead. - def __defineNonNumeric( self, name, values ): - Globals.z3types[name] = list( values ) - return [ i for i in range( len( values ) ) ] - - # z3-specific routine: - # get the parameter corresponding to a numeric value - def __numericToNonNumeric( self, name, value, num ): - return Globals.z3types[name][num] - - # z3-specific routine: - # get the numeric value corresponding to a parameter - def __nonNumericToNumeric( self, name, value, param ): - return Globals.z3types[name].index( param ) - - # z3-specific routine: - # change constraint from infix notation (used in the input file) to prefix notation (used by z3) - def __infixToPrefix( self, expr ): - if "or" in expr or "and" in expr: - if "and" in expr: - operandsAND = expr.split( "and" ) - return "z3.And(" + ", ".join( [ infixToPrefix( op ) if "or" in op or "and" in op else op for op in operandsAND ] ) + " ) " - elif "or" in expr: - operandsOR = expr.split( "or" ) - return "z3.Or(" + ", ".join( [ infixToPrefix( op ) if "or" in op or "and" in op else op for op in operandsOR ] ) + " ) " - else: - return expr - else: - return expr - - # Add a forbidden point in the solver (and the optimizer) - # Input: a dictionary of performance parameters. - def __addPoint( self, point ): - # get the variables corresponding to the axis names - for name in self.axis_names: - locals()[name] = Globals.z3variables[name] - point2 = {} - # if there is a non-numeric value here, translate it - for idx, name in enumerate( point.keys() ): - # translate non-numeric values - if not self.z3IsNumeric( idx ): # non-numeric points -> coord to value - elem = Globals.z3types[name].index( point[name] ) - else: - elem = point[name] - point2[name] = elem - - # remove this point - for s in [ self.solver, self.optim ]: - s.add( z3.Or( [ locals()[name] != point2[name] for name in self.axis_names ] ) ) - - # Tests whether a z3 variable is numeric. Returns False for non-numeric ones. - def z3IsNumeric( self, dimensionNumber ): - return not self.axis_names[dimensionNumber] in Globals.z3types - - def z3abs( self, x ): - return z3.If(x >= 0,x,-x) - - #----------------------------------------------------- - - # Converts a model (returned by z3) into a point. - # Returns a list - def z3ToPoint( self, point ): - res = [] - # get the variables corresponding to the axis names - for idx, i in enumerate( self.axis_names ): - locals()[i] = Globals.z3variables[i] - if i in Globals.z3types: # non-numeric points -> coord to value - value = Globals.z3types[i][point[locals()[i]].as_long()] - elif None == point[locals()[i]]: - info( "no value for %s, take %r (incomplete model)" % ( self.axis_names[idx], self.axis_val_ranges[idx][0] ) ) - value = self.axis_val_ranges[idx][ 0] - elif z3.is_int_value( point[locals()[i]] ): - value = point[locals()[i]].as_long() - elif z3.is_true( point[locals()[i]] ) or z3.is_false( point[locals()[i]] ): - value = z3.is_true( point[locals()[i]] ) - res.append( value ) - return res - - def coordToPerfParams(self, coord): - '''To convert the given coordinate to the corresponding performance parameters''' - # get the performance parameters that correspond the given coordinate - perf_params = {} - for i in range(0, self.total_dims): - ipoint = coord[i] - # If the point is not in the definition domain, take the nearest feasible value - 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] - # return the obtained performance parameters - return perf_params - - def perfParamToCoord( self, params ): - coord = [None]*self.total_dims - for i in range( self.total_dims ): - coord[i] = params[self.axis_names[i]] - if not self.z3IsNumeric( i ): - name = self.axis_names[i] - coord[i] = Globals.z3types[name].index( coord[i] ) - return coord - - def coordToTabOfPerfParams( self, coord ): - params = self.coordToPerfParams( coord ) - perftab = [] - for i, name in enumerate( self.axis_names ): - c = params[name] - if not self.z3IsNumeric( i ): - c = Globals.z3types[name].index( c ) - perftab.append( c ) - return perftab - - def perfParamTabToCoord( self, params ): - coord = [None]*self.total_dims - for i in range( self.total_dims ): - coord[i] = self.axis_val_ranges[i].index( params[i] ) - return coord - - - #----------------------------------------------------- - - # For a given point, returns the nearest feasible point - def __getNearestFeasible(self, coord ): - # get the variables corresponding to the axis names - for i in self.axis_names: - locals()[i] = Globals.z3variables[i] - - # Convert into parameters - rpp = self.coordToPerfParams( coord ) - for i, name in enumerate( self.axis_names ): - if not self.z3IsNumeric( i ): - rpp[name] = Globals.z3types[name].index( rpp[name] ) - - # create a new scope - self.optim.push() - - # Get a possible point that minimizes the 1-norm distance to this random point - # forget the booleans - self.optim.minimize( z3.Sum( [ self.z3abs( locals()[name] - rpp[name] )for name in self.axis_names if not z3.is_bool( locals()[name] ) ] ) ) - if z3.unsat == self.optim.check(): - return None - model = self.optim.model() - - # restore the state (exit the scope) - self.optim.pop() - return self.z3ToPoint( model ) diff --git a/orio/main/tuner/search/simplex/z3_search.py b/orio/main/tuner/search/simplex/z3_search.py new file mode 100644 index 00000000..5666ea64 --- /dev/null +++ b/orio/main/tuner/search/simplex/z3_search.py @@ -0,0 +1,315 @@ +from orio.main.util.globals import * +#import orio.main.tuner.search.search +import z3 + +class Z3search: + + def __init__( self, total_dims, axis_names, axis_val_ranges, dim_uplimits, constraints ): + self.axis_names = axis_names + self.axis_val_ranges = axis_val_ranges + self.constraints = constraints + self.total_dims = total_dims + self.dim_uplimits = dim_uplimits + + # Initialize the solver itself + self.variables = [] + self.solver = z3.Solver() + self.optim = z3.Optimize() + Globals.z3types = {} + Globals.z3variables = {} + + # find what we have on the axis + self.__addVariableNames( self.axis_names, self.axis_val_ranges ) + self.__addConstraints( self.constraints ) + + #----------------------------------------------------- + + # Defines the variables, their type and, for numeric ones, their definition domain + def __addVariableNames( self, names, ranges ): + for idx, name in enumerate( names ): + values = ranges[idx] + if ( [ True, False ] == values ) or ( [ False, True ] == values ): #len( values ) == 2 and ( False in values or True in values ): + Globals.z3variables[name] = z3.Bool( name ) + self.__addDefinitionDomain( name, values ) + else: + try: + toto = int( values[0] ) + Globals.z3variables[name] = z3.Int( name ) + self.__addDefinitionDomain( name, values ) + except ValueError: + # if the parameter is non-numeric + # TODO we can add a case to handle floats + Globals.z3variables[name] = z3.Int( name ) + numvalues = self.__defineNonNumeric( name, values ) + self.__addDefinitionDomain( name, numvalues ) + self.variables.append( name ) # FIXME variables is axis_names + return + + # Defines a variable's definition domain + def __addDefinitionDomain( self, var, dom ): + # get the variables + for k,v in Globals.z3variables.iteritems( ): + locals()[k] = v + if len( dom ) == 0: + return + definition = z3.Or( [ eval( "(" + var + " == " + str( v ) + ")" ) for v in dom ] ) + # definition = z3.And( [ v >= 0, v < len( dom ) ] ) + + self.solver.add( definition ) + self.optim.add( definition ) + return + + # Add the constraints + def __addConstraints( self, constraints ): + # get the variables + for k,v in Globals.z3variables.iteritems( ): + locals()[k] = v + for vname, rhs in constraints: + # convert to constraint to prefix syntax + toto = eval( self.__infixToPrefix( rhs ) ) + self.solver.add( toto ) + self.optim.add( toto ) + return + + # in case a parameter is not numeric (ie, alphanumeric), we cannot store it + # as a regular value with constraints in z3. Hence, put the values in a list and + # use their index in the list instead. + def __defineNonNumeric( self, name, values ): + Globals.z3types[name] = list( values ) + return [ i for i in range( len( values ) ) ] + + # get the parameter corresponding to a numeric value + def __numericToNonNumeric( self, name, value, num ): + return Globals.z3types[name][num] + + # get the numeric value corresponding to a parameter + def __nonNumericToNumeric( self, name, value, param ): + return Globals.z3types[name].index( param ) + + # Tests whether a z3 variable is numeric. Returns False for non-numeric ones. + def z3IsNumeric( self, dimensionNumber ): + return not self.axis_names[dimensionNumber] in Globals.z3types + + def z3abs( self, x ): + return z3.If(x >= 0,x,-x) + + #----------------------------------------------------- + + # change constraint from infix notation (used in the input file) to prefix notation (used by z3) + def __infixToPrefix( self, expr ): + if "or" in expr or "and" in expr: + if "and" in expr: + operandsAND = expr.split( "and" ) + return "z3.And(" + ", ".join( [ infixToPrefix( op ) if "or" in op or "and" in op else op for op in operandsAND ] ) + " ) " + elif "or" in expr: + operandsOR = expr.split( "or" ) + return "z3.Or(" + ", ".join( [ infixToPrefix( op ) if "or" in op or "and" in op else op for op in operandsOR ] ) + " ) " + else: + return expr + else: + return expr + + #----------------------------------------------------- + + # Add the constraints + def __addConstraints( self, constraints ): + # get the variables + for k,v in Globals.z3variables.iteritems( ): + locals()[k] = v + for vname, rhs in constraints: + # convert to constraint to prefix syntax + toto = eval( self.__infixToPrefix( rhs ) ) + self.solver.add( toto ) + self.optim.add( toto ) + return + + # Add a forbidden point in the solver (and the optimizer) + # Input: a dictionary of performance parameters. + def __addPoint( self, point ): + # get the variables corresponding to the axis names + for name in self.axis_names: + locals()[name] = Globals.z3variables[name] + point2 = {} + # if there is a non-numeric value here, translate it + for idx, name in enumerate( point.keys() ): + # translate non-numeric values + if not self.z3IsNumeric( idx ): # non-numeric points -> coord to value + elem = Globals.z3types[name].index( point[name] ) + else: + elem = point[name] + point2[name] = elem + + # remove this point + for s in [ self.solver, self.optim ]: + s.add( z3.Or( [ locals()[name] != point2[name] for name in self.axis_names ] ) ) + return + + #----------------------------------------------------- + + # Returns a *feasible* random point + def getRandomCoord_z3( self ): + if self.solver.check() == z3.unsat: + return None + else: + model = self.solver.model() + return model + + # Getting a random point from an SMT solver is not a trivial question. + # This one gives a somehow random point, but the distribution is not uniform. + # TODO: David's idea involving SAT. + # TODO: non-constrained variables? + def getRandomCoord_z3_distance( self ): + if self.solver.check() == z3.unsat: + return None + else: + # Pick a random point in the solution space + rpc = [] + for i in range( self.total_dims ): + iuplimit = self.dim_uplimits[i] + ipoint = self.getRandomInt(0, iuplimit-1) + rpc.append(ipoint) + + # Get the nearest feasible point + point = self.getNearestFeasible( rpc ) + return self.perfParamTabToCoord( point ) + + # This is copied from search.py. Not exactly the cleanest way to do it, but simpler for the moment. + def getRandomInt(self, lbound, ubound): + '''To generate a random integer N such that lbound <= N <= ubound''' + from random import randint + + if lbound > ubound: + err('orio.main.tuner.search.search internal error: the lower bound of genRandomInt must not be ' + + 'greater than the upper bound') + return randint(lbound, ubound) + + #----------------------------------------------------- + + # For a given point, returns the nearest feasible point + def getNearestFeasible( self, coord ): + # get the variables corresponding to the axis names + for i in self.axis_names: + locals()[i] = Globals.z3variables[i] + + # Convert into parameters + rpp = self.coordToPerfParams( coord ) + for i, name in enumerate( self.axis_names ): + if not self.z3IsNumeric( i ): + rpp[name] = Globals.z3types[name].index( rpp[name] ) + + # create a new scope + self.optim.push() + + # Get a possible point that minimizes the 1-norm distance to this random point + # forget the booleans + self.optim.minimize( z3.Sum( [ self.z3abs( locals()[name] - rpp[name] )for name in self.axis_names if not z3.is_bool( locals()[name] ) ] ) ) + if z3.unsat == self.optim.check(): + return None + model = self.optim.model() + + # restore the state (exit the scope) + self.optim.pop() + return self.z3ToPoint( model ) + + #----------------------------------------------------- + + # Defines the variables, their type and, for numeric ones, their definition domain + def __addVariableNames( self, names, ranges ): + for idx, name in enumerate( names ): + values = ranges[idx] + if ( [ True, False ] == values ) or ( [ False, True ] == values ): #len( values ) == 2 and ( False in values or True in values ): + Globals.z3variables[name] = z3.Bool( name ) + self.__addDefinitionDomain( name, values ) + else: + try: + toto = int( values[0] ) + Globals.z3variables[name] = z3.Int( name ) + self.__addDefinitionDomain( name, values ) + except ValueError: + # if the parameter is non-numeric + # TODO we can add a case to handle floats + Globals.z3variables[name] = z3.Int( name ) + numvalues = self.__defineNonNumeric( name, values ) + self.__addDefinitionDomain( name, numvalues ) + self.variables.append( name ) # FIXME variables is axis_names + return + + # z3-specific routine: + # Defines a variable's definition domain + def __addDefinitionDomain( self, var, dom ): + # get the variables + for k,v in Globals.z3variables.iteritems( ): + locals()[k] = v + if len( dom ) == 0: + return + definition = z3.Or( [ eval( "(" + var + " == " + str( v ) + ")" ) for v in dom ] ) + # definition = z3.And( [ v >= 0, v < len( dom ) ] ) + + self.solver.add( definition ) + self.optim.add( definition ) + return + + #----------------------------------------------------- + + # Converts a model (returned by z3) into a point. + # Returns a list + def z3ToPoint( self, point ): + res = [] + # get the variables corresponding to the axis names + for idx, i in enumerate( self.axis_names ): + locals()[i] = Globals.z3variables[i] + if i in Globals.z3types: # non-numeric points -> coord to value + value = Globals.z3types[i][point[locals()[i]].as_long()] + elif None == point[locals()[i]]: + info( "no value for %s, take %r (incomplete model)" % ( self.axis_names[idx], self.axis_val_ranges[idx][0] ) ) + value = self.axis_val_ranges[idx][ 0] + elif z3.is_int_value( point[locals()[i]] ): + value = point[locals()[i]].as_long() + elif z3.is_true( point[locals()[i]] ) or z3.is_false( point[locals()[i]] ): + value = z3.is_true( point[locals()[i]] ) + res.append( value ) + return res + + def coordToPerfParams(self, coord): + '''To convert the given coordinate to the corresponding performance parameters''' + # get the performance parameters that correspond the given coordinate + perf_params = {} + for i in range(0, self.total_dims): + ipoint = coord[i] + # If the point is not in the definition domain, take the nearest feasible value + 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] + # return the obtained performance parameters + return perf_params + + def perfParamToCoord( self, params ): + coord = [None]*self.total_dims + for i in range( self.total_dims ): + coord[i] = params[self.axis_names[i]] + if not self.z3IsNumeric( i ): + name = self.axis_names[i] + coord[i] = Globals.z3types[name].index( coord[i] ) + return coord + + def coordToTabOfPerfParams( self, coord ): + params = self.coordToPerfParams( coord ) + perftab = [] + for i, name in enumerate( self.axis_names ): + c = params[name] + if not self.z3IsNumeric( i ): + c = Globals.z3types[name].index( c ) + perftab.append( c ) + return perftab + + def perfParamTabToCoord( self, params ): + coord = [None]*self.total_dims + for i in range( self.total_dims ): + coord[i] = self.axis_val_ranges[i].index( params[i] ) + return coord + + From a32128e261c539b73cf721ee56a0d5a34a815a9c Mon Sep 17 00:00:00 2001 From: Camille Coti Date: Tue, 22 Dec 2020 10:13:57 -0800 Subject: [PATCH 04/11] Put the z3-related routines in a separate class in a separate file --- .../tuner/search/randomsimple/randomsimple.py | 171 +--------- .../tuner/search/randomsimple/z3_search.py | 315 ++++++++++++++++++ 2 files changed, 324 insertions(+), 162 deletions(-) create mode 100644 orio/main/tuner/search/randomsimple/z3_search.py diff --git a/orio/main/tuner/search/randomsimple/randomsimple.py b/orio/main/tuner/search/randomsimple/randomsimple.py index d76c1f7a..8309d71b 100644 --- a/orio/main/tuner/search/randomsimple/randomsimple.py +++ b/orio/main/tuner/search/randomsimple/randomsimple.py @@ -9,6 +9,7 @@ try: import z3 _have_z3 = True + import z3_search except Exception as e: _have_z3 = False @@ -21,11 +22,10 @@ def __init__(self, params): self.__readAlgoArgs() if _have_z3: self.have_z3 = True - self.initZ3() + self.z3solver = z3_search.Z3search( self.total_dims, self.axis_names, self.axis_val_ranges, self.dim_uplimits, self.params['ptdriver'].tinfo.pparam_constraints ) else: self.have_z3 = False - self.solver = None - self.optim = None + self.z3Solver = None if self.time_limit <= 0 and self.total_runs <= 0: err(('orio.main.tuner.search.randomsimple.randomsimple: %s search requires either (both) the search time limit or (and) the ' + @@ -68,7 +68,7 @@ def searchBestCoord(self, startCoord=None): visited.append( coord ) else: point = self.coordToPerfParams( coord ) - self.__addPoint( point ) + self.z3solver.addPoint( point ) search_time = time.time() - start_time return bestcoord, bestperfcost, search_time, runs @@ -90,169 +90,16 @@ def __readAlgoArgs(self): err('orio.main.tuner.search.randomsimple: unrecognized %s algorithm-specific argument: "%s"' % (self.__class__.__name__, vname)) - def initZ3(self): - # Initialize the solver itself - self.variables = [] - self.solver = z3.Solver() - self.optim = z3.Optimize() - Globals.z3types = {} - Globals.z3variables = {} - - # find what we have on the axis - self.__addVariableNames( self.axis_names, self.axis_val_ranges ) - self.__addConstraints( self.params['ptdriver'].tinfo.pparam_constraints ) - # In this function, either z3 finds a feasible point, or we ask the default function draw one. def __getRandomPoint(self): if not self.have_z3: - self.getRandomCoord() + coord = self.getRandomCoord() else: # if I have z3, get a *feasible* random coord - model = self._getRandomCoordZ3() - #model = self._getRandomCoordZ3Distance() - point = self._z3ToPoint( model ) - coord = self._perfParamTabToCoord( point ) + coord = self.z3solver.getRandomCoord_z3_distance() + # If I could not find any feasible point, just return a random point if None != coord: - return coord - - # Defines the variables, their type and, for numeric ones, their definition domain - def __addVariableNames( self, names, ranges ): - for idx, name in enumerate( names ): - values = ranges[idx] - if ( [ True, False ] == values ) or ( [ False, True ] == values ): #len( values ) == 2 and ( False in values or True in values ): - Globals.z3variables[name] = z3.Bool( name ) - self.__addDefinitionDomain( name, values ) - else: - try: - toto = int( values[0] ) - Globals.z3variables[name] = z3.Int( name ) - self.__addDefinitionDomain( name, values ) - except ValueError: - # if the parameter is non-numeric - # TODO we can add a case to handle floats - Globals.z3variables[name] = z3.Int( name ) - numvalues = self.__defineNonNumeric( name, values ) - self.__addDefinitionDomain( name, numvalues ) - self.variables.append( name ) # FIXME variables is axis_names - return - - # z3-specific routine: - # Defines a variable's definition domain - def __addDefinitionDomain( self, var, dom ): - # get the variables - for k,v in Globals.z3variables.iteritems( ): - locals()[k] = v - if len( dom ) == 0: - return - definition = z3.Or( [ eval( "(" + var + " == " + str( v ) + ")" ) for v in dom ] ) - # definition = z3.And( [ v >= 0, v < len( dom ) ] ) - - self.solver.add( definition ) - self.optim.add( definition ) - return - - # z3-specific routine: - # Add the constraints - def __addConstraints( self, constraints ): - # get the variables - for k,v in Globals.z3variables.iteritems( ): - locals()[k] = v - for vname, rhs in constraints: - # convert to constraint to prefix syntax - toto = eval( self.__infixToPrefix( rhs ) ) - self.solver.add( toto ) - self.optim.add( toto ) - return - - # z3-specific routine: - # in case a parameter is not numeric (ie, alphanumeric), we cannot store it - # as a regular value with constraints in z3. Hence, put the values in a list and - # use their index in the list instead. - def __defineNonNumeric( self, name, values ): - Globals.z3types[name] = list( values ) - return [ i for i in range( len( values ) ) ] - - # z3-specific routine: - # get the parameter corresponding to a numeric value - def __numericToNonNumeric( self, name, value, num ): - return Globals.z3types[name][num] - - # z3-specific routine: - # get the numeric value corresponding to a parameter - def __nonNumericToNumeric( self, name, value, param ): - return Globals.z3types[name].index( param ) - - # z3-specific routine: - # change constraint from infix notation (used in the input file) to prefix notation (used by z3) - def __infixToPrefix( self, expr ): - if "or" in expr or "and" in expr: - if "and" in expr: - operandsAND = expr.split( "and" ) - return "z3.And(" + ", ".join( [ infixToPrefix( op ) if "or" in op or "and" in op else op for op in operandsAND ] ) + " ) " - elif "or" in expr: - operandsOR = expr.split( "or" ) - return "z3.Or(" + ", ".join( [ infixToPrefix( op ) if "or" in op or "and" in op else op for op in operandsOR ] ) + " ) " - else: - return expr - else: - return expr - - # Add a forbidden point in the solver (and the optimizer) - # Input: a dictionary of performance parameters. - def __addPoint( self, point ): - # get the variables corresponding to the axis names - for name in self.axis_names: - locals()[name] = Globals.z3variables[name] - point2 = {} - # if there is a non-numeric value here, translate it - for idx, name in enumerate( point.keys() ): - # translate non-numeric values - if not self.z3IsNumeric( idx ): # non-numeric points -> coord to value - elem = Globals.z3types[name].index( point[name] ) - else: - elem = point[name] - point2[name] = elem - - # remove this point - for s in [ self.solver, self.optim ]: - s.add( z3.Or( [ locals()[name] != point2[name] for name in self.axis_names ] ) ) - - # Tests whether a z3 variable is numeric. Returns False for non-numeric ones. - def z3IsNumeric( self, dimensionNumber ): - return not self.axis_names[dimensionNumber] in Globals.z3types - - # Returns a *feasible* random point - def _getRandomCoordZ3( self ): - if self.solver.check() == z3.unsat: - return None - else: - model = self.solver.model() - return model - - # Converts a model (returned by z3) into a point. - # Returns a list - def z3ToPoint( self, point ): - res = [] - # get the variables corresponding to the axis names - for idx, i in enumerate( self.axis_names ): - locals()[i] = Globals.z3variables[i] - if i in Globals.z3types: # non-numeric points -> coord to value - value = Globals.z3types[i][point[locals()[i]].as_long()] - elif None == point[locals()[i]]: - info( "no value for %s, take %r (incomplete model)" % ( self.axis_names[idx], self.axis_val_ranges[idx][0] ) ) - value = self.axis_val_ranges[idx][ 0] - elif z3.is_int_value( point[locals()[i]] ): - value = point[locals()[i]].as_long() - elif z3.is_true( point[locals()[i]] ) or z3.is_false( point[locals()[i]] ): - value = z3.is_true( point[locals()[i]] ) - res.append( value ) - return res - - def perfParamTabToCoord( self, params ): - coord = [None]*self.total_dims - for i in range( self.total_dims ): - coord[i] = self.axis_val_ranges[i].index( params[i] ) + coord = self.getRandomCoord() return coord - - + diff --git a/orio/main/tuner/search/randomsimple/z3_search.py b/orio/main/tuner/search/randomsimple/z3_search.py new file mode 100644 index 00000000..36daac47 --- /dev/null +++ b/orio/main/tuner/search/randomsimple/z3_search.py @@ -0,0 +1,315 @@ +from orio.main.util.globals import * +#import orio.main.tuner.search.search +import z3 + +class Z3search: + + def __init__( self, total_dims, axis_names, axis_val_ranges, dim_uplimits, constraints ): + self.axis_names = axis_names + self.axis_val_ranges = axis_val_ranges + self.constraints = constraints + self.total_dims = total_dims + self.dim_uplimits = dim_uplimits + + # Initialize the solver itself + self.variables = [] + self.solver = z3.Solver() + self.optim = z3.Optimize() + Globals.z3types = {} + Globals.z3variables = {} + + # find what we have on the axis + self.__addVariableNames( self.axis_names, self.axis_val_ranges ) + self.__addConstraints( self.constraints ) + + #----------------------------------------------------- + + # Defines the variables, their type and, for numeric ones, their definition domain + def __addVariableNames( self, names, ranges ): + for idx, name in enumerate( names ): + values = ranges[idx] + if ( [ True, False ] == values ) or ( [ False, True ] == values ): #len( values ) == 2 and ( False in values or True in values ): + Globals.z3variables[name] = z3.Bool( name ) + self.__addDefinitionDomain( name, values ) + else: + try: + toto = int( values[0] ) + Globals.z3variables[name] = z3.Int( name ) + self.__addDefinitionDomain( name, values ) + except ValueError: + # if the parameter is non-numeric + # TODO we can add a case to handle floats + Globals.z3variables[name] = z3.Int( name ) + numvalues = self.__defineNonNumeric( name, values ) + self.__addDefinitionDomain( name, numvalues ) + self.variables.append( name ) # FIXME variables is axis_names + return + + # Defines a variable's definition domain + def __addDefinitionDomain( self, var, dom ): + # get the variables + for k,v in Globals.z3variables.iteritems( ): + locals()[k] = v + if len( dom ) == 0: + return + definition = z3.Or( [ eval( "(" + var + " == " + str( v ) + ")" ) for v in dom ] ) + # definition = z3.And( [ v >= 0, v < len( dom ) ] ) + + self.solver.add( definition ) + self.optim.add( definition ) + return + + # Add the constraints + def __addConstraints( self, constraints ): + # get the variables + for k,v in Globals.z3variables.iteritems( ): + locals()[k] = v + for vname, rhs in constraints: + # convert to constraint to prefix syntax + toto = eval( self.__infixToPrefix( rhs ) ) + self.solver.add( toto ) + self.optim.add( toto ) + return + + # in case a parameter is not numeric (ie, alphanumeric), we cannot store it + # as a regular value with constraints in z3. Hence, put the values in a list and + # use their index in the list instead. + def __defineNonNumeric( self, name, values ): + Globals.z3types[name] = list( values ) + return [ i for i in range( len( values ) ) ] + + # get the parameter corresponding to a numeric value + def __numericToNonNumeric( self, name, value, num ): + return Globals.z3types[name][num] + + # get the numeric value corresponding to a parameter + def __nonNumericToNumeric( self, name, value, param ): + return Globals.z3types[name].index( param ) + + # Tests whether a z3 variable is numeric. Returns False for non-numeric ones. + def z3IsNumeric( self, dimensionNumber ): + return not self.axis_names[dimensionNumber] in Globals.z3types + + def z3abs( self, x ): + return z3.If(x >= 0,x,-x) + + #----------------------------------------------------- + + # change constraint from infix notation (used in the input file) to prefix notation (used by z3) + def __infixToPrefix( self, expr ): + if "or" in expr or "and" in expr: + if "and" in expr: + operandsAND = expr.split( "and" ) + return "z3.And(" + ", ".join( [ infixToPrefix( op ) if "or" in op or "and" in op else op for op in operandsAND ] ) + " ) " + elif "or" in expr: + operandsOR = expr.split( "or" ) + return "z3.Or(" + ", ".join( [ infixToPrefix( op ) if "or" in op or "and" in op else op for op in operandsOR ] ) + " ) " + else: + return expr + else: + return expr + + #----------------------------------------------------- + + # Add the constraints + def __addConstraints( self, constraints ): + # get the variables + for k,v in Globals.z3variables.iteritems( ): + locals()[k] = v + for vname, rhs in constraints: + # convert to constraint to prefix syntax + toto = eval( self.__infixToPrefix( rhs ) ) + self.solver.add( toto ) + self.optim.add( toto ) + return + + # Add a forbidden point in the solver (and the optimizer) + # Input: a dictionary of performance parameters. + def addPoint( self, point ): + # get the variables corresponding to the axis names + for name in self.axis_names: + locals()[name] = Globals.z3variables[name] + point2 = {} + # if there is a non-numeric value here, translate it + for idx, name in enumerate( point.keys() ): + # translate non-numeric values + if not self.z3IsNumeric( idx ): # non-numeric points -> coord to value + elem = Globals.z3types[name].index( point[name] ) + else: + elem = point[name] + point2[name] = elem + + # remove this point + for s in [ self.solver, self.optim ]: + s.add( z3.Or( [ locals()[name] != point2[name] for name in self.axis_names ] ) ) + return + + #----------------------------------------------------- + + # Returns a *feasible* random point + def getRandomCoord_z3( self ): + if self.solver.check() == z3.unsat: + return None + else: + model = self.solver.model() + return model + + # Getting a random point from an SMT solver is not a trivial question. + # This one gives a somehow random point, but the distribution is not uniform. + # TODO: David's idea involving SAT. + # TODO: non-constrained variables? + def getRandomCoord_z3_distance( self ): + if self.solver.check() == z3.unsat: + return None + else: + # Pick a random point in the solution space + rpc = [] + for i in range( self.total_dims ): + iuplimit = self.dim_uplimits[i] + ipoint = self.getRandomInt(0, iuplimit-1) + rpc.append(ipoint) + + # Get the nearest feasible point + point = self.getNearestFeasible( rpc ) + return self.perfParamTabToCoord( point ) + + # This is copied from search.py. Not exactly the cleanest way to do it, but simpler for the moment. + def getRandomInt(self, lbound, ubound): + '''To generate a random integer N such that lbound <= N <= ubound''' + from random import randint + + if lbound > ubound: + err('orio.main.tuner.search.search internal error: the lower bound of genRandomInt must not be ' + + 'greater than the upper bound') + return randint(lbound, ubound) + + #----------------------------------------------------- + + # For a given point, returns the nearest feasible point + def getNearestFeasible( self, coord ): + # get the variables corresponding to the axis names + for i in self.axis_names: + locals()[i] = Globals.z3variables[i] + + # Convert into parameters + rpp = self.coordToPerfParams( coord ) + for i, name in enumerate( self.axis_names ): + if not self.z3IsNumeric( i ): + rpp[name] = Globals.z3types[name].index( rpp[name] ) + + # create a new scope + self.optim.push() + + # Get a possible point that minimizes the 1-norm distance to this random point + # forget the booleans + self.optim.minimize( z3.Sum( [ self.z3abs( locals()[name] - rpp[name] )for name in self.axis_names if not z3.is_bool( locals()[name] ) ] ) ) + if z3.unsat == self.optim.check(): + return None + model = self.optim.model() + + # restore the state (exit the scope) + self.optim.pop() + return self.z3ToPoint( model ) + + #----------------------------------------------------- + + # Defines the variables, their type and, for numeric ones, their definition domain + def __addVariableNames( self, names, ranges ): + for idx, name in enumerate( names ): + values = ranges[idx] + if ( [ True, False ] == values ) or ( [ False, True ] == values ): #len( values ) == 2 and ( False in values or True in values ): + Globals.z3variables[name] = z3.Bool( name ) + self.__addDefinitionDomain( name, values ) + else: + try: + toto = int( values[0] ) + Globals.z3variables[name] = z3.Int( name ) + self.__addDefinitionDomain( name, values ) + except ValueError: + # if the parameter is non-numeric + # TODO we can add a case to handle floats + Globals.z3variables[name] = z3.Int( name ) + numvalues = self.__defineNonNumeric( name, values ) + self.__addDefinitionDomain( name, numvalues ) + self.variables.append( name ) # FIXME variables is axis_names + return + + # z3-specific routine: + # Defines a variable's definition domain + def __addDefinitionDomain( self, var, dom ): + # get the variables + for k,v in Globals.z3variables.iteritems( ): + locals()[k] = v + if len( dom ) == 0: + return + definition = z3.Or( [ eval( "(" + var + " == " + str( v ) + ")" ) for v in dom ] ) + # definition = z3.And( [ v >= 0, v < len( dom ) ] ) + + self.solver.add( definition ) + self.optim.add( definition ) + return + + #----------------------------------------------------- + + # Converts a model (returned by z3) into a point. + # Returns a list + def z3ToPoint( self, point ): + res = [] + # get the variables corresponding to the axis names + for idx, i in enumerate( self.axis_names ): + locals()[i] = Globals.z3variables[i] + if i in Globals.z3types: # non-numeric points -> coord to value + value = Globals.z3types[i][point[locals()[i]].as_long()] + elif None == point[locals()[i]]: + info( "no value for %s, take %r (incomplete model)" % ( self.axis_names[idx], self.axis_val_ranges[idx][0] ) ) + value = self.axis_val_ranges[idx][ 0] + elif z3.is_int_value( point[locals()[i]] ): + value = point[locals()[i]].as_long() + elif z3.is_true( point[locals()[i]] ) or z3.is_false( point[locals()[i]] ): + value = z3.is_true( point[locals()[i]] ) + res.append( value ) + return res + + def coordToPerfParams(self, coord): + '''To convert the given coordinate to the corresponding performance parameters''' + # get the performance parameters that correspond the given coordinate + perf_params = {} + for i in range(0, self.total_dims): + ipoint = coord[i] + # If the point is not in the definition domain, take the nearest feasible value + 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] + # return the obtained performance parameters + return perf_params + + def perfParamToCoord( self, params ): + coord = [None]*self.total_dims + for i in range( self.total_dims ): + coord[i] = params[self.axis_names[i]] + if not self.z3IsNumeric( i ): + name = self.axis_names[i] + coord[i] = Globals.z3types[name].index( coord[i] ) + return coord + + def coordToTabOfPerfParams( self, coord ): + params = self.coordToPerfParams( coord ) + perftab = [] + for i, name in enumerate( self.axis_names ): + c = params[name] + if not self.z3IsNumeric( i ): + c = Globals.z3types[name].index( c ) + perftab.append( c ) + return perftab + + def perfParamTabToCoord( self, params ): + coord = [None]*self.total_dims + for i in range( self.total_dims ): + coord[i] = self.axis_val_ranges[i].index( params[i] ) + return coord + + From dacee8d0e4c4af2f9ea2fb37243b17b3d5665585 Mon Sep 17 00:00:00 2001 From: Camille Coti Date: Tue, 22 Dec 2020 10:18:59 -0800 Subject: [PATCH 05/11] Renamed a function to make it callable from anywhere --- orio/main/tuner/search/simplex/z3_search.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/orio/main/tuner/search/simplex/z3_search.py b/orio/main/tuner/search/simplex/z3_search.py index 5666ea64..36daac47 100644 --- a/orio/main/tuner/search/simplex/z3_search.py +++ b/orio/main/tuner/search/simplex/z3_search.py @@ -125,7 +125,7 @@ def __addConstraints( self, constraints ): # Add a forbidden point in the solver (and the optimizer) # Input: a dictionary of performance parameters. - def __addPoint( self, point ): + def addPoint( self, point ): # get the variables corresponding to the axis names for name in self.axis_names: locals()[name] = Globals.z3variables[name] From e4d98c17513fe413b5dd330b9ac846f0d1abf78e Mon Sep 17 00:00:00 2001 From: Camille Coti Date: Tue, 22 Dec 2020 18:29:15 -0800 Subject: [PATCH 06/11] Point search using a constraint solver (z3) --- orio/main/tuner/search/search.py | 48 +++- orio/main/tuner/search/simplex/simplex.py | 67 ++--- orio/main/tuner/search/z3_search.py | 305 ++++++++++++++++++++++ 3 files changed, 379 insertions(+), 41 deletions(-) create mode 100644 orio/main/tuner/search/z3_search.py diff --git a/orio/main/tuner/search/search.py b/orio/main/tuner/search/search.py index e3ead81f..0ed908f6 100644 --- a/orio/main/tuner/search/search.py +++ b/orio/main/tuner/search/search.py @@ -4,7 +4,6 @@ import sys, math, time from orio.main.util.globals import * - class Search: '''The search engine used to explore the search space ''' @@ -74,12 +73,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): @@ -154,15 +168,25 @@ def search(self, startCoord=None): #---------------------------------------------------------- def coordToPerfParams(self, coord): - '''To convert the given coordinate to the corresponding performance parameters''' + """ + Convert coordinate to the corresponding performance parameters + :param coord The coordinate (integer array) + :return dictionary with parameter name-value pairs + """ # get the performance parameters that correspond the given coordinate 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 + 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] - # return the obtained performance parameters return perf_params #---------------------------------------------------------- @@ -461,7 +485,11 @@ 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 ) + return self.z3solver.perfParamTabToCoord( point ) + else: + return random_coord def getInitCoord(self): @@ -472,9 +500,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 #---------------------------------------------------------- diff --git a/orio/main/tuner/search/simplex/simplex.py b/orio/main/tuner/search/simplex/simplex.py index e6cedf23..355ca46d 100644 --- a/orio/main/tuner/search/simplex/simplex.py +++ b/orio/main/tuner/search/simplex/simplex.py @@ -202,10 +202,10 @@ def searchBestCoord(self, startCoord=None): second_worst_perf_cost = perf_costs[len(perf_costs)-2] # calculate centroid - centroid = self.getCentroid(simplex[:len(simplex)-1]) + centroid = self.__getCentroid(simplex[:len(simplex)-1]) # reflection - refl_coords = self.getReflection(worst_coord, centroid) + refl_coords = self.__getReflection(worst_coord, centroid) refl_perf_costs = map(self.getPerfCost, refl_coords) refl_perf_costs = map(lambda x: x[0] if len(x)==1 else sum(x[1:])/(len(x)-1), refl_perf_costs) @@ -227,7 +227,7 @@ def searchBestCoord(self, startCoord=None): elif refl_perf_cost < best_perf_cost: # expansion - exp_coords = self.getExpansion(refl_coord, centroid) + exp_coords = self.__getExpansion(refl_coord, centroid) exp_perf_costs = map(self.getPerfCost, exp_coords) exp_perf_costs = map(lambda x: x[0] if len(x)==1 else sum(x[1:])/(len(x)-1), exp_perf_costs) @@ -249,7 +249,7 @@ def searchBestCoord(self, startCoord=None): elif refl_perf_cost < worst_perf_cost: # outer contraction - cont_coords = self.getContraction(refl_coord, centroid) + cont_coords = self.__getContraction(refl_coord, centroid) cont_perf_costs = map(self.getPerfCost, cont_coords) cont_perf_costs = map(lambda x: x[0] if len(x)==1 else sum(x[1:])/(len(x)-1), cont_perf_costs) @@ -267,7 +267,7 @@ def searchBestCoord(self, startCoord=None): else: # inner contraction - cont_coords = self.getContraction(worst_coord, centroid) + cont_coords = self.__getContraction(worst_coord, centroid) cont_perf_costs = map(self.getPerfCost, cont_coords) cont_perf_costs = map(lambda x: x[0] if len(x)==1 else sum(x[1:])/(len(x)-1), cont_perf_costs) @@ -285,7 +285,7 @@ def searchBestCoord(self, startCoord=None): if next_coord == None and next_perf_cost == None: # shrinkage - simplex = self.getShrinkage(best_coord, simplex) + simplex = self.__getShrinkage(best_coord, simplex) perf_costs = map(self.getPerfCost, simplex) perf_costs = map(lambda x: x[0] if len(x)==1 else sum(x[1:])/(len(x)-1), perf_costs) @@ -560,7 +560,7 @@ 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): + def __getCentroid(self, coords): # Get a centroid total_coords = len(coords) centroid = coords[0] @@ -568,7 +568,7 @@ def getCentroid(self, coords): centroid = self.addCoords(centroid, c) centroid = self.mulCoords((1.0/total_coords), centroid) - if self.have_z3: + if self.use_z3: # Get the nearest feasible point point = self.z3solver.getNearestFeasible( centroid ) return self.z3solver.perfParamTabToCoord( point ) @@ -577,44 +577,47 @@ def getCentroid(self, coords): #----------------------------------------------------- - def getReflection(self, coord, centroid): + def __getReflection(self, coord, centroid): '''Return a reflection coordinate''' sub_coord = self.subCoords(centroid, coord) - point = map(lambda x: self.addCoords(centroid, self.mulCoords(x, sub_coord)), - self.refl_coefs) - if self.have_z3: - p = self.z3solver.getNearestFeasible( point[0] ) - return [ self.z3solver.perfParamTabToCoord( p ) ] - else: + 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 point - - def getExpansion(self, coord, centroid): + + def __getExpansion(self, coord, centroid): '''Return an expansion coordinate''' sub_coord = self.subCoords(coord, centroid) point = map(lambda x: self.addCoords(centroid, self.mulCoords(x, sub_coord)), - self.exp_coefs) - if self.have_z3: - return [ self.z3solver.perfParamTabToCoord( self.z3solver.getNearestFeasible( point[0] ) )] - else: + 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 point - def getContraction(self, coord, centroid): + def __getContraction(self, coord, centroid): '''Return a contraction coordinate''' sub_coord = self.subCoords(coord, centroid) point = map(lambda x: self.addCoords(centroid, self.mulCoords(x, sub_coord)), - self.cont_coefs) - if self.have_z3: - return [ self.z3solver.perfParamTabToCoord( self.z3solver.getNearestFeasible( point[0] ) )] - else: + 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 point - def getShrinkage(self, coord, rest_coords): + def __getShrinkage(self, coord, rest_coords): '''Return a shrinkage simplex''' point = map(lambda x: self.addCoords(coord, self.mulCoords(self.shri_coef, - self.subCoords(x, coord))), - rest_coords) - if self.have_z3: + 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: + else: return point - + diff --git a/orio/main/tuner/search/z3_search.py b/orio/main/tuner/search/z3_search.py new file mode 100644 index 00000000..9bf8a741 --- /dev/null +++ b/orio/main/tuner/search/z3_search.py @@ -0,0 +1,305 @@ +from orio.main.util.globals import * + +try: + import z3 + Globals.have_z3 = True +except Exception as e: + Globals.have_z3 = False + raise ImportError( "Could not load z3. Will not be using it." ) +# raise ImportError() # Silent + +class Z3search: + + def __init__( self, total_dims, axis_names, axis_val_ranges, dim_uplimits, constraints, s ): + self.axis_names = axis_names + self.axis_val_ranges = axis_val_ranges + self.constraints = constraints + self.total_dims = total_dims + self.dim_uplimits = dim_uplimits + self.search = s + + # Initialize the solver itself + self.variables = [] + self.solver = z3.Solver() + self.optim = z3.Optimize() + Globals.z3types = {} + Globals.z3variables = {} + + # find what we have on the axis + self.__addVariableNames( self.axis_names, self.axis_val_ranges ) + self.__addConstraints( self.constraints ) + + #----------------------------------------------------- + + # Defines the variables, their type and, for numeric ones, their definition domain + def __addVariableNames( self, names, ranges ): + for idx, name in enumerate( names ): + values = ranges[idx] + if ( [ True, False ] == values ) or ( [ False, True ] == values ): #len( values ) == 2 and ( False in values or True in values ): + Globals.z3variables[name] = z3.Bool( name ) + self.__addDefinitionDomain( name, values ) + else: + try: + toto = int( values[0] ) + Globals.z3variables[name] = z3.Int( name ) + self.__addDefinitionDomain( name, values ) + except ValueError: + # if the parameter is non-numeric + # TODO we can add a case to handle floats + Globals.z3variables[name] = z3.Int( name ) + numvalues = self.__defineNonNumeric( name, values ) + self.__addDefinitionDomain( name, numvalues ) + self.variables.append( name ) # FIXME variables is axis_names + return + + # Defines a variable's definition domain + def __addDefinitionDomain( self, var, dom ): + # get the variables + for k,v in Globals.z3variables.iteritems( ): + locals()[k] = v + if len( dom ) == 0: + return + definition = z3.Or( [ eval( "(" + var + " == " + str( v ) + ")" ) for v in dom ] ) + # definition = z3.And( [ v >= 0, v < len( dom ) ] ) + + self.solver.add( definition ) + self.optim.add( definition ) + return + + # Add the constraints + def __addConstraints( self, constraints ): + # get the variables + for k,v in Globals.z3variables.iteritems( ): + locals()[k] = v + for vname, rhs in constraints: + # convert to constraint to prefix syntax + toto = eval( self.__infixToPrefix( rhs ) ) + self.solver.add( toto ) + self.optim.add( toto ) + return + + # in case a parameter is not numeric (ie, alphanumeric), we cannot store it + # as a regular value with constraints in z3. Hence, put the values in a list and + # use their index in the list instead. + def __defineNonNumeric( self, name, values ): + Globals.z3types[name] = list( values ) + return [ i for i in range( len( values ) ) ] + + # get the parameter corresponding to a numeric value + def __numericToNonNumeric( self, name, value, num ): + return Globals.z3types[name][num] + + # get the numeric value corresponding to a parameter + def __nonNumericToNumeric( self, name, value, param ): + return Globals.z3types[name].index( param ) + + # Tests whether a z3 variable is numeric. Returns False for non-numeric ones. + def z3IsNumeric( self, dimensionNumber ): + return not self.axis_names[dimensionNumber] in Globals.z3types + + def z3abs( self, x ): + return z3.If(x >= 0,x,-x) + + #----------------------------------------------------- + + # change constraint from infix notation (used in the input file) to prefix notation (used by z3) + def __infixToPrefix( self, expr ): + if "or" in expr or "and" in expr: + if "and" in expr: + operandsAND = expr.split( "and" ) + return "z3.And(" + ", ".join( [ infixToPrefix( op ) if "or" in op or "and" in op else op for op in operandsAND ] ) + " ) " + elif "or" in expr: + operandsOR = expr.split( "or" ) + return "z3.Or(" + ", ".join( [ infixToPrefix( op ) if "or" in op or "and" in op else op for op in operandsOR ] ) + " ) " + else: + return expr + else: + return expr + + #----------------------------------------------------- + + # Add the constraints + def __addConstraints( self, constraints ): + # get the variables + for k,v in Globals.z3variables.iteritems( ): + locals()[k] = v + for vname, rhs in constraints: + # convert to constraint to prefix syntax + toto = eval( self.__infixToPrefix( rhs ) ) + self.solver.add( toto ) + self.optim.add( toto ) + return + + # Add a forbidden point in the solver (and the optimizer) + # Input: a dictionary of performance parameters. + def addPoint( self, point ): + # get the variables corresponding to the axis names + for name in self.axis_names: + locals()[name] = Globals.z3variables[name] + point2 = {} + # if there is a non-numeric value here, translate it + for idx, name in enumerate( point.keys() ): + # translate non-numeric values + if not self.z3IsNumeric( idx ): # non-numeric points -> coord to value + elem = Globals.z3types[name].index( point[name] ) + else: + elem = point[name] + point2[name] = elem + + # remove this point + for s in [ self.solver, self.optim ]: + s.add( z3.Or( [ locals()[name] != point2[name] for name in self.axis_names ] ) ) + return + + #----------------------------------------------------- + + # Returns a *feasible* random point + def getRandomCoord_z3( self ): + if self.solver.check() == z3.unsat: + return None + else: + model = self.solver.model() + return model + + # Getting a random point from an SMT solver is not a trivial question. + # This one gives a somehow random point, but the distribution is not uniform. + # TODO: David's idea involving SAT. + # TODO: non-constrained variables? + def getRandomCoord_z3_distance( self ): + if self.solver.check() == z3.unsat: + return None + else: + # Pick a random point in the solution space + rpc = [] + for i in range( self.total_dims ): + iuplimit = self.dim_uplimits[i] + ipoint = self.getRandomInt(0, iuplimit-1) + rpc.append(ipoint) + + # Get the nearest feasible point + point = self.getNearestFeasible( rpc ) + return self.perfParamTabToCoord( point ) + + # This is copied from search.py. Not exactly the cleanest way to do it, but simpler for the moment. + def getRandomInt(self, lbound, ubound): + '''To generate a random integer N such that lbound <= N <= ubound''' + from random import randint + + if lbound > ubound: + err('orio.main.tuner.search.search internal error: the lower bound of genRandomInt must not be ' + + 'greater than the upper bound') + return randint(lbound, ubound) + + #----------------------------------------------------- + + # For a given point, returns the nearest feasible point + def getNearestFeasible( self, coord ): + # get the variables corresponding to the axis names + for i in self.axis_names: + locals()[i] = Globals.z3variables[i] + + # Convert into parameters + rpp = self.search.coordToPerfParams( coord ) + for i, name in enumerate( self.axis_names ): + if not self.z3IsNumeric( i ): + rpp[name] = Globals.z3types[name].index( rpp[name] ) + + # create a new scope + self.optim.push() + + # Get a possible point that minimizes the 1-norm distance to this random point + # forget the booleans + self.optim.minimize( z3.Sum( [ self.z3abs( locals()[name] - rpp[name] )for name in self.axis_names if not z3.is_bool( locals()[name] ) ] ) ) + if z3.unsat == self.optim.check(): + return None + model = self.optim.model() + + # restore the state (exit the scope) + self.optim.pop() + return self.z3ToPoint( model ) + + #----------------------------------------------------- + + # Defines the variables, their type and, for numeric ones, their definition domain + def __addVariableNames( self, names, ranges ): + for idx, name in enumerate( names ): + values = ranges[idx] + if ( [ True, False ] == values ) or ( [ False, True ] == values ): #len( values ) == 2 and ( False in values or True in values ): + Globals.z3variables[name] = z3.Bool( name ) + self.__addDefinitionDomain( name, values ) + else: + try: + toto = int( values[0] ) + Globals.z3variables[name] = z3.Int( name ) + self.__addDefinitionDomain( name, values ) + except ValueError: + # if the parameter is non-numeric + # TODO we can add a case to handle floats + Globals.z3variables[name] = z3.Int( name ) + numvalues = self.__defineNonNumeric( name, values ) + self.__addDefinitionDomain( name, numvalues ) + self.variables.append( name ) # FIXME variables is axis_names + return + + # z3-specific routine: + # Defines a variable's definition domain + def __addDefinitionDomain( self, var, dom ): + # get the variables + for k,v in Globals.z3variables.iteritems( ): + locals()[k] = v + if len( dom ) == 0: + return + definition = z3.Or( [ eval( "(" + var + " == " + str( v ) + ")" ) for v in dom ] ) + # definition = z3.And( [ v >= 0, v < len( dom ) ] ) + + self.solver.add( definition ) + self.optim.add( definition ) + return + + #----------------------------------------------------- + + # Converts a model (returned by z3) into a point. + # Returns a list + def z3ToPoint( self, point ): + res = [] + # get the variables corresponding to the axis names + for idx, i in enumerate( self.axis_names ): + locals()[i] = Globals.z3variables[i] + if i in Globals.z3types: # non-numeric points -> coord to value + value = Globals.z3types[i][point[locals()[i]].as_long()] + elif None == point[locals()[i]]: + info( "no value for %s, take %r (incomplete model)" % ( self.axis_names[idx], self.axis_val_ranges[idx][0] ) ) + value = self.axis_val_ranges[idx][ 0] + elif z3.is_int_value( point[locals()[i]] ): + value = point[locals()[i]].as_long() + elif z3.is_true( point[locals()[i]] ) or z3.is_false( point[locals()[i]] ): + value = z3.is_true( point[locals()[i]] ) + res.append( value ) + return res + + def perfParamToCoord( self, params ): + coord = [None]*self.total_dims + for i in range( self.total_dims ): + coord[i] = params[self.axis_names[i]] + if not self.z3IsNumeric( i ): + name = self.axis_names[i] + coord[i] = Globals.z3types[name].index( coord[i] ) + return coord + + def coordToTabOfPerfParams( self, coord ): + params = self.search.coordToPerfParams( coord ) + perftab = [] + for i, name in enumerate( self.axis_names ): + c = params[name] + if not self.z3IsNumeric( i ): + c = Globals.z3types[name].index( c ) + perftab.append( c ) + return perftab + + def perfParamTabToCoord( self, params ): + coord = [None]*self.total_dims + for i in range( self.total_dims ): + coord[i] = self.axis_val_ranges[i].index( params[i] ) + return coord + + From a107add4a8f23dddbf524e41478e6b22dbc2b9a3 Mon Sep 17 00:00:00 2001 From: Camille Coti Date: Tue, 22 Dec 2020 18:32:27 -0800 Subject: [PATCH 07/11] Removed now unnecessary files --- orio/main/tuner/search/simplex/z3_search.py | 315 -------------------- orio/main/tuner/search/z3_search.py | 305 ------------------- 2 files changed, 620 deletions(-) delete mode 100644 orio/main/tuner/search/simplex/z3_search.py delete mode 100644 orio/main/tuner/search/z3_search.py diff --git a/orio/main/tuner/search/simplex/z3_search.py b/orio/main/tuner/search/simplex/z3_search.py deleted file mode 100644 index 36daac47..00000000 --- a/orio/main/tuner/search/simplex/z3_search.py +++ /dev/null @@ -1,315 +0,0 @@ -from orio.main.util.globals import * -#import orio.main.tuner.search.search -import z3 - -class Z3search: - - def __init__( self, total_dims, axis_names, axis_val_ranges, dim_uplimits, constraints ): - self.axis_names = axis_names - self.axis_val_ranges = axis_val_ranges - self.constraints = constraints - self.total_dims = total_dims - self.dim_uplimits = dim_uplimits - - # Initialize the solver itself - self.variables = [] - self.solver = z3.Solver() - self.optim = z3.Optimize() - Globals.z3types = {} - Globals.z3variables = {} - - # find what we have on the axis - self.__addVariableNames( self.axis_names, self.axis_val_ranges ) - self.__addConstraints( self.constraints ) - - #----------------------------------------------------- - - # Defines the variables, their type and, for numeric ones, their definition domain - def __addVariableNames( self, names, ranges ): - for idx, name in enumerate( names ): - values = ranges[idx] - if ( [ True, False ] == values ) or ( [ False, True ] == values ): #len( values ) == 2 and ( False in values or True in values ): - Globals.z3variables[name] = z3.Bool( name ) - self.__addDefinitionDomain( name, values ) - else: - try: - toto = int( values[0] ) - Globals.z3variables[name] = z3.Int( name ) - self.__addDefinitionDomain( name, values ) - except ValueError: - # if the parameter is non-numeric - # TODO we can add a case to handle floats - Globals.z3variables[name] = z3.Int( name ) - numvalues = self.__defineNonNumeric( name, values ) - self.__addDefinitionDomain( name, numvalues ) - self.variables.append( name ) # FIXME variables is axis_names - return - - # Defines a variable's definition domain - def __addDefinitionDomain( self, var, dom ): - # get the variables - for k,v in Globals.z3variables.iteritems( ): - locals()[k] = v - if len( dom ) == 0: - return - definition = z3.Or( [ eval( "(" + var + " == " + str( v ) + ")" ) for v in dom ] ) - # definition = z3.And( [ v >= 0, v < len( dom ) ] ) - - self.solver.add( definition ) - self.optim.add( definition ) - return - - # Add the constraints - def __addConstraints( self, constraints ): - # get the variables - for k,v in Globals.z3variables.iteritems( ): - locals()[k] = v - for vname, rhs in constraints: - # convert to constraint to prefix syntax - toto = eval( self.__infixToPrefix( rhs ) ) - self.solver.add( toto ) - self.optim.add( toto ) - return - - # in case a parameter is not numeric (ie, alphanumeric), we cannot store it - # as a regular value with constraints in z3. Hence, put the values in a list and - # use their index in the list instead. - def __defineNonNumeric( self, name, values ): - Globals.z3types[name] = list( values ) - return [ i for i in range( len( values ) ) ] - - # get the parameter corresponding to a numeric value - def __numericToNonNumeric( self, name, value, num ): - return Globals.z3types[name][num] - - # get the numeric value corresponding to a parameter - def __nonNumericToNumeric( self, name, value, param ): - return Globals.z3types[name].index( param ) - - # Tests whether a z3 variable is numeric. Returns False for non-numeric ones. - def z3IsNumeric( self, dimensionNumber ): - return not self.axis_names[dimensionNumber] in Globals.z3types - - def z3abs( self, x ): - return z3.If(x >= 0,x,-x) - - #----------------------------------------------------- - - # change constraint from infix notation (used in the input file) to prefix notation (used by z3) - def __infixToPrefix( self, expr ): - if "or" in expr or "and" in expr: - if "and" in expr: - operandsAND = expr.split( "and" ) - return "z3.And(" + ", ".join( [ infixToPrefix( op ) if "or" in op or "and" in op else op for op in operandsAND ] ) + " ) " - elif "or" in expr: - operandsOR = expr.split( "or" ) - return "z3.Or(" + ", ".join( [ infixToPrefix( op ) if "or" in op or "and" in op else op for op in operandsOR ] ) + " ) " - else: - return expr - else: - return expr - - #----------------------------------------------------- - - # Add the constraints - def __addConstraints( self, constraints ): - # get the variables - for k,v in Globals.z3variables.iteritems( ): - locals()[k] = v - for vname, rhs in constraints: - # convert to constraint to prefix syntax - toto = eval( self.__infixToPrefix( rhs ) ) - self.solver.add( toto ) - self.optim.add( toto ) - return - - # Add a forbidden point in the solver (and the optimizer) - # Input: a dictionary of performance parameters. - def addPoint( self, point ): - # get the variables corresponding to the axis names - for name in self.axis_names: - locals()[name] = Globals.z3variables[name] - point2 = {} - # if there is a non-numeric value here, translate it - for idx, name in enumerate( point.keys() ): - # translate non-numeric values - if not self.z3IsNumeric( idx ): # non-numeric points -> coord to value - elem = Globals.z3types[name].index( point[name] ) - else: - elem = point[name] - point2[name] = elem - - # remove this point - for s in [ self.solver, self.optim ]: - s.add( z3.Or( [ locals()[name] != point2[name] for name in self.axis_names ] ) ) - return - - #----------------------------------------------------- - - # Returns a *feasible* random point - def getRandomCoord_z3( self ): - if self.solver.check() == z3.unsat: - return None - else: - model = self.solver.model() - return model - - # Getting a random point from an SMT solver is not a trivial question. - # This one gives a somehow random point, but the distribution is not uniform. - # TODO: David's idea involving SAT. - # TODO: non-constrained variables? - def getRandomCoord_z3_distance( self ): - if self.solver.check() == z3.unsat: - return None - else: - # Pick a random point in the solution space - rpc = [] - for i in range( self.total_dims ): - iuplimit = self.dim_uplimits[i] - ipoint = self.getRandomInt(0, iuplimit-1) - rpc.append(ipoint) - - # Get the nearest feasible point - point = self.getNearestFeasible( rpc ) - return self.perfParamTabToCoord( point ) - - # This is copied from search.py. Not exactly the cleanest way to do it, but simpler for the moment. - def getRandomInt(self, lbound, ubound): - '''To generate a random integer N such that lbound <= N <= ubound''' - from random import randint - - if lbound > ubound: - err('orio.main.tuner.search.search internal error: the lower bound of genRandomInt must not be ' + - 'greater than the upper bound') - return randint(lbound, ubound) - - #----------------------------------------------------- - - # For a given point, returns the nearest feasible point - def getNearestFeasible( self, coord ): - # get the variables corresponding to the axis names - for i in self.axis_names: - locals()[i] = Globals.z3variables[i] - - # Convert into parameters - rpp = self.coordToPerfParams( coord ) - for i, name in enumerate( self.axis_names ): - if not self.z3IsNumeric( i ): - rpp[name] = Globals.z3types[name].index( rpp[name] ) - - # create a new scope - self.optim.push() - - # Get a possible point that minimizes the 1-norm distance to this random point - # forget the booleans - self.optim.minimize( z3.Sum( [ self.z3abs( locals()[name] - rpp[name] )for name in self.axis_names if not z3.is_bool( locals()[name] ) ] ) ) - if z3.unsat == self.optim.check(): - return None - model = self.optim.model() - - # restore the state (exit the scope) - self.optim.pop() - return self.z3ToPoint( model ) - - #----------------------------------------------------- - - # Defines the variables, their type and, for numeric ones, their definition domain - def __addVariableNames( self, names, ranges ): - for idx, name in enumerate( names ): - values = ranges[idx] - if ( [ True, False ] == values ) or ( [ False, True ] == values ): #len( values ) == 2 and ( False in values or True in values ): - Globals.z3variables[name] = z3.Bool( name ) - self.__addDefinitionDomain( name, values ) - else: - try: - toto = int( values[0] ) - Globals.z3variables[name] = z3.Int( name ) - self.__addDefinitionDomain( name, values ) - except ValueError: - # if the parameter is non-numeric - # TODO we can add a case to handle floats - Globals.z3variables[name] = z3.Int( name ) - numvalues = self.__defineNonNumeric( name, values ) - self.__addDefinitionDomain( name, numvalues ) - self.variables.append( name ) # FIXME variables is axis_names - return - - # z3-specific routine: - # Defines a variable's definition domain - def __addDefinitionDomain( self, var, dom ): - # get the variables - for k,v in Globals.z3variables.iteritems( ): - locals()[k] = v - if len( dom ) == 0: - return - definition = z3.Or( [ eval( "(" + var + " == " + str( v ) + ")" ) for v in dom ] ) - # definition = z3.And( [ v >= 0, v < len( dom ) ] ) - - self.solver.add( definition ) - self.optim.add( definition ) - return - - #----------------------------------------------------- - - # Converts a model (returned by z3) into a point. - # Returns a list - def z3ToPoint( self, point ): - res = [] - # get the variables corresponding to the axis names - for idx, i in enumerate( self.axis_names ): - locals()[i] = Globals.z3variables[i] - if i in Globals.z3types: # non-numeric points -> coord to value - value = Globals.z3types[i][point[locals()[i]].as_long()] - elif None == point[locals()[i]]: - info( "no value for %s, take %r (incomplete model)" % ( self.axis_names[idx], self.axis_val_ranges[idx][0] ) ) - value = self.axis_val_ranges[idx][ 0] - elif z3.is_int_value( point[locals()[i]] ): - value = point[locals()[i]].as_long() - elif z3.is_true( point[locals()[i]] ) or z3.is_false( point[locals()[i]] ): - value = z3.is_true( point[locals()[i]] ) - res.append( value ) - return res - - def coordToPerfParams(self, coord): - '''To convert the given coordinate to the corresponding performance parameters''' - # get the performance parameters that correspond the given coordinate - perf_params = {} - for i in range(0, self.total_dims): - ipoint = coord[i] - # If the point is not in the definition domain, take the nearest feasible value - 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] - # return the obtained performance parameters - return perf_params - - def perfParamToCoord( self, params ): - coord = [None]*self.total_dims - for i in range( self.total_dims ): - coord[i] = params[self.axis_names[i]] - if not self.z3IsNumeric( i ): - name = self.axis_names[i] - coord[i] = Globals.z3types[name].index( coord[i] ) - return coord - - def coordToTabOfPerfParams( self, coord ): - params = self.coordToPerfParams( coord ) - perftab = [] - for i, name in enumerate( self.axis_names ): - c = params[name] - if not self.z3IsNumeric( i ): - c = Globals.z3types[name].index( c ) - perftab.append( c ) - return perftab - - def perfParamTabToCoord( self, params ): - coord = [None]*self.total_dims - for i in range( self.total_dims ): - coord[i] = self.axis_val_ranges[i].index( params[i] ) - return coord - - diff --git a/orio/main/tuner/search/z3_search.py b/orio/main/tuner/search/z3_search.py deleted file mode 100644 index 9bf8a741..00000000 --- a/orio/main/tuner/search/z3_search.py +++ /dev/null @@ -1,305 +0,0 @@ -from orio.main.util.globals import * - -try: - import z3 - Globals.have_z3 = True -except Exception as e: - Globals.have_z3 = False - raise ImportError( "Could not load z3. Will not be using it." ) -# raise ImportError() # Silent - -class Z3search: - - def __init__( self, total_dims, axis_names, axis_val_ranges, dim_uplimits, constraints, s ): - self.axis_names = axis_names - self.axis_val_ranges = axis_val_ranges - self.constraints = constraints - self.total_dims = total_dims - self.dim_uplimits = dim_uplimits - self.search = s - - # Initialize the solver itself - self.variables = [] - self.solver = z3.Solver() - self.optim = z3.Optimize() - Globals.z3types = {} - Globals.z3variables = {} - - # find what we have on the axis - self.__addVariableNames( self.axis_names, self.axis_val_ranges ) - self.__addConstraints( self.constraints ) - - #----------------------------------------------------- - - # Defines the variables, their type and, for numeric ones, their definition domain - def __addVariableNames( self, names, ranges ): - for idx, name in enumerate( names ): - values = ranges[idx] - if ( [ True, False ] == values ) or ( [ False, True ] == values ): #len( values ) == 2 and ( False in values or True in values ): - Globals.z3variables[name] = z3.Bool( name ) - self.__addDefinitionDomain( name, values ) - else: - try: - toto = int( values[0] ) - Globals.z3variables[name] = z3.Int( name ) - self.__addDefinitionDomain( name, values ) - except ValueError: - # if the parameter is non-numeric - # TODO we can add a case to handle floats - Globals.z3variables[name] = z3.Int( name ) - numvalues = self.__defineNonNumeric( name, values ) - self.__addDefinitionDomain( name, numvalues ) - self.variables.append( name ) # FIXME variables is axis_names - return - - # Defines a variable's definition domain - def __addDefinitionDomain( self, var, dom ): - # get the variables - for k,v in Globals.z3variables.iteritems( ): - locals()[k] = v - if len( dom ) == 0: - return - definition = z3.Or( [ eval( "(" + var + " == " + str( v ) + ")" ) for v in dom ] ) - # definition = z3.And( [ v >= 0, v < len( dom ) ] ) - - self.solver.add( definition ) - self.optim.add( definition ) - return - - # Add the constraints - def __addConstraints( self, constraints ): - # get the variables - for k,v in Globals.z3variables.iteritems( ): - locals()[k] = v - for vname, rhs in constraints: - # convert to constraint to prefix syntax - toto = eval( self.__infixToPrefix( rhs ) ) - self.solver.add( toto ) - self.optim.add( toto ) - return - - # in case a parameter is not numeric (ie, alphanumeric), we cannot store it - # as a regular value with constraints in z3. Hence, put the values in a list and - # use their index in the list instead. - def __defineNonNumeric( self, name, values ): - Globals.z3types[name] = list( values ) - return [ i for i in range( len( values ) ) ] - - # get the parameter corresponding to a numeric value - def __numericToNonNumeric( self, name, value, num ): - return Globals.z3types[name][num] - - # get the numeric value corresponding to a parameter - def __nonNumericToNumeric( self, name, value, param ): - return Globals.z3types[name].index( param ) - - # Tests whether a z3 variable is numeric. Returns False for non-numeric ones. - def z3IsNumeric( self, dimensionNumber ): - return not self.axis_names[dimensionNumber] in Globals.z3types - - def z3abs( self, x ): - return z3.If(x >= 0,x,-x) - - #----------------------------------------------------- - - # change constraint from infix notation (used in the input file) to prefix notation (used by z3) - def __infixToPrefix( self, expr ): - if "or" in expr or "and" in expr: - if "and" in expr: - operandsAND = expr.split( "and" ) - return "z3.And(" + ", ".join( [ infixToPrefix( op ) if "or" in op or "and" in op else op for op in operandsAND ] ) + " ) " - elif "or" in expr: - operandsOR = expr.split( "or" ) - return "z3.Or(" + ", ".join( [ infixToPrefix( op ) if "or" in op or "and" in op else op for op in operandsOR ] ) + " ) " - else: - return expr - else: - return expr - - #----------------------------------------------------- - - # Add the constraints - def __addConstraints( self, constraints ): - # get the variables - for k,v in Globals.z3variables.iteritems( ): - locals()[k] = v - for vname, rhs in constraints: - # convert to constraint to prefix syntax - toto = eval( self.__infixToPrefix( rhs ) ) - self.solver.add( toto ) - self.optim.add( toto ) - return - - # Add a forbidden point in the solver (and the optimizer) - # Input: a dictionary of performance parameters. - def addPoint( self, point ): - # get the variables corresponding to the axis names - for name in self.axis_names: - locals()[name] = Globals.z3variables[name] - point2 = {} - # if there is a non-numeric value here, translate it - for idx, name in enumerate( point.keys() ): - # translate non-numeric values - if not self.z3IsNumeric( idx ): # non-numeric points -> coord to value - elem = Globals.z3types[name].index( point[name] ) - else: - elem = point[name] - point2[name] = elem - - # remove this point - for s in [ self.solver, self.optim ]: - s.add( z3.Or( [ locals()[name] != point2[name] for name in self.axis_names ] ) ) - return - - #----------------------------------------------------- - - # Returns a *feasible* random point - def getRandomCoord_z3( self ): - if self.solver.check() == z3.unsat: - return None - else: - model = self.solver.model() - return model - - # Getting a random point from an SMT solver is not a trivial question. - # This one gives a somehow random point, but the distribution is not uniform. - # TODO: David's idea involving SAT. - # TODO: non-constrained variables? - def getRandomCoord_z3_distance( self ): - if self.solver.check() == z3.unsat: - return None - else: - # Pick a random point in the solution space - rpc = [] - for i in range( self.total_dims ): - iuplimit = self.dim_uplimits[i] - ipoint = self.getRandomInt(0, iuplimit-1) - rpc.append(ipoint) - - # Get the nearest feasible point - point = self.getNearestFeasible( rpc ) - return self.perfParamTabToCoord( point ) - - # This is copied from search.py. Not exactly the cleanest way to do it, but simpler for the moment. - def getRandomInt(self, lbound, ubound): - '''To generate a random integer N such that lbound <= N <= ubound''' - from random import randint - - if lbound > ubound: - err('orio.main.tuner.search.search internal error: the lower bound of genRandomInt must not be ' + - 'greater than the upper bound') - return randint(lbound, ubound) - - #----------------------------------------------------- - - # For a given point, returns the nearest feasible point - def getNearestFeasible( self, coord ): - # get the variables corresponding to the axis names - for i in self.axis_names: - locals()[i] = Globals.z3variables[i] - - # Convert into parameters - rpp = self.search.coordToPerfParams( coord ) - for i, name in enumerate( self.axis_names ): - if not self.z3IsNumeric( i ): - rpp[name] = Globals.z3types[name].index( rpp[name] ) - - # create a new scope - self.optim.push() - - # Get a possible point that minimizes the 1-norm distance to this random point - # forget the booleans - self.optim.minimize( z3.Sum( [ self.z3abs( locals()[name] - rpp[name] )for name in self.axis_names if not z3.is_bool( locals()[name] ) ] ) ) - if z3.unsat == self.optim.check(): - return None - model = self.optim.model() - - # restore the state (exit the scope) - self.optim.pop() - return self.z3ToPoint( model ) - - #----------------------------------------------------- - - # Defines the variables, their type and, for numeric ones, their definition domain - def __addVariableNames( self, names, ranges ): - for idx, name in enumerate( names ): - values = ranges[idx] - if ( [ True, False ] == values ) or ( [ False, True ] == values ): #len( values ) == 2 and ( False in values or True in values ): - Globals.z3variables[name] = z3.Bool( name ) - self.__addDefinitionDomain( name, values ) - else: - try: - toto = int( values[0] ) - Globals.z3variables[name] = z3.Int( name ) - self.__addDefinitionDomain( name, values ) - except ValueError: - # if the parameter is non-numeric - # TODO we can add a case to handle floats - Globals.z3variables[name] = z3.Int( name ) - numvalues = self.__defineNonNumeric( name, values ) - self.__addDefinitionDomain( name, numvalues ) - self.variables.append( name ) # FIXME variables is axis_names - return - - # z3-specific routine: - # Defines a variable's definition domain - def __addDefinitionDomain( self, var, dom ): - # get the variables - for k,v in Globals.z3variables.iteritems( ): - locals()[k] = v - if len( dom ) == 0: - return - definition = z3.Or( [ eval( "(" + var + " == " + str( v ) + ")" ) for v in dom ] ) - # definition = z3.And( [ v >= 0, v < len( dom ) ] ) - - self.solver.add( definition ) - self.optim.add( definition ) - return - - #----------------------------------------------------- - - # Converts a model (returned by z3) into a point. - # Returns a list - def z3ToPoint( self, point ): - res = [] - # get the variables corresponding to the axis names - for idx, i in enumerate( self.axis_names ): - locals()[i] = Globals.z3variables[i] - if i in Globals.z3types: # non-numeric points -> coord to value - value = Globals.z3types[i][point[locals()[i]].as_long()] - elif None == point[locals()[i]]: - info( "no value for %s, take %r (incomplete model)" % ( self.axis_names[idx], self.axis_val_ranges[idx][0] ) ) - value = self.axis_val_ranges[idx][ 0] - elif z3.is_int_value( point[locals()[i]] ): - value = point[locals()[i]].as_long() - elif z3.is_true( point[locals()[i]] ) or z3.is_false( point[locals()[i]] ): - value = z3.is_true( point[locals()[i]] ) - res.append( value ) - return res - - def perfParamToCoord( self, params ): - coord = [None]*self.total_dims - for i in range( self.total_dims ): - coord[i] = params[self.axis_names[i]] - if not self.z3IsNumeric( i ): - name = self.axis_names[i] - coord[i] = Globals.z3types[name].index( coord[i] ) - return coord - - def coordToTabOfPerfParams( self, coord ): - params = self.search.coordToPerfParams( coord ) - perftab = [] - for i, name in enumerate( self.axis_names ): - c = params[name] - if not self.z3IsNumeric( i ): - c = Globals.z3types[name].index( c ) - perftab.append( c ) - return perftab - - def perfParamTabToCoord( self, params ): - coord = [None]*self.total_dims - for i in range( self.total_dims ): - coord[i] = self.axis_val_ranges[i].index( params[i] ) - return coord - - From 1bb48d39cad9e033abab63f57d9ead5e34c523a5 Mon Sep 17 00:00:00 2001 From: Camille Coti Date: Tue, 22 Dec 2020 18:35:05 -0800 Subject: [PATCH 08/11] Now this is done in search.py --- orio/main/tuner/search/simplex/simplex.py | 19 +------------------ 1 file changed, 1 insertion(+), 18 deletions(-) diff --git a/orio/main/tuner/search/simplex/simplex.py b/orio/main/tuner/search/simplex/simplex.py index 355ca46d..3d394fbb 100644 --- a/orio/main/tuner/search/simplex/simplex.py +++ b/orio/main/tuner/search/simplex/simplex.py @@ -10,14 +10,6 @@ import orio.main.tuner.search.search from orio.main.util.globals import * -try: - import z3 - _have_z3 = True - import z3_search - -except Exception as e: - _have_z3 = False - #----------------------------------------------------- class Simplex(orio.main.tuner.search.search.Search): @@ -68,12 +60,6 @@ def __init__(self, params): # read all algorithm-specific arguments self.__readAlgoArgs() - if _have_z3: - self.have_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 ) - else: - self.have_z3 = False - self.z3solver = None # complain if both the search time limit and the total number of search runs are undefined if self.time_limit <= 0 and self.total_runs <= 0: @@ -541,10 +527,7 @@ def __initRandomSimplex(self, simplex_records): # randomly pick (N+1) vertices to form a simplex, where N is the number of dimensions simplex = [] while True: - if self.have_z3: - coord = self.z3solver.getRandomCoord_z3_distance() - else: - coord = self.getRandomCoord() + coord = self.getRandomCoord() if coord not in simplex: simplex.append(coord) if len(simplex) == self.__simplex_size: From 18695eb14571e8bbadf89546654a70df78718667 Mon Sep 17 00:00:00 2001 From: Camille Coti Date: Wed, 23 Dec 2020 16:05:49 -0800 Subject: [PATCH 09/11] Updated the randomsimple search algo to make it use the z3-enabled search methods. --- .../tuner/search/randomsimple/randomsimple.py | 34 +++---------------- orio/main/tuner/search/search.py | 4 ++- .../search/{randomsimple => }/z3_search.py | 34 +++++++------------ 3 files changed, 20 insertions(+), 52 deletions(-) rename orio/main/tuner/search/{randomsimple => }/z3_search.py (92%) diff --git a/orio/main/tuner/search/randomsimple/randomsimple.py b/orio/main/tuner/search/randomsimple/randomsimple.py index 8309d71b..5324e0f8 100644 --- a/orio/main/tuner/search/randomsimple/randomsimple.py +++ b/orio/main/tuner/search/randomsimple/randomsimple.py @@ -6,13 +6,6 @@ import orio.main.tuner.search.search from orio.main.util.globals import * -try: - import z3 - _have_z3 = True - import z3_search -except Exception as e: - _have_z3 = False - class Randomsimple(orio.main.tuner.search.search.Search): def __init__(self, params): @@ -20,13 +13,6 @@ def __init__(self, params): orio.main.tuner.search.search.Search.__init__(self, params) self.__readAlgoArgs() - if _have_z3: - self.have_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 ) - else: - self.have_z3 = False - self.z3Solver = None - if self.time_limit <= 0 and self.total_runs <= 0: err(('orio.main.tuner.search.randomsimple.randomsimple: %s search requires either (both) the search time limit or (and) the ' + 'total number of search runs to be defined') % self.__class__.__name__) @@ -51,7 +37,10 @@ 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 None == coord: + print( "no point left in the parameter space" ) + break + if not self.checkValidity( coord ) or coord in visited: print( "invalid point" ) continue try: @@ -64,7 +53,7 @@ def searchBestCoord(self, startCoord=None): except Exception, e: info('FAILED: %s %s' % (e.__class__.__name__, e)) runs += 1 - if not self.have_z3: + if not self.use_z3: visited.append( coord ) else: point = self.coordToPerfParams( coord ) @@ -90,16 +79,3 @@ def __readAlgoArgs(self): err('orio.main.tuner.search.randomsimple: unrecognized %s algorithm-specific argument: "%s"' % (self.__class__.__name__, vname)) - # In this function, either z3 finds a feasible point, or we ask the default function draw one. - def __getRandomPoint(self): - if not self.have_z3: - coord = self.getRandomCoord() - else: - # if I have z3, get a *feasible* random coord - coord = self.z3solver.getRandomCoord_z3_distance() - - # If I could not find any feasible point, just return a random point - if None != coord: - coord = self.getRandomCoord() - return coord - diff --git a/orio/main/tuner/search/search.py b/orio/main/tuner/search/search.py index 0ed908f6..26cd2c10 100644 --- a/orio/main/tuner/search/search.py +++ b/orio/main/tuner/search/search.py @@ -86,7 +86,7 @@ def __init__(self, params): _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 ) @@ -487,6 +487,8 @@ def getRandomCoord(self): random_coord.append(ipoint) if self.use_z3: point = self.z3solver.getNearestFeasible( random_coord ) + if None == point: + return None return self.z3solver.perfParamTabToCoord( point ) else: return random_coord diff --git a/orio/main/tuner/search/randomsimple/z3_search.py b/orio/main/tuner/search/z3_search.py similarity index 92% rename from orio/main/tuner/search/randomsimple/z3_search.py rename to orio/main/tuner/search/z3_search.py index 36daac47..9bf8a741 100644 --- a/orio/main/tuner/search/randomsimple/z3_search.py +++ b/orio/main/tuner/search/z3_search.py @@ -1,15 +1,22 @@ from orio.main.util.globals import * -#import orio.main.tuner.search.search -import z3 + +try: + import z3 + Globals.have_z3 = True +except Exception as e: + Globals.have_z3 = False + raise ImportError( "Could not load z3. Will not be using it." ) +# raise ImportError() # Silent class Z3search: - def __init__( self, total_dims, axis_names, axis_val_ranges, dim_uplimits, constraints ): + def __init__( self, total_dims, axis_names, axis_val_ranges, dim_uplimits, constraints, s ): self.axis_names = axis_names self.axis_val_ranges = axis_val_ranges self.constraints = constraints self.total_dims = total_dims self.dim_uplimits = dim_uplimits + self.search = s # Initialize the solver itself self.variables = [] @@ -192,7 +199,7 @@ def getNearestFeasible( self, coord ): locals()[i] = Globals.z3variables[i] # Convert into parameters - rpp = self.coordToPerfParams( coord ) + rpp = self.search.coordToPerfParams( coord ) for i, name in enumerate( self.axis_names ): if not self.z3IsNumeric( i ): rpp[name] = Globals.z3types[name].index( rpp[name] ) @@ -270,23 +277,6 @@ def z3ToPoint( self, point ): res.append( value ) return res - def coordToPerfParams(self, coord): - '''To convert the given coordinate to the corresponding performance parameters''' - # get the performance parameters that correspond the given coordinate - perf_params = {} - for i in range(0, self.total_dims): - ipoint = coord[i] - # If the point is not in the definition domain, take the nearest feasible value - 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] - # return the obtained performance parameters - return perf_params - def perfParamToCoord( self, params ): coord = [None]*self.total_dims for i in range( self.total_dims ): @@ -297,7 +287,7 @@ def perfParamToCoord( self, params ): return coord def coordToTabOfPerfParams( self, coord ): - params = self.coordToPerfParams( coord ) + params = self.search.coordToPerfParams( coord ) perftab = [] for i, name in enumerate( self.axis_names ): c = params[name] From 0f1043fbfbf9d1baf4b728f77c9251f386d29633 Mon Sep 17 00:00:00 2001 From: Camille Coti Date: Wed, 23 Dec 2020 16:05:49 -0800 Subject: [PATCH 10/11] Updated the randomsimple search algo to make it use the z3-enabled search methods. --- .../tuner/search/randomsimple/randomsimple.py | 42 ++++--------------- orio/main/tuner/search/search.py | 4 +- .../search/{randomsimple => }/z3_search.py | 34 ++++++--------- 3 files changed, 24 insertions(+), 56 deletions(-) rename orio/main/tuner/search/{randomsimple => }/z3_search.py (92%) diff --git a/orio/main/tuner/search/randomsimple/randomsimple.py b/orio/main/tuner/search/randomsimple/randomsimple.py index 8309d71b..25846762 100644 --- a/orio/main/tuner/search/randomsimple/randomsimple.py +++ b/orio/main/tuner/search/randomsimple/randomsimple.py @@ -6,13 +6,6 @@ import orio.main.tuner.search.search from orio.main.util.globals import * -try: - import z3 - _have_z3 = True - import z3_search -except Exception as e: - _have_z3 = False - class Randomsimple(orio.main.tuner.search.search.Search): def __init__(self, params): @@ -20,13 +13,6 @@ def __init__(self, params): orio.main.tuner.search.search.Search.__init__(self, params) self.__readAlgoArgs() - if _have_z3: - self.have_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 ) - else: - self.have_z3 = False - self.z3Solver = None - if self.time_limit <= 0 and self.total_runs <= 0: err(('orio.main.tuner.search.randomsimple.randomsimple: %s search requires either (both) the search time limit or (and) the ' + 'total number of search runs to be defined') % self.__class__.__name__) @@ -34,8 +20,8 @@ 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 @@ -51,11 +37,14 @@ 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: - print( "invalid point" ) + if None == coord: + info( "no point left in the parameter space" ) + break + if not self.checkValidity( coord ) or coord in visited: + info( "invalid point" ) continue try: - print( "coord:", coord, "run", runs ) + info( "coord: %s run %s" % (coord, 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 ) ) @@ -64,7 +53,7 @@ def searchBestCoord(self, startCoord=None): except Exception, e: info('FAILED: %s %s' % (e.__class__.__name__, e)) runs += 1 - if not self.have_z3: + if not self.use_z3: visited.append( coord ) else: point = self.coordToPerfParams( coord ) @@ -90,16 +79,3 @@ def __readAlgoArgs(self): err('orio.main.tuner.search.randomsimple: unrecognized %s algorithm-specific argument: "%s"' % (self.__class__.__name__, vname)) - # In this function, either z3 finds a feasible point, or we ask the default function draw one. - def __getRandomPoint(self): - if not self.have_z3: - coord = self.getRandomCoord() - else: - # if I have z3, get a *feasible* random coord - coord = self.z3solver.getRandomCoord_z3_distance() - - # If I could not find any feasible point, just return a random point - if None != coord: - coord = self.getRandomCoord() - return coord - diff --git a/orio/main/tuner/search/search.py b/orio/main/tuner/search/search.py index 0ed908f6..26cd2c10 100644 --- a/orio/main/tuner/search/search.py +++ b/orio/main/tuner/search/search.py @@ -86,7 +86,7 @@ def __init__(self, params): _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 ) @@ -487,6 +487,8 @@ def getRandomCoord(self): random_coord.append(ipoint) if self.use_z3: point = self.z3solver.getNearestFeasible( random_coord ) + if None == point: + return None return self.z3solver.perfParamTabToCoord( point ) else: return random_coord diff --git a/orio/main/tuner/search/randomsimple/z3_search.py b/orio/main/tuner/search/z3_search.py similarity index 92% rename from orio/main/tuner/search/randomsimple/z3_search.py rename to orio/main/tuner/search/z3_search.py index 36daac47..9bf8a741 100644 --- a/orio/main/tuner/search/randomsimple/z3_search.py +++ b/orio/main/tuner/search/z3_search.py @@ -1,15 +1,22 @@ from orio.main.util.globals import * -#import orio.main.tuner.search.search -import z3 + +try: + import z3 + Globals.have_z3 = True +except Exception as e: + Globals.have_z3 = False + raise ImportError( "Could not load z3. Will not be using it." ) +# raise ImportError() # Silent class Z3search: - def __init__( self, total_dims, axis_names, axis_val_ranges, dim_uplimits, constraints ): + def __init__( self, total_dims, axis_names, axis_val_ranges, dim_uplimits, constraints, s ): self.axis_names = axis_names self.axis_val_ranges = axis_val_ranges self.constraints = constraints self.total_dims = total_dims self.dim_uplimits = dim_uplimits + self.search = s # Initialize the solver itself self.variables = [] @@ -192,7 +199,7 @@ def getNearestFeasible( self, coord ): locals()[i] = Globals.z3variables[i] # Convert into parameters - rpp = self.coordToPerfParams( coord ) + rpp = self.search.coordToPerfParams( coord ) for i, name in enumerate( self.axis_names ): if not self.z3IsNumeric( i ): rpp[name] = Globals.z3types[name].index( rpp[name] ) @@ -270,23 +277,6 @@ def z3ToPoint( self, point ): res.append( value ) return res - def coordToPerfParams(self, coord): - '''To convert the given coordinate to the corresponding performance parameters''' - # get the performance parameters that correspond the given coordinate - perf_params = {} - for i in range(0, self.total_dims): - ipoint = coord[i] - # If the point is not in the definition domain, take the nearest feasible value - 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] - # return the obtained performance parameters - return perf_params - def perfParamToCoord( self, params ): coord = [None]*self.total_dims for i in range( self.total_dims ): @@ -297,7 +287,7 @@ def perfParamToCoord( self, params ): return coord def coordToTabOfPerfParams( self, coord ): - params = self.coordToPerfParams( coord ) + params = self.search.coordToPerfParams( coord ) perftab = [] for i, name in enumerate( self.axis_names ): c = params[name] From 0d6f81e3bc57fc7dd6cba31b9510d9e3f99538ac Mon Sep 17 00:00:00 2001 From: Boyana Norris Date: Sun, 27 Dec 2020 08:38:25 -0800 Subject: [PATCH 11/11] python3 error fix --- orio/main/tuner/search/simplex/simplex.py | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/orio/main/tuner/search/simplex/simplex.py b/orio/main/tuner/search/simplex/simplex.py index 83b94ac7..17ec1a51 100644 --- a/orio/main/tuner/search/simplex/simplex.py +++ b/orio/main/tuner/search/simplex/simplex.py @@ -571,7 +571,7 @@ def __getReflection(self, coord, centroid): # Get the nearest feasible point return [ self.z3solver.perfParamTabToCoord( self.z3solver.getNearestFeasible( p ) ) for p in point ] else: - return point + return list(point) def __getExpansion(self, coord, centroid): '''Return an expansion coordinate''' @@ -582,7 +582,7 @@ def __getExpansion(self, coord, centroid): # Get the nearest feasible point return [ self.z3solver.perfParamTabToCoord( self.z3solver.getNearestFeasible( p ) ) for p in point ] else: - return point + return list(point) def __getContraction(self, coord, centroid): '''Return a contraction coordinate''' @@ -594,7 +594,7 @@ def __getContraction(self, coord, centroid): # Get the nearest feasible point return [ self.z3solver.perfParamTabToCoord( self.z3solver.getNearestFeasible( p ) ) for p in point ] else: - return point + return list(point) def __getShrinkage(self, coord, rest_coords): '''Return a shrinkage simplex''' @@ -605,5 +605,5 @@ def __getShrinkage(self, coord, rest_coords): # Get the nearest feasible point return [ self.z3solver.perfParamTabToCoord( self.z3solver.getNearestFeasible( p ) ) for p in point ] else: - return point + return list(point)