How to update output range？

[ytsao]

Hi,

I'm currently using Marabou to develop my research project that is related to neural network verification.
I have a couple of questions in your implementation as follows;

1. After we perform any abstract interpretation-based approach, how to update/access the bounds for each neuron?
   Because I saw that there are different ways to provide the bound information, for example, inEngine.cpp, we can use inputQuery, _preprocessedQuery, _networkLevelReasoner or _tableau.
   First time, I just use inputQuery to be the argument in extractBounds(), similar with calculateBounds() in MarabouCore.cpp, but I didn't see any update in the output neurons, they are still remaining infinite bounds.
   Yet, I can obtain the updated output bounds from both _networkLevelReasoner and _tableau.
   Therefore, I'm curious if that should be using either _networkLevelReasoner or _tableau to have update to date bound information?

2. What is the difference between inputQuery and _preprocessedQuery? Is that to distinguish the property before and after pre-process step? Will _preprocessedQuery be always having update to date information? or just right after pre-process step only?

Thank you in advance.

Best regards,
Yi-Nung