Wanted smart definition of a comparing predicate on compound propositional terms

General
1

I have found a predicate named seq_compare defined below is drastically effective for a problem, which I didn’t expected so much befere.
This is a sample of the ordering.

   a==b < a->b < xor(a, b) < a*b < a+b < a < -a

However the current definition looks not smart. Maybe I should write term_expansion/2 which expands a list

[==/2, ->/2, xor/2, */2, +/2, -/1]

to the target definition.

Is there smarter way than term_expansion ? Use of the compare predicate is so busy in my application, comparative time efficiency is required. Thanks for suggestions in the future.

seq_compare(=, X, X):-!.
seq_compare(C, ==(X, Y), ==(U, V)):-!, seq_compare(C, X, Y, U, V).
seq_compare(C, ->(X, Y), ->(U, V)):-!, seq_compare(C, X, Y, U, V).
seq_compare(C, +(X, Y), +(U, V)):-!, seq_compare(C, X, Y, U, V).
seq_compare(C, *(X, Y), *(U, V)):-!, seq_compare(C, X, Y, U, V).
seq_compare(C, xor(X, Y), xor(U, V)):-!, seq_compare(C, X, Y, U, V).
seq_compare(<, ==(_, _), _):-!.
seq_compare(>, _, ==(_, _)):-!.
seq_compare(<, ->(_, _), _):-!.
seq_compare(>, _, ->(_, _)):-!.
seq_compare(<, xor(_, _), _):-!.
seq_compare(>, _, xor(_, _)):-!.
seq_compare(<, *(_, _), _)	:-!.
seq_compare(>, _, *(_, _))	:-!.
seq_compare(<, +(_, _), _)	:-!.
seq_compare(>, _, +(_, _))	:-!.
seq_compare(C, -(X), -(Y))	:-!, seq_compare(C, X, Y).
seq_compare(C, X, -(Y))	:-!,
	(	X = Y ->  C = (<)
	;	seq_compare(C, X, Y)
	).
seq_compare(C, -(X), Y):-!,
	(	X = Y ->  C = (>)
	;	seq_compare(C, X, Y)
	).
seq_compare(C, X, Y):- compare(C, X, Y).

% seq_compare/5
seq_compare(C, X, Y, U, V):-
	seq_compare(C0, X, U),
	(	C0 = (=) -> seq_compare(C, Y, V)
	;	C = C0
	).
2

Is this related to your recent resolution theorem prover post here?
You possibly heed the ordering to order some resolution theorem proofs?
Now I stepped over this interesting paper, which picks up the idea as well:

Generating Extended Resolution Proofs with a BDD-Based SAT Solver
Randal E. Bryant et al. - March 29, 2023
https://arxiv.org/pdf/2105.00885.pdf

Whereas I understood your resolution theorem prover post,
I could npt yet digest the paper. But a further find of the paper is
that they takle the examples Parity-9750 and Urquhart-Li-38.

Did you try these examples with your ZDD solver? Or with some
modification you are working on?

3

No. It’s not related at least for now. Rather I am getting interested in extended use of atoms in ZDD, which so far I have been unaware of. In short slogan, “use zdd (engine) as a parser”, which is behind the post of mine. Ordering on atoms is a key to parse with ZDD, and I wanted to smart specification of the ordering to be expanded the current compare/3.

BTW, I was told for the sake of most of readers not to keep thread long, and I agree. Thanks for paying attention for my post.