diff --git a/.travis.yml b/.travis.yml index 9f51dcc9..f3321d2b 100644 --- a/.travis.yml +++ b/.travis.yml @@ -3,10 +3,13 @@ language: julia os: - linux - osx + - windows julia: - 1.0 - 1.1 + - 1.2 + - 1.3 - nightly notifications: @@ -15,6 +18,7 @@ notifications: matrix: allow_failures: - julia: nightly + - julia: 1.3 before_install: # Install TeX and Qt5 to build plots for documentation diff --git a/Manifest.toml b/Manifest.toml index ab9515fd..ce53a14f 100644 --- a/Manifest.toml +++ b/Manifest.toml @@ -1,12 +1,18 @@ [[AxisAlgorithms]] -deps = ["Compat", "WoodburyMatrices"] -git-tree-sha1 = "99dabbe853e4f641ab21a676131f2cf9fb29937e" +deps = ["LinearAlgebra", "Random", "SparseArrays", "WoodburyMatrices"] +git-tree-sha1 = "a4d07a1c313392a77042855df46c5f534076fab9" uuid = "13072b0f-2c55-5437-9ae7-d433b7a33950" -version = "0.3.0" +version = "1.0.0" [[Base64]] uuid = "2a0f44e3-6c83-55bd-87e4-b1978d98bd5f" +[[BenchmarkTools]] +deps = ["JSON", "Printf", "Statistics"] +git-tree-sha1 = "90b73db83791c5f83155016dd1cc1f684d4e1361" +uuid = "6e4b80f9-dd63-53aa-95a3-0cdb28fa8baf" +version = "0.4.3" + [[BinDeps]] deps = ["Compat", "Libdl", "SHA", "URIParser"] git-tree-sha1 = "12093ca6cdd0ee547c39b1870e0c9c3f154d9ca9" @@ -14,22 +20,16 @@ uuid = "9e28174c-4ba2-5203-b857-d8d62c4213ee" version = "0.8.10" [[BinaryProvider]] -deps = ["Libdl", "Pkg", "SHA", "Test"] -git-tree-sha1 = "055eb2690182ebc31087859c3dd8598371d3ef9e" +deps = ["Libdl", "SHA"] +git-tree-sha1 = "29995a7b317bbd06be147e1974a3541ce2502dca" uuid = "b99e7846-7c00-51b0-8f62-c81ae34c0232" -version = "0.5.3" - -[[BufferedStreams]] -deps = ["Compat", "Test"] -git-tree-sha1 = "5d55b9486590fdda5905c275bb21ce1f0754020f" -uuid = "e1450e63-4bb3-523b-b2a4-4ffa8c0fd77d" -version = "1.0.0" +version = "0.5.7" [[CDDLib]] -deps = ["BinDeps", "Homebrew", "Libdl", "LinearAlgebra", "MathProgBase", "Polyhedra", "SparseArrays", "Test", "WinRPM"] -git-tree-sha1 = "ffcdc397eb04167798e80cd4719090b7551ed0a6" +deps = ["BinaryProvider", "JuMP", "Libdl", "LinearAlgebra", "Polyhedra", "SparseArrays"] +git-tree-sha1 = "4b7df5e31c00516546fa47f36f6425194a2adfde" uuid = "3391f64e-dcde-5f30-b752-e11513730f60" -version = "0.4.1" +version = "0.5.3" [[CRlibm]] deps = ["Libdl", "Test"] @@ -39,15 +39,15 @@ version = "0.7.1" [[Calculus]] deps = ["Compat"] -git-tree-sha1 = "f60954495a7afcee4136f78d1d60350abd37a409" +git-tree-sha1 = "bd8bbd105ba583a42385bd6dc4a20dad8ab3dc11" uuid = "49dc2e85-a5d0-5ad3-a950-438e2897f1b9" -version = "0.4.1" +version = "0.5.0" [[ColorTypes]] -deps = ["FixedPointNumbers", "Random", "Test"] -git-tree-sha1 = "f73b0e10f2a5756de7019818a41654686da06b09" +deps = ["FixedPointNumbers", "Random"] +git-tree-sha1 = "10050a24b09e8e41b951e9976b109871ce98d965" uuid = "3da002f7-5984-5a60-b8a6-cbb66c0b333f" -version = "0.7.5" +version = "0.8.0" [[CommonSubexpressions]] deps = ["Test"] @@ -57,15 +57,15 @@ 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 = "195a3ffcb8b0762684b6821de18f83a16455c6ea" +git-tree-sha1 = "ed2c4abadf84c53d9e58510b5fc48912c2336fbb" uuid = "34da2185-b29b-5c13-b0c7-acf172513d20" -version = "2.0.0" +version = "2.2.0" [[DataStructures]] -deps = ["InteractiveUtils", "OrderedCollections", "Random", "Serialization", "Test"] -git-tree-sha1 = "ca971f03e146cf144a9e2f2ce59674f5bf0e8038" +deps = ["InteractiveUtils", "OrderedCollections"] +git-tree-sha1 = "1fe8fad5fc84686dcbc674aa255bc867a64f8132" uuid = "864edb3b-99cc-5e75-8d2d-829cb0a9cfe8" -version = "0.15.0" +version = "0.17.5" [[Dates]] deps = ["Printf"] @@ -92,16 +92,9 @@ deps = ["LinearAlgebra", "Random", "Serialization", "Sockets"] uuid = "8ba89e20-285c-5b6f-9357-94700520ee1b" [[ErrorfreeArithmetic]] -deps = ["Test"] -git-tree-sha1 = "e38834f24946eb8c7dcf2bb00580e087faa60c44" +git-tree-sha1 = "a2b7d5a7962e5bfaab0e2e87c9cde7d3087f4e2c" uuid = "90fa49ef-747e-5e6f-a989-263ba693cf1a" -version = "0.3.2" - -[[Expokit]] -deps = ["LinearAlgebra", "SparseArrays", "Test"] -git-tree-sha1 = "b0313f5f1825aabb1adb186c837e0d339d02f351" -uuid = "a1e7a1ef-7a5d-5822-a38c-be74e1bb89f4" -version = "0.2.0" +version = "0.4.0" [[FastRounding]] deps = ["ErrorfreeArithmetic", "Test"] @@ -110,22 +103,21 @@ uuid = "fa42c844-2597-5d31-933b-ebd51ab2693f" version = "0.2.0" [[FixedPointNumbers]] -deps = ["Test"] -git-tree-sha1 = "b8045033701c3b10bf2324d7203404be7aef88ba" +git-tree-sha1 = "d14a6fa5890ea3a7e5dcab6811114f132fec2b4b" uuid = "53c48c17-4a7d-5ca2-90c5-79b7896eea93" -version = "0.5.3" +version = "0.6.1" [[ForwardDiff]] -deps = ["CommonSubexpressions", "DiffResults", "DiffRules", "InteractiveUtils", "LinearAlgebra", "NaNMath", "Random", "SparseArrays", "SpecialFunctions", "StaticArrays", "Test"] -git-tree-sha1 = "4c4d727f1b7e0092134fabfab6396b8945c1ea5b" +deps = ["CommonSubexpressions", "DiffResults", "DiffRules", "NaNMath", "Random", "SpecialFunctions", "StaticArrays"] +git-tree-sha1 = "adf88d6da1f0294058f38295becf8807986bb7d0" uuid = "f6369f11-7733-5829-9624-2563aa707210" -version = "0.10.3" +version = "0.10.5" [[GLPK]] -deps = ["BinaryProvider", "Compat", "Libdl", "LinQuadOptInterface"] -git-tree-sha1 = "82f64bfd090a95b7670ed0d7c734220f32983386" +deps = ["BinaryProvider", "Libdl", "MathOptInterface", "SparseArrays"] +git-tree-sha1 = "514692c8ffb0cb4f37afcb0f175573f31551c408" uuid = "60bf3e95-4087-53dc-ae20-288a0d20c6a6" -version = "0.9.1" +version = "0.11.4" [[GLPKMathProgInterface]] deps = ["Compat", "GLPK", "MathProgBase"] @@ -134,32 +126,20 @@ uuid = "3c7084bd-78ad-589a-b5bb-dbd673274bea" version = "0.4.4" [[GeometryTypes]] -deps = ["ColorTypes", "FixedPointNumbers", "IterTools", "LinearAlgebra", "StaticArrays", "Test"] -git-tree-sha1 = "a9bc71d5a7eb971b61db353eb66c4a1de0551d8c" +deps = ["ColorTypes", "FixedPointNumbers", "IterTools", "LinearAlgebra", "StaticArrays"] +git-tree-sha1 = "4bf5706f3b9a2c5adbbc473c8c91582c1fa816a3" uuid = "4d00f742-c7ba-57c2-abde-4428a4b178cb" -version = "0.7.3" - -[[HTTPClient]] -deps = ["Compat", "LibCURL"] -git-tree-sha1 = "161d5776ae8e585ac0b8c20fb81f17ab755b3671" -uuid = "0862f596-cf2d-50af-8ef4-f2be67dfa83f" -version = "0.2.1" - -[[Homebrew]] -deps = ["BinDeps", "InteractiveUtils", "JSON", "Libdl", "Test", "Unicode"] -git-tree-sha1 = "f01fb2f34675f9839d55ba7238bab63ebd2e531e" -uuid = "d9be37ee-ecc9-5288-90f1-b9ca67657a75" -version = "0.7.1" +version = "0.7.6" [[InteractiveUtils]] deps = ["LinearAlgebra", "Markdown"] uuid = "b77e0a4c-d291-57a0-90e8-8db25a27a240" [[Interpolations]] -deps = ["AxisAlgorithms", "LinearAlgebra", "OffsetArrays", "Random", "Ratios", "SharedArrays", "SparseArrays", "StaticArrays", "Test", "WoodburyMatrices"] -git-tree-sha1 = "3493536a64dae5a21c0cc8aecf680647f3e12313" +deps = ["AxisAlgorithms", "LinearAlgebra", "OffsetArrays", "Random", "Ratios", "SharedArrays", "SparseArrays", "StaticArrays", "WoodburyMatrices"] +git-tree-sha1 = "b55fc7d44f5be845aceb86a359fa072bb12fdc28" uuid = "a98d9a8b-a2ab-59e6-89dd-64a1c18fca59" -version = "0.11.0" +version = "0.12.4" [[IntervalArithmetic]] deps = ["CRlibm", "FastRounding", "LinearAlgebra", "Markdown", "RecipesBase", "SetRounding", "StaticArrays", "Test"] @@ -168,42 +148,27 @@ uuid = "d1acc4aa-44c8-5952-acd4-ba5d80a2a253" version = "0.15.2" [[IterTools]] -deps = ["SparseArrays", "Test"] -git-tree-sha1 = "79246285c43602384e6f1943b3554042a3712056" +git-tree-sha1 = "2ebe60d7343962966d1779a74a760f13217a6901" uuid = "c8e1da08-722c-5040-9ed9-7db0dc04731e" -version = "1.1.1" +version = "1.2.0" [[JSON]] -deps = ["Dates", "Distributed", "Mmap", "Sockets", "Test", "Unicode"] -git-tree-sha1 = "1f7a25b53ec67f5e9422f1f551ee216503f4a0fa" +deps = ["Dates", "Mmap", "Parsers", "Unicode"] +git-tree-sha1 = "b34d7cef7b337321e97d22242c3c2b91f476748e" uuid = "682c06a0-de6a-54ab-a142-c8b1cf79cde6" -version = "0.20.0" +version = "0.21.0" [[JuMP]] -deps = ["Calculus", "DataStructures", "ForwardDiff", "LinearAlgebra", "MathOptInterface", "NaNMath", "Random", "SparseArrays", "Statistics", "Test"] -git-tree-sha1 = "db9f08540c1a23269acbae5d520c79f4722899f4" +deps = ["Calculus", "DataStructures", "ForwardDiff", "LinearAlgebra", "MathOptInterface", "NaNMath", "Random", "SparseArrays", "Statistics"] +git-tree-sha1 = "ba7f96010ed290d77d5c941c32e5df107ca688a4" uuid = "4076af6c-e467-56ae-b986-b466b2749572" -version = "0.19.0" +version = "0.20.1" [[LazySets]] -deps = ["Compat", "Distributed", "Expokit", "GLPKMathProgInterface", "InteractiveUtils", "IntervalArithmetic", "LinearAlgebra", "MathProgBase", "Pkg", "Random", "RecipesBase", "Requires", "SharedArrays", "SparseArrays"] -git-tree-sha1 = "6958221ff2efb2a0240d4016ba469a2ca03c29e1" -repo-rev = "master" -repo-url = "https://github.com/JuliaReach/LazySets.jl.git" +deps = ["Compat", "Distributed", "GLPKMathProgInterface", "IntervalArithmetic", "LinearAlgebra", "MathProgBase", "Pkg", "Random", "RecipesBase", "Requires", "SharedArrays", "SparseArrays"] +git-tree-sha1 = "5636e37bac362205e216358570c51328c7d5cd94" uuid = "b4f0291d-fe17-52bc-9479-3d1a343d9043" -version = "1.9.0+" - -[[LibCURL]] -deps = ["BinaryProvider", "Compat", "Libdl", "Printf"] -git-tree-sha1 = "6339c87cb76923a3cf947fcd213cbc364355c9c9" -uuid = "b27032c2-a3e7-50c8-80cd-2d36dbcbfd21" -version = "0.4.1" - -[[LibExpat]] -deps = ["Compat"] -git-tree-sha1 = "fde352ec13479e2f90e57939da2440fb78c5e388" -uuid = "522f3ed2-3f36-55e3-b6df-e94fee9b0c07" -version = "0.5.0" +version = "1.11.0" [[LibGit2]] uuid = "76f85450-5226-5b5a-8eaa-529ad045b433" @@ -211,18 +176,6 @@ uuid = "76f85450-5226-5b5a-8eaa-529ad045b433" [[Libdl]] uuid = "8f399da3-3557-5675-b5ff-fb832c97cbdb" -[[Libz]] -deps = ["BufferedStreams", "Random", "Test"] -git-tree-sha1 = "d405194ffc0293c3519d4f7251ce51baac9cc871" -uuid = "2ec943e9-cfe8-584d-b93d-64dcb6d567b7" -version = "1.0.0" - -[[LinQuadOptInterface]] -deps = ["Compat", "MathOptInterface"] -git-tree-sha1 = "d6692a09d0424e34c884cd819b8ed47943eefc20" -uuid = "f8899e07-120b-5979-ab1d-7b97bb9e1a48" -version = "0.6.0" - [[LinearAlgebra]] deps = ["Libdl"] uuid = "37e2e46d-f89d-539d-b4ee-838fcccc9c8e" @@ -235,10 +188,10 @@ deps = ["Base64"] uuid = "d6f4376e-aef5-505a-96c1-9c027394607a" [[MathOptInterface]] -deps = ["Compat", "Unicode"] -git-tree-sha1 = "ed9457bdd246a3302d791c5e8f0aad3c3de2e121" +deps = ["BenchmarkTools", "LinearAlgebra", "OrderedCollections", "SparseArrays", "Test", "Unicode"] +git-tree-sha1 = "78427dcc212e0c0ad9658049bc56a50303ad9737" uuid = "b8f27783-ece8-5eb3-8dc8-9495eed66fee" -version = "0.8.3" +version = "0.9.7" [[MathProgBase]] deps = ["Compat"] @@ -256,38 +209,51 @@ uuid = "77ba4419-2d1f-58cd-9bb1-8ffee604a2e3" version = "0.3.2" [[OffsetArrays]] -deps = ["DelimitedFiles", "Test"] -git-tree-sha1 = "e6893807f09c1d5517861ded8b203cb96cb7d44a" +git-tree-sha1 = "1af2f79c7eaac3e019a0de41ef63335ff26a0a57" uuid = "6fe1bfb0-de20-5000-8ca7-80f57d26f881" -version = "0.10.0" +version = "0.11.1" [[OrderedCollections]] deps = ["Random", "Serialization", "Test"] -git-tree-sha1 = "85619a3f3e17bb4761fe1b1fd47f0e979f964d5b" +git-tree-sha1 = "c4c13474d23c60d20a67b217f1d7f22a40edf8f1" uuid = "bac558e1-5e72-5ebc-8fee-abe8a469f55d" -version = "1.0.2" +version = "1.1.0" + +[[ParameterJuMP]] +deps = ["JuMP", "MathOptInterface", "SparseArrays"] +git-tree-sha1 = "061bbb1cfaed57f3a65c5e688285f8da9bef0178" +uuid = "774612a8-9878-5177-865a-ca53ae2495f9" +version = "0.1.2" [[Parameters]] -deps = ["Markdown", "OrderedCollections", "REPL", "Test"] -git-tree-sha1 = "70bdbfb2bceabb15345c0b54be4544813b3444e4" +deps = ["OrderedCollections"] +git-tree-sha1 = "b62b2558efb1eef1fa44e4be5ff58a515c287e38" uuid = "d96e819e-fc66-5662-9728-84c9c7592b0a" -version = "0.10.3" +version = "0.12.0" + +[[Parsers]] +deps = ["Dates", "Test"] +git-tree-sha1 = "ef0af6c8601db18c282d092ccbd2f01f3f0cd70b" +uuid = "69de0a69-1ddd-5017-9359-2bf0b02dc9f0" +version = "0.3.7" [[PicoSAT]] -deps = ["Test"] -git-tree-sha1 = "07b5a21ae117b9e5434421e8414ce2a0e7a79485" +deps = ["BinaryProvider", "Libdl", "Test"] +git-tree-sha1 = "7268928c934f978e3e78b76c267f08ce51d04d7a" +repo-rev = "master" +repo-url = "https://github.com/jakebolewski/PicoSAT.jl.git" 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", "MathProgBase", "RecipesBase", "SparseArrays", "StaticArrays", "Test"] -git-tree-sha1 = "04123e891d4a7fb1a2831f09cb07e26233fdff9c" +deps = ["GeometryTypes", "JuMP", "LinearAlgebra", "ParameterJuMP", "RecipesBase", "SparseArrays", "StaticArrays"] +git-tree-sha1 = "cc6e3b2e436f227d89b440c7cc01b2fd47a39269" uuid = "67491407-f73d-577b-9b50-8179a7c68029" -version = "0.4.5" +version = "0.5.6" [[Printf]] deps = ["Unicode"] @@ -303,15 +269,14 @@ uuid = "9a3f8284-a2c9-5f02-9a11-845980a1fd5c" [[Ratios]] deps = ["Compat"] -git-tree-sha1 = "fd159bead0a24e6270fd0573a340312bd4645cc2" +git-tree-sha1 = "cdbbe0f350581296f3a2e3e7a91b214121934407" uuid = "c84ed2f1-dad5-54f0-aa8e-dbefe2724439" -version = "0.3.0" +version = "0.3.1" [[RecipesBase]] -deps = ["Random", "Test"] -git-tree-sha1 = "0b3cb370ee4dc00f47f1193101600949f3dcf884" +git-tree-sha1 = "7bdce29bc9b2f5660a6e5e64d64d91ec941f6aa2" uuid = "3cdcf5f2-1ef4-517c-9805-6587b60abb01" -version = "0.6.0" +version = "0.7.0" [[Reexport]] deps = ["Pkg"] @@ -326,10 +291,10 @@ uuid = "ae029012-a4dd-5104-9daa-d747884805df" version = "0.5.2" [[SCS]] -deps = ["BinaryProvider", "Compat", "Libdl", "MathOptInterface", "MathProgBase"] -git-tree-sha1 = "f3372fde752302d3cd38d00e2adaf3a7731f7061" +deps = ["BinaryProvider", "Libdl", "LinearAlgebra", "MathOptInterface", "MathProgBase", "SparseArrays"] +git-tree-sha1 = "f777069f119d26b021b773756c2510e4fb8a3f99" uuid = "c946c3f1-0d1f-5ce8-9dea-7daa1f7e2d13" -version = "0.5.1" +version = "0.6.2" [[SHA]] uuid = "ea8e919c-243c-51af-8825-aaa63cd721ce" @@ -355,16 +320,16 @@ deps = ["LinearAlgebra", "Random"] uuid = "2f01184e-e22b-5df5-ae63-d93ebab69eaf" [[SpecialFunctions]] -deps = ["BinDeps", "BinaryProvider", "Libdl", "Test"] -git-tree-sha1 = "0b45dc2e45ed77f445617b99ff2adf0f5b0f23ea" +deps = ["BinDeps", "BinaryProvider", "Libdl"] +git-tree-sha1 = "3bdd374b6fd78faf0119b8c5d538788dbf910c6e" uuid = "276daf66-3868-5448-9aa4-cd146d93841b" -version = "0.7.2" +version = "0.8.0" [[StaticArrays]] -deps = ["InteractiveUtils", "LinearAlgebra", "Random", "Statistics", "Test"] -git-tree-sha1 = "3841b39ed5f047db1162627bf5f80a9cd3e39ae2" +deps = ["LinearAlgebra", "Random", "Statistics"] +git-tree-sha1 = "1e9c5d89cba8047d518f1ffef432906ef1a3e8bd" uuid = "90137ffa-7385-5640-81b9-e52037218182" -version = "0.10.3" +version = "0.12.0" [[Statistics]] deps = ["LinearAlgebra", "SparseArrays"] @@ -387,12 +352,6 @@ uuid = "cf7118a7-6976-5b1a-9a39-7adc72f591a4" [[Unicode]] uuid = "4ec0a83e-493e-50e2-b9ac-8f72acf5a8f5" -[[WinRPM]] -deps = ["BinDeps", "Compat", "HTTPClient", "LibExpat", "Libdl", "Libz", "URIParser"] -git-tree-sha1 = "2a889d320f3b77d17c037f295859fe570133cfbf" -uuid = "c17dfb99-b4f7-5aad-8812-456da1ad7187" -version = "0.4.2" - [[WoodburyMatrices]] deps = ["LinearAlgebra", "Random", "SparseArrays", "Test"] git-tree-sha1 = "21772c33b447757ec7d3e61fcdfb9ea5c47eedcf" diff --git a/src/NeuralVerification.jl b/src/NeuralVerification.jl index aab69173..795b1f50 100644 --- a/src/NeuralVerification.jl +++ b/src/NeuralVerification.jl @@ -1,9 +1,9 @@ module NeuralVerification using JuMP -using PicoSAT # needed for Planet -using GLPK, SCS # SCS only needed for Certify +using GLPK, SCS # SCS only needed for Certify +using PicoSAT # needed for Planet using LazySets, LazySets.Approximations using Polyhedra, CDDLib @@ -76,10 +76,12 @@ include("reachability/ai2.jl") export ExactReach, MaxSens, Ai2 include("satisfiability/bab.jl") -include("satisfiability/planet.jl") include("satisfiability/sherlock.jl") include("satisfiability/reluplex.jl") -export BaB, Planet, Sherlock, Reluplex +export BaB, Sherlock, Reluplex + +include("satisfiability/planet.jl") +export Planet include("adversarial/reluVal.jl") include("adversarial/fastLin.jl")