Reimplement conversion modulo AC

[fblanqui]

This PR reimplements conversion modulo AC without enforcing terms to be in AC-canonical form.
This is much more efficient but may not work with any rewrite system.
It seems to work well with:

• the theory ACI = AC + Idempotence used in max-suc algebra for universe levels,
• the theory of commutative groups AG = AC + Inverse + Neutral used in linear arithmetic.
  This fixes the issue The modifier associative commutative can be slow with large terms #1200.

Main changes in term.ml and eval.ml:

• do not declare the type term as private and remove the mk_* construction functions, except mk_Arrow
  (it reduces checking time of holide by 7%)
• sym type: add field sym_rstrat: red_strat = Outermost (default) | Innermost (for symbols defined by matching on AC symbols); with Innermost, in a function symbol application, arguments are normalized before trying to apply a rule
• add type side = Left | Right for the rewrite tactic and AC symbols (bool arguments are replaced by arguments of type side)

Other changes:

• Term: add type side = Left | Right, used in properties and rewrite tactic
• Term: remove property Assoc
• when declaring a symbol as associative commutative, a side must be given now
• LibTerm: add contains_ac_sym
• List: add rev_append2
• Logger.set_debug_in: permute arguments and use string argument instead of char

TODO:

• do not declare term as private and remove functions mk_
• handle commutativity alone, fix tests/OK/ac.lp
• fix compute
• in applications, compare arguments from left to right
• try improve eq_modulo further
• update CHANGES
• update doc, add links to examples
• Logger.set_debug: permute arguments?

[fblanqui]

@NotBad4U Could you please try this PR on some other examples for linear arithmetic ?

[fblanqui]

Be careful that I changed the ordering: arguments are now compared from left to right. So, you need to permute the arguments of var.

[NotBad4U]

I experimented the new AC on my previous test here. It is very fast now! Before we could only compute AC with ~20 variables, and I remember it took >5min for 23 variables. In the test, I can compute with 40 variables very quickly. I will try this feature on an SMT solver bench.

[NotBad4U]

@fblanqui I tried the new AC on my benchmarks and it is swift. I can do a computation with 500 variables, and it is faster than my current solution that compute the normal form without AC and reduces a term with a context varmap for none-interpreted term. In my current solution, the normalisation is fast but the calculation is very slow on large expression.
In my opinion, it is the multiple access to the context varmap that slow down the calculation. I still need to do more tests.

However, I have a strange behavior that I can even replicate in my gist. If I compute with only the ⇧ (reify function) then the term is reduced into cst 0.

compute (⇧ 
    (
        (T1 + T2 + T3)
        + (
            (— 1) * (T1 + T2  + T3)
        )
    )
);

However, if compose ⇧ with the interpretation function ⇓ such as:

compute ⇓ (⇧ 
    (
        (T1 + T2 + T3)
        + (
            (— 1) * (T1 + T2  + T3)
        )
    )
);

Then I got the result ((1 * T1) + ((1 * T2) + (1 * T3))) + ((-1 * T1) + ((-1 * T2) + (-1 * T3))). It looks like the ⇧ has not been applied. Do you have an idea why?

I updated the gist and the calculation is L127 if you want to reproduce on your side. Maybe we can add this gist in the folder /test/OK.

[NotBad4U]

It also does not work with my proof by reflexivity on reordering the pivot.
In the code below, the algebra that represents Clause does not compute an AC form.
The constructor P has an arity of 1. Does this PR normalize only symbols with an arity of 2?

symbol ℂ: TYPE;
symbol P: Prop → ℂ;
right associative commutative symbol ⊔: ℂ → ℂ → ℂ; notation ⊔ infix right 2;
symbol ⬓: ℂ;

symbol F: Clause → ℂ;

rule F ($x ⟇ $xs) ↪ (P $x) ⊔ (F $xs)
with F ▩ ↪ ⬓
;

sequential symbol  ⩦: ℂ → ℂ → 𝔹; notation ⩦ infix 11;
rule (P $x) ⩦ (P $x) ↪ true
with (P $x) ⩦ (P $y) ↪ false
with ($x ⊔ $xs) ⩦ ($y ⊔ $ys) ↪ ($x ⩦ $y) Stdlib.Bool.and ($xs ⩦ $ys)
with ⬓ ⩦ ⬓ ↪ true
with ⬓ ⩦ (P _) ↪ false
with (P _) ⩦ ⬓ ↪ false
with (_ ⊔ _) ⩦ ⬓ ↪ false
with ⬓ ⩦ (_ ⊔ _) ↪ false
with (P _) ⩦ (_ ⊔ _) ↪ false
with (_ ⊔ _) ⩦ (P _) ↪ false;

compute ((P b ⊔ P a ⊔ ⬓)  ⩦  (P a ⊔ P b ⊔ ⬓)); // No AC computed here

[fblanqui]

@NotBad4U https://gist.github.com/NotBad4U/1638cd3787b8e5284c7030ca8a8534ec now works with the last commits. Could you please provide me with a complete file to test the example with Clause too?

[NotBad4U]

Thanks a lot for your work! I will give you an example as soon as possible!