From 0008e99e1bd06b246f50366cb94a9f636ff1140f Mon Sep 17 00:00:00 2001 From: tomer arnon Date: Sun, 12 Jul 2020 21:52:32 +0300 Subject: [PATCH] tests pass with latest versions --- Manifest.toml | 312 ++++++++++++++++------------ src/NeuralVerification.jl | 4 +- src/adversarial/dlv.jl | 2 +- src/adversarial/fastLin.jl | 2 +- src/adversarial/fastLip.jl | 2 +- src/adversarial/reluVal.jl | 2 +- src/optimization/certify.jl | 2 +- src/optimization/convDual.jl | 2 +- src/optimization/duality.jl | 2 +- src/optimization/iLP.jl | 2 +- src/optimization/mipVerify.jl | 2 +- src/optimization/nsVerify.jl | 2 +- src/optimization/utils/variables.jl | 27 ++- src/reachability/ai2.jl | 2 +- src/reachability/exactReach.jl | 2 +- src/reachability/maxSens.jl | 2 +- src/satisfiability/bab.jl | 4 +- src/satisfiability/planet.jl | 6 +- src/satisfiability/reluplex.jl | 2 +- src/satisfiability/sherlock.jl | 4 +- src/utils/flux.jl | 6 +- src/utils/problem.jl | 1 + test/complements.jl | 4 +- 23 files changed, 231 insertions(+), 165 deletions(-) diff --git a/Manifest.toml b/Manifest.toml index ce53a14f..4b7a17a0 100644 --- a/Manifest.toml +++ b/Manifest.toml @@ -1,3 +1,5 @@ +# This file is machine-generated - editing it directly is not advised + [[AxisAlgorithms]] deps = ["LinearAlgebra", "Random", "SparseArrays", "WoodburyMatrices"] git-tree-sha1 = "a4d07a1c313392a77042855df46c5f534076fab9" @@ -8,149 +10,171 @@ version = "1.0.0" uuid = "2a0f44e3-6c83-55bd-87e4-b1978d98bd5f" [[BenchmarkTools]] -deps = ["JSON", "Printf", "Statistics"] -git-tree-sha1 = "90b73db83791c5f83155016dd1cc1f684d4e1361" +deps = ["JSON", "Logging", "Printf", "Statistics", "UUIDs"] +git-tree-sha1 = "9e62e66db34540a0c919d72172cc2f642ac71260" uuid = "6e4b80f9-dd63-53aa-95a3-0cdb28fa8baf" -version = "0.4.3" +version = "0.5.0" [[BinDeps]] -deps = ["Compat", "Libdl", "SHA", "URIParser"] -git-tree-sha1 = "12093ca6cdd0ee547c39b1870e0c9c3f154d9ca9" +deps = ["Libdl", "Pkg", "SHA", "URIParser", "Unicode"] +git-tree-sha1 = "46cf2c1668ad07aba5a9d331bdeea994a1f13856" uuid = "9e28174c-4ba2-5203-b857-d8d62c4213ee" -version = "0.8.10" +version = "1.0.1" [[BinaryProvider]] -deps = ["Libdl", "SHA"] -git-tree-sha1 = "29995a7b317bbd06be147e1974a3541ce2502dca" +deps = ["Libdl", "Logging", "SHA"] +git-tree-sha1 = "ecdec412a9abc8db54c0efc5548c64dfce072058" uuid = "b99e7846-7c00-51b0-8f62-c81ae34c0232" -version = "0.5.7" +version = "0.5.10" [[CDDLib]] -deps = ["BinaryProvider", "JuMP", "Libdl", "LinearAlgebra", "Polyhedra", "SparseArrays"] -git-tree-sha1 = "4b7df5e31c00516546fa47f36f6425194a2adfde" +deps = ["BinaryProvider", "JuMP", "Libdl", "LinearAlgebra", "MathOptInterface", "Polyhedra", "SparseArrays"] +git-tree-sha1 = "2330fd11fc4a4fbb89fa2f5d4de87efbc91a8941" uuid = "3391f64e-dcde-5f30-b752-e11513730f60" -version = "0.5.3" +version = "0.6.2" [[CRlibm]] -deps = ["Libdl", "Test"] -git-tree-sha1 = "805164abcd31facf3a7e5b7d803a0d16b23329bc" +deps = ["Libdl"] +git-tree-sha1 = "9d1c22cff9c04207f336b8e64840d0bd40d86e0e" uuid = "96374032-68de-5a5b-8d9e-752f78720389" -version = "0.7.1" +version = "0.8.0" [[Calculus]] -deps = ["Compat"] -git-tree-sha1 = "bd8bbd105ba583a42385bd6dc4a20dad8ab3dc11" +deps = ["LinearAlgebra"] +git-tree-sha1 = "f641eb0a4f00c343bbc32346e1217b86f3ce9dad" uuid = "49dc2e85-a5d0-5ad3-a950-438e2897f1b9" -version = "0.5.0" +version = "0.5.1" + +[[CodecBzip2]] +deps = ["BinaryProvider", "Libdl", "TranscodingStreams"] +git-tree-sha1 = "5db086e510c11b4c87d05067627eadb2dc079995" +uuid = "523fee87-0ab8-5b00-afb7-3ecf72e48cfd" +version = "0.6.0" + +[[CodecZlib]] +deps = ["BinaryProvider", "Libdl", "TranscodingStreams"] +git-tree-sha1 = "05916673a2627dd91b4969ff8ba6941bc85a960e" +uuid = "944b1d66-785c-5afd-91f1-9de20f533193" +version = "0.6.0" [[ColorTypes]] deps = ["FixedPointNumbers", "Random"] -git-tree-sha1 = "10050a24b09e8e41b951e9976b109871ce98d965" +git-tree-sha1 = "6e7aa35d0294f647bb9c985ccc34d4f5d371a533" uuid = "3da002f7-5984-5a60-b8a6-cbb66c0b333f" -version = "0.8.0" +version = "0.10.6" [[CommonSubexpressions]] -deps = ["Test"] -git-tree-sha1 = "efdaf19ab11c7889334ca247ff4c9f7c322817b0" +deps = ["MacroTools", "Test"] +git-tree-sha1 = "7b8a93dba8af7e3b42fecabf646260105ac373f7" uuid = "bbf7d656-a473-5ed7-a52c-81e309532950" -version = "0.2.0" - -[[Compat]] -deps = ["Base64", "Dates", "DelimitedFiles", "Distributed", "InteractiveUtils", "LibGit2", "Libdl", "LinearAlgebra", "Markdown", "Mmap", "Pkg", "Printf", "REPL", "Random", "Serialization", "SharedArrays", "Sockets", "SparseArrays", "Statistics", "Test", "UUIDs", "Unicode"] -git-tree-sha1 = "ed2c4abadf84c53d9e58510b5fc48912c2336fbb" -uuid = "34da2185-b29b-5c13-b0c7-acf172513d20" -version = "2.2.0" +version = "0.3.0" [[DataStructures]] deps = ["InteractiveUtils", "OrderedCollections"] -git-tree-sha1 = "1fe8fad5fc84686dcbc674aa255bc867a64f8132" +git-tree-sha1 = "edad9434967fdc0a2631a65d902228400642120c" uuid = "864edb3b-99cc-5e75-8d2d-829cb0a9cfe8" -version = "0.17.5" +version = "0.17.19" [[Dates]] deps = ["Printf"] uuid = "ade2ca70-3891-5945-98fb-dc099432e06a" -[[DelimitedFiles]] -deps = ["Mmap"] -uuid = "8bb1440f-4735-579b-a4ab-409b98df4dab" - [[DiffResults]] -deps = ["Compat", "StaticArrays"] -git-tree-sha1 = "34a4a1e8be7bc99bc9c611b895b5baf37a80584c" +deps = ["StaticArrays"] +git-tree-sha1 = "da24935df8e0c6cf28de340b958f6aac88eaa0cc" uuid = "163ba53b-c6d8-5494-b064-1a9d43ac40c5" -version = "0.0.4" +version = "1.0.2" [[DiffRules]] -deps = ["Random", "Test"] -git-tree-sha1 = "dc0869fb2f5b23466b32ea799bd82c76480167f7" +deps = ["NaNMath", "Random", "SpecialFunctions"] +git-tree-sha1 = "eb0c34204c8410888844ada5359ac8b96292cfd1" uuid = "b552c78f-8df3-52c6-915a-8e097449b14b" -version = "0.0.10" +version = "1.0.1" [[Distributed]] -deps = ["LinearAlgebra", "Random", "Serialization", "Sockets"] +deps = ["Random", "Serialization", "Sockets"] uuid = "8ba89e20-285c-5b6f-9357-94700520ee1b" [[ErrorfreeArithmetic]] -git-tree-sha1 = "a2b7d5a7962e5bfaab0e2e87c9cde7d3087f4e2c" +git-tree-sha1 = "a5198ab6c8a724dd3965b31ddd11ccde65300f5b" uuid = "90fa49ef-747e-5e6f-a989-263ba693cf1a" -version = "0.4.0" +version = "0.5.0" [[FastRounding]] -deps = ["ErrorfreeArithmetic", "Test"] -git-tree-sha1 = "224175e213fd4fe112db3eea05d66b308dc2bf6b" +deps = ["ErrorfreeArithmetic", "LinearAlgebra"] +git-tree-sha1 = "6344aa18f654196be82e62816935225b3b9abe44" uuid = "fa42c844-2597-5d31-933b-ebd51ab2693f" -version = "0.2.0" +version = "0.3.1" [[FixedPointNumbers]] -git-tree-sha1 = "d14a6fa5890ea3a7e5dcab6811114f132fec2b4b" +deps = ["Statistics"] +git-tree-sha1 = "266baee2e9d875cb7a3bfdcc6cab553c543ff8ab" uuid = "53c48c17-4a7d-5ca2-90c5-79b7896eea93" -version = "0.6.1" +version = "0.8.2" [[ForwardDiff]] deps = ["CommonSubexpressions", "DiffResults", "DiffRules", "NaNMath", "Random", "SpecialFunctions", "StaticArrays"] -git-tree-sha1 = "adf88d6da1f0294058f38295becf8807986bb7d0" +git-tree-sha1 = "1d090099fb82223abc48f7ce176d3f7696ede36d" uuid = "f6369f11-7733-5829-9624-2563aa707210" -version = "0.10.5" +version = "0.10.12" [[GLPK]] -deps = ["BinaryProvider", "Libdl", "MathOptInterface", "SparseArrays"] -git-tree-sha1 = "514692c8ffb0cb4f37afcb0f175573f31551c408" +deps = ["BinaryProvider", "GLPK_jll", "Libdl", "MathOptInterface", "SparseArrays"] +git-tree-sha1 = "86573ecb852e303b209212046af44871f1c0e49c" uuid = "60bf3e95-4087-53dc-ae20-288a0d20c6a6" -version = "0.11.4" +version = "0.13.0" [[GLPKMathProgInterface]] -deps = ["Compat", "GLPK", "MathProgBase"] -git-tree-sha1 = "a7802595ed7e2ab69cd4e496bf2cf8f633082237" +deps = ["GLPK", "LinearAlgebra", "MathProgBase", "SparseArrays"] +git-tree-sha1 = "dcca815a687d8f398c8fc701c3796a36ef6b73a5" uuid = "3c7084bd-78ad-589a-b5bb-dbd673274bea" -version = "0.4.4" +version = "0.5.0" + +[[GLPK_jll]] +deps = ["GMP_jll", "Libdl", "Pkg"] +git-tree-sha1 = "ccc855de74292e478d4278e3a6fdd8212f75e81e" +uuid = "e8aa6df9-e6ca-548a-97ff-1f85fc5b8b98" +version = "4.64.0+0" + +[[GMP_jll]] +deps = ["Libdl", "Pkg"] +git-tree-sha1 = "4dd9301d3a027c05ec403e756ee7a60e3c367e5d" +uuid = "781609d7-10c4-51f6-84f2-b8444358ff6d" +version = "6.1.2+5" [[GeometryTypes]] -deps = ["ColorTypes", "FixedPointNumbers", "IterTools", "LinearAlgebra", "StaticArrays"] -git-tree-sha1 = "4bf5706f3b9a2c5adbbc473c8c91582c1fa816a3" +deps = ["ColorTypes", "FixedPointNumbers", "LinearAlgebra", "StaticArrays"] +git-tree-sha1 = "34bfa994967e893ab2f17b864eec221b3521ba4d" uuid = "4d00f742-c7ba-57c2-abde-4428a4b178cb" -version = "0.7.6" +version = "0.8.3" + +[[HTTP]] +deps = ["Base64", "Dates", "IniFile", "MbedTLS", "Sockets"] +git-tree-sha1 = "eca61b35cdd8cd2fcc5eec1eda766424a995b02f" +uuid = "cd3eb016-35fb-5094-929b-558a96fad6f3" +version = "0.8.16" + +[[IniFile]] +deps = ["Test"] +git-tree-sha1 = "098e4d2c533924c921f9f9847274f2ad89e018b8" +uuid = "83e8ac13-25f8-5344-8a64-a9f2b223428f" +version = "0.5.0" [[InteractiveUtils]] -deps = ["LinearAlgebra", "Markdown"] +deps = ["Markdown"] uuid = "b77e0a4c-d291-57a0-90e8-8db25a27a240" [[Interpolations]] deps = ["AxisAlgorithms", "LinearAlgebra", "OffsetArrays", "Random", "Ratios", "SharedArrays", "SparseArrays", "StaticArrays", "WoodburyMatrices"] -git-tree-sha1 = "b55fc7d44f5be845aceb86a359fa072bb12fdc28" +git-tree-sha1 = "2b7d4e9be8b74f03115e64cf36ed2f48ae83d946" uuid = "a98d9a8b-a2ab-59e6-89dd-64a1c18fca59" -version = "0.12.4" +version = "0.12.10" [[IntervalArithmetic]] -deps = ["CRlibm", "FastRounding", "LinearAlgebra", "Markdown", "RecipesBase", "SetRounding", "StaticArrays", "Test"] -git-tree-sha1 = "e2379c6b0b48ce6e414e8eeabec95cd6982aad22" +deps = ["CRlibm", "FastRounding", "LinearAlgebra", "Markdown", "RecipesBase", "SetRounding", "StaticArrays"] +git-tree-sha1 = "f97d8d63c3f849b0f545062de4634bc9f100d8ec" uuid = "d1acc4aa-44c8-5952-acd4-ba5d80a2a253" -version = "0.15.2" - -[[IterTools]] -git-tree-sha1 = "2ebe60d7343962966d1779a74a760f13217a6901" -uuid = "c8e1da08-722c-5040-9ed9-7db0dc04731e" -version = "1.2.0" +version = "0.16.1" [[JSON]] deps = ["Dates", "Mmap", "Parsers", "Unicode"] @@ -158,17 +182,23 @@ git-tree-sha1 = "b34d7cef7b337321e97d22242c3c2b91f476748e" uuid = "682c06a0-de6a-54ab-a142-c8b1cf79cde6" version = "0.21.0" +[[JSONSchema]] +deps = ["HTTP", "JSON", "ZipFile"] +git-tree-sha1 = "832a4d327d9dafdae55a6ecae04f9997c83615cc" +uuid = "7d188eb4-7ad8-530c-ae41-71a32a6d4692" +version = "0.3.0" + [[JuMP]] -deps = ["Calculus", "DataStructures", "ForwardDiff", "LinearAlgebra", "MathOptInterface", "NaNMath", "Random", "SparseArrays", "Statistics"] -git-tree-sha1 = "ba7f96010ed290d77d5c941c32e5df107ca688a4" +deps = ["Calculus", "DataStructures", "ForwardDiff", "LinearAlgebra", "MathOptInterface", "MutableArithmetics", "NaNMath", "Random", "SparseArrays", "Statistics"] +git-tree-sha1 = "cbab42e2e912109d27046aa88f02a283a9abac7c" uuid = "4076af6c-e467-56ae-b986-b466b2749572" -version = "0.20.1" +version = "0.21.3" [[LazySets]] -deps = ["Compat", "Distributed", "GLPKMathProgInterface", "IntervalArithmetic", "LinearAlgebra", "MathProgBase", "Pkg", "Random", "RecipesBase", "Requires", "SharedArrays", "SparseArrays"] -git-tree-sha1 = "5636e37bac362205e216358570c51328c7d5cd94" +deps = ["Distributed", "GLPK", "GLPKMathProgInterface", "InteractiveUtils", "IntervalArithmetic", "JuMP", "LinearAlgebra", "MathProgBase", "Random", "RecipesBase", "Reexport", "Requires", "SharedArrays", "SparseArrays"] +git-tree-sha1 = "6f7f153673122ee3d50dfb81905a76557a8f8c2f" uuid = "b4f0291d-fe17-52bc-9479-3d1a343d9043" -version = "1.11.0" +version = "1.36.3" [[LibGit2]] uuid = "76f85450-5226-5b5a-8eaa-529ad045b433" @@ -183,77 +213,85 @@ uuid = "37e2e46d-f89d-539d-b4ee-838fcccc9c8e" [[Logging]] uuid = "56ddb016-857b-54e1-b83d-db4d58db5568" +[[MacroTools]] +deps = ["Markdown", "Random"] +git-tree-sha1 = "f7d2e3f654af75f01ec49be82c231c382214223a" +uuid = "1914dd2f-81c6-5fcd-8719-6d5c9610ff09" +version = "0.5.5" + [[Markdown]] deps = ["Base64"] uuid = "d6f4376e-aef5-505a-96c1-9c027394607a" [[MathOptInterface]] -deps = ["BenchmarkTools", "LinearAlgebra", "OrderedCollections", "SparseArrays", "Test", "Unicode"] -git-tree-sha1 = "78427dcc212e0c0ad9658049bc56a50303ad9737" +deps = ["BenchmarkTools", "CodecBzip2", "CodecZlib", "JSON", "JSONSchema", "LinearAlgebra", "MutableArithmetics", "OrderedCollections", "SparseArrays", "Test", "Unicode"] +git-tree-sha1 = "cd2049c055c7d192a235670d50faa375361624ba" uuid = "b8f27783-ece8-5eb3-8dc8-9495eed66fee" -version = "0.9.7" +version = "0.9.14" [[MathProgBase]] -deps = ["Compat"] -git-tree-sha1 = "3bf2e534e635df810e5f4b4f1a8b6de9004a0d53" +deps = ["LinearAlgebra", "SparseArrays"] +git-tree-sha1 = "9abbe463a1e9fc507f12a69e7f29346c2cdc472c" uuid = "fdba3010-5040-5b88-9595-932c9decdf73" -version = "0.7.7" +version = "0.7.8" + +[[MbedTLS]] +deps = ["BinaryProvider", "Dates", "Libdl", "Random", "Sockets"] +git-tree-sha1 = "85f5947b53c8cfd53ccfa3f4abae31faa22c2181" +uuid = "739be429-bea8-5141-9913-cc70e7f3736d" +version = "0.7.0" [[Mmap]] uuid = "a63ad114-7e13-5084-954f-fe012c677804" +[[MutableArithmetics]] +deps = ["LinearAlgebra", "SparseArrays", "Test"] +git-tree-sha1 = "6cf09794783b9de2e662c4e8b60d743021e338d0" +uuid = "d8a4904e-b15c-11e9-3269-09a3773c0cb0" +version = "0.2.10" + [[NaNMath]] -deps = ["Compat"] -git-tree-sha1 = "ce3b85e484a5d4c71dd5316215069311135fa9f2" +git-tree-sha1 = "928b8ca9b2791081dc71a51c55347c27c618760f" uuid = "77ba4419-2d1f-58cd-9bb1-8ffee604a2e3" -version = "0.3.2" +version = "0.3.3" [[OffsetArrays]] -git-tree-sha1 = "1af2f79c7eaac3e019a0de41ef63335ff26a0a57" +git-tree-sha1 = "4ba4cd84c88df8340da1c3e2d8dcb9d18dd1b53b" uuid = "6fe1bfb0-de20-5000-8ca7-80f57d26f881" -version = "0.11.1" +version = "1.1.1" [[OrderedCollections]] -deps = ["Random", "Serialization", "Test"] -git-tree-sha1 = "c4c13474d23c60d20a67b217f1d7f22a40edf8f1" +git-tree-sha1 = "293b70ac1780f9584c89268a6e2a560d938a7065" uuid = "bac558e1-5e72-5ebc-8fee-abe8a469f55d" -version = "1.1.0" - -[[ParameterJuMP]] -deps = ["JuMP", "MathOptInterface", "SparseArrays"] -git-tree-sha1 = "061bbb1cfaed57f3a65c5e688285f8da9bef0178" -uuid = "774612a8-9878-5177-865a-ca53ae2495f9" -version = "0.1.2" +version = "1.3.0" [[Parameters]] -deps = ["OrderedCollections"] -git-tree-sha1 = "b62b2558efb1eef1fa44e4be5ff58a515c287e38" +deps = ["OrderedCollections", "UnPack"] +git-tree-sha1 = "38b2e970043613c187bd56a995fe2e551821eb4a" uuid = "d96e819e-fc66-5662-9728-84c9c7592b0a" -version = "0.12.0" +version = "0.12.1" [[Parsers]] deps = ["Dates", "Test"] -git-tree-sha1 = "ef0af6c8601db18c282d092ccbd2f01f3f0cd70b" +git-tree-sha1 = "10134f2ee0b1978ae7752c41306e131a684e1f06" uuid = "69de0a69-1ddd-5017-9359-2bf0b02dc9f0" -version = "0.3.7" +version = "1.0.7" [[PicoSAT]] -deps = ["BinaryProvider", "Libdl", "Test"] -git-tree-sha1 = "7268928c934f978e3e78b76c267f08ce51d04d7a" -repo-rev = "master" -repo-url = "https://github.com/jakebolewski/PicoSAT.jl.git" +deps = ["Test"] +git-tree-sha1 = "07b5a21ae117b9e5434421e8414ce2a0e7a79485" uuid = "ff2beb65-d7cd-5ff1-a187-74671133a339" -version = "0.3.2+" +version = "0.3.2" [[Pkg]] deps = ["Dates", "LibGit2", "Markdown", "Printf", "REPL", "Random", "SHA", "UUIDs"] uuid = "44cfe95a-1eb2-52ea-b672-e2afdf69b78f" [[Polyhedra]] -deps = ["GeometryTypes", "JuMP", "LinearAlgebra", "ParameterJuMP", "RecipesBase", "SparseArrays", "StaticArrays"] -git-tree-sha1 = "cc6e3b2e436f227d89b440c7cc01b2fd47a39269" +deps = ["GeometryTypes", "JuMP", "LinearAlgebra", "RecipesBase", "SparseArrays", "StaticArrays"] +git-tree-sha1 = "2f29d9fbe6e25bf7b9a5bf90cae56c083fcaf9dc" uuid = "67491407-f73d-577b-9b50-8179a7c68029" -version = "0.5.6" +version = "0.6.5" [[Printf]] deps = ["Unicode"] @@ -268,15 +306,14 @@ deps = ["Serialization"] uuid = "9a3f8284-a2c9-5f02-9a11-845980a1fd5c" [[Ratios]] -deps = ["Compat"] -git-tree-sha1 = "cdbbe0f350581296f3a2e3e7a91b214121934407" +git-tree-sha1 = "37d210f612d70f3f7d57d488cb3b6eff56ad4e41" uuid = "c84ed2f1-dad5-54f0-aa8e-dbefe2724439" -version = "0.3.1" +version = "0.4.0" [[RecipesBase]] -git-tree-sha1 = "7bdce29bc9b2f5660a6e5e64d64d91ec941f6aa2" +git-tree-sha1 = "54f8ceb165a0f6d083f0d12cb4996f5367c6edbc" uuid = "3cdcf5f2-1ef4-517c-9805-6587b60abb01" -version = "0.7.0" +version = "1.0.1" [[Reexport]] deps = ["Pkg"] @@ -285,16 +322,16 @@ uuid = "189a3867-3050-52da-a836-e630ba90ab69" version = "0.2.0" [[Requires]] -deps = ["Test"] -git-tree-sha1 = "f6fbf4ba64d295e146e49e021207993b6b48c7d1" +deps = ["UUIDs"] +git-tree-sha1 = "d37400976e98018ee840e0ca4f9d20baa231dc6b" uuid = "ae029012-a4dd-5104-9daa-d747884805df" -version = "0.5.2" +version = "1.0.1" [[SCS]] deps = ["BinaryProvider", "Libdl", "LinearAlgebra", "MathOptInterface", "MathProgBase", "SparseArrays"] -git-tree-sha1 = "f777069f119d26b021b773756c2510e4fb8a3f99" +git-tree-sha1 = "936d43feaceae3290472ddf800b496be094d727b" uuid = "c946c3f1-0d1f-5ce8-9dea-7daa1f7e2d13" -version = "0.6.2" +version = "0.6.6" [[SHA]] uuid = "ea8e919c-243c-51af-8825-aaa63cd721ce" @@ -327,9 +364,9 @@ version = "0.8.0" [[StaticArrays]] deps = ["LinearAlgebra", "Random", "Statistics"] -git-tree-sha1 = "1e9c5d89cba8047d518f1ffef432906ef1a3e8bd" +git-tree-sha1 = "016d1e1a00fabc556473b07161da3d39726ded35" uuid = "90137ffa-7385-5640-81b9-e52037218182" -version = "0.12.0" +version = "0.12.4" [[Statistics]] deps = ["LinearAlgebra", "SparseArrays"] @@ -339,21 +376,38 @@ uuid = "10745b16-79ce-11e8-11f9-7d13ad32a3b2" deps = ["Distributed", "InteractiveUtils", "Logging", "Random"] uuid = "8dfed614-e22c-5e08-85e1-65c5234f0b40" +[[TranscodingStreams]] +deps = ["Random", "Test"] +git-tree-sha1 = "7c53c35547de1c5b9d46a4797cf6d8253807108c" +uuid = "3bb67fe8-82b1-5028-8e26-92a6c54297fa" +version = "0.9.5" + [[URIParser]] -deps = ["Test", "Unicode"] -git-tree-sha1 = "6ddf8244220dfda2f17539fa8c9de20d6c575b69" +deps = ["Unicode"] +git-tree-sha1 = "53a9f49546b8d2dd2e688d216421d050c9a31d0d" uuid = "30578b45-9adc-5946-b283-645ec420af67" -version = "0.4.0" +version = "0.4.1" [[UUIDs]] -deps = ["Random"] +deps = ["Random", "SHA"] uuid = "cf7118a7-6976-5b1a-9a39-7adc72f591a4" +[[UnPack]] +git-tree-sha1 = "d4bfa022cd30df012700cf380af2141961bb3bfb" +uuid = "3a884ed6-31ef-47d7-9d2a-63182c4928ed" +version = "1.0.1" + [[Unicode]] uuid = "4ec0a83e-493e-50e2-b9ac-8f72acf5a8f5" [[WoodburyMatrices]] -deps = ["LinearAlgebra", "Random", "SparseArrays", "Test"] -git-tree-sha1 = "21772c33b447757ec7d3e61fcdfb9ea5c47eedcf" +deps = ["LinearAlgebra", "SparseArrays"] +git-tree-sha1 = "28ffe06d28b1ba8fdb2f36ec7bb079fac81bac0d" uuid = "efce3f68-66dc-5838-9240-27a6d6f5f9b6" -version = "0.4.1" +version = "0.5.2" + +[[ZipFile]] +deps = ["BinaryProvider", "Libdl", "Printf"] +git-tree-sha1 = "7fbfbc51c186f0ccdbe091f32d3dff8608973f8e" +uuid = "a5390f91-8eb1-5f08-bee0-b1d1ffed6cea" +version = "0.8.4" diff --git a/src/NeuralVerification.jl b/src/NeuralVerification.jl index 2e71df10..82a715ce 100644 --- a/src/NeuralVerification.jl +++ b/src/NeuralVerification.jl @@ -15,11 +15,11 @@ import LazySets: dim, HalfSpace # necessary to avoid conflict with Polyhedra using Requires -# abstract type Solver end # no longer needed +abstract type Solver end # For optimization methods: import JuMP.MOI.OPTIMAL, JuMP.MOI.INFEASIBLE -JuMP.Model(solver) = Model(with_optimizer(solver.optimizer)) +JuMP.Model(solver::Solver) = Model(solver.optimizer) JuMP.value(vars::Vector{VariableRef}) = value.(vars) include("utils/activation.jl") diff --git a/src/adversarial/dlv.jl b/src/adversarial/dlv.jl index 70fa3287..764631c0 100644 --- a/src/adversarial/dlv.jl +++ b/src/adversarial/dlv.jl @@ -31,7 +31,7 @@ in *International Conference on Computer Aided Verification*, 2017.](https://arx [https://github.com/VeriDeep/DLV](https://github.com/VeriDeep/DLV) """ -@with_kw struct DLV +@with_kw struct DLV <: Solver optimizer = GLPK.Optimizer ϵ::Float64 = 1.0 end diff --git a/src/adversarial/fastLin.jl b/src/adversarial/fastLin.jl index f8edf55f..a53f275b 100644 --- a/src/adversarial/fastLin.jl +++ b/src/adversarial/fastLin.jl @@ -27,7 +27,7 @@ Sound but not complete. "Towards Fast Computation of Certified Robustness for ReLU Networks," *ArXiv Preprint ArXiv:1804.09699*, 2018.](https://arxiv.org/abs/1804.09699) """ -@with_kw struct FastLin +@with_kw struct FastLin <: Solver maxIter::Int64 = 10 ϵ0::Float64 = 100.0 accuracy::Float64 = 0.1 diff --git a/src/adversarial/fastLip.jl b/src/adversarial/fastLip.jl index 90a7c4ae..447a0081 100644 --- a/src/adversarial/fastLip.jl +++ b/src/adversarial/fastLip.jl @@ -25,7 +25,7 @@ Sound but not complete. "Towards Fast Computation of Certified Robustness for ReLU Networks," *ArXiv Preprint ArXiv:1804.09699*, 2018.](https://arxiv.org/abs/1804.09699) """ -@with_kw struct FastLip +@with_kw struct FastLip <: Solver maxIter::Int64 = 10 ϵ0::Float64 = 100.0 accuracy::Float64 = 0.1 diff --git a/src/adversarial/reluVal.jl b/src/adversarial/reluVal.jl index ab579a09..51aad4d9 100644 --- a/src/adversarial/reluVal.jl +++ b/src/adversarial/reluVal.jl @@ -26,7 +26,7 @@ Sound but not complete. [https://github.com/tcwangshiqi-columbia/ReluVal](https://github.com/tcwangshiqi-columbia/ReluVal) """ -@with_kw struct ReluVal +@with_kw struct ReluVal <: Solver max_iter::Int64 = 10 tree_search::Symbol = :DFS # only :DFS/:BFS allowed? If so, we should assert this. end diff --git a/src/optimization/certify.jl b/src/optimization/certify.jl index 62343da9..81252c56 100644 --- a/src/optimization/certify.jl +++ b/src/optimization/certify.jl @@ -23,7 +23,7 @@ Sound but not complete. "Certified Defenses against Adversarial Examples," *ArXiv Preprint ArXiv:1801.09344*, 2018.](https://arxiv.org/abs/1801.09344) """ -@with_kw struct Certify +@with_kw struct Certify <: Solver optimizer = SCS.Optimizer end diff --git a/src/optimization/convDual.jl b/src/optimization/convDual.jl index 293321ab..8e756666 100644 --- a/src/optimization/convDual.jl +++ b/src/optimization/convDual.jl @@ -23,7 +23,7 @@ Sound but not complete. [https://github.com/locuslab/convex_adversarial](https://github.com/locuslab/convex_adversarial) """ -struct ConvDual end +struct ConvDual <: Solver end function solve(solver::ConvDual, problem::Problem) o = dual_value(solver, problem.network, problem.input, problem.output) diff --git a/src/optimization/duality.jl b/src/optimization/duality.jl index c109b628..bad697dd 100644 --- a/src/optimization/duality.jl +++ b/src/optimization/duality.jl @@ -23,7 +23,7 @@ Sound but not complete. "A Dual Approach to Scalable Verification of Deep Networks," *ArXiv Preprint ArXiv:1803.06567*, 2018.](https://arxiv.org/abs/1803.06567) """ -@with_kw struct Duality +@with_kw struct Duality <: Solver optimizer = GLPK.Optimizer end diff --git a/src/optimization/iLP.jl b/src/optimization/iLP.jl index b49a443f..36f51572 100644 --- a/src/optimization/iLP.jl +++ b/src/optimization/iLP.jl @@ -27,7 +27,7 @@ Sound but not complete. "Measuring Neural Net Robustness with Constraints," in *Advances in Neural Information Processing Systems*, 2016.](https://arxiv.org/abs/1605.07262) """ -@with_kw struct ILP +@with_kw struct ILP <: Solver optimizer = GLPK.Optimizer iterative::Bool = true end diff --git a/src/optimization/mipVerify.jl b/src/optimization/mipVerify.jl index cbf18f38..a80f98a6 100644 --- a/src/optimization/mipVerify.jl +++ b/src/optimization/mipVerify.jl @@ -26,7 +26,7 @@ V. Tjeng, K. Xiao, and R. Tedrake, [https://github.com/vtjeng/MIPVerify.jl](https://github.com/vtjeng/MIPVerify.jl) """ -@with_kw struct MIPVerify +@with_kw struct MIPVerify <: Solver optimizer = GLPK.Optimizer end diff --git a/src/optimization/nsVerify.jl b/src/optimization/nsVerify.jl index 678059b9..17fb9413 100644 --- a/src/optimization/nsVerify.jl +++ b/src/optimization/nsVerify.jl @@ -23,7 +23,7 @@ Sound and complete. "An Approach to Reachability Analysis for Feed-Forward Relu Neural Networks," *ArXiv Preprint ArXiv:1706.07351*, 2017.](https://arxiv.org/abs/1706.07351) """ -@with_kw struct NSVerify +@with_kw struct NSVerify <: Solver optimizer = GLPK.Optimizer m::Float64 = 1000.0 # The big M in the linearization end diff --git a/src/optimization/utils/variables.jl b/src/optimization/utils/variables.jl index 7b895540..0bbfcda7 100644 --- a/src/optimization/utils/variables.jl +++ b/src/optimization/utils/variables.jl @@ -27,15 +27,26 @@ function init_variables(model::Model, layers::Vector{Layer}; binary = false, inc return vars end + +_model(a::Number) = nothing +_model(a::VariableRef) = a.model +_model(a::Array) = _model(first(a)) +_model(a::GenericAffExpr) = isempty(a.terms) ? nothing : _model(first(keys(a.terms))) +_model(as...) = something(_model.(as)..., missing) + +# These should only be hit if we're comparing 0 with 0 or if we somehow +# hit a branch that is numbers only (no variables or expressions). Shouldn't happen +symbolic_max(m::Missing, a, b) = @show zero(promote_type(typeof(a), typeof(b))) +symbolic_abs(m::Missing, a, b) = @show zero(promote_type(typeof(a), typeof(b))) + function symbolic_max(m::Model, a, b) aux = @variable(m) @constraint(m, aux >= a) @constraint(m, aux >= b) return aux end -symbolic_max(a::VariableRef, b::VariableRef) = symbolic_max(a.model, a, b) -symbolic_max(a::GenericAffExpr, b::GenericAffExpr) = symbolic_max(first(first(a.terms)).model, a, b) -symbolic_max(a::Array{<:GenericAffExpr}, b::Array{<:GenericAffExpr}) = symbolic_max.(a, b) +symbolic_max(a, b) = symbolic_max(_model(a, b), a, b) + function symbolic_abs(m::Model, v) aux = @variable(m) #get an anonymous variable @@ -44,9 +55,8 @@ function symbolic_abs(m::Model, v) @constraint(m, aux >= -v) return aux end -symbolic_abs(v::VariableRef) = symbolic_abs(v.m, v) -symbolic_abs(v::GenericAffExpr) = symbolic_abs(first(first(v.terms)).model, v) -symbolic_abs(v::Array{<:GenericAffExpr}) = symbolic_abs.(v) +symbolic_abs(v) = symbolic_abs(_model(v), v) + function symbolic_infty_norm(m::Model, v::Array{<:GenericAffExpr}) aux = @variable(m) @@ -55,7 +65,4 @@ function symbolic_infty_norm(m::Model, v::Array{<:GenericAffExpr}) @constraint(m, aux .>= -v) return aux end -# # in general, default to symbolic_abs behavior: -# symbolic_infty_norm(v) = symbolic_abs(v) -# only Array{<:GenericAffExpr} is needed -symbolic_infty_norm(v::Array{<:GenericAffExpr}) = symbolic_infty_norm(first(first(first(v).terms)).model, v) +symbolic_infty_norm(v::Array{<:GenericAffExpr}) = symbolic_infty_norm(_model(v), v) diff --git a/src/reachability/ai2.jl b/src/reachability/ai2.jl index a914b900..7bbe252e 100644 --- a/src/reachability/ai2.jl +++ b/src/reachability/ai2.jl @@ -22,7 +22,7 @@ T. Gehr, M. Mirman, D. Drashsler-Cohen, P. Tsankov, S. Chaudhuri, and M. Vechev, "Ai2: Safety and Robustness Certification of Neural Networks with Abstract Interpretation," in *2018 IEEE Symposium on Security and Privacy (SP)*, 2018. """ -struct Ai2 end +struct Ai2 <: Solver end function solve(solver::Ai2, problem::Problem) reach = forward_network(solver, problem.network, problem.input) diff --git a/src/reachability/exactReach.jl b/src/reachability/exactReach.jl index e7e6cfa1..d839e3c7 100644 --- a/src/reachability/exactReach.jl +++ b/src/reachability/exactReach.jl @@ -22,7 +22,7 @@ Sound and complete. "Reachable Set Computation and Safety Verification for Neural Networks with ReLU Activations," *ArXiv Preprint ArXiv:1712.08163*, 2017.](https://arxiv.org/abs/1712.08163) """ -struct ExactReach end +struct ExactReach <: Solver end function solve(solver::ExactReach, problem::Problem) reach = forward_network(solver, problem.network, problem.input) diff --git a/src/reachability/maxSens.jl b/src/reachability/maxSens.jl index 5cfd1693..41f99b1d 100644 --- a/src/reachability/maxSens.jl +++ b/src/reachability/maxSens.jl @@ -25,7 +25,7 @@ Sound but not complete. "Output Reachable Set Estimation and Verification for Multi-Layer Neural Networks," *ArXiv Preprint ArXiv:1708.03322*, 2017.](https://arxiv.org/abs/1708.03322) """ -@with_kw struct MaxSens +@with_kw struct MaxSens <: Solver resolution::Float64 = 1.0 tight::Bool = false end diff --git a/src/satisfiability/bab.jl b/src/satisfiability/bab.jl index 9616c697..92803f1b 100644 --- a/src/satisfiability/bab.jl +++ b/src/satisfiability/bab.jl @@ -26,7 +26,7 @@ Sound and complete. "A Unified View of Piecewise Linear Neural Network Verification," *ArXiv Preprint ArXiv:1711.00455*, 2017.](https://arxiv.org/abs/1711.00455) """ -@with_kw struct BaB +@with_kw struct BaB <: Solver optimizer = GLPK.Optimizer ϵ::Float64 = 0.1 end @@ -109,7 +109,7 @@ end function approx_bound(nnet::Network, dom::Hyperrectangle, optimizer, type::Symbol) bounds = get_bounds(nnet, dom) - model = Model(with_optimizer(optimizer)) + model = Model(optimizer) neurons = init_neurons(model, nnet) add_set_constraint!(model, dom, first(neurons)) encode_network!(model, nnet, neurons, bounds, TriangularRelaxedLP()) diff --git a/src/satisfiability/planet.jl b/src/satisfiability/planet.jl index 00cfb7c4..339a7edc 100644 --- a/src/satisfiability/planet.jl +++ b/src/satisfiability/planet.jl @@ -25,7 +25,7 @@ in *International Symposium on Automated Technology for Verification and Analysi [https://github.com/progirep/planet](https://github.com/progirep/planet) """ -@with_kw struct Planet +@with_kw struct Planet <: Solver optimizer = GLPK.Optimizer eager::Bool = false end @@ -79,7 +79,7 @@ end function elastic_filtering(problem::Problem, δ::Vector{Vector{Bool}}, bounds::Vector{Hyperrectangle}, optimizer) - model = Model(with_optimizer(optimizer)) + model = Model(optimizer) neurons = init_neurons(model, problem.network) add_set_constraint!(model, problem.input, first(neurons)) add_complementary_set_constraint!(model, problem.output, last(neurons)) @@ -129,7 +129,7 @@ end # Only use tighten_bounds for feasibility check function tighten_bounds(problem::Problem, optimizer) bounds = get_bounds(problem) - model = Model(with_optimizer(optimizer)) + model = Model(optimizer) neurons = init_neurons(model, problem.network) add_set_constraint!(model, problem.input, first(neurons)) add_complementary_set_constraint!(model, problem.output, last(neurons)) diff --git a/src/satisfiability/reluplex.jl b/src/satisfiability/reluplex.jl index 9a631bad..0ce89143 100644 --- a/src/satisfiability/reluplex.jl +++ b/src/satisfiability/reluplex.jl @@ -22,7 +22,7 @@ Sound and complete. "Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks," in *International Conference on Computer Aided Verification*, 2017.](https://arxiv.org/abs/1702.01135) """ -@with_kw struct Reluplex +@with_kw struct Reluplex <: Solver optimizer = GLPK.Optimizer end diff --git a/src/satisfiability/sherlock.jl b/src/satisfiability/sherlock.jl index 8d0d67bb..e4850de4 100644 --- a/src/satisfiability/sherlock.jl +++ b/src/satisfiability/sherlock.jl @@ -27,7 +27,7 @@ Sound but not complete. [https://github.com/souradeep-111/sherlock](https://github.com/souradeep-111/sherlock) """ -@with_kw struct Sherlock +@with_kw struct Sherlock <: Solver optimizer = GLPK.Optimizer ϵ::Float64 = 0.1 end @@ -63,7 +63,7 @@ function local_search(problem::Problem, x::Vector{Float64}, optimizer, type::Sym nnet = problem.network act_pattern = get_activation(nnet, x) gradient = get_gradient(nnet, x) - model = Model(with_optimizer(optimizer)) + model = Model(optimizer) neurons = init_neurons(model, nnet) add_set_constraint!(model, problem.input, first(neurons)) encode_network!(model, nnet, neurons, act_pattern, StandardLP()) diff --git a/src/utils/flux.jl b/src/utils/flux.jl index 26ede186..5f7e526f 100644 --- a/src/utils/flux.jl +++ b/src/utils/flux.jl @@ -9,7 +9,11 @@ activation(::typeof(relu)) = ReLU() layer(x) = error("Can't use $x as a layer.") -layer(d::Dense) = Layer(data(d.W), data(d.b), activation(d.σ)) +if isdefined(Flux, :Tracker) + layer(d::Dense) = Layer(Flux.Tracker.data(d.W), Flux.Tracker.data(d.b), activation(d.σ)) +else + layer(d::Dense) = Layer(d.W, d.b, activation(d.σ)) +end network(c::Chain) = Network([layer.(c.layers)...]) diff --git a/src/utils/problem.jl b/src/utils/problem.jl index 1833fc8d..6ef93f87 100644 --- a/src/utils/problem.jl +++ b/src/utils/problem.jl @@ -32,6 +32,7 @@ LazySets.tohrep(PC::PolytopeComplement) = PolytopeComplement(convert(HPolytope, Base.in(pt, PC::PolytopeComplement) = pt ∉ PC.P complement(PC::PolytopeComplement) = PC.P complement(P::LazySet) = PolytopeComplement(P) +Base.:(==)(pc1::PolytopeComplement, pc2::PolytopeComplement) = pc1.P == pc2.P # etc. diff --git a/test/complements.jl b/test/complements.jl index e636e802..1d620bae 100644 --- a/test/complements.jl +++ b/test/complements.jl @@ -9,8 +9,8 @@ @test [5.0, 5.0] ∈ HS && [5.0, 5.0] ∉ PC @test [-1.0, -1.0] ∉ HS && [-1.0, -1.0] ∈ PC - @test complement(PC) === HS - @test complement(HS) === PC + @test complement(PC) == HS + @test complement(HS) == PC # Hyperrectangle contained in HS hr = Hyperrectangle(low = [1.0, 1.0], high = [2.0, 2.0])