Adding reordering rule to the Spec

Opening this issue to keep track of this missing rule. We had decided to add it to the standard but it was not added at that time. I will put in a PR if I have the time.

The reorder rule described informally:

======== reorder

i1. F1 ... j. F2 where set representation of F1 and F2 are the same and the number of literals in C2 is the same of that of C1.

assigned to @Lachnitt and @hjsc

added todo-specification label

Is this supported by Carcara and Isabelle?

It is by Isabelle

I am trying to understand the informal description you gave above. First, I assume "F1" and "C1" (F2, C2) are the same clause. could F1 be

a \lor b \lor c \lor c

and F2 is

a \lor b \lor b \lor c

Both have the same number of literals, and the same set representation. However, this is not what I would normally expect from a reordering rule.

The description Hanna wrote is the same as the one we have for the corresponding cvc5 rule in CPC. As you point out, this is not what we should expect of this rule. :) I think I'm the one who wrote that, and I got it wrong.

I think it'd suffice to say that they have the same multi-set representation, right? The intended semantics is that the premise and the conclusion are the same clause modulo reordering the literals.

Yeah multi-set representation is the right notion here. I will implement the rule in the spec, and I can also fix the cpc comment.

Yes, I just copied it. Thanks @hjsc

mentioned in commit 5d615575

Seems like I did this in the spec a while ago and never pushed. CPC left.

removed todo-specification label

I think this is done.

closed