search

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/
Apache License 2.0
16 stars 3 forks source link

Localisation of non-quantifier dependencies #64

Open kiranandcode opened 3 months ago

kiranandcode commented 3 months ago

Is there some way to identify dependencies on non-quantifier terms in a z3 file?

To clarify what I mean, I have this simple SMT Query (in boogie form for simplicity):

axiom (forall x y z :: {length(x), length(y), empty(z)}
                          (non_empty(x) || non_empty(y)) == non_empty(append(x,y)));

axiom (forall x :: {non_empty(x)} non_empty(x) == (1 <= length(x)));

axiom (empty(null));

procedure foo(x : Seq, y : Seq)
     requires non_empty(x);
     requires non_empty(y); 
     ensures non_empty(append(x,y)); {
}

So the point is that the key axiom (the first one) has a trigger that can only be activated by a term that is produced by two irrelevant axioms -- the second axiom and the third axiom.

By using the axiom-profiler, I can identify that the second axiom is used and which part of the source file is used (by the qid), but I don't know how to recover the location of the third axiom because it is not a quantified expression:

This is the resulting graph on the online gui: image the enode e11 is corresponds to the term that was needed to prove unsat, but there is no metadata associated with it that would allow me to infer which line in the source it corresponds to.

Is this information recoverable from the smt log file?