viperproject / axiom-profiler-2

The axiom profiler for exploring and visualizing SMT solver quantifier instantiations (made via E-matching).
https://viperproject.github.io/axiom-profiler-2/
8 stars 3 forks source link

Term generalisation with shared parser #16

Closed oskari1 closed 5 months ago

oskari1 commented 6 months ago

In this version, I'm just adding the generalised terms to the end of Terms::terms. I have not yet implemented the hash-map for avoiding duplicate generalised terms so it's not particularly memory-efficient yet. Also, the buckets for the edges are still just based on the quantifiers of the end-nodes. EDIT: hash-map for avoiding duplicate generalised terms has now been implemented EDIT 2: the buckets for the edges are now also based on the trigger used for the instantiation