Code

Optimizations#87

Code

Merged

guykatzz merged 33 commits intomasterNeuralNetworkVerification/Marabou:masterfrom cmd_line_optionsNeuralNetworkVerification/Marabou:cmd_line_optionsCopy head branch name to clipboardAug 22, 2018

+1,828-197

Commits

Commits on Aug 14, 2018

• initial work

  GuyKatzHuji

  committed
  21c5721

• cleanup

  GuyKatzHuji

  committed
  10846af

• introducing an Options singleton

  GuyKatzHuji

  committed
  8bcf079

Commits on Aug 15, 2018

• WIP

  GuyKatzHuji

  committed
  02562e3

Commits on Aug 16, 2018

• boost

  Show description for 7fe9b87
  GuyKatzHuji

  committed
  7fe9b87

• a basic executable, capable of taking an NNET file from the command

  Show description for e6d23b4
  GuyKatzHuji

  committed
  e6d23b4

• get number of inputs and outputs

  GuyKatzHuji

  committed
  4e0ebc1

• input query supports inputs and outputs

  GuyKatzHuji

  committed
  786a459

• basic working example of taking as input a network and a property

  Show description for 77e3dd1
  GuyKatzHuji

  committed
  77e3dd1

• regress makefile

  GuyKatzHuji

  committed
  979e17e

• fix regress makefile

  GuyKatzHuji

  committed
  707362d

• when SAT, print inputs and outputs

  GuyKatzHuji

  committed
  730051b

• added support for properties with equations of the form x1 + x2 >= 5

  Show description for 681eae9
  GuyKatzHuji

  committed
  681eae9

• cleanup

  GuyKatzHuji

  committed
  e48a622

Commits on Aug 19, 2018

• support for input/output variabels also in the preprocessor

  GuyKatzHuji

  committed
  7def995

• Merge branch 'master' into cmd_line_options

  GuyKatzHuji

  committed
  316e0c5

• special treatment for properties that include bounds, not just equations

  GuyKatzHuji

  committed
  1d65835

• some easy optimizations

  GuyKatzHuji

  committed
  c8e04e0

• cleanup: remove the basis factorization flag

  GuyKatzHuji

  committed
  d1afdae

• preparing the infrastructure for sparse FT

  GuyKatzHuji

  committed
  7858e99

• more infrastructure

  GuyKatzHuji

  committed
  60da3fd

• reset H (the equivalent of emptying the eta queue)

  GuyKatzHuji

  committed
  173bc78

• use H as a marker for when the explicit basis is avaialble

  GuyKatzHuji

  committed
  f52ec35

Commits on Aug 20, 2018

• first version of sparse FT (not tested yet)

  GuyKatzHuji

  committed
  570e24f

Commits on Aug 21, 2018

• FT unit tests are passing

  GuyKatzHuji

  committed
  66da99c

• include also the sparse bases

  GuyKatzHuji

  committed
  f5f78fb

• computing the explicit basis stored in the FT factorization (for

  Show description for 18f8a59
  GuyKatzHuji

  committed
  18f8a59

Commits on Aug 22, 2018

• debugging: comptue and dump the explicit basis

  GuyKatzHuji

  committed
  a284a4a

• a mechanism for fixing the permutation matrix P used for comuting L,

  Show description for b1898ab
  GuyKatzHuji

  committed
  b1898ab

• WIP

  GuyKatzHuji

  committed
  4a15152

• refactorization

  GuyKatzHuji

  committed
  301ebdf

• cleanup

  GuyKatzHuji

  committed
  48878dc

• cleanup

  GuyKatzHuji

  committed
  8150fce