Commits · 08183a408f6cd44d7d77c99b21094490779f229c · pub / caisar · GitLab

Snippets Groups Projects

Jun 02, 2023
- [aimos][saver] Uniformize code style. · 08183a40
  Michele Alberti authored 1 year ago
  
  08183a40
- [verification] Factor out code for building the prover command. · 3a593054
  Michele Alberti authored 1 year ago
  
  3a593054
- [config] Add first support for abcrown config files. · 293ef4db
  Michele Alberti authored 1 year ago
  
  293ef4db
May 31, 2023
- Merge branch 'feature/tristan/abcrown' into 'master' · 4e6567fb
  Michele Alberti authored 1 year ago
  
  Add support for alpha-beta-CROWN See merge request laiser/caisar!86
  4e6567fb
- [trans] Better code style. · 8ca73d5f
  Michele Alberti authored 1 year ago
  
  8ca73d5f
- [config] Fix result interpretation in abcrown driver. · dd181d55
  Michele Alberti authored 1 year ago
  
  dd181d55
- [trans] Add comments to and rename the native nn prover transformation. · 4a6046da
  Michele Alberti authored 1 year ago
  
  4a6046da
May 30, 2023
- [trans] Add meta related to nn filename once, just when encountering its declaration. · 6e354031
  Michele Alberti authored 1 year ago
  
  6e354031
- [interpretation][trans] Use caisar_x/caisar_y to refer to input/output variables. · 7c92a88b
  Michele Alberti authored 1 year ago
  
  7c92a88b
May 29, 2023
- [trans] Declare all output variables for nn native transformation. · 500c1a3a
  Michele Alberti authored 1 year ago
  
  500c1a3a
May 25, 2023
- [language] Use common function for building float64 type symbol. · a2a2b924
  Michele Alberti authored 1 year ago
  
  a2a2b924
- [language] Rework neural networks interface. · e4fd53c3
  Michele Alberti authored 1 year ago
  
  e4fd53c3
- [interpretation] Remove type alias for term lsymbol. · b6ed30cd
  Michele Alberti authored 1 year ago
  
  b6ed30cd
- [printers] Shorten code style for PyRAT printer. · 3b3bb6aa
  Michele Alberti authored 1 year ago
  
  3b3bb6aa
- [printers] declare-const must have Real type in VNN-LIB printer. · f7359a4f
  Michele Alberti authored 1 year ago
  
  f7359a4f
- [trans] Make metas appear before actual corresponding input/output variable declarations. · 54db081e
  Michele Alberti authored 1 year ago
  
  54db081e
- [verification] Add other cases which abcrown may be used for. · 4a36e432
  Michele Alberti authored 1 year ago
  
  4a36e432
- [abcrown] Rework driver. · 99f588dd
  Michele Alberti authored 1 year ago
  
  99f588dd
- [tests] Add abcrown to autodetection test, plus some fixes. · 50aeffb5
  Michele Alberti authored 1 year ago
  
  50aeffb5
- [config] Rework scripts for launching nnenum and abcrown, and their dummy version. · 6234ff47
  Michele Alberti authored 1 year ago
  
  6234ff47
- [abcrown] Add support for the prover alpha-beta-CROWN. · c80215e4
  Tristan Le Gall authored 1 year ago and Michele Alberti committed 1 year ago
  
  c80215e4
May 24, 2023
- [printers] Fix newline after goal formula for PyRAT. · f9ac6d8a
  Michele Alberti authored 1 year ago
  
  f9ac6d8a
- [ci] Rework descriptions of the make_public stage and targets. · a89585eb
  Michele Alberti authored 1 year ago
  
  a89585eb
May 23, 2023
- Merge branch 'feature/michele/interpretation' into 'master' · baf3f20c
  Michele Alberti authored 1 year ago
  
  Integrate interpretation See merge request laiser/caisar!80
  baf3f20c
May 17, 2023
- [printers] Add ending newline after goal formula for PyRAT. · e1ec3fd1
  Michele Alberti authored 1 year ago
  
  e1ec3fd1
- [printers] Support lt and gt as relational operators for Marabou. · 77baf78f
  Michele Alberti authored 1 year ago
  
  77baf78f
- [interpretation] Some function renaming. · bdbbde88
  Michele Alberti authored 1 year ago
  
  bdbbde88
- [interpretation] Hack to reconstruct original non-interpreted terms. · e67a9505
  Michele Alberti authored 1 year ago
  
  e67a9505
- [interpretation] Rename utility functions for building CRE values. · ad9802e7
  Michele Alberti authored 1 year ago
  
  ad9802e7
- [interpretation] Remove scopes from library theories. · a88e69dd
  Michele Alberti authored 1 year ago
  
  a88e69dd
- [verification] Interpret task for classic provers also. · 4ca9b508
  Michele Alberti authored 1 year ago
  
  On such tasks, the interpretation should provide no effect.
  4ca9b508
- [proof_strategy] Strategy for native nn provers splits top-level conjunctions in goal formula. · 77c43c8f
  Michele Alberti authored 1 year ago
  
  77c43c8f
- [interpretation] Clean up and update codebase wrt interpretation. · 3901e213
  Michele Alberti authored 1 year ago
  
  3901e213
- [interpretation] Rename infix operator for neural network application. · 96aa0a0c
  Michele Alberti authored 1 year ago
  
  96aa0a0c
- [interpretation] Remove comments only useful for debugging. · 5ed733e2
  Michele Alberti authored 1 year ago
  
  5ed733e2
- [stdlib] Prefer using more generic theory name NeuralNetwork. · 11812fc7
  Michele Alberti authored 1 year ago
  
  Instead of Classifier. Also update the codebase accordingly.
  11812fc7
- [interpretation] Extract Language lsymbols declaration into a function. · ad0772ab
  Michele Alberti authored 1 year ago
  
  ad0772ab
- [interpretation] Proper silencing of warning for debug printing. · fc78a9d1
  Michele Alberti authored 1 year ago
  
  fc78a9d1
- [interpretation] Prefer using type name also for values. · c3a76ebd
  Michele Alberti authored 1 year ago
  
  c3a76ebd
- [language] Do not use type alias as type inference becomes confused. · ad2f7fc0
  Michele Alberti authored 1 year ago
  
  ad2f7fc0