caisar

How to add a solver

Make sure the solver is added to your systems for tests. Simplest way to do that is to add the binary directly to the root of CAISAR repo.

1. Create a new_solver.drv in config/drivers/. A driver is a serie of whyml modules describing the theories the solver will use during its call by why3. It is also parsing the output of the solver and sending it to why3 inner representation.

2. Add a new field inside of config/caisar-detection-data.conf. Here, you need to define the name of the solver's executable as well as the supported versions for CAISAR. You also need to define the command that the solver will execute. There are several Why3 built-in identifiers:

• %f is for a file
• %e is for the executable We also added custom identifiers: %{nnet-onnx} and %{svm}. Those identifiers will be replaced in src/verification.ml by their actual value (the model filename).

1. Now, the solver will be recognized by CAISAR. However, in order to exploit it, you should write a printer of its output in src/printers/. This printer should have a init function that must be called at the top of src/main.ml. A printer is something that, given a Why3 formula, transform it into something the solver can use.