Fast mutable expressions

[ctrekker]

The amount of memory allocations currently required for manipulating expressions in proof algorithms is absolutely rediculous. Expression immutability allows for some insurance as to the validity of the variables and operations sets, which contain the recursively used variables and operations of a tree respectively, which helps tremendously for speeding up other algorithms. Fields like this will require propagating updates on all parents of a modified expression tree.