Commits · 99f588ddf1c8d40632e2896b7433115390f9d6f3 · pub / caisar · GitLab

Snippets Groups Projects

May 25, 2023
- [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
- [interpretation] Remove notion of tensor from code and library. · 687dd42c
  Michele Alberti authored 1 year ago
  
  687dd42c
- [tests] Remove unnecessary files. · 2269f8ea
  Michele Alberti authored 1 year ago
  
  2269f8ea
- [tests] Fix constant pi value. · f64b4c6a
  Michele Alberti authored 1 year ago
  
  f64b4c6a
- [interpretation] Declare only logic symbols relative to classifiers and vectors. · 4ad94e14
  Michele Alberti authored 1 year ago
  
  4ad94e14
- [trans] Add transformation for simplifying linear inequalities. · 31beca91
  Michele Alberti authored 1 year ago
  
  31beca91
- [pyrat] Negate goal formula if needed. · 14592781
  Michele Alberti authored 1 year ago
  
  14592781
- [vnnlib] Just simplify already negated formula. · 02031377
  Michele Alberti authored 1 year ago
  
  02031377
- [marabou] Just simplify already negated formula. · a7465725
  Michele Alberti authored 1 year ago
  
  a7465725
- [verification] Early goal split before applying transformations. · 669b6cd3
  Michele Alberti authored 1 year ago
  
  669b6cd3
- [tests] Update test commands (not oracles). · 03794fb2
  Michele Alberti authored 1 year ago
  
  03794fb2
- [trans] Separate utility functions for gathering input symbols. · 0af3edb2
  Michele Alberti authored 1 year ago
  
  0af3edb2
- [trans] Fix utility count_nn_classifiers to count only different classifier symbols. · 0bebd680
  Michele Alberti authored 1 year ago
  
  0bebd680
- [interpretation] Remove interpret command and integrate task interpretation into verification. · ce07c066
  Michele Alberti authored 1 year ago
  
  ce07c066
- [drivers] Rework drivers for handling floats with rounding information. · a62054f6
  Michele Alberti authored 1 year ago
  
  a62054f6
- [tests] Use /\ instead of -> the most in ACAS-Xu. · cc4df3cc
  Michele Alberti authored 1 year ago
  
  cc4df3cc
- [main] Catch system errors. · 27a8f47e
  Michele Alberti authored 1 year ago
  
  27a8f47e
- [trans] Remove useless transformation sequencing. · 330a9345
  Michele Alberti authored 1 year ago
  
  330a9345