Z3 allows creating a function called "true"

[cheshire]

Using C API I was able to create a 0-argument UF which is called "true", which caused a lot of chaos down the line. Created formula can not even be dumped and parsed by Z3, as "true" is a reserved word.

I think creating functions with such a name should be disallowed.

[wintersteiger]

Can you add a little more detail for this problem? I've tried replicating it, but everythings seems to be working OK. Sure, the name clash can be confusing and should perhaps be avoided anyways, but as of now I'm not sure this is actually at the heart of the problem that you're experiencing. Here's what I tried: test input (feel free to modify).

[cheshire]

After you have such a function created, try serializing the formula with it, and then reading it back using the corresponding Z3 functions for SMT-LIB serialization.

[wintersteiger]

There's too many different ways to do that, just paste your SMT2 file? The problem's likely in the parser anyways, because 'true' is indeed a keyword in SMT2 (but not in Z3; but perhaps it should be).

[cheshire]

@wintersteiger I have used benchmark_to_smtlib_string followed by parse_smtlib2_string.

The problem's likely in the parser anyways, because 'true' is indeed a keyword in SMT2 (but not in Z3; but perhaps it should be).

Yes, so I think that if you allow SMT-LIB serialization it should be a keyword in Z3 as well (otherwise the serialized formula is not valid).

[wintersteiger]

benchmark_to_smtlib_string does not contain a "2" in it's name. It's an SMT1 function, the output is not necessarily compliant with the SMT2 standard.

(although setting the default printer mode to SMT2 it can be close to that).

[wintersteiger]

So, using benchmark_to_smtlib_string in my example I can get this:

(declare-fun true () Bool)
(assert (= true false))
(check-sat)

and Z3 rightly complains:

(error "line 1 column 26: invalid declaration, builtin symbol true")

Did you call the file something.smt2 or pass the -smt2 option, so that Z3 knows which parser to use?

[cheshire]

It's an SMT1 function, the output is not necessarily compliant with the SMT2 standard.

Ah, ok, I haven't realized that.

I thought it would be a useful sanity check, as one can shoot themselves in the foot by creating such a function and then being extremely confused on what does it do. Feel free to close otherwise.

[wintersteiger]

Absolutely, as it is, those functions are hard to use at the best of times. Since SMT1 has been deprecated for a long time (even if your functions weren't marked as such), I think we should remove support for that altogether. @NikolajBjorner what do you think, can we kill benchmark_to_smtlib_string or is there some case for keeping and maintaining it further?

[cheshire]

We actually extensively use benchmark_to_smtlib_string to pass formulas between different solvers. Or maybe there's some other function we should use instead?

[wintersteiger]

Yes, you should use SMT2. There are functions for parsing files and strings (Z3_parse_smtlib2*) and expressions can be translated to SMT2 by using Z3_ast_to_string after the default print mode is set to Z3_PRINT_SMTLIB2_COMPLIANT via Z3_set_ast_print_mode. When that is done, Z3_solver_to_string will also produce SMT2 compliant output, including declarations (either by default or after setting an option, not sure whether one of us wrote the code for that down already).

[cheshire]

OK thanks! If formula with a 0-argument UF called "true" can be created, can it be serialized to SMT-LIB2 at all?

[wintersteiger]

It can be written down, but the SMT2 frontend will reject it later. If you expect to clash with SMT2-defined function names (this applies not just to the core Boolean functions, but also too all other theory functions), then you may find it easier to just prefix every function name with _ or something like that, so you're sure you only use your own functions.

[NikolajBjorner]

You can also use the Z3_solver_to_string method to generate SMT-LIB2 benchmarks.

[NikolajBjorner]

I am inclined to punt on adding checks for basic names in the API functions that create function declarations. The issue is going to be that different theories are loaded on demand. So what is a reserved name changes depending on what theories you load in SMT-LIB2. The connection between SMT-LIB2 and binary API will have to be up to proper behavior of the caller. Z3 already determines when a string used for a symbol has to be quoted.

[cheshire]

Sorry for the late reply!

Yes, you should use SMT2. There are functions for parsing files and strings (Z3_parse_smtlib2*) and expressions can be translated to SMT2 by using Z3_ast_to_string after the default print mode is set to Z3_PRINT_SMTLIB2_COMPLIANT via Z3_set_ast_print_mode. When that is done, Z3_solver_to_string will also produce SMT2 compliant output, including declarations (either by default or after setting an option, not sure whether one of us wrote the code for that down already).

It feels rather redundant to create a solver and add an assertion just to perform a serialization, discarding the solver object later. Should I just ignore that feeling and use that procedure for serialization?

[wintersteiger]

Yes. We don't offer full serialization at the moment, so some computational effort is required to be visible on your end (and we'd do the same internally, you just wouldn't see it).