Compare two SMT ASTs

[JonathanSalwan]

Done with the next v0.3 (#226, #93). The operator == is now available to compare two ASTs. This operator go through an AST and computes a checksum recursively.

As we must keep a bit of logic when we compare two nodes, we have two kinds of hash routines.

hash routine 1

When we don't care about the order. e.g: (add a b c) is equal to (add b c a).

hash = kind * number_of_childs * (forall child in childs, hash(child)).

e.g with bvadd:

 114     double smtAstBvaddNode::hash(void) {
 115       double h = this->kind * this->childs.size();
 116       for (triton::uint32 index = 0; index < this->childs.size(); index++)
 117         h = h * this->childs[index]->hash();
 118       return h;
 119     }

hash routine 2

When the order is important. e.q (div a b) is not equal to (div b a)

hash = kind * number_of_childs * (forall child in childs, hash(child)^index).

e.g with bvudiv

 845     double smtAstBvudivNode::hash(void) {
 846       double h = this->kind * this->childs.size();
 847       for (triton::uint32 index = 0; index < this->childs.size(); index++)
 848         h = h * std::pow(this->childs[index]->hash(), index+1);
 849       return h;
 850     }

[JonathanSalwan]

However, we still must perform more tests to evaluate collisions.