我们从Python开源项目中，提取了以下50个代码示例，用于说明如何使用math.inf()。
def _actual_result(self, result, line): actual = None distance = inf if line == -inf: # precondition actual = result.get_node_result(self.cfg.in_node)[0] return actual elif line == inf: # postcondition actual = result.get_node_result(self.cfg.out_node)[0] return actual elif line < 0: for edge in self.cfg.edges.values(): if isinstance(edge, Conditional): current = edge.condition.pp.line + line if current < distance: states = result.get_node_result(edge.source) actual = states[0] distance = current for node in self.cfg.nodes.values(): states = result.get_node_result(node) for i, stmt in enumerate(node.stmts): current = stmt.pp.line - line if abs(current) < distance: actual = states[i+1] if current < 0 else states[i] distance = abs(current) return actual
def __init__(self, attention_units, memory, sequence_length=None, time_major=True, mode=0): self.attention_units = attention_units self.enc_units = memory.get_shape()[-1].value if time_major: memory = tf.transpose(memory, perm=(1,0,2)) self.enc_length = tf.shape(memory)[1] self.batch_size = tf.shape(memory)[0] self.mode = mode self.mask = array_ops.sequence_mask(sequence_length, self.enc_length) if sequence_length is not None else None self.tiny = -math.inf * tf.ones(shape=(self.batch_size, self.enc_length)) self.memory = tf.reshape(memory, (tf.shape(memory)[0], self.enc_length, 1, self.enc_units)) ### pre-compute Uahj to minimize the computational cost with tf.variable_scope('attention'): Ua = tf.get_variable(name='Ua', shape=(1, 1, self.enc_units, self.attention_units)) self.hidden_feats = tf.nn.conv2d(self.memory, Ua, [1,1,1,1], "SAME")
def gen_adj_mat(longs, lats, prob_edge=.2, additional_length=lambda: np.random.exponential(20,1)): '''Get an adjacency matrix for the cities whose longitudes and latitudes are passed. Each entry will either be a number somewhat greater than the crow-flies distance between the two cities (with probability prob_edge), or math.inf. The matrix will consist of floats, and be symmetric. The diagonal will be all zeroes. The "somewhat greater" is controlled by the additional_length parameter, a function returning a random amount.''' # Generate full nxn Bernoulli's, even though we'll only use the upper # triangle. edges = np.random.binomial(1, prob_edge, size=(len(longs),len(longs))) am = np.zeros((len(longs),len(longs))) for i in range(len(longs)): for j in range(len(longs)): if i==j: am[i,i] = 0 elif i < j: if edges[i,j] == 1: am[i,j] = (math.hypot(longs[i]-longs[j],lats[i]-lats[j]) + additional_length()) am[j,i] = am[i,j] else: am[i,j] = am[j,i] = math.inf return np.around(am,1)
def run_bellman_ford(test_num, num_nodes, make_graph_fn): print("\t\t~~~ Test: %s ~~~" % test_num) distance = [math.inf for _ in range(num_nodes)] parents = [-1 for _ in range(num_nodes)] graph, source, target, expected = make_graph_fn() no_neg_cycle = bellman_ford(graph, source, parents, distance) nodes = graph.get_vertices() distances_labeled = [] for i in range(len(nodes)): distances_labeled.append((nodes[i].rep, distance[i])) print("Distances labeled: %s" % distances_labeled) print("Parents: %s" % parents) if no_neg_cycle: path = [] current = target.index while current != -1: path.append(nodes[current].rep) current = parents[current] path = path[::-1] print("Shortest path from: %s to %s is \n%s" % (source.rep, target.rep, path)) else: print("Has negative cycle, no solution.") print("Passed: %s\n" % (expected == distance if no_neg_cycle else no_neg_cycle == expected)) # -------------------------------------- driver functions ----------------------------------------
def dijkstra(graph, source): pq = [] nodes = graph.get_all_vertices() distances = [math.inf] * len(nodes) path = [-1] * len(nodes) distances[source.index] = 0 for node in nodes: # Store as (priority, task) tuples, heapq will sort on first element. heapq.heappush(pq, (distances[node.index], node)) while pq: # Assumes non negative weights, so when popping a node it is the best way to get there. dist, node = heapq.heappop(pq) for edge in graph.get_adjacent_edges(node): # Note: can't terminate early and do this. # Eg: (s) -3-> (c) -12-> (d) # \-20->(d) will be wrong # if distances[edge.destination.index] != math.inf: # We already have the shortest path to this node. # continue if relax(node, edge.destination, edge, distances): # Found a better way to get to a next node, add that to the pq and set the parent. heapq.heappush(pq, (distances[edge.destination.index], edge.destination)) path[edge.destination.index] = node.index return distances, path # Shortest path from source to any other node in distances.
def __str__(self): """String representation of IntegerSet obj.""" interval_strs = [] for start, end in self.intervals: if start > -math.inf: start_str = "%d" % start else: start_str = "-inf" if end < math.inf: end_str = "%d" % end else: end_str = "inf" if start_str != end_str: interval_strs.append("[" + start_str + ", " + end_str + "]") else: interval_strs.append("{" + start_str + "}") return ", ".join(interval_strs)
def _get_split_point_candidates(self): splits = SortedList() min_value = math.inf max_value = -math.inf for class_val, att_estimator in self._class_lookup.items(): min_val_observed_for_class_val = self._min_val_observed_per_class.get(class_val, None) if min_val_observed_for_class_val is not None: if min_val_observed_for_class_val < min_value: min_value = min_val_observed_for_class_val max_val_observed_for_class_val = self._max_val_observed_per_class.get(class_val) if max_val_observed_for_class_val > max_value: max_value = max_val_observed_for_class_val if min_value < math.inf: new_bin = max_value - min_value new_bin /= (self._num_bins + 1) for i in range(self._num_bins): split = min_value + (new_bin * (i + 1)) if split > min_value and split < max_value: splits.add(split) return splits
def instantiateFrameForge(self, structT, DATA_WIDTH=64, maxFrameLen=inf, maxPaddingWords=inf, trimPaddingWordsOnStart=False, trimPaddingWordsOnEnd=False, randomized=True): tmpl = TransTmpl(structT) frames = list(FrameTmpl.framesFromTransTmpl( tmpl, DATA_WIDTH, maxFrameLen=maxFrameLen, maxPaddingWords=maxPaddingWords, trimPaddingWordsOnStart=trimPaddingWordsOnStart, trimPaddingWordsOnEnd=trimPaddingWordsOnEnd)) u = self.u = AxiS_frameForge(AxiStream, structT, tmpl, frames) self.DATA_WIDTH = DATA_WIDTH u.DATA_WIDTH.set(self.DATA_WIDTH) self.prepareUnit(self.u) if randomized: self.randomize(u.dataOut) for intf in u.dataIn._fieldsToInterfaces.values(): self.randomize(intf)
def __init__(self, rate=0.0, autojump_threshold=inf): # when the real clock said 'real_base', the virtual time was # 'virtual_base', and since then it's advanced at 'rate' virtual # seconds per real second. self._real_base = 0.0 self._virtual_base = 0.0 self._rate = 0.0 self._autojump_threshold = 0.0 self._autojump_task = None self._autojump_cancel_scope = None # kept as an attribute so that our tests can monkeypatch it self._real_clock = time.monotonic # use the property update logic to set initial values self.rate = rate self.autojump_threshold = autojump_threshold
def _might_change_effective_deadline(self): try: yield finally: old = self._effective_deadline if self.cancel_called or not self._tasks: new = inf else: new = self._deadline if old != new: self._effective_deadline = new runner = GLOBAL_RUN_CONTEXT.runner if old != inf: del runner.deadlines[old, id(self)] if new != inf: runner.deadlines[new, id(self)] = self
def checkpoint(): """A pure :ref:`checkpoint <checkpoints>`. This checks for cancellation and allows other tasks to be scheduled, without otherwise blocking. Note that the scheduler has the option of ignoring this and continuing to run the current task if it decides this is appropriate (e.g. for increased efficiency). Equivalent to ``await trio.sleep(0)`` (which is implemented by calling :func:`checkpoint`.) """ with open_cancel_scope(deadline=-inf) as scope: await _core.wait_task_rescheduled(lambda _: _core.Abort.SUCCEEDED)
def checkpoint_if_cancelled(): """Issue a :ref:`checkpoint <checkpoints>` if the calling context has been cancelled. Equivalent to (but potentially more efficient than):: if trio.current_deadline() == -inf: await trio.hazmat.checkpoint() This is either a no-op, or else it allow other tasks to be scheduled and then raises :exc:`trio.Cancelled`. Typically used together with :func:`cancel_shielded_checkpoint`. """ task = current_task() if (task._pending_cancel_scope() is not None or (task is task._runner.main_task and task._runner.ki_pending)): await _core.checkpoint() assert False # pragma: no cover task._cancel_points += 1
def get_effective_bsoftclip(self): """Return bsoftclip or compute it from paramters and effective bmax""" bsoftclip = self.bsoftclip if bsoftclip is None: return math.inf if isinstance(bsoftclip, dict): bmax = self.get_effective_bmax() bhardclip = self.get_effective_bhardclip() bmin = bsoftclip.get('bmin', 0) base = bsoftclip.get('bbase', 0) scale = bsoftclip.get('scale', 0) hcscale = bsoftclip.get('hcscale', math.inf) bsoftclip = max(bmin, base + (bmax - base) * scale, max(0, bmax - (bhardclip - bmax) * hcscale)) return bsoftclip
def get_shortest_paths(self): ''' Return a dictionary containing lists of all possible paths within the graph, keyed by tuple of start and end ''' shortest_paths = {} for start in self.edges: paths_from_start = self.get_all_paths_from(start) for weight, path in paths_from_start: end = path[-1] if start == end: continue # Skip over self paths shortest, _ = shortest_paths.get( (start, end), (math.inf, None)) if weight < shortest: shortest_paths[(start, end)] = (weight, path) # Overlay preferred paths shortest_paths.update(self.preferred_paths) return shortest_paths
def shortestPath(self,algo): # 1) Assign to each node a tentative distance value (0 for initial, inf for all others) # 2) Create a set of visited nodes. Starts with initial node # 3) For the current node, consider all of its unvisited neighbors and calulate # (distance to the current node) + (dustance from current node to neighbor) # if this calculated value is less than their tentative value, replace the tentative value with this new value # 4) Mark the current node visited # 5) if the destination node is marked visited, the search is done # 6) set the unvisited node marked with the smallest tentative distance as the next 'current node' and repeat from 3 if algo == "dijkstra": return self.dijkstra_search() elif algo == "astar": return self.astar_search() else: print("unknown search algorithm.")
def floyd_warshall(g: Graph) -> Dict[Vertex, Dict[Vertex, float]]: dist: Dict[Vertex, Dict[Vertex, float]] = {} vertices = g.vertices for v1 in vertices: dist[v1] = {} for v2 in vertices: if v1 is v2: dist[v1][v2] = 0 elif g.has_edge(v1, v2): dist[v1][v2] = g.weight[v1, v2] else: dist[v1][v2] = inf for k in vertices: for i in vertices: for j in vertices: if dist[i][j] > dist[i][k] + dist[k][j]: dist[i][j] = dist[i][k] + dist[k][j] return dist
def __init__(self, env_spec, **kwargs): super(HighLowMemory, self).__init__(env_spec) # use the old self.exp as buffer, remember to clear self.last_exp = self.exp self.epi_memory_high = [] self.epi_memory_low = [] self.max_reward = -math.inf self.min_reward = math.inf # 1st 5 epis goes into bad half, recompute every 5 epis self.threshold = math.inf self.threshold_history = [] self.epi_num = 0 self.prob_high = 0.66 self.num_epis_to_sample = 3 self.max_epis_in_mem = 15 self.recompute_freq = 10 log_self(self)
def choose_move(self, macroboard): bestmoves = [] bestscore = - math.inf macroboard = deepcopy(macroboard) if not macroboard.available_moves: raise GameEndedError moves = macroboard.available_moves for px, py in moves: macroboard.make_move(px, py) move_score = - score(macroboard) # move_score = - greedy_score(macroboard) if move_score > bestscore: bestscore = move_score bestmoves = [(px, py)] if move_score == bestscore: bestmoves.append((px, py)) macroboard.undo_last_move() return random.choice(bestmoves)
def minimax(macroboard, depth, maximizing=True): """ Perform a minimax search on a game moves tree. If optional parameter maximizing is True, assume that maximizing player is on turn. If is False - assume minimizing player. True, by default. """ if macroboard.state != State.IN_PROGRESS or depth <= 0: return score(macroboard) * (maximizing * 2 - 1) if maximizing: bestscore = - math.inf else: bestscore = math.inf moves = macroboard.available_moves depth = balance_depth(depth, len(moves)) for px, py in moves: child = deepcopy(macroboard) child.make_move(px, py) move_score = minimax(child, depth - 1, not maximizing) if maximizing: bestscore = max(bestscore, move_score) else: bestscore = min(bestscore, move_score) return bestscore
def choose_move(self, macroboard): worstmoves = [] macroboard = deepcopy(macroboard) moves = macroboard.available_moves if not moves: raise GameEndedError worstscore = math.inf depth = balance_depth(DEPTH, len(moves)) for px, py in moves: macroboard.make_move(px, py) move_score = alphaBeta(macroboard, depth) if move_score < worstscore: worstscore = move_score worstmoves = [(px, py)] if move_score == worstscore: worstmoves.append((px, py)) macroboard.undo_last_move() return random.choice(worstmoves)
def grado(self): """Devuelve el grado del polinomio. >>> f = PolinomioZp([1, 0, 0, 1], p=2) >>> f X^3 + 1 >>> f.grado() 3 El grado puede ser: * \- :py:data:`math.inf` : si el polinomio es el polinomio cero. * ``n`` : si el término lider tiene exponente n. Returns: int: el grado del polinomio. """ if self == PolinomioZp([0], self.primo()): return -math.inf else: return len(self.coeficientes) - 1
def _get_nearest_opponent_index(self, team_name, team_agent_index): # Get the opponent team name opponent_team_name = self.get_opponent_team_name(team_name) # Get the agent position agent_index = self.get_agent_index(team_name, team_agent_index) agent_pos = self.state.get_agent_pos(agent_index) # Find the nearest opponent position nearest_opponent_index = None nearest_dist = math.inf for opponent_team_agent_index in range(self.options.team_size): opponent_index = self.get_agent_index( opponent_team_name, opponent_team_agent_index) opponent_pos = self.state.get_agent_pos(opponent_index) # Calculate the distance dist = self.get_pos_distance(agent_pos, opponent_pos) if dist < nearest_dist: nearest_opponent_index = opponent_index nearest_dist = dist return nearest_opponent_index
def get_bounds(cls, area): """Return the rectangular bounds of the area. Args: area (list): A list of positions. Returns: list: [x1, y1, x2, y2] where (x1, y1) is the top-left point and (x2, y2) is the bottom-right point. """ x1 = math.inf y1 = math.inf x2 = (-math.inf) y2 = (-math.inf) for pos in area: if pos[0] < x1: x1 = pos[0] if pos[1] < y1: y1 = pos[1] if pos[0] > x2: x2 = pos[0] if pos[1] > y2: y2 = pos[1] return [x1, y1, x2, y2]
def test_infinity_and_nan_constants(self): # inf wasn't added to the math module until 3.5. try: inf = math.inf except AttributeError: inf = float("inf") self.assertEqual(cmath.inf.real, inf) self.assertEqual(cmath.inf.imag, 0.0) self.assertEqual(cmath.infj.real, 0.0) self.assertEqual(cmath.infj.imag, inf) self.assertTrue(math.isnan(cmath.nan.real)) self.assertEqual(cmath.nan.imag, 0.0) self.assertEqual(cmath.nanj.real, 0.0) self.assertTrue(math.isnan(cmath.nanj.imag)) # Check consistency with reprs. self.assertEqual(repr(cmath.inf), "inf") self.assertEqual(repr(cmath.infj), "infj") self.assertEqual(repr(cmath.nan), "nan") self.assertEqual(repr(cmath.nanj), "nanj")
def __init__(self, query: str, before_context: str = '', after_context: str = '', max_translations: int = 1, budget: TranslationBudget = None): self.query = query self.before_context = before_context self.after_context = after_context self.max_translations = max_translations self.budget = budget if self.budget is None: self.budget = TranslationBudget( time=math.inf, money=math.inf, )
def hello(): data = request.get_json() source_language, target_language = data['source_language'], data['target_language'] if (source_language, target_language) not in translators: create_translator(source_language, target_language) query = TranslationQuery( before_context=data['before_context'] if 'before_context' in data else '', query=data['query'] if 'query' in data else '', after_context=data['after_context'] if 'after_context' in data else '', max_translations=data['max_translations'] if 'max_translations' in data else 10, budget=TranslationBudget( money=data['budget']['money'] if ('budget' in data and 'money' in data['budget']) else math.inf, time=data['budget']['time'] if ('budget' in data and 'time' in data['budget']) else math.inf ) ) translator = translators[(source_language, target_language)] response = translator.translate(query) return Response(response.to_json(), mimetype='text/json')
def query(self, idx, l, r, a, b): #query(1, 1, N, a, b) for query max of [a,b] if self.flag[idx] == True: self.st[idx] = self.lazy[idx] self.flag[idx] = False if l != r: self.lazy[self.left(idx)] = self.lazy[idx] self.lazy[self.right(idx)] = self.lazy[idx] self.flag[self.left(idx)] = True self.flag[self.right(idx)] = True if r < a or l > b: return -math.inf if l >= a and r <= b: return self.st[idx] mid = (l+r)//2 q1 = self.query(self.left(idx),l,mid,a,b) q2 = self.query(self.right(idx),mid+1,r,a,b) return max(q1,q2)
def __init__(self, a: Point, b: Point, precision: int=PRECISION) -> None: x_diff = round(a.x, precision) - round(b.x, precision) y_diff = round(a.y, precision) - round(b.y, precision) if x_diff < 0 or (x_diff == 0 and a.y < b.y): self._start, self._end = a, b else: self._start, self._end = b, a if a == b: self._slope = None self._offset = None elif x_diff == 0: self._slope = math.inf self._offset = self._start.x else: self._slope = y_diff / x_diff self._offset = self._start.y - (self._start.x * self._slope) self._precision = precision
def __init__(self, data, batch_size, num_steps=None, offset=0, epoch_num=None, transpose=False): self.i = 0 self.data = data self.max_length = data.shape[1] self.num_steps = self.max_length if num_steps is None else num_steps self._sentence_size = self.max_length // self.num_steps self.batch_size = batch_size self.max_epoch_num = math.inf if epoch_num is None else int(epoch_num) self.epoch_num = 0 self.offset = offset self.transpose = transpose self._epoch_size = self.data.shape[0] // batch_size * self.sentence_size self.embedding = data.ndim == 3 _shape = [self.num_steps, batch_size] if transpose else [batch_size, self.num_steps] if self.embedding: _shape.append(data.shape[2]) self._shape = _shape
def cost(order_num): min_coste = math.inf ware_optima = 0 inst = self.instance (cx,cy,cprods) = inst.orders[order_num] # Para cada warehouse for wn in range(len(warehouses)): (wx,wy,wprods) = warehouses[wn] # Comprueba que aquí esté todo for cosa in cprods: if cosa not in wprods: continue # Calcula el coste coste = dist((self.x,self.y), (wx,wy)) + dist((wx,wy), (cx,cy)) + 2 #+1 por el load y el delivery if (coste < min_coste): ware_optima = wn min_coste = coste return (coste, wn)
def topScores(channel, stat='exp', reverse=False): columns = ['name', 'exp', 'killed_ducks', 'shoots_fired'] if stat not in columns: columns.append(stat) table = getChannelPlayers(channel, columns=columns) players_list = [] for player in table: if checks.is_player_check(player): players_list.append(player) # print(str(player["name"]) + " | " + str(player["exp"]) + "|" + str(player["killed_ducks"])) try: # Retourne l'ensemble des joueurs dans une liste par stat # FIXME : le truc de l'infini est un moyen dégueulasse de ne pas avoir "None" devant 0 pour best_time # éventuellement on pourrait ne pas mettre les gens avec None dans le top (à faire dans exp.py) return sorted(players_list, key=lambda k: (k.get(stat, None) or (math.inf if stat == 'best_time' else 0)), reverse=not reverse) except: return []
def typical_height(csize: SizeClass, metric: bool=False) -> (float, float): """ Returns the minimum/maximum height range for a creature of the given size. Values are given in feet by default. """ size_to_height = { SizeClass.Fine: (0.0, 0.5), SizeClass.Diminutive: (0.5, 1), SizeClass.Tiny: (1, 2), SizeClass.Small: (2, 4), SizeClass.Medium: (4, 8), SizeClass.Large: (8, 16), SizeClass.Huge: (16, 32), SizeClass.Gargantuan: (32, 64), SizeClass.Colossal: (64, inf), } height = size_to_height[csize] return height * 0.3048 if metric else height
def typical_weight(csize: SizeClass, metric: bool=False) -> (float, float): """ Returns the minimum/maximum weight range for a creature of the given size. Values are given in pounds by default. """ size_to_weight = { SizeClass.Fine: (0.0, 0.125), SizeClass.Diminutive: (0.125, 1), SizeClass.Tiny: (1, 8), SizeClass.Small: (8, 60), SizeClass.Medium: (60, 500), SizeClass.Large: (500, 4000), SizeClass.Huge: (4000, 32000), SizeClass.Gargantuan: (32000, 250000), SizeClass.Colossal: (250000, inf), } weight = size_to_weight[csize] return weight * 0.45359237 if metric else weight
def isGameComplete(self) -> bool: if self.strikes == 3 or self.score >= self.maxScore: return True if self.turnCount > (self.endTurn or math.inf): return True return False
def __init__(self, s: float = 0, u: float = 0, o: float = 0): """Used list start analysis abstract domain representation. :param s: initial end of S-elements in list: should be a float in ``[0,1,2,..., inf]`` :param u: initial end of U-elements in list: should be a float in ``[0,1,2,..., inf]`` :param o: initial end of O-elements in list: should be a float in ``[0,1,2,..., inf]`` """ super().__init__() self._suo = OrderedDict([ (S, s), (U, u), (O, o) ])
def is_top(self) -> bool: return all(upper == inf for upper in self.suo.values())
def test_combine(self): # we assume that following test lists are 6 element long (implicit, not necessary to specify) a = UsedListStartLattice(6, 4, 0) # UUUUSS b = UsedListStartLattice(0, 2, 6) # UUOOOO ab = a.combine(b) self.assertEqual(list(ab.suo.values()), [0, 2, 6]) # UUOOOO a = UsedListStartLattice(6, 4, 0) # UUUUSS b = UsedListStartLattice(6, 2, 0) # UUSSSS ab = a.combine(b) self.assertEqual(list(ab.suo.values()), [6, 4, 0]) # UUUUSS a = UsedListStartLattice(4, 2, 0) # UUSSNN b = UsedListStartLattice(0, 2, 5) # UUOOON ab = a.combine(b) self.assertEqual(list(ab.suo.values()), [0, 2, 5]) # UUOOON a = UsedListStartLattice(0, 5, 0) # UUUUUN b = UsedListStartLattice(0, 2, 5) # UUOOON ab = a.combine(b) self.assertEqual(list(ab.suo.values()), [0, 2, 5]) # UUOOON # we assume that following test lists are infinite long a = UsedListStartLattice(inf, 2, 0) # UUSSSS... b = UsedListStartLattice(0, inf, 0) # UUUUUU... ab = a.combine(b) self.assertEqual(list(ab.suo.values()), [0, inf, 0]) # UUUUUU... a = UsedListStartLattice(0, inf, 0) # UUUUUU... b = UsedListStartLattice(0, 0, inf) # OOOOOO... ab = a.combine(b) self.assertEqual(list(ab.suo.values()), [0, 0, inf]) # OOOOOO...
def nan2inf(f): return inf if isnan(f) else f
def __init__(self, size): assert size % 2 == 0, "The size of a CDBM has to be even!" self._size = size self._m = [] for i in range(size): row = [inf] * min((i + 2) // 2 * 2, size) self._m.append(row)
def is_top(self) -> bool: return self.lower == -inf and self.upper == inf
def _widening(self, other: 'IntervalLattice') -> 'IntervalLattice': """``[a, b] ? [c, d] = [(c < a? -oo : a), (b < d? +oo : b)]``.""" lower = self.lower upper = self.upper if other.lower < self.lower: lower = -inf if self.upper < other.upper: upper = inf return self.replace(IntervalLattice(lower, upper)) # arithmetic operations
def __repr__(self): if self.is_bottom(): return "?" elif self.is_top(): return "?" else: res = [] # represent unary constraints first for var in self.variables: lower = - self[PLUS, var, MINUS, var] // 2 upper = self[MINUS, var, PLUS, var] // 2 if lower < inf and upper < inf: res.append(f"{lower}?{var.name}?{upper}") elif lower < inf: res.append(f"{lower}?{var.name}") elif upper < inf: res.append(f"{var.name}?{upper}") # represent binary constraints second, do not repeat identical inequalities for i, var1 in enumerate(self.variables): for j, var2 in enumerate(self.variables): if i > j: c = self[MINUS, var1, PLUS, var2] if c < inf: res.append(f"{var1.name}+{var2.name}?{c}") c = self[MINUS, var1, MINUS, var2] if c < inf: res.append(f"{var1.name}-{var2.name}?{c}") c = self[PLUS, var1, PLUS, var2] if c < inf: res.append(f"-{var1.name}+{var2.name}?{c}") c = self[PLUS, var1, MINUS, var2] if c < inf: res.append(f"-{var1.name}-{var2.name}?{c}") return ", ".join(res)
def top(self): for key in self.dbm.keys(): self.dbm[key] = inf return self
def is_top(self) -> bool: return all([isinf(b) for k, b in self.dbm.items() if k[0] != k[1]]) # check all inf, ignore diagonal for check
def forget(self, var: VariableIdentifier): # close first to not lose implicit constraints about other variables self.close() # forget binary constraints for index in self.binary_constraints_indices(sign1=None, var1=var): self[index] = inf # forget unary constraints self[PLUS, var, MINUS, var] = inf self[MINUS, var, PLUS, var] = inf
def _expected_result(self): initial = re.compile('INITIAL:?\s*(?P<state>.*)') state = re.compile('STATE:?\s*(?P<state>.*)') loop = re.compile('LOOP:?\s*(?P<state>.*)') final = re.compile('FINAL:?\s*(?P<state>.*)') for token in tokenize.tokenize(io.BytesIO(self.source.encode('utf-8')).readline): if token.type == tokenize.COMMENT: comment = token.string.strip("# ") initial_match = initial.match(comment) state_match = state.match(comment) loop_match = loop.match(comment) final_match = final.match(comment) if initial_match: result = initial_match.group('state') line = -inf # -inf for a precondition yield line, result if state_match: result = state_match.group('state') line = token.start[0] yield line, result if loop_match: result = loop_match.group('state') line = -token.start[0] # negative line number for a loop invariant yield line, result if final_match: result = final_match.group('state') line = inf # inf for a postcondition yield line, result
def test_init(self): self.assertFalse(IntervalLattice().is_bottom()) self.assertTrue(IntervalLattice().is_top()) self.assertFalse(IntervalLattice(0, 1).is_bottom()) self.assertFalse(IntervalLattice(0, 1).is_top()) self.assertEqual(IntervalLattice(upper=2), IntervalLattice(-inf, 2)) self.assertEqual(IntervalLattice(lower=3), IntervalLattice(3, inf)) self.assertTrue(IntervalLattice(1, 0).is_bottom()) self.assertFalse(IntervalLattice(1, 0).is_top())
def make_qq_unstratified(variants, include_qq): neglog10_pvals = sorted((v.neglog10_pval for v in variants), reverse=True) rv = {} if include_qq: rv['qq'] = compute_qq(neglog10_pvals) rv['count'] = len(neglog10_pvals) rv['gc_lambda'] = {} for perc in ['0.5', '0.1', '0.01', '0.001']: gc = gc_value_from_list(neglog10_pvals, float(perc)) if math.isnan(gc) or abs(gc) == math.inf: print('WARNING: got gc_value {!r}'.format(gc)) else: rv['gc_lambda'][perc] = round_sig(gc, 5) return rv
def round_sig(x, digits): if x == 0: return 0 elif abs(x) == math.inf or math.isnan(x): raise ValueError("Cannot round infinity or NaN") else: log = math.log10(abs(x)) digits_above_zero = int(math.floor(log)) return round(x, digits - 1 - digits_above_zero)
