From a9ca7d60ee82f10c2dadcefd64ef1e6b717192fb Mon Sep 17 00:00:00 2001 From: MatthewDaggitt Date: Thu, 12 Dec 2024 18:34:44 +0800 Subject: [PATCH] Collapse warnings in vector properties into single warning (#871) * Collapse warnings in vector properties into single warning * Fix GHC 8.X compatability --- ChangeLog.md | 2 + vehicle/src/Vehicle/Compile/Print/Warning.hs | 83 +++++++++++++------ vehicle/src/Vehicle/Prelude/Warning.hs | 72 ++++++++-------- .../issue712/MarabouQueries.err.golden | 3 +- .../issue765/MarabouQueries.err.golden | 3 +- .../simple-arithmetic/Marabou.err.golden | 3 +- .../Marabou.err.golden | 3 +- .../compile/simple-foreach/Marabou.err.golden | 8 +- .../simple-fourierMotzkin/Marabou.err.golden | 12 ++- .../compile/simple-if/Marabou.err.golden | 6 +- .../compile/simple-tensor/Marabou.err.golden | 3 +- .../compile/simple-vector/Marabou.err.golden | 3 +- .../missingVerifier/Marabou.err.golden | 3 +- .../golden/warning/trivial/Marabou.err.golden | 2 +- 14 files changed, 125 insertions(+), 81 deletions(-) diff --git a/ChangeLog.md b/ChangeLog.md index 260bb17ee..73dd7d349 100644 --- a/ChangeLog.md +++ b/ChangeLog.md @@ -8,6 +8,8 @@ * Improved the ordering of constraints in generated query files. +* When multiple similar warnings are thrown at different indices of the same property vector (i.e. properties of type `Vector Bool n`), they are now collapsed into a single warning. + ## Version 0.15 * Added functions `min` and `max` over rationals. diff --git a/vehicle/src/Vehicle/Compile/Print/Warning.hs b/vehicle/src/Vehicle/Compile/Print/Warning.hs index f6264ecb2..b4550e07c 100644 --- a/vehicle/src/Vehicle/Compile/Print/Warning.hs +++ b/vehicle/src/Vehicle/Compile/Print/Warning.hs @@ -1,11 +1,18 @@ {-# OPTIONS_GHC -Wno-orphans #-} +{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-} + +{-# HLINT ignore "Use <$>" #-} module Vehicle.Compile.Print.Warning where +import Data.Bifunctor (Bifunctor (..)) import Data.List (sortOn) import Data.List.NonEmpty (NonEmpty, sort) -import Data.Set qualified as Set +import Data.List.NonEmpty qualified as NonEmpty +import Data.Map qualified as Map +import Data.Tuple (swap) import Vehicle.Data.Assertion (UnderConstrainedVariableStatus, prettyUnderConstrainedVariable) +import Vehicle.Data.Tensor (TensorIndices) import Vehicle.Prelude import Vehicle.Prelude.Warning import Vehicle.Verify.Core @@ -25,19 +32,14 @@ instance Pretty SummarisedCompileWarning where <+> quotePretty status <+> "without needing to call the verifier. This usually indicates a fault with either the" <+> "specification or any external datasets used." - UnderSpecifiedProblemSpaceVariablesSummary propertyAddress unsolvedVars -> do - let varsDoc = concatWith (\u v -> u <> "," <+> v) (fmap quotePretty (Set.toList unsolvedVars)) - let pluralisedVarsDoc - | length unsolvedVars == 1 = "variable" <+> varsDoc <+> "is" - | otherwise = "variables" <+> varsDoc <+> "are" - + UnderSpecifiedProblemSpaceVariablesSummary _ propertyName unsolvedVars -> do "In property" - <+> quotePretty propertyAddress - <+> "the quantified" - <+> pluralisedVarsDoc - <+> "not always directly related to the input or output of a network." - <+> "This is frequently indicative of a bug in the specification." - UnsoundStrictOrderConversionsSummary queryFormatID propertyAddress _ -> + <+> quotePretty propertyName + <+> "there are quantified variables that not always directly related to the input or output of a network." + <+> "This is frequently indicative of a bug in the specification. These variables are:" + <> line + <> prettyObjectsAndTensorIndicesList prettyVariables propertyName unsolvedVars + UnsoundStrictOrderConversionsSummary queryFormatID _ propertyAddress _ -> "In property" <+> quotePretty propertyAddress <> ", at least one of the generated queries were found" @@ -56,18 +58,18 @@ instance Pretty SummarisedCompileWarning where <> line <> line <> "See https://github.com/vehicle-lang/vehicle/issues/74 for further details." - AllConstantNetworkInputVariablesSummary _ propertyAddress queryIDs -> - "In property" - <+> quotePretty propertyAddress - <> ", in" - <+> prettyQueryIDs queryIDs - <+> "all network inputs were fixed to be constants." - <+> "Unfortunately there is a known bug in Marabou that it sometimes erroneously returns" - <+> "'unsat' for these type of queries." + AllConstantNetworkInputVariablesSummary _ _ propertyName queryIDs -> + "In some of the queries generated by property" + <+> quotePretty propertyName + <+> "all network inputs were fixed to be constants." + <+> "Unfortunately there is a known bug in Marabou that it sometimes erroneously returns" + <+> "'unsat' for these type of queries. The queries are:" + <> line + <> prettyObjectsAndTensorIndicesList prettyQueryIDs propertyName queryIDs <> line <> line <> "See https://github.com/NeuralNetworkVerification/Marabou/issues/670 for details." - UnboundedNetworkInputVariablesSummary queryFormat propertyAddress varsByQueryID -> + UnboundedNetworkInputVariablesSummary queryFormat _ propertyAddress varsByQueryID -> "In property" <+> quotePretty propertyAddress <> ", the following network input variables do not always have both" @@ -85,7 +87,36 @@ instance Pretty SummarisedCompileWarning where <> line <> indent 2 (vsep $ dotDotList 5 $ fmap prettyUnderConstrainedVariable vars) -prettyQueryIDs :: NonEmpty QueryID -> Doc a -prettyQueryIDs ids = - (if length ids == 1 then "query" else "queries") - <+> prettyNonEmptyList (fmap pretty (sort ids)) +prettyObjects :: (Ord a, Pretty a) => Bool -> Doc b -> Doc b -> NonEmpty a -> Doc b +prettyObjects quote single plural ids = + (if length ids == 1 then single else plural) + <+> prettyNonEmptyList (fmap (if quote then quotePretty else pretty) (sort ids)) + +prettyQueryIDs :: NonEmpty QueryID -> Doc b +prettyQueryIDs = prettyObjects False "query" "queries" + +prettyVariables :: NonEmpty Name -> Doc a +prettyVariables = prettyObjects True "variable" "variables" + +prettyTensorIndices :: PropertyName -> NonEmpty TensorIndices -> Maybe (Doc b) +prettyTensorIndices name indices + | indices == [[]] = Nothing + | otherwise = do + let addresses = fmap (quotePretty . PropertyAddress (-1) name) indices + Just $ prettyNonEmptyList addresses + +prettyObjectsAndTensorIndices :: (NonEmpty a -> Doc b) -> PropertyName -> (NonEmpty a, NonEmpty TensorIndices) -> Doc b +prettyObjectsAndTensorIndices prettyObject name (ids, indices) = do + let indicesDoc = prettyTensorIndices name indices + prettyObject ids <> maybe "" (" in" <+>) indicesDoc + +prettyObjectsAndTensorIndicesList :: (Ord a) => (NonEmpty a -> Doc b) -> PropertyName -> NonEmpty (a, TensorIndices) -> Doc b +prettyObjectsAndTensorIndicesList prettyObject name objectsAndIndices = do + -- Singleton.nonEmpty doesn't exist until base 4.15 + let nonEmptySingleton x = [x] + -- First map by indices that share the same objects + let indicesMap = Map.fromListWith (<>) (NonEmpty.toList $ fmap (second nonEmptySingleton) objectsAndIndices) + -- Then find the objects that share the same queries + let objectsMap = Map.fromListWith (<>) $ fmap (second nonEmptySingleton . swap) (Map.toList indicesMap) + let finalGroups = fmap swap $ Map.toList objectsMap + indent 2 (vsep (fmap (\x -> "-" <+> prettyObjectsAndTensorIndices prettyObject name x) finalGroups)) diff --git a/vehicle/src/Vehicle/Prelude/Warning.hs b/vehicle/src/Vehicle/Prelude/Warning.hs index e6d5e4e26..f37af794c 100644 --- a/vehicle/src/Vehicle/Prelude/Warning.hs +++ b/vehicle/src/Vehicle/Prelude/Warning.hs @@ -6,17 +6,17 @@ module Vehicle.Prelude.Warning where import Data.List (sortBy) -import Data.List.NonEmpty (NonEmpty, sort) +import Data.List.NonEmpty (NonEmpty) import Data.Map (Map) import Data.Map qualified as Map (insertWith, singleton, toList, unionWith) import Data.Set (Set) -import Data.Set qualified as Set (singleton) import Data.Tuple (swap) import Vehicle.Compile.Context.Bound.Core import Vehicle.Data.Assertion import Vehicle.Data.Builtin.Core import Vehicle.Data.Builtin.Tensor import Vehicle.Data.Code.Value +import Vehicle.Data.Tensor (TensorIndices) import Vehicle.Prelude (Name) import Vehicle.Resource (ExternalResource) import Vehicle.Verify.Core @@ -36,10 +36,10 @@ data CompileWarning data SummarisedCompileWarning = UnusedResourcesSummary ExternalResource (Set Name) | TrivialPropertySummary PropertyAddress Bool - | UnderSpecifiedProblemSpaceVariablesSummary PropertyAddress (Set Name) - | UnsoundStrictOrderConversionsSummary QueryFormatID PropertyAddress Int - | AllConstantNetworkInputVariablesSummary QueryFormatID PropertyAddress (NonEmpty QueryID) - | UnboundedNetworkInputVariablesSummary QueryFormatID PropertyAddress [(NonEmpty QueryID, [(Name, UnderConstrainedVariableStatus)])] + | UnderSpecifiedProblemSpaceVariablesSummary PropertyID PropertyName (NonEmpty (Name, TensorIndices)) + | UnsoundStrictOrderConversionsSummary QueryFormatID PropertyID PropertyName Int + | AllConstantNetworkInputVariablesSummary QueryFormatID PropertyID PropertyName (NonEmpty (QueryID, TensorIndices)) + | UnboundedNetworkInputVariablesSummary QueryFormatID PropertyID PropertyName [(NonEmpty QueryID, [(Name, UnderConstrainedVariableStatus)])] -------------------------------------------------------------------------------- -- Combinable compile warnings @@ -48,10 +48,10 @@ type UnderConstrainedSignature = [(Name, UnderConstrainedVariableStatus)] data CombiningState = CombiningState { uniqueWarnings :: [SummarisedCompileWarning], - underSpecifiedProblemSpaceVars :: Map PropertyAddress (Set Name), - unsoundStrictnessConversions :: Map (QueryFormatID, PropertyAddress) Int, - allConstantNetworkInputVars :: Map (QueryFormatID, PropertyAddress) (NonEmpty QueryID), - unboundedNetworkInputs :: Map (QueryFormatID, PropertyAddress) (Map UnderConstrainedSignature (NonEmpty QueryID)), + underSpecifiedProblemSpaceVars :: Map (PropertyID, PropertyName) (NonEmpty (Name, TensorIndices)), + unsoundStrictnessConversions :: Map (QueryFormatID, PropertyID, PropertyName) Int, + allConstantNetworkInputVars :: Map (QueryFormatID, PropertyID, PropertyName) (NonEmpty (QueryID, TensorIndices)), + unboundedNetworkInputs :: Map (QueryFormatID, PropertyID, PropertyName) (Map UnderConstrainedSignature (NonEmpty QueryID)), inefficientTensorCode :: Map Name [(Builtin, NamedBoundCtx, Value TensorBuiltin)] } @@ -70,24 +70,25 @@ addWarningToState CombiningState {..} = \case { uniqueWarnings = TrivialPropertySummary r names : uniqueWarnings, .. } - UnderSpecifiedProblemSpaceVar property var -> + UnderSpecifiedProblemSpaceVar PropertyAddress {..} var -> CombiningState - { underSpecifiedProblemSpaceVars = Map.insertWith (<>) property (Set.singleton var) underSpecifiedProblemSpaceVars, + { underSpecifiedProblemSpaceVars = Map.insertWith (<>) (propertyID, propertyName) [(var, propertyIndices)] underSpecifiedProblemSpaceVars, .. } - UnsoundStrictOrderConversion queryFormat (propertyAddress, _queryID) -> + UnsoundStrictOrderConversion queryFormat (PropertyAddress {..}, _queryID) -> CombiningState - { unsoundStrictnessConversions = Map.insertWith (+) (queryFormat, propertyAddress) 1 unsoundStrictnessConversions, + { unsoundStrictnessConversions = Map.insertWith (+) (queryFormat, propertyID, propertyName) 1 unsoundStrictnessConversions, .. } - AllConstantNetworkInputVars queryFormat (propertyAddress, queryID) -> + AllConstantNetworkInputVars queryFormat (PropertyAddress {..}, queryID) -> CombiningState - { allConstantNetworkInputVars = Map.insertWith (<>) (queryFormat, propertyAddress) [queryID] allConstantNetworkInputVars, + { allConstantNetworkInputVars = + Map.insertWith (<>) (queryFormat, propertyID, propertyName) [(queryID, propertyIndices)] allConstantNetworkInputVars, .. } - UnboundedNetworkInputVariables queryFormat (propertyAddress, queryID) vars -> + UnboundedNetworkInputVariables queryFormat (PropertyAddress {..}, queryID) vars -> CombiningState - { unboundedNetworkInputs = Map.insertWith (Map.unionWith (<>)) (queryFormat, propertyAddress) (Map.singleton vars [queryID]) unboundedNetworkInputs, + { unboundedNetworkInputs = Map.insertWith (Map.unionWith (<>)) (queryFormat, propertyID, propertyName) (Map.singleton vars [queryID]) unboundedNetworkInputs, .. } @@ -97,36 +98,37 @@ groupWarnings warnings = stateToWarnings $ foldl addWarningToState emptyState wa stateToWarnings :: CombiningState -> [SummarisedCompileWarning] stateToWarnings CombiningState {..} = sortBy compareWarning $ - do - uniqueWarnings + uniqueWarnings <> fmap combineUnderSpecifiedProblemSpaceVars (Map.toList underSpecifiedProblemSpaceVars) <> fmap combineUnsoundStrictnessConversions (Map.toList unsoundStrictnessConversions) <> fmap combineAllConstantNetworkInputVars (Map.toList allConstantNetworkInputVars) <> fmap combineUnboundedNetworkInputVars (Map.toList unboundedNetworkInputs) -combineUnderSpecifiedProblemSpaceVars :: (PropertyAddress, Set Name) -> SummarisedCompileWarning -combineUnderSpecifiedProblemSpaceVars (property, vars) = UnderSpecifiedProblemSpaceVariablesSummary property vars +combineUnderSpecifiedProblemSpaceVars :: ((PropertyID, PropertyName), NonEmpty (Name, TensorIndices)) -> SummarisedCompileWarning +combineUnderSpecifiedProblemSpaceVars ((propertyID, property), vars) = UnderSpecifiedProblemSpaceVariablesSummary propertyID property vars -combineUnsoundStrictnessConversions :: ((QueryFormatID, PropertyAddress), Int) -> SummarisedCompileWarning -combineUnsoundStrictnessConversions ((queryFormatID, property), number) = UnsoundStrictOrderConversionsSummary queryFormatID property number +combineUnsoundStrictnessConversions :: ((QueryFormatID, PropertyID, PropertyName), Int) -> SummarisedCompileWarning +combineUnsoundStrictnessConversions ((queryFormatID, propertyID, property), number) = + UnsoundStrictOrderConversionsSummary queryFormatID propertyID property number -combineAllConstantNetworkInputVars :: ((QueryFormatID, PropertyAddress), NonEmpty QueryID) -> SummarisedCompileWarning -combineAllConstantNetworkInputVars ((queryFormatID, property), queries) = AllConstantNetworkInputVariablesSummary queryFormatID property (sort queries) +combineAllConstantNetworkInputVars :: ((QueryFormatID, PropertyID, PropertyName), NonEmpty (QueryID, TensorIndices)) -> SummarisedCompileWarning +combineAllConstantNetworkInputVars ((queryFormatID, propertyID, property), queries) = + AllConstantNetworkInputVariablesSummary queryFormatID propertyID property queries -combineUnboundedNetworkInputVars :: ((QueryFormatID, PropertyAddress), Map UnderConstrainedSignature (NonEmpty QueryID)) -> SummarisedCompileWarning -combineUnboundedNetworkInputVars ((queryFormatID, property), constraintsBySignature) = do +combineUnboundedNetworkInputVars :: ((QueryFormatID, PropertyID, PropertyName), Map UnderConstrainedSignature (NonEmpty QueryID)) -> SummarisedCompileWarning +combineUnboundedNetworkInputVars ((queryFormatID, propertyID, property), constraintsBySignature) = do let result = swap <$> Map.toList constraintsBySignature - UnboundedNetworkInputVariablesSummary queryFormatID property result + UnboundedNetworkInputVariablesSummary queryFormatID propertyID property result compareWarning :: SummarisedCompileWarning -> SummarisedCompileWarning -> Ordering compareWarning w1 w2 = compare (warningPropertyId w1) (warningPropertyId w2) where warningPropertyId :: SummarisedCompileWarning -> Maybe PropertyID warningPropertyId w = - propertyID <$> case w of + case w of UnusedResourcesSummary {} -> Nothing - TrivialPropertySummary address _ -> Just address - UnderSpecifiedProblemSpaceVariablesSummary address _ -> Just address - UnsoundStrictOrderConversionsSummary _ address _ -> Just address - AllConstantNetworkInputVariablesSummary _ address _ -> Just address - UnboundedNetworkInputVariablesSummary _ address _ -> Just address + TrivialPropertySummary address _ -> Just $ propertyID address + UnderSpecifiedProblemSpaceVariablesSummary propertyID _ _ -> Just propertyID + UnsoundStrictOrderConversionsSummary _ propertyID _ _ -> Just propertyID + AllConstantNetworkInputVariablesSummary _ propertyID _ _ -> Just propertyID + UnboundedNetworkInputVariablesSummary _ propertyID _ _ -> Just propertyID diff --git a/vehicle/tests/golden/compile/issue712/MarabouQueries.err.golden b/vehicle/tests/golden/compile/issue712/MarabouQueries.err.golden index 3f1957c57..b674bed8e 100644 --- a/vehicle/tests/golden/compile/issue712/MarabouQueries.err.golden +++ b/vehicle/tests/golden/compile/issue712/MarabouQueries.err.golden @@ -1,5 +1,6 @@  -Warning: In property 'isMalicious', in query 1 all network inputs were fixed to be constants. Unfortunately there is a known bug in Marabou that it sometimes erroneously returns 'unsat' for these type of queries. +Warning: In some of the queries generated by property 'isMalicious' all network inputs were fixed to be constants. Unfortunately there is a known bug in Marabou that it sometimes erroneously returns 'unsat' for these type of queries. The queries are: + - query 1 See https://github.com/NeuralNetworkVerification/Marabou/issues/670 for details.  diff --git a/vehicle/tests/golden/compile/issue765/MarabouQueries.err.golden b/vehicle/tests/golden/compile/issue765/MarabouQueries.err.golden index 66189be1f..5a2dabd33 100644 --- a/vehicle/tests/golden/compile/issue765/MarabouQueries.err.golden +++ b/vehicle/tests/golden/compile/issue765/MarabouQueries.err.golden @@ -1,5 +1,6 @@  -Warning: In property 'p', in query 1 all network inputs were fixed to be constants. Unfortunately there is a known bug in Marabou that it sometimes erroneously returns 'unsat' for these type of queries. +Warning: In some of the queries generated by property 'p' all network inputs were fixed to be constants. Unfortunately there is a known bug in Marabou that it sometimes erroneously returns 'unsat' for these type of queries. The queries are: + - query 1 See https://github.com/NeuralNetworkVerification/Marabou/issues/670 for details.  diff --git a/vehicle/tests/golden/compile/simple-arithmetic/Marabou.err.golden b/vehicle/tests/golden/compile/simple-arithmetic/Marabou.err.golden index 67624da6e..9c034b339 100644 --- a/vehicle/tests/golden/compile/simple-arithmetic/Marabou.err.golden +++ b/vehicle/tests/golden/compile/simple-arithmetic/Marabou.err.golden @@ -1,5 +1,6 @@  -Warning: In property 'property', in query 1 all network inputs were fixed to be constants. Unfortunately there is a known bug in Marabou that it sometimes erroneously returns 'unsat' for these type of queries. +Warning: In some of the queries generated by property 'property' all network inputs were fixed to be constants. Unfortunately there is a known bug in Marabou that it sometimes erroneously returns 'unsat' for these type of queries. The queries are: + - query 1 See https://github.com/NeuralNetworkVerification/Marabou/issues/670 for details.  diff --git a/vehicle/tests/golden/compile/simple-constantNetworkInput/Marabou.err.golden b/vehicle/tests/golden/compile/simple-constantNetworkInput/Marabou.err.golden index 66189be1f..5a2dabd33 100644 --- a/vehicle/tests/golden/compile/simple-constantNetworkInput/Marabou.err.golden +++ b/vehicle/tests/golden/compile/simple-constantNetworkInput/Marabou.err.golden @@ -1,5 +1,6 @@  -Warning: In property 'p', in query 1 all network inputs were fixed to be constants. Unfortunately there is a known bug in Marabou that it sometimes erroneously returns 'unsat' for these type of queries. +Warning: In some of the queries generated by property 'p' all network inputs were fixed to be constants. Unfortunately there is a known bug in Marabou that it sometimes erroneously returns 'unsat' for these type of queries. The queries are: + - query 1 See https://github.com/NeuralNetworkVerification/Marabou/issues/670 for details.  diff --git a/vehicle/tests/golden/compile/simple-foreach/Marabou.err.golden b/vehicle/tests/golden/compile/simple-foreach/Marabou.err.golden index 53338b8e8..7fdf92995 100644 --- a/vehicle/tests/golden/compile/simple-foreach/Marabou.err.golden +++ b/vehicle/tests/golden/compile/simple-foreach/Marabou.err.golden @@ -1,10 +1,6 @@  -Warning: In property 'index!0', in query 1 all network inputs were fixed to be constants. Unfortunately there is a known bug in Marabou that it sometimes erroneously returns 'unsat' for these type of queries. - -See https://github.com/NeuralNetworkVerification/Marabou/issues/670 for details. - - -Warning: In property 'index!1', in query 1 all network inputs were fixed to be constants. Unfortunately there is a known bug in Marabou that it sometimes erroneously returns 'unsat' for these type of queries. +Warning: In some of the queries generated by property 'index' all network inputs were fixed to be constants. Unfortunately there is a known bug in Marabou that it sometimes erroneously returns 'unsat' for these type of queries. The queries are: + - query 1 in 'index!0' and 'index!1' See https://github.com/NeuralNetworkVerification/Marabou/issues/670 for details. diff --git a/vehicle/tests/golden/compile/simple-fourierMotzkin/Marabou.err.golden b/vehicle/tests/golden/compile/simple-fourierMotzkin/Marabou.err.golden index 816e19bf4..3aa64c68e 100644 --- a/vehicle/tests/golden/compile/simple-fourierMotzkin/Marabou.err.golden +++ b/vehicle/tests/golden/compile/simple-fourierMotzkin/Marabou.err.golden @@ -1,5 +1,6 @@  -Warning: In property 'unusedVar' the quantified variable 'y' is not always directly related to the input or output of a network. This is frequently indicative of a bug in the specification. +Warning: In property 'unusedVar' there are quantified variables that not always directly related to the input or output of a network. This is frequently indicative of a bug in the specification. These variables are: + - variable 'y' Warning: In property 'unusedVar', the following network input variables do not always have both a lower and a upper bound. This is not currently supported by the Marabou query format. @@ -7,7 +8,8 @@ Warning: In property 'unusedVar', the following network input variables do not a f₀[input]!0 - no lower or upper bound -Warning: In property 'underConstrainedVar1' the quantified variable 'x' is not always directly related to the input or output of a network. This is frequently indicative of a bug in the specification. +Warning: In property 'underConstrainedVar1' there are quantified variables that not always directly related to the input or output of a network. This is frequently indicative of a bug in the specification. These variables are: + - variable 'x' Warning: In property 'underConstrainedVar1', the following network input variables do not always have both a lower and a upper bound. This is not currently supported by the Marabou query format. @@ -15,7 +17,8 @@ Warning: In property 'underConstrainedVar1', the following network input variabl f₀[input]!0 - no upper bound -Warning: In property 'underConstrainedVar2' the quantified variable 'x' is not always directly related to the input or output of a network. This is frequently indicative of a bug in the specification. +Warning: In property 'underConstrainedVar2' there are quantified variables that not always directly related to the input or output of a network. This is frequently indicative of a bug in the specification. These variables are: + - variable 'x' Warning: In property 'underConstrainedVar2', the following network input variables do not always have both a lower and a upper bound. This is not currently supported by the Marabou query format. @@ -23,7 +26,8 @@ Warning: In property 'underConstrainedVar2', the following network input variabl f₀[input]!0 - no upper bound -Warning: In property 'underConstrainedVars' the quantified variables 'x!1', 'x!2', 'x!3', 'x!4' are not always directly related to the input or output of a network. This is frequently indicative of a bug in the specification. +Warning: In property 'underConstrainedVars' there are quantified variables that not always directly related to the input or output of a network. This is frequently indicative of a bug in the specification. These variables are: + - variables 'x!1', 'x!2', 'x!3' and 'x!4' Warning: In property 'underConstrainedVars', the following network input variables do not always have both a lower and a upper bound. This is not currently supported by the Marabou query format. diff --git a/vehicle/tests/golden/compile/simple-if/Marabou.err.golden b/vehicle/tests/golden/compile/simple-if/Marabou.err.golden index ffdd92558..9c73dc7ef 100644 --- a/vehicle/tests/golden/compile/simple-if/Marabou.err.golden +++ b/vehicle/tests/golden/compile/simple-if/Marabou.err.golden @@ -13,7 +13,8 @@ Warning: In property 'prop1', the following network input variables do not alway f₀[input]!0 - no lower bound -Warning: In property 'prop2' the quantified variable 'x' is not always directly related to the input or output of a network. This is frequently indicative of a bug in the specification. +Warning: In property 'prop2' there are quantified variables that not always directly related to the input or output of a network. This is frequently indicative of a bug in the specification. These variables are: + - variable 'x' Warning: In property 'prop2', at least one of the generated queries were found to contain a strict inequality (i.e. constraints of the form 'x < y'). Unfortunately the Marabou query format only supports non-strict inequalities (i.e. constraints of the form 'x <= y'). @@ -23,7 +24,8 @@ In order to provide support, Vehicle has automatically converted the strict ineq See https://github.com/vehicle-lang/vehicle/issues/74 for further details. -Warning: In property 'prop2', in query 2 all network inputs were fixed to be constants. Unfortunately there is a known bug in Marabou that it sometimes erroneously returns 'unsat' for these type of queries. +Warning: In some of the queries generated by property 'prop2' all network inputs were fixed to be constants. Unfortunately there is a known bug in Marabou that it sometimes erroneously returns 'unsat' for these type of queries. The queries are: + - query 2 See https://github.com/NeuralNetworkVerification/Marabou/issues/670 for details. diff --git a/vehicle/tests/golden/compile/simple-tensor/Marabou.err.golden b/vehicle/tests/golden/compile/simple-tensor/Marabou.err.golden index 4821ac6c2..e4c6e52b3 100644 --- a/vehicle/tests/golden/compile/simple-tensor/Marabou.err.golden +++ b/vehicle/tests/golden/compile/simple-tensor/Marabou.err.golden @@ -1,5 +1,6 @@  -Warning: In property 'p', in queries 1, 2, 3 and 4 all network inputs were fixed to be constants. Unfortunately there is a known bug in Marabou that it sometimes erroneously returns 'unsat' for these type of queries. +Warning: In some of the queries generated by property 'p' all network inputs were fixed to be constants. Unfortunately there is a known bug in Marabou that it sometimes erroneously returns 'unsat' for these type of queries. The queries are: + - queries 1, 2, 3 and 4 See https://github.com/NeuralNetworkVerification/Marabou/issues/670 for details.  diff --git a/vehicle/tests/golden/compile/simple-vector/Marabou.err.golden b/vehicle/tests/golden/compile/simple-vector/Marabou.err.golden index 66189be1f..5a2dabd33 100644 --- a/vehicle/tests/golden/compile/simple-vector/Marabou.err.golden +++ b/vehicle/tests/golden/compile/simple-vector/Marabou.err.golden @@ -1,5 +1,6 @@  -Warning: In property 'p', in query 1 all network inputs were fixed to be constants. Unfortunately there is a known bug in Marabou that it sometimes erroneously returns 'unsat' for these type of queries. +Warning: In some of the queries generated by property 'p' all network inputs were fixed to be constants. Unfortunately there is a known bug in Marabou that it sometimes erroneously returns 'unsat' for these type of queries. The queries are: + - query 1 See https://github.com/NeuralNetworkVerification/Marabou/issues/670 for details.  diff --git a/vehicle/tests/golden/error/argument/missingVerifier/Marabou.err.golden b/vehicle/tests/golden/error/argument/missingVerifier/Marabou.err.golden index 179bb878b..a615ab7d6 100644 --- a/vehicle/tests/golden/error/argument/missingVerifier/Marabou.err.golden +++ b/vehicle/tests/golden/error/argument/missingVerifier/Marabou.err.golden @@ -6,7 +6,8 @@ In order to provide support, Vehicle has automatically converted the strict ineq See https://github.com/vehicle-lang/vehicle/issues/74 for further details. -Warning: In property 'trivial', in query 1 all network inputs were fixed to be constants. Unfortunately there is a known bug in Marabou that it sometimes erroneously returns 'unsat' for these type of queries. +Warning: In some of the queries generated by property 'trivial' all network inputs were fixed to be constants. Unfortunately there is a known bug in Marabou that it sometimes erroneously returns 'unsat' for these type of queries. The queries are: + - query 1 See https://github.com/NeuralNetworkVerification/Marabou/issues/670 for details.  diff --git a/vehicle/tests/golden/warning/trivial/Marabou.err.golden b/vehicle/tests/golden/warning/trivial/Marabou.err.golden index 20313a0f6..edef4d607 100644 --- a/vehicle/tests/golden/warning/trivial/Marabou.err.golden +++ b/vehicle/tests/golden/warning/trivial/Marabou.err.golden @@ -8,7 +8,7 @@ Warning: The property 'multiProperty!0!2' was found to evaluate to 'False' witho Warning: The property 'multiProperty!0!0' was found to evaluate to 'True' without needing to call the verifier. This usually indicates a fault with either the specification or any external datasets used. -Warning: In property 'multiProperty!0!1', the following network input variables do not always have both a lower and a upper bound. This is not currently supported by the Marabou query format. +Warning: In property 'multiProperty', the following network input variables do not always have both a lower and a upper bound. This is not currently supported by the Marabou query format. In query 1: f₀[input]!0 - no lower or upper bound