From 032e30d89cf9d684ab419e80172caae9fc0ad324 Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Wed, 14 Dec 2022 12:05:50 +0100
Subject: [PATCH] Update changelog and readme files.

---
 CHANGES.md | 11 +++++++++++
 README.md  | 11 +++++++----
 2 files changed, 18 insertions(+), 4 deletions(-)

diff --git a/CHANGES.md b/CHANGES.md
index bd3f5e07..3c2441c1 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -1,5 +1,16 @@
 ## 0.1.1 (Unreleased)
 
+- Add `verify-json` command for verifying a robustness property via a JSON
+  configuration file.
+- Integration of the [nnenum](https://github.com/stanleybak/nnenum) prover.
+- Add printer for VNN-LIB format for property specification as supported by the
+  `nnenum` prover.
+- Add transformation to translate ONNX format into SMT-LIB format for allowing
+  classic solvers to understand and operate on neural networks.
+- Add verification of datasets for classification tasks in terms of a specific
+  CSV format: each line provides the label in 1st column, and data features in
+  the other columns. Also, add builtin implementations of min-max scaling and
+  z-score normalization for data normalization.
 - Rework the section in `README.md` for obtaining CAISAR in order to mention the
   `opam` package just released.
 
diff --git a/README.md b/README.md
index c75e1687..25e60087 100644
--- a/README.md
+++ b/README.md
@@ -102,13 +102,16 @@ $ caisar config --detect
 
 The following are the provers for which a support is provided in CAISAR:
 
-* PyRAT (to be released)
+* PyRAT
 * [Marabou](https://github.com/NeuralNetworkVerification/Marabou)
+* [nnenum](https://github.com/stanleybak/nnenum)
 * [SAVer](https://github.com/abstract-machine-learning/saver)
 
-Under active development is the support for the [SMT-LIB](https://smtlib.cs.uiowa.edu/) which
-is used by many satisfiability modulo theories solvers (e.g. [Alt-Ergo](https://alt-ergo.ocamlpro.com/),
-[Z3](https://github.com/Z3Prover/z3/wiki), [Colibri](https://colibri.frama-c.com/), etc.).
+Moreover, CAISAR supports the [SMT-LIB](https://smtlib.cs.uiowa.edu/) format
+which is used by many satisfiability modulo theories solvers (e.g.
+[Alt-Ergo](https://alt-ergo.ocamlpro.com/), [cvc5](https://cvc5.github.io/),
+[Z3](https://github.com/Z3Prover/z3/wiki),
+[Colibri](https://colibri.frama-c.com/), etc.).
 
 ## Advanced usage
 
-- 
GitLab