Recover changes in native_nn_prover from varasse experiments.

See merge request laiser/caisar!140

François Bobot authored 11 months ago and Michele Alberti committed 9 months ago

   So an invariant for normal formula is that application of nn are always of the shape `nn@@vv[cst]`

François Bobot authored 11 months ago and Michele Alberti committed 9 months ago

    But (y * 56) + 12 < 34 is not handled

Ensure goal is printable by the VNNLIB printer

See merge request laiser/caisar!132

Once negated, consider the conjunctive normal form (CNF) of the goal if it is
not printable as is. This prevents failures on formula which are OK besides
their form. Indeed, CNF is logically equivalent to the original formula.

Parse NNet format into NIER

See merge request laiser/caisar!128

Keep only the new IR

See merge request laiser/caisar!136

Julien Girard-Satabin authored 10 months ago and Michele Alberti committed 10 months ago

Moved a lot of files in the process.

Add support for Maraboupy

See merge request laiser/caisar!135

Feature/bobot/mk onnx

See merge request laiser/caisar!123