diff --git a/vehicle/src/Vehicle/Backend/Queries/PostProcessing.hs b/vehicle/src/Vehicle/Backend/Queries/PostProcessing.hs index bdf6aed85..ea1f2d809 100644 --- a/vehicle/src/Vehicle/Backend/Queries/PostProcessing.hs +++ b/vehicle/src/Vehicle/Backend/Queries/PostProcessing.hs @@ -8,7 +8,6 @@ import Control.Monad.Reader (MonadReader (..)) import Control.Monad.State (get) import Data.Bifunctor (Bifunctor (..)) import Data.Foldable (foldlM) -import Data.HashMap.Strict qualified as HashMap import Data.LinkedHashMap qualified as LinkedHashMap import Data.List (sort, sortOn) import Data.List.NonEmpty (NonEmpty (..)) @@ -96,7 +95,7 @@ reconstructNetworkTensorVars :: reconstructNetworkTensorVars GlobalCtx {..} solutions = do let networkApplicationInfos = snd <$> LinkedHashMap.toList networkApplications let networkVariables = Set.fromList $ concatMap (\r -> [inputVariable r, outputVariable r]) networkApplicationInfos - let allTensorVars = filter (\(var, _) -> var `Set.member` networkVariables) $ HashMap.toList tensorVariableInfo + let allTensorVars = filter (\(var, _) -> var `Set.member` networkVariables) $ Map.toList tensorVariableInfo let networkTensorVars = sortOn fst allTensorVars let mkStep (var, TensorVariableInfo {..}) = ReconstructTensor OtherVariable tensorVariableShape var elementVariables return $ foldr (\v -> (mkStep v :)) solutions networkTensorVars @@ -282,7 +281,7 @@ compileQueryVariables :: compileQueryVariables globalCtx compileVariable metaNetworkApps assertions = do -- Compute the set of new input and output variables let initialState = IndexingState mempty mempty mempty - let tensorVars = HashMap.toList (tensorVariableInfo globalCtx) + let tensorVars = sortOn fst $ Map.toList (tensorVariableInfo globalCtx) let usedNetworkTensorVars = Set.fromList $ concatMap (\x -> [inputVariable x, outputVariable x]) metaNetworkApps let compileVars = compileTensorVariable compileVariable (globalBoundVarCtx globalCtx) usedNetworkTensorVars indexingState@IndexingState {..} <- foldlM compileVars initialState tensorVars diff --git a/vehicle/src/Vehicle/Backend/Queries/UserVariableElimination/Core.hs b/vehicle/src/Vehicle/Backend/Queries/UserVariableElimination/Core.hs index 6fbe290c8..f0e1a3f2a 100644 --- a/vehicle/src/Vehicle/Backend/Queries/UserVariableElimination/Core.hs +++ b/vehicle/src/Vehicle/Backend/Queries/UserVariableElimination/Core.hs @@ -1,3 +1,6 @@ +{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-} + +{-# HLINT ignore "Use fewer imports" #-} module Vehicle.Backend.Queries.UserVariableElimination.Core where import Control.DeepSeq (NFData) @@ -5,8 +8,6 @@ import Control.Monad.Reader (MonadReader (..)) import Control.Monad.State (MonadState (..), gets) import Data.Aeson (FromJSON, ToJSON) import Data.Bifunctor (Bifunctor (..)) -import Data.HashMap.Strict (HashMap) -import Data.HashMap.Strict qualified as HashMap (insert, lookup) import Data.LinkedHashMap (LinkedHashMap) import Data.LinkedHashMap qualified as LinkedHashMap import Data.List.NonEmpty qualified as NonEmpty @@ -70,7 +71,7 @@ data PropertyMetaData = PropertyMetaData data GlobalCtx = GlobalCtx { globalBoundVarCtx :: !(GenericBoundCtx Name), - tensorVariableInfo :: !(HashMap TensorVariable TensorVariableInfo), + tensorVariableInfo :: !(Map TensorVariable TensorVariableInfo), networkApplications :: !(LinkedHashMap NetworkApplication NetworkApplicationReplacement) } @@ -105,7 +106,7 @@ addUserVarToGlobalContext userVarName shape GlobalCtx {..} = do let newGlobalCtx = GlobalCtx { globalBoundVarCtx = addVectorVarToBoundVarCtx userVarName reducedUseVars globalBoundVarCtx, - tensorVariableInfo = HashMap.insert userVar variableInfo tensorVariableInfo, + tensorVariableInfo = Map.insert userVar variableInfo tensorVariableInfo, .. } (userVar, newGlobalCtx) @@ -168,8 +169,8 @@ addNetworkApplicationToGlobalCtx app@(networkName, _) networkInfo GlobalCtx {..} } let newTensorVariableInfo = - HashMap.insert inputVar inputVarInfo $ - HashMap.insert outputVar outputVarInfo tensorVariableInfo + Map.insert inputVar inputVarInfo $ + Map.insert outputVar outputVarInfo tensorVariableInfo let newGlobalCtx = GlobalCtx @@ -303,10 +304,10 @@ getTensorVariableShape var = do return (tensorVariableShape info) getRationalVariable :: (MonadState GlobalCtx m) => Lv -> m ElementVariable -getRationalVariable lv = do +getRationalVariable var = do ctx <- get - case HashMap.lookup lv (tensorVariableInfo ctx) of - Nothing -> return lv + case Map.lookup var (tensorVariableInfo ctx) of + Nothing -> return var Just info -> do let rvs = elementVariables info case rvs of @@ -315,7 +316,7 @@ getRationalVariable lv = do getTensorVariableInfo :: GlobalCtx -> TensorVariable -> TensorVariableInfo getTensorVariableInfo GlobalCtx {..} var = do - case HashMap.lookup var tensorVariableInfo of + case Map.lookup var tensorVariableInfo of Just info -> info Nothing -> developerError $ @@ -327,7 +328,7 @@ getReducedVariablesFor globalCtx var = elementVariables $ getTensorVariableInfo getReducedVariableExprFor :: (MonadState GlobalCtx m, MonadLogger m) => Lv -> m (Maybe (Value Builtin)) getReducedVariableExprFor var = do ctx <- get - return $ reducedVarExpr <$> HashMap.lookup var (tensorVariableInfo ctx) + return $ reducedVarExpr <$> Map.lookup var (tensorVariableInfo ctx) reduceTensorExpr :: GlobalCtx -> diff --git a/vehicle/tests/golden/compile/autoencoderError/Marabou.queries/identity-query1.txt.golden b/vehicle/tests/golden/compile/autoencoderError/Marabou.queries/identity-query1.txt.golden index dc944544a..15024edcb 100644 --- a/vehicle/tests/golden/compile/autoencoderError/Marabou.queries/identity-query1.txt.golden +++ b/vehicle/tests/golden/compile/autoencoderError/Marabou.queries/identity-query1.txt.golden @@ -3,6 +3,6 @@ // Metadata: // - Marabou query format version: unknown // - Vehicle version: 0.15.0+dev --x0 +y0 <= -0.1 -+x5 -y5 = 0.0 -+x6 -y6 = 0.0 \ No newline at end of file +-x0 +y2 <= -0.1 ++x5 -y0 = 0.0 ++x6 -y1 = 0.0 \ No newline at end of file diff --git a/vehicle/tests/golden/compile/autoencoderError/Marabou.queries/identity-query10.txt.golden b/vehicle/tests/golden/compile/autoencoderError/Marabou.queries/identity-query10.txt.golden index 453af3928..8aa5eec21 100644 --- a/vehicle/tests/golden/compile/autoencoderError/Marabou.queries/identity-query10.txt.golden +++ b/vehicle/tests/golden/compile/autoencoderError/Marabou.queries/identity-query10.txt.golden @@ -3,6 +3,6 @@ // Metadata: // - Marabou query format version: unknown // - Vehicle version: 0.15.0+dev -+x4 -y4 <= -0.1 -+x5 -y5 = 0.0 -+x6 -y6 = 0.0 \ No newline at end of file ++x4 -y6 <= -0.1 ++x5 -y0 = 0.0 ++x6 -y1 = 0.0 \ No newline at end of file diff --git a/vehicle/tests/golden/compile/autoencoderError/Marabou.queries/identity-query2.txt.golden b/vehicle/tests/golden/compile/autoencoderError/Marabou.queries/identity-query2.txt.golden index ae4ea882e..f94ba777f 100644 --- a/vehicle/tests/golden/compile/autoencoderError/Marabou.queries/identity-query2.txt.golden +++ b/vehicle/tests/golden/compile/autoencoderError/Marabou.queries/identity-query2.txt.golden @@ -3,6 +3,6 @@ // Metadata: // - Marabou query format version: unknown // - Vehicle version: 0.15.0+dev -+x0 -y0 <= -0.1 -+x5 -y5 = 0.0 -+x6 -y6 = 0.0 \ No newline at end of file ++x0 -y2 <= -0.1 ++x5 -y0 = 0.0 ++x6 -y1 = 0.0 \ No newline at end of file diff --git a/vehicle/tests/golden/compile/autoencoderError/Marabou.queries/identity-query3.txt.golden b/vehicle/tests/golden/compile/autoencoderError/Marabou.queries/identity-query3.txt.golden index f977c3f15..7dc194baf 100644 --- a/vehicle/tests/golden/compile/autoencoderError/Marabou.queries/identity-query3.txt.golden +++ b/vehicle/tests/golden/compile/autoencoderError/Marabou.queries/identity-query3.txt.golden @@ -3,6 +3,6 @@ // Metadata: // - Marabou query format version: unknown // - Vehicle version: 0.15.0+dev --x1 +y1 <= -0.1 -+x5 -y5 = 0.0 -+x6 -y6 = 0.0 \ No newline at end of file +-x1 +y3 <= -0.1 ++x5 -y0 = 0.0 ++x6 -y1 = 0.0 \ No newline at end of file diff --git a/vehicle/tests/golden/compile/autoencoderError/Marabou.queries/identity-query4.txt.golden b/vehicle/tests/golden/compile/autoencoderError/Marabou.queries/identity-query4.txt.golden index ee2c354ba..503097b07 100644 --- a/vehicle/tests/golden/compile/autoencoderError/Marabou.queries/identity-query4.txt.golden +++ b/vehicle/tests/golden/compile/autoencoderError/Marabou.queries/identity-query4.txt.golden @@ -3,6 +3,6 @@ // Metadata: // - Marabou query format version: unknown // - Vehicle version: 0.15.0+dev -+x1 -y1 <= -0.1 -+x5 -y5 = 0.0 -+x6 -y6 = 0.0 \ No newline at end of file ++x1 -y3 <= -0.1 ++x5 -y0 = 0.0 ++x6 -y1 = 0.0 \ No newline at end of file diff --git a/vehicle/tests/golden/compile/autoencoderError/Marabou.queries/identity-query5.txt.golden b/vehicle/tests/golden/compile/autoencoderError/Marabou.queries/identity-query5.txt.golden index 0b0cbd446..6287a43c3 100644 --- a/vehicle/tests/golden/compile/autoencoderError/Marabou.queries/identity-query5.txt.golden +++ b/vehicle/tests/golden/compile/autoencoderError/Marabou.queries/identity-query5.txt.golden @@ -3,6 +3,6 @@ // Metadata: // - Marabou query format version: unknown // - Vehicle version: 0.15.0+dev --x2 +y2 <= -0.1 -+x5 -y5 = 0.0 -+x6 -y6 = 0.0 \ No newline at end of file +-x2 +y4 <= -0.1 ++x5 -y0 = 0.0 ++x6 -y1 = 0.0 \ No newline at end of file diff --git a/vehicle/tests/golden/compile/autoencoderError/Marabou.queries/identity-query6.txt.golden b/vehicle/tests/golden/compile/autoencoderError/Marabou.queries/identity-query6.txt.golden index 88bd45c3a..fb7991d97 100644 --- a/vehicle/tests/golden/compile/autoencoderError/Marabou.queries/identity-query6.txt.golden +++ b/vehicle/tests/golden/compile/autoencoderError/Marabou.queries/identity-query6.txt.golden @@ -3,6 +3,6 @@ // Metadata: // - Marabou query format version: unknown // - Vehicle version: 0.15.0+dev -+x2 -y2 <= -0.1 -+x5 -y5 = 0.0 -+x6 -y6 = 0.0 \ No newline at end of file ++x2 -y4 <= -0.1 ++x5 -y0 = 0.0 ++x6 -y1 = 0.0 \ No newline at end of file diff --git a/vehicle/tests/golden/compile/autoencoderError/Marabou.queries/identity-query7.txt.golden b/vehicle/tests/golden/compile/autoencoderError/Marabou.queries/identity-query7.txt.golden index b7b20f550..e7b1f8699 100644 --- a/vehicle/tests/golden/compile/autoencoderError/Marabou.queries/identity-query7.txt.golden +++ b/vehicle/tests/golden/compile/autoencoderError/Marabou.queries/identity-query7.txt.golden @@ -3,6 +3,6 @@ // Metadata: // - Marabou query format version: unknown // - Vehicle version: 0.15.0+dev --x3 +y3 <= -0.1 -+x5 -y5 = 0.0 -+x6 -y6 = 0.0 \ No newline at end of file +-x3 +y5 <= -0.1 ++x5 -y0 = 0.0 ++x6 -y1 = 0.0 \ No newline at end of file diff --git a/vehicle/tests/golden/compile/autoencoderError/Marabou.queries/identity-query8.txt.golden b/vehicle/tests/golden/compile/autoencoderError/Marabou.queries/identity-query8.txt.golden index 2082ad746..cd520d858 100644 --- a/vehicle/tests/golden/compile/autoencoderError/Marabou.queries/identity-query8.txt.golden +++ b/vehicle/tests/golden/compile/autoencoderError/Marabou.queries/identity-query8.txt.golden @@ -3,6 +3,6 @@ // Metadata: // - Marabou query format version: unknown // - Vehicle version: 0.15.0+dev -+x3 -y3 <= -0.1 -+x5 -y5 = 0.0 -+x6 -y6 = 0.0 \ No newline at end of file ++x3 -y5 <= -0.1 ++x5 -y0 = 0.0 ++x6 -y1 = 0.0 \ No newline at end of file diff --git a/vehicle/tests/golden/compile/autoencoderError/Marabou.queries/identity-query9.txt.golden b/vehicle/tests/golden/compile/autoencoderError/Marabou.queries/identity-query9.txt.golden index cd789fd2b..edccf120e 100644 --- a/vehicle/tests/golden/compile/autoencoderError/Marabou.queries/identity-query9.txt.golden +++ b/vehicle/tests/golden/compile/autoencoderError/Marabou.queries/identity-query9.txt.golden @@ -3,6 +3,6 @@ // Metadata: // - Marabou query format version: unknown // - Vehicle version: 0.15.0+dev --x4 +y4 <= -0.1 -+x5 -y5 = 0.0 -+x6 -y6 = 0.0 \ No newline at end of file +-x4 +y6 <= -0.1 ++x5 -y0 = 0.0 ++x6 -y1 = 0.0 \ No newline at end of file diff --git a/vehicle/tests/golden/compile/autoencoderError/Marabou.queries/identity.vcl-plan.golden b/vehicle/tests/golden/compile/autoencoderError/Marabou.queries/identity.vcl-plan.golden index b8578827f..5fde003d8 100644 --- a/vehicle/tests/golden/compile/autoencoderError/Marabou.queries/identity.vcl-plan.golden +++ b/vehicle/tests/golden/compile/autoencoderError/Marabou.queries/identity.vcl-plan.golden @@ -77,12 +77,12 @@ [ 13, "encode₀[output]!0", - "y5" + "y0" ], [ 14, "encode₀[output]!1", - "y6" + "y1" ], [ 15, @@ -107,27 +107,27 @@ [ 19, "decode₀[output]!0", - "y0" + "y2" ], [ 20, "decode₀[output]!1", - "y1" + "y3" ], [ 21, "decode₀[output]!2", - "y2" + "y4" ], [ 22, "decode₀[output]!3", - "y3" + "y5" ], [ 23, "decode₀[output]!4", - "y4" + "y6" ] ], "reconstructionSteps": [ @@ -359,12 +359,12 @@ [ 13, "encode₀[output]!0", - "y5" + "y0" ], [ 14, "encode₀[output]!1", - "y6" + "y1" ], [ 15, @@ -389,27 +389,27 @@ [ 19, "decode₀[output]!0", - "y0" + "y2" ], [ 20, "decode₀[output]!1", - "y1" + "y3" ], [ 21, "decode₀[output]!2", - "y2" + "y4" ], [ 22, "decode₀[output]!3", - "y3" + "y5" ], [ 23, "decode₀[output]!4", - "y4" + "y6" ] ], "reconstructionSteps": [ @@ -641,12 +641,12 @@ [ 13, "encode₀[output]!0", - "y5" + "y0" ], [ 14, "encode₀[output]!1", - "y6" + "y1" ], [ 15, @@ -671,27 +671,27 @@ [ 19, "decode₀[output]!0", - "y0" + "y2" ], [ 20, "decode₀[output]!1", - "y1" + "y3" ], [ 21, "decode₀[output]!2", - "y2" + "y4" ], [ 22, "decode₀[output]!3", - "y3" + "y5" ], [ 23, "decode₀[output]!4", - "y4" + "y6" ] ], "reconstructionSteps": [ @@ -923,12 +923,12 @@ [ 13, "encode₀[output]!0", - "y5" + "y0" ], [ 14, "encode₀[output]!1", - "y6" + "y1" ], [ 15, @@ -953,27 +953,27 @@ [ 19, "decode₀[output]!0", - "y0" + "y2" ], [ 20, "decode₀[output]!1", - "y1" + "y3" ], [ 21, "decode₀[output]!2", - "y2" + "y4" ], [ 22, "decode₀[output]!3", - "y3" + "y5" ], [ 23, "decode₀[output]!4", - "y4" + "y6" ] ], "reconstructionSteps": [ @@ -1205,12 +1205,12 @@ [ 13, "encode₀[output]!0", - "y5" + "y0" ], [ 14, "encode₀[output]!1", - "y6" + "y1" ], [ 15, @@ -1235,27 +1235,27 @@ [ 19, "decode₀[output]!0", - "y0" + "y2" ], [ 20, "decode₀[output]!1", - "y1" + "y3" ], [ 21, "decode₀[output]!2", - "y2" + "y4" ], [ 22, "decode₀[output]!3", - "y3" + "y5" ], [ 23, "decode₀[output]!4", - "y4" + "y6" ] ], "reconstructionSteps": [ @@ -1487,12 +1487,12 @@ [ 13, "encode₀[output]!0", - "y5" + "y0" ], [ 14, "encode₀[output]!1", - "y6" + "y1" ], [ 15, @@ -1517,27 +1517,27 @@ [ 19, "decode₀[output]!0", - "y0" + "y2" ], [ 20, "decode₀[output]!1", - "y1" + "y3" ], [ 21, "decode₀[output]!2", - "y2" + "y4" ], [ 22, "decode₀[output]!3", - "y3" + "y5" ], [ 23, "decode₀[output]!4", - "y4" + "y6" ] ], "reconstructionSteps": [ @@ -1769,12 +1769,12 @@ [ 13, "encode₀[output]!0", - "y5" + "y0" ], [ 14, "encode₀[output]!1", - "y6" + "y1" ], [ 15, @@ -1799,27 +1799,27 @@ [ 19, "decode₀[output]!0", - "y0" + "y2" ], [ 20, "decode₀[output]!1", - "y1" + "y3" ], [ 21, "decode₀[output]!2", - "y2" + "y4" ], [ 22, "decode₀[output]!3", - "y3" + "y5" ], [ 23, "decode₀[output]!4", - "y4" + "y6" ] ], "reconstructionSteps": [ @@ -2051,12 +2051,12 @@ [ 13, "encode₀[output]!0", - "y5" + "y0" ], [ 14, "encode₀[output]!1", - "y6" + "y1" ], [ 15, @@ -2081,27 +2081,27 @@ [ 19, "decode₀[output]!0", - "y0" + "y2" ], [ 20, "decode₀[output]!1", - "y1" + "y3" ], [ 21, "decode₀[output]!2", - "y2" + "y4" ], [ 22, "decode₀[output]!3", - "y3" + "y5" ], [ 23, "decode₀[output]!4", - "y4" + "y6" ] ], "reconstructionSteps": [ @@ -2333,12 +2333,12 @@ [ 13, "encode₀[output]!0", - "y5" + "y0" ], [ 14, "encode₀[output]!1", - "y6" + "y1" ], [ 15, @@ -2363,27 +2363,27 @@ [ 19, "decode₀[output]!0", - "y0" + "y2" ], [ 20, "decode₀[output]!1", - "y1" + "y3" ], [ 21, "decode₀[output]!2", - "y2" + "y4" ], [ 22, "decode₀[output]!3", - "y3" + "y5" ], [ 23, "decode₀[output]!4", - "y4" + "y6" ] ], "reconstructionSteps": [ @@ -2615,12 +2615,12 @@ [ 13, "encode₀[output]!0", - "y5" + "y0" ], [ 14, "encode₀[output]!1", - "y6" + "y1" ], [ 15, @@ -2645,27 +2645,27 @@ [ 19, "decode₀[output]!0", - "y0" + "y2" ], [ 20, "decode₀[output]!1", - "y1" + "y3" ], [ 21, "decode₀[output]!2", - "y2" + "y4" ], [ 22, "decode₀[output]!3", - "y3" + "y5" ], [ 23, "decode₀[output]!4", - "y4" + "y6" ] ], "reconstructionSteps": [ diff --git a/vehicle/tests/golden/compile/issue86/Marabou.queries/p3-query1.txt.golden b/vehicle/tests/golden/compile/issue86/Marabou.queries/p3-query1.txt.golden index 13d264e89..220cbf1c4 100644 --- a/vehicle/tests/golden/compile/issue86/Marabou.queries/p3-query1.txt.golden +++ b/vehicle/tests/golden/compile/issue86/Marabou.queries/p3-query1.txt.golden @@ -3,6 +3,6 @@ // Metadata: // - Marabou query format version: unknown // - Vehicle version: 0.15.0+dev --x1 +x0 = 0.0 +-x0 +x1 = 0.0 y0 <= 0.0 y1 <= 0.0 \ No newline at end of file diff --git a/vehicle/tests/golden/compile/issue86/Marabou.queries/p3-query2.txt.golden b/vehicle/tests/golden/compile/issue86/Marabou.queries/p3-query2.txt.golden index eac57fa18..864be65f6 100644 --- a/vehicle/tests/golden/compile/issue86/Marabou.queries/p3-query2.txt.golden +++ b/vehicle/tests/golden/compile/issue86/Marabou.queries/p3-query2.txt.golden @@ -3,6 +3,6 @@ // Metadata: // - Marabou query format version: unknown // - Vehicle version: 0.15.0+dev -x1 = 0.0 +x0 = 0.0 y0 <= 0.0 y1 >= 0.0 \ No newline at end of file diff --git a/vehicle/tests/golden/compile/issue86/Marabou.queries/p3.vcl-plan.golden b/vehicle/tests/golden/compile/issue86/Marabou.queries/p3.vcl-plan.golden index dad6ff92b..3b5464d5a 100644 --- a/vehicle/tests/golden/compile/issue86/Marabou.queries/p3.vcl-plan.golden +++ b/vehicle/tests/golden/compile/issue86/Marabou.queries/p3.vcl-plan.golden @@ -27,7 +27,7 @@ [ 3, "f₀[input]!0", - "x1" + "x0" ], [ 4, @@ -47,7 +47,7 @@ [ 7, "f₁[input]!0", - "x0" + "x1" ], [ 8, @@ -222,7 +222,7 @@ [ 3, "f₀[input]!0", - "x1" + "x0" ], [ 4, @@ -242,7 +242,7 @@ [ 7, "f₁[input]!0", - "x0" + "x1" ], [ 8,