keep the constraints unchanged after creating a new cterm

[Stevengre]

No description provided.

[Stevengre]

@PetarMax Here is the fastest way to solve the disordered problem for CSubst.

k/pyk/src/pyk/kcfg/minimize.py

Lines 76 to 110 in c8d0bee

	def lift_split_edge(self, b_id: NodeIdLike) -> None:
	"""Lift a split up an edge directly preceding it.
	`A --M steps--> B --[cond_1, ..., cond_N]--> [C_1, ..., C_N]` becomes
	`A --[cond_1, ..., cond_N]--> [A #And cond_1 --M steps--> C_1, ..., A #And cond_N --M steps--> C_N]`.
	Node `B` is removed.
	Args:
	b_id: The identifier of the central node `B` of the structure `A --> B --> [C_1, ..., C_N]`.
	Raises:
	AssertionError: If the structure in question is not in place.
	AssertionError: If any of the `cond_i` contain variables not present in `A`.
	"""
	# Obtain edge `A -> B`, split `[cond_I, C_I | I = 1..N ]`
	a_to_b = single(self.kcfg.edges(target_id=b_id))
	a = a_to_b.source
	split_from_b = single(self.kcfg.splits(source_id=b_id))
	ci, csubsts = list(split_from_b.splits.keys()), list(split_from_b.splits.values())
	# Ensure split can be lifted soundly (i.e., that it does not introduce fresh variables)
	assert (
	len(split_from_b.source_vars.difference(a.free_vars)) == 0
	and len(split_from_b.target_vars.difference(split_from_b.source_vars)) == 0 # <-- Can we delete this check?
	)
	# Create CTerms and CSubsts corresponding to the new targets of the split
	new_cterms = [csubst(a.cterm) for csubst in csubsts]
	# Remove the node `B`, effectively removing the entire initial structure
	self.kcfg.remove_node(b_id)
	# Create the nodes `[ A #And cond_I | I = 1..N ]`.
	ai: list[NodeIdLike] = [self.kcfg.create_node(cterm).id for cterm in new_cterms]
	# Create the edges `[A #And cond_1 --M steps--> C_I | I = 1..N ]`
	for i in range(len(ai)):
	self.kcfg.create_edge(ai[i], ci[i], a_to_b.depth, a_to_b.rules)
	# Create the split `A --[cond_1, ..., cond_N]--> [A #And cond_1, ..., A #And cond_N]
	self.kcfg.create_split_by_nodes(a.id, ai)

Take the above function as an example. line 101 should create a cterm with ordered constraints that the new constraints locates at the end of all the constraints.

k/pyk/src/pyk/cterm/cterm.py

Lines 348 to 352 in c8d0bee

	def apply(self, cterm: CTerm) -> CTerm:
	"""Apply this `CSubst` to the given `CTerm` (instantiating the free variables, and adding the constraints)."""
	config = self.subst(cterm.config)
	constraints = [self.subst(constraint) for constraint in cterm.constraints] + list(self.constraints)
	return CTerm(config, constraints)

But even the line 351 gives a correct order for the CTerm, the line 352 will re-sort the constraints after calling __init__.

k/pyk/src/pyk/kcfg/kcfg.py

Lines 755 to 760 in c8d0bee

	def create_node(self, cterm: CTerm) -> KCFG.Node:
	node = KCFG.Node(self._node_id, cterm)
	self._node_id += 1
	self._nodes[node.id] = node
	self._created_nodes.add(node.id)
	return node

What makes this situation harder to tackle is that the = in line 759 will call __init__ by default, which makes the sort_constraints flag useless.

[tothtamas28]

I think there's a copy-paste error here: even if sort_constraints=True, the constraints won't be sorted.

[Stevengre]

@tothtamas28 Yes, it's an issue that I don't know how to solve it. Because the following code will call CTerm.__init__ by default and make the previous order-keeping efforts useless. Do you have any suggestions for it? And why should we sort the constraints, btw?

k/pyk/src/pyk/kcfg/kcfg.py

Line 758 in c8d0bee

self._nodes[node.id] = node

[tothtamas28]

I'm not familiar with the context of this change. But my point is, instead of

def _normalize_constraints(constraints: Iterable[KInner], sort_constraints: bool = True) -> tuple[KInner, ...]:
    if sort_constraints:
        constraints = normalize_constraints(constraints)
        # constraints = sorted(normalize_constraints(constraints), key=CTerm._constraint_sort_key)
    else:
        constraints = normalize_constraints(constraints)

you could have

def _normalize_constraints(constraints: Iterable[KInner]) -> tuple[KInner, ...]:
    constraints = normalize_constraints(constraints)

[Stevengre]

Thank you! I want to refactor the function this way. But I'm not sure if there is any other applications / functions relying on the sorted function. Do you think it's safe to just remove the sorted?

[tothtamas28]

One thing I can think of where the constraints being sorted is useful is for equality checking between CTerm-s. I'm not sure if it's a common use case in the prover though.

Just to make sure, please check the history of this piece of code. Then we'll have a better idea of why constraints are sorted in the first place.

[Stevengre]

I think the sorted function is introduced by Petar in this PR. What's your suggesions? @PetarMax