Deduplicate equivalent expressions
Suppose we wanted to generate all expressions containing at most 2 of + and −. We might have a list like this:
a + b + c b + c + a
a + b - c b + c - a
a - b + c b - c + a
a - b - c b - c - a
a + c + b c + a + b
a + c - b c + a - b
a - c + b c - a + b
a - c - b c - a - b
b + a + c c + b + a
b + a - c c + b - a
b - a + c c - b + a
b - a - c c - b - a
There is a lot of repetition here. It surely isn't necessary to include all of a + b + c, a + c + b, b + a + c, b + c + a, c + a + b, and c + b + a, since they all mean the same thing. This can be deduced from knowing that, for any x and y, x + y is the same as y + x.
Similarly, b + a - c and a - c + b are equivalent. To deduce this, one must know that, for any x and y, x - y is the same as x + (-y).
Let's assume the following:
[1]: a + b == b + a
[2]: a - b == a + -b
Then, we can deduce that b + a - c and a - c + b are equivalent:
start: b + a - c
b + a + -c by 2
a + b + -c by 1
a + -c + b by 1
end: a - c + b by 2
Therefore, they are the same. After performing similar proofs, we are left with the list:
a + b + c
a + b - c
a - b + c
a - b - c
b - a + c
b - c - a
c - b - a
Definition of an expression
An expression can be described as:
variable = "a" | "b" | "c" | ... | "y" | "z";
digit = "0" | "1" | "2" | ... | "8" | "9";
number = digit . digit*;
operator = "!" | "#" | "$" | "%" | "&" | "*" | "+"
| "~" | "-" | "." | "/" | ":" | ";" | "<"
| "=" | ">" | "?" | "@" | "^" | "_" | "`"
| "|";
data = number | variable;
subexpr = data | operator* . data;
expression = subexpr
| subexpr . operator . expression;
Where | suggests alternatives, . suggests concatenation (with potential whitespace around each operand), * suggests "0 or more times", and " is a string literal.
x + y, j * i - 3, u & 4 * 2 < ~4, q % ~*^t and r are all expressions.
You should assume all operators are left-associative.
Definition of assumptions
An assumption is a pair of expressions said to be equivalent. This means one can be transformed into the other. When performing a transformation using an assumption, one replaces all the appropriate variables and maintains the numbers as they are. (These "variables" can also be sub-expressions, which is any expression not using an operator in the assumption.)
For example, if the assumption is !a == a + 5, then one can transform t + 5 into !t and 3 + 5 into !3.
Another example: if the assumption is a + b == a * b @ b, then 5 + 2 can become 5 * 2 @ 2 and z * 3 @ 3 can become z + 3, but z * 4 @ a cannot be reduced further using this rule.
One last example: if the assumption is a < b == a, then 1 + 3 & 5 < 2 * 3 + 6 would become 1 + 3 & 5, and 1 + 2 < x + y < 7 $ q would become 1 + 2, since it would be equivalent to (1 + 2) < (x + y) < (7 $ q), which is thus 1 + 2.
If either side of the assumption is a single variable, numbers are excluded from this assumption. E.g., the assumption a == 3 would only apply to variables.
Expression equality
Two expressions are equal if they can be proven to be the same. Variables must be the same for each expression; for example, a + b is not by default the same as b + c.
Challenge
Your task is to remove "duplicate" expressions given some assumptions. You can use any unambiguous symbol or method, including taking a pair of strings, to represent an expression. The expressions remaining in the result do not necessarily have to be in the set, but must be equivalent by the given assumptions. E.g., if you have a + b - c and b - c + a in the input, you can have -c + b + a represent these in the resultant set. You should try each equation in the order that it's given to you (to simulate "precedence").
The input consists of a list of assumptions and a list of input expressions. The input expressions can be an array or container of strings or string pointers, or in any way standard to your language. (E.g., for C, one should expect null-terminated strings.) The input format must be consistent for all runs.
The output can be a list representation (as is standard to your language), can be separated by newlines (\r, \n, and \r\n are acceptable), or separated by commas. The output format must be consistent between runs.
This is a code-golf, so the shortest program in bytes wins.
Test cases
Every output is merely an example, and is not the only valid output.
Assumptions: { e1 == e2, e3 == e4, ... eN-1 == eN }
Input: { expr1, expr2, ... exprN }
Output: { expr1, expr2, ..., exprK }
Assumptions: { "a + b" == "b + a" }
Input: { "3 + 4", "4 + 3", "5 * a", "a + 2", "2 * a", "a * 5", "a + b", "2 + a" }
Output: { "3 + 4", "5 * a", "a + 2", "2 * a", "a * 5", "a + b" }
Assumptions: { "a + 0" == "a", "a * 1" == "a", "a * b" == "b * a", "a + b" == "b + a" }
Input: { "1 * 2 * 3", "3 * 2 + 0", "1 + 2 + 3" }
Output: { "1 * 2 * 3", "1 + 2 + 3" }
OR: { "2 * 3", "1 + 2 + 3" }
Assumptions: { "~a" == "a ~ a" }
Input: { "~z", "z ~ z", "~a", "~~a", "a ~ a ~ a ~ a" }
Output: { "~a", "~z", "~~a" }
Assumptions: { "a + b" == "0" }
Input: { "x + y", "0", "3 + y + a + v + k", "75", "4 + 2" }
Output: { "0", "75" }
Assumptions: { }
Input: { "x + y", "x + y", "y + x", "3", "3 ! 3" }
Output: { "x + y", "y + x", "3", "3 ! 3" }
Assumptions: { "j" == "3" }
Input: { "v + t", "z", "q", "q + r + t", "4 + 2" }
Output: { "v + t", "z", "q + r + t", "4 + 2" }
Assumptions: { "a" == "b" }
Input: { "a", "b + c", "e % t", "q & t", "!3", "z" }
Output: { "a", "b + c", "e % t", "q & t", "!3" }
Assumptions: { "1 & 0" == "0", "1 & 1" == "1", "0 & 0" == "0", "a & b" == "b & a", "0 ? a : b" == "b", "1 ? a : b" == "a" }
Input: { "1 & 1 & 0", "j & k", "y & z", "z & y", "1 & 0 ? k & j : 0" }
Output: { "0", "j & k", "y & z" }
