Z3 4.0: get complete model

2
votes

I need a complete model of an SMTLIB2 formula:

http://pastebin.com/KiwFJTrK

Z3 (version 3.2 and 4.0) returns values for all variables but not for var4. I tried some configuration settings like 

MODEL_COMPLETION = true

but it did not seem to work. Does anybody have a suggestion? CVC3 in comparison returns a model (including var4), so it is not an issue of SMTLIB or my example.

The reason I need this is explained here in detail. In short: I want to use the C API for incremental solving. For this reason I have to use the function Z3_parse_smtlib2_string multiple times. This function needs previously declared functions and constants as parameters. I am unable to get this information via Z3_get_smtlib_decl because these kind of functions work just when z3_parse_smtlib_string is called, not Z3_parse_smtlib2_string.

1
z3

1 Answers

3
votes

You can avoid this problem by adding the following option in the beginning of your script.

(set-option :auto-config false)

I will fix it for the next release. Here is a short explanation of what is going on. Z3 has a solver for 0-1 integer problems. After preprocessing, your script is tagged as a 0-1 integer problem by Z3. The value of var4 is a "don't care" when the problem is viewed as a 0-1 problem, but it is not a "don't care" when the problem is viewed as an integer problem (var4 must be 0 or 1). By default, Z3 will not display the value of "don't care" variables.

The MODEL_COMPLETION=true will complete the model as you request values for constants that are not included in the model. For example, if we execute (eval var4), Z3 will produce an interepretation for var4.