Generalize Nim API - Githubissues

pmetras commented 4 years ago

Though nimz3 is based on Z3 integration into Nim, I think that to open the syntax to other SMT libraries (like CVC4, SMT-RAT, veriT, etc.), you should define a more general API without direct reference to Z3.

The SMT DSL that you defined in nimz3 is simple and general enough that it shouldn't be bound to Z3 only.

You would only have to rename the public facing keywords: z3: block and Z3Exception exception as far as I see. I'm not good at suggesting replacement keywords, but let's try:

for the z3: template: theory: or smt_theory:, smt:, problem:, solver:
for the exception: SMTException for general error and/or add SMTUnsatException for unsatisfiability and SMTUnknown in case of indecidability.

Do you need to expose the Z3_L_TRUE, Z3_L_FALSE and Z3_L_UNDEF constants for general user problem solving? If that's the case, perhaps they could be hidden in a general enum. The examples should be rewritten to replace if s.check() == Z3_L_TRUE: with s.check_model: or change check() signature to use this enum.

Araq commented 4 years ago

Good point about the enum. The DSL should be changed once we have a second backend, not before we have one.

pcarbonn commented 4 years ago

I would propose to have a syntax aligned with the SMTLIB language.

zevv / nimz3

Generalize Nim API #3