During the check for inductive invariant, we were previously trying to push lemmas to the next level one by one.
Now, we attempt to push them in batches, gradually dropping those that cannot be pushed to the next level.
We use activation literals to track which lemmas we already showed cannot be pushed to disable them from further considerations. We basically simulate check-sat-assuming, which OpenSMT does not support yet, with push and pop.
The idea is the following:
We maintain a record of all active lemmas, which could still be pushed.
At each iteration, we try to push all active lemmas. If this is not possible, we obtain a model, a counterexample-to-induction (CTI). We iterate over all active lemmas and disable those that are falsified by this model (we actually maintain the list of negation of lemmas, so we check if the negations are true in the model).
We update the activation literals to disable falsified lemmas from further consideration and repeat the whole process.
The process stops when we successfully push all remaining active lemmas or if we disable all lemmas.
This had overall very positive effect on both LIA-Lin and LIA-nonlin benchmarks.
blishko
commented
1 year ago
During the check for inductive invariant, we were previously trying to push lemmas to the next level one by one. Now, we attempt to push them in batches, gradually dropping those that cannot be pushed to the next level.
We use activation literals to track which lemmas we already showed cannot be pushed to disable them from further considerations. We basically simulate
check-sat-assuming, which OpenSMT does not support yet, withpushandpop. The idea is the following: We maintain a record of all active lemmas, which could still be pushed. At each iteration, we try to push all active lemmas. If this is not possible, we obtain a model, a counterexample-to-induction (CTI). We iterate over all active lemmas and disable those that are falsified by this model (we actually maintain the list of negation of lemmas, so we check if the negations are true in the model). We update the activation literals to disable falsified lemmas from further consideration and repeat the whole process. The process stops when we successfully push all remaining active lemmas or if we disable all lemmas.This had overall very positive effect on both LIA-Lin and LIA-nonlin benchmarks.