Disable modules to reduce binary size

[chriseth]

Sorry if this is more a question than an issue to be reported.

We are trying to integrate z3 into a compiler ( http://github.com/ethereum/solidity/ ) but are currently a little hesitant to make the z3 library mandatory due to its size. I have seen that some parts of the source have a plugin architecture. Is it possible to disable unneeded plugins at compile time to reduce the size of the binary?

[NikolajBjorner]

We haven't exposed compile-time slicing. Indeed the size of the library / executable has been steadily growing and will keep growing as features are added. The plugin architecture is dynamic and for theory solvers or tactics that are used in some cases. If you would want to slice away tactics or solvers it would have to be in a specialized build. Not sure how strongly the linker slice away dead code. If it does a good job, then perceivably one can slice tactics away to creating compile time variants of the ADD_TACTIC macro. Other components are tougher to prune. For example, nlsat is a standalone module that is used 2-3 places as part of tactics (and any time also theory solvers). the "sat" module is used for bit-vector intensive problems. It's likely you need this. The "lp" module solves LRA at this point over theory_lra. etc.

[delcypher]

@chriseth Support for statically disabling components is not implemented but it is definitely do-able. If you're going to give this a go I'd advise you do this in the CMake build system and not the legacy build system because you're going to have an easier time.

If you look at https://github.com/Z3Prover/z3/blob/d2e27f6f1f33cf6e0ae05cb78976a35fd6423f5f/src/CMakeLists.txt#L111 you can see that the list of components comes from a global property named Z3_LIBZ3_COMPONENTS. This component gets appended to by the z3_add_component macro.

https://github.com/Z3Prover/z3/blob/d2e27f6f1f33cf6e0ae05cb78976a35fd6423f5f/cmake/z3_add_component.cmake#L46-L283

You can use this as basis for statically disabling components. Here is a sketch for how I think you should implement this.

1. Add a new CMake cache option Z3_ENABLED_COMPONENTS that is a list of Z3 components to include in libz3. This value would be used in the z3_add_component() macro and it would not not build that component (and therefore not append to the component to Z3_LIB_Z3_COMPONENTS) if the value does not appear in the list. However we will have a special all value for this list that means build all components.

2. Teach z3_add_component() to define a component specific compiler macro (e.g. Z3_COMPONENT_NLSAT_ENABLED) when the component is actually enabled and then conditionalize using#ifdef`s all of Z3's code where those components get loaded so that it is possible to compile Z3 without some components loaded.

This would then allow you as a consumer of Z3 to set Z3_ENABLED_COMPONENTS to be whatever you want at configure time.

One thing that will need careful handling is transitive dependencies. You need to decide if it's the user's job to explicitly list transitive dependencies in Z3_ENABLED_COMPONENTS or if they should be inferred automatically. If they are to be inferred automatically the implementation will be more complicated.

[rainoftime]

@delcypher @NikolajBjorner I believe further efforts are deserved to make z3's build system more flexible and adjustable. Suppose a user only needs the bit-blasting based bit-vector solver(qfbv_tactic), it seems we can make z3 much smaller.

[delcypher]

@chriseth Just to note. Seeing as I have the CMake expertise here I don't mind implementing the CMake side of this for you but I'd probably need some help to write the Z3 code that handles the cases when certain components are not compiled in.

[wintersteiger]

@rainoftime The "bit-blasting bit-vector solver" is not a single, isolated piece of code. It is implemented via multiple preprocessing tactics (i.e. you need the complete tactic framework), then the SAT solver, but also the SMT solver, in case there are uninterpreted functions in the problem (e.g. bit-vector division by 0). So, in the end you'll need pretty much everything anyways... I'm not sure this will be worth the effort.

In the past I've also compiled Z3 to a static library ( --staticlib on mk_make.py ). This may help to get the size of your binaries down a little, if the compiler finds that some things aren't used. But, I think the main reason for the huge binary is the extensive use of C++ templates and inlined functions, resulting in lots of duplicated binary code. It would be great if someone could look into that! Are there any tools that try to identify such problems?