fix bug in dnc evaluate

[wu-haoze]

Fixing issue #330.
The issue is that when some worker finds a SAT instance and returns a mapping from variable indices to assignments, it is using variable indices after preprocessing. This is because the worker itself does not preprocess the query but directly take in the preprocessed query, so it does not store the mapping from original variable index to the new index.
This information is stored in DnCManager._baseEngine. Therefore, we copy the tableau state of DnCManager._engineWithSATAssignment into DnCManager._baseEngine and extract solutions from the latter object, instead of the former object.

[kjulian3]

We need to add tests for DNC mode in Maraboupy. I tried adding one just now, and ran into an unexpected error. Here's the test I was trying to run:

# Tests Marabou's DNC option
import pytest
from .. import Marabou
import os
import numpy as np

# Global settings
OPT = Marabou.createOptions(verbosity=2, dnc=True, numWorkers=2) # Turn off printing, turn on DNC with two workers
TOL = 1e-6                                                       # Set tolerance for checking Marabou evaluations
NETWORK_FOLDER = "../../resources/nnet/acasxu"                   # Folder for test networks

def test_dnc_unsat():
    """
    Test the 1,1 experimental ACAS Xu network. 
    Evaluate a simple local robustness property for a network with DNC mode activated
    """
    filename =  "ACASXU_experimental_v2a_1_1.nnet"
    filename = os.path.join(os.path.dirname(__file__), NETWORK_FOLDER, filename)
    network = Marabou.read_nnet(filename)
    
    # Local robustness input constraint
    centerPoint = [-0.2454504737724233, -0.4774648292756546, 0.0, -0.3181818181818182, 0.0]
    for var, val in zip(network.inputVars[0], centerPoint):
        network.setLowerBound(var, val - 0.002)
        network.setUpperBound(var, val + 0.002)

    # Solve with no output constraint
    # Should return SAT, and vals should be a populated dictionary
    vals, stats = network.solve(options = OPT, filename = "", verbose=True)
    assert len(vals) > 0

I created a new file with this code in it (maraboupy/test/test_dnc.py), and calling pytest via pytest test/test_dnc.py from the maraboupy directory will produce the Marabou Error, code 6.