Search code examples
z3smt

Are C API more problematic than standard inputs SMTLIB2 for z3?

I'm completely new to z3. I wonder what the difference is between the two inputs, Are C API more problematic than standard inputs SMTLIB2 for z3? I would appreciate it if you could answer_(:з」∠)_

Solution

  • I'm not sure what you mean by "problematic." You'd use the C-API if you want to integrate z3 into a C/C++ based framework. You'd use SMTLib if you want a common language understood by many solvers, not just z3. So, it really depends on what your goals are.

    If you're just experimenting with it, I'd advise using an interface in a higher level language like Python, as it is much easier to get started. SMTLib is generally not intended for human consumption, but rather generated by other programs. Only use the C/C++ API if you have some other requirement that requires you to stay in C/C++.

    Long story short, it really depends on what your goal is; if you tell us more about what your use case is, we can recommend something more specific.