Commits · ba36a34d422e4df290a24feffbadb2ab58318a54 · pub / caisar

Sep 01, 2021
- Add PyRAT data for autodetection. · ba36a34d
  Michele Alberti authored 3 years ago
  
  ba36a34d
Aug 31, 2021
- Set autodetect debug flag wrt global caisar verbosity. · 9e5423c4
  Michele Alberti authored 3 years ago
  
  9e5423c4
Aug 13, 2021
- Add Marabou data for autodetection. · 06fe8467
  Michele Alberti authored 3 years ago
  
  06fe8467
Jul 30, 2021
- Rename caisar configuration file for autodetection. · ecb0735f
  Michele Alberti authored 3 years ago
  
  ecb0735f
- Some rework and plug config command in with autodection. · 85eb4067
  Michele Alberti authored 3 years ago
  
  85eb4067
Jul 23, 2021
- Some meaningless rework. · 015766f9
  Michele Alberti authored 3 years ago
  
  015766f9
- POC for autodetection and task printing · 3c04c325
  François Bobot authored 3 years ago
  
  3c04c325
Jul 21, 2021
- Version for ocamlformat. · 1dbc8a01
  Michele Alberti authored 3 years ago
  
  1dbc8a01
- Just some not so meaningful rework. · 1ac03fbe
  Michele Alberti authored 3 years ago
  
  1ac03fbe
Jul 16, 2021
- Add NNet input language · fcb78c15
  François Bobot authored 3 years ago
  
  fcb78c15
Jul 09, 2021
- Add Makefile · 0a6e75c7
  François Bobot authored 3 years ago
  
  0a6e75c7
- Start command line command config. · ab0b6cb7
  Michele Alberti authored 3 years ago
  
  ab0b6cb7
- Add csv package as dependency. · 9ceb4e8b
  Michele Alberti authored 3 years ago
  
  9ceb4e8b
Jun 30, 2021
- Use csv library to parse nnet model wrt CSV format. · 377c194e
  Michele Alberti authored 3 years ago
  
  377c194e
- Start version using Why3 and move out nnet parser. · 9aceca1a
  François Bobot authored 3 years ago and Michele Alberti committed 3 years ago
  
  9aceca1a
- Move first version to standalone directory · f93791f4
  François Bobot authored 3 years ago
  
  f93791f4
Jun 28, 2021
- Add ACAS XU property #1 in why3 syntax. · b146b421
  Michele Alberti authored 3 years ago
  
  b146b421
- Update dune-projet and opam file. · 60d33b29
  Michele Alberti authored 3 years ago
  
  60d33b29
May 17, 2021
- Merge branch 'feature/michele/elapsed-time' into 'master' · d0f5a885
  Michele Alberti authored 3 years ago
  
  Compute elapsed time for verifying a goal (in seconds). See merge request laiser/caisar!5
  d0f5a885
May 11, 2021
- Compute elapsed time for verifying a goal (in seconds). · 352a6235
  Michele Alberti authored 3 years ago
  
  352a6235
- Merge branch 'feature/michele/rework-sat-marabou' into 'master' · 5ba5de6a
  Michele Alberti authored 3 years ago
  
  Rework Marabou support in terms of satisfiability. See merge request laiser/caisar!4
  5ba5de6a
May 07, 2021
- Rework Marabou support in terms of satisfiability. · 34f22a4d
  Michele Alberti authored 3 years ago
  
  34f22a4d
- Try to extract the result first before checking return code of the run command. · 93957881
  Michele Alberti authored 3 years ago
  
  93957881
- Precise the pyrat regexp for the result. · 9f70807c
  Michele Alberti authored 3 years ago
  
  9f70807c
- Merge branch 'feature/michele/keep-tmp' into 'master' · a429d3c6
  Michele Alberti authored 3 years ago
  
  Do not remove temporary files on verbose mode Closes #4 See merge request laiser/caisar!3
  a429d3c6
- Fix temporary file removing on normal mode. · 13ffb566
  Michele Alberti authored 3 years ago
  
  13ffb566
May 06, 2021
- Remove temporary files only when computation correctly terminates. · e86dd911
  Michele Alberti authored 3 years ago
  
  e86dd911
- Remove temporary files only in app mode (keep them with verbosity activated). · e58920f9
  Michele Alberti authored 3 years ago
  
  e58920f9
Apr 29, 2021
- Update dune-project and opam files. · 6f81e06c
  Michele Alberti authored 3 years ago
  
  6f81e06c
- Do not print tasks when only one is present. · 0141f076
  Michele Alberti authored 3 years ago
  
  0141f076
- Fix style. · f85eb7e3
  Michele Alberti authored 3 years ago
  
  f85eb7e3
- Catch conversion failures. · 2a34193b
  Michele Alberti authored 3 years ago
  
  2a34193b
Apr 19, 2021
- Avoid to index subgoals when not needed. · 264d6732
  Michele Alberti authored 3 years ago
  
  264d6732
- Add support to axioms for input constraints. · 712afe63
  Michele Alberti authored 3 years ago
  
  712afe63
Apr 16, 2021
- Rework property language and restructure code. · 1525ffdd
  Michele Alberti authored 3 years ago
  
  1525ffdd
Apr 13, 2021
- Compute solver name list in help message. · e9e4df8e
  Michele Alberti authored 3 years ago
  
  e9e4df8e
Apr 10, 2021

Merge branch 'feature/unify-output' into 'master' · 181bcab3

Michele Alberti authored 3 years ago

Unify solver output to print just the result of verification.

Closes #1

See merge request malberti/caisar!2

181bcab3

Unify solver output to print just the result of verification. · 63663169

Michele Alberti authored 3 years ago

- Solver output is redirected to a temporary file.
- Result is extracted by means of regexps from such temporary file.

63663169

Mar 24, 2021
- Add some info logs about model format checking. · 3911f85d
  Michele Alberti authored 4 years ago
  
  3911f85d
Mar 18, 2021
- Fix the way a solver's executable is found and used. · f74e2942
  Michele Alberti authored 4 years ago
  
  f74e2942