CODEWITHSUNDEEP
leon
Ravi Mad
Ravi Mad

Reputation: 48

Why are there multiple options for the same SMT solver

In Leon verifier, why are there different options that use the same solver even when inductive reasoning happens within Leon? Eg. all the 3 options: fairz3, smt-z3 and unrollz3 seem to use a z3 solver and perform inductive reasoning in leon.

Upvotes: 1

Views: 69

Answers (1)

Regis Blanc
Regis Blanc

Reputation: 549

All three options are doing the thing in principle, but differ slightly in implementation (leading to different performances/reliability).

The fairz3 option use the native Z3 api (via the ScalaZ3 library) while the smt-z3 communicates with a Z3 process standard input (using the SMT-LIB standard via the Scala SMT-LIB library). In order to use smt-z3 you will need to make sure a z3 command is in your PATH.

With fairz3, Leon and Z3 are running in the same process, which means that a crash in Z3 would bring down the whole process, and there is nothing that can be done in Leon to prevent it. When using smt-z3, we run Z3 as a separate process, and we can run Leon in isolation from that process. The process can be killed at any point if it becomes unresponsive (or if Leon decides to time out the solver).

The fair name is due to historical reason. The original implementation of Leon was based on the native API of Z3 (apparently for performance reason, it is faster to build formula trees directly in Z3 instead of building them in Leon and then translating them for Z3). The solver in Leon ended up being named FairZ3Solver, with Fair as in fair unrolling of the functions. All the unrolling logic was mixed with Z3 communication.

There is a second (new) implementation of the inductive unrolling in Leon (known as UnrollingSolver) that is independent of the underlying solver (Z3, CVC4, RandomSolver). That unrolling is just as "fair" as the one provided by fairz3. When you use unrollz3 you are using this UnrollingSolver (which is also used with smt-z3) with the underlying solver being the native interface of Z3 (not using SMT-LIB text interface). The main difference with FairZ3Solver is that, besides being more general, the unrolling is done on Leon tree. This slightly impacts the performance.

Upvotes: 1

Related Questions