Constraining or conditionally enabling axioms inside a verification condition

[kiranandcode]

Hiya, I have a file that has a lot of quantified axioms -- I'm trying to speed up my verification by trying to restrict the instantiations of axioms per sub-branch of a larger query.

So far, the approach I have been using is to try and use triggers to do this:

For example, the following axiom

(assert (forall ((x Seq)) (! (>= (seq#length x) 0) :pattern (((seq#length x))) ))

into

(declare-fun ax1 (Bool) Bool)
(assert (forall ((x Seq) (b Bool)) (! (>= (seq#length x) 0) :pattern (((seq#length x) (ax1 b))))

and then within the sub branch in which this axiom should be available, I ensure that it is assumed to be true (=> (ax1 true) ...)

This seems to be effective at disabling axioms -- if an axiom is neccesary for a proof to go through, then the guard has to be present for the solver to return SAT, however, Z3 still seems to slow down as unneccesary axioms are added, even if their axiom guards are not assumed, and I see no significant improvement over just submitting everything to z3 as is.

In other words, I am currently trying to guide z3's search process and constrain it to only look at a particular subset of axioms and their instantiations, but it seems like this encoding doesn't seem to be effective in that regard, as it seems like the search process considers all axioms even though I have tried to indicate that they are not needed.

[NikolajBjorner]

1. the truth value of ax1 is not taken into account when triggering the pattern.
2. the axiom may be instantiated in one case and then the instantiation remains as a clause. Recall the instantiation creates a clause of the form (=> (forall x phi[x]) phi[t]).