Fix creating 1st-hit sis (ebbe77d8) · Commits · Marek Chalupa / slowbeast

slowbeast/bse/bself.py

+7 −14

Original line number	Original line	Diff line number	Diff line
	@@ -630,30 +630,27 @@ class BSELFChecker(BaseBSE):
	sets.append(tmp)		sets.append(tmp)
	return sets		return sets

	def _match_included_indsets(self, isets, sets):		def _match_included_indsets(self, isets, sets, E):
	create_set = self.create_set		create_set = self.create_set
	# replace every set in 'sets' with an inductive set that we already have		# replace every set in 'sets' with an inductive set that we already have
	# if the IS already includes the set		# if the IS already includes the set
	newsets = []		newsets = []
	union_matched = self.options.union_matched		union_matched = self.options.union_matched
	for s in sets:		for s in sets:
			# gather the sets that subsume 's' and are disjunctive with unsafe
			# states
	cov = [		cov = [
	I for I in isets if intersection(I.I, s).is_empty() and I.I.contains(s)		I for I in isets if intersection(E, s).is_empty() and I.includes(s)
	]		]
	if cov:		if cov:
	dbg("Matched stored inductive sequences")		dbg("Matched stored inductive sequences")
	S = create_set() if union_matched else None		S = create_set() if union_matched else None
	for I in cov:		for I in cov:
	if union_matched:		if union_matched:
	# and not S.contains(I.I):		# todo: could the inclusion check weaken inferring relations from path condition? Probably yes.
	# todo: could the inclusion check break inferring relations from path condition? Probably yes.
	S.add(I.I)		S.add(I.I)
	else:		else:
	newsets.append(I.I)		newsets.append(I.I)
	# remove the matched set from inductive sets
	# l = len(isets)
	# isets.remove(I)
	# assert l - 1 == len(isets), "Did not pop the element"
	newsets.append(S)		newsets.append(S)
	else:		else:
	newsets.append(s)		newsets.append(s)
	@@ -673,7 +670,7 @@ class BSELFChecker(BaseBSE):
	if isets is None:		if isets is None:
	return sets		return sets

	return self._match_included_indsets(isets, sets)		return self._match_included_indsets(isets, sets, E)

	def initial_sets_from_is(self, E, L):		def initial_sets_from_is(self, E, L):
	# get the inductive sets that we have created for this header.		# get the inductive sets that we have created for this header.
	@@ -688,15 +685,11 @@ class BSELFChecker(BaseBSE):
	dbg("Checking inductive sets that we have")		dbg("Checking inductive sets that we have")
	sets = []		sets = []
	included_sets = []		included_sets = []
	# newisets = []
	for I in isets:		for I in isets:
	if intersection(I.I, E).is_empty():		if intersection(I.I, E).is_empty():
	sets.append(I.I)		sets.append(I.I)
	if exit_sets and I.I.contains_any(*exit_sets):		if exit_sets and I.includes_any(*exit_sets):
	included_sets.append(I.I)		included_sets.append(I.I)
	# else:
	# newisets.append(I)
	# self.inductive_sets[L.header()] = newisets

	# use the sets that include some of the sets created for exit sets		# use the sets that include some of the sets created for exit sets
	if included_sets:		if included_sets:

slowbeast/bse/inductiveset.py

+6 −0

Original line number	Original line	Diff line number	Diff line
	@@ -41,5 +41,11 @@ class InductiveSet:
	# intersection(complement(self.I), elem).is_empty()		# intersection(complement(self.I), elem).is_empty()
	return self.cI.is_sat(elem.as_expr()) is False		return self.cI.is_sat(elem.as_expr()) is False

			def includes_any(self, *elems):
			if isinstance(elem, InductiveSet):
			elem = elem.I
			is_sat = self.cI.is_sat
			return any(is_sat(elem.as_expr()) is False, elems)

	def __repr__(self):		def __repr__(self):
	return self.I.__repr__()		return self.I.__repr__()