If I mark it after (get-model)?

Question

If only (check-sat) is done, It mark as no sat. But if you try (get-model), it doesn't mark, and the error comes out right away. Is there any way that mark me without being error?

I struggle to understand the meaning of the verb *"to mark [something/someone]"* in your question, and what you are asking here. Please edit your question and include a [MCVE](https://stackoverflow.com/help/minimal-reproducible-example). It seems that you are dealing with an **unsatisfiable** formula, for which there is no model. You may want to use `z3`'s API (e.g. its Python API) to solve your problem, rather than running the tool from the command-line. That will make it easier to deal with unsatisfiability and fiddle with the formula to enumerate all of its models. — Patrick Trentin, Sep 29 '19 at 09:38

score 1 · Accepted Answer · answered Sep 29 '19 at 16:24

As Patrick commented, it's really hard to decipher what you're asking. Please provide some code snippets to show what you get and what you hope to achieve.

Having said that, I'll take a wild guess that you are in a situation where the solver is unsat, i.e., (check-sat) returns an unsat response. Yet, your script has (get-model) in the next line, which of course errors out since there's no model. And you'd like a way to avoid the error message.

This is a known limitation of SMTLib command language: You cannot programmatically inspect the output of commands, unfortunately. The usual way to solve this sort of problem is to have a "live" connection to the solver (typically in the form of a text pipe), and read a line after issuing (check-sat), and programmatically continue depending on the response. This is how most systems built on top of SMT-solvers work.

Alternatively, you can use higher-level APIs in other languages (C/C++/Java/Python/Haskell..) and program z3 that way; and use the facilities of the host language to direct that interaction. This requires you to learn another interface on top of SMTLib, but for serious uses of this technology, you probably don't want to limit yourself to a pure SMTLib interface anyhow.

Also see this answer for a related discussion: Executing get-model or unsat-core depending on solver's decision

Hope this addresses your issue, though it's hard from your question whether this is what you were getting at.

If I mark it after (get-model)?

1 Answers1