Problem with MarabouNetwork.loadQuery()

[darioguidotti]

Hello,

I have tried to use MarabouNetwork.loadQuery() in order to load my
verification query but it gives me the following error:

~/Marabou-master/maraboupy/MarabouNetwork.py in loadQuery(self, filename, verbose, timeout)
220 """
221 #ipq = self.getMarabouQuery()
--> 222 ipq = MarabouCore.loadQuery(filename)
223 vals, stats = MarabouCore.solve(ipq, filename, timeout=0)
224 if verbose:

AttributeError: module 'maraboupy.MarabouCore' has no attribute 'loadQuery'

Do you have any suggestions?
Thank you!

[kjulian3]

@clazarus, I think you added loadQuery to maraboupy in #61. Have you tested that method? It looks like loadQuery was never added to MarabouCore.cpp like saveQuery was, so I think a fix is needed. Do you have time to look at this? I can try to fix this if not.

[darioguidotti]

Hello,

Thank you for your help!

Right now loadQuery appears to return a "MarabouCore.InputQuery": how can I use it alongside a
MarabouNetworkNNet to check the property of the network?

Thank you again!

[kjulian3]

The old loadQuery would try to load the query and solve it, so the function name was misleading. Now, loadQuery returns a MarabouCore.InputQuery object, which can be solved by calling Marabou.solve_query. So now if you have a serialized inputQuery file, you can load and solve it with

from maraboupy import Marabou
ipq = Marabou.load_query(filename)
vals, stats = Marabou.solve_query(ipq)

Are you checking an nnet file, or a serialized inputQuery file?

[darioguidotti]

Hi,

Actually I need to check the union of both, i.e., I have a network loaded using .nnet file and then I have a .txt file with the properties of interest encoded following the Marabou specifications. I am not sure how I can check the network against the property as in the command line example:

./build/Marabou resources/nnet/acasxu/ACASXU_experimental_v2a_2_7.nnet resources/properties/acas_property_3.txt

Thank you for your time!

[kjulian3]

The property file you've written is different than a serialized inputQuery file. The save/load query functions contain all of the equations, constraints, and upper/lower bounds for all variables in a format that's not made to be easily readable. The serialized inputQuery files can be useful for debugging issues but are not meant to be written by hand.

To use the nnet file and property file, the easiest way is to use the compiled C++ program (./build/Marabou) instead of using the python interface by calling (from the Marabou directory)

./build/Marabou path/to/nnet_file.nnet path/to/property_file.txt

If you want to use the python interface, you would do something like

from maraboupy import Marabou
network = Marabou.read_nnet(nnet_file)
inputVars = network.inputVars[0][0]
outputVars = network.outputVars[0]
network.setLowerBound(inputVars[0],-10.0)
network.setUpperBound(inputVars[0], 10.0)
network.setLowerBound(inputVars[1],-10.0)
network.setUpperBound(inputVars[1], 10.0)
network.setLowerBound(outputVars[1], 194.0)
network.setUpperBound(outputVars[1], 210.0)

There isn't support yet for parsing property files in python, but you can still specify the same constraints in python using the above method. After the constraints are set up, you can solve the query with
vals, stats = network.solve("marabou.log")

[darioguidotti]

Ok, thank you for your reply!