feat: De-Bruijn Style Nameless Bound Variables

[jrosain]

Description

Simplify internal representation of formulas by using De Bruijn's variables (i.e., bound variables are now integers). It greatly simplifies the operations we want to do on formulas and terms, e.g., instantiation and substitution, as well as the representation of quantifiers (that do not have multiple variables anymore).

I've also tried to remove unused stuff that complexified the base structure of terms and formulas. I couldn't get rid of the formula field in the metavariables though. I've also factorized the operations on n-ari and binary formulas, like it has been done for the quantifiers. Note that as we don't preserve the names anymore, a meta is always called Mi where i is its unique index. A bound variable is called Xi.

I've temporarily disabled the cache of the metavariables, introducing hashconsing will fix this.

PR dependencies

• feat: remove invasive index in formulas and terms #71
• Allow unification between terms #78

Test-suite update

Updated the expected output of the .out files with the de bruijn bound variables.