Get-assignment in Z3

Question

The (get-assignment) command should return a list of symbols and their true/false value if they are of sort Bool. From my understanding, this can only be done if :produce-assignments is set to true, and when (check-sat) returns sat. However, when I run a small script to test this on Z3, (get-assignment) just returns () - blank. Here is my script:

(set-option :produce-assignments true)
(set-logic QF_UF)
(declare-fun a () Bool)
(declare-fun b () Bool)
(assert (= a b )) 
(check-sat)
(get-assignment)

For what it's worth, I can confirm this behaviour for Z3 [version 4.3.2 - 64 bit - build hashcode 96f4606a7f2d]. Interestingly, putting (set-option :produce-models true) into the preamble and placing (get-value (a b)) after (check-sat) yields ((a false)(b false)), so the assignment seems to be available (see rise4fun.com/Z3/zGH7). It looks as if (get-assignment) were not supported and as if using it didn't raise an error. — Malte Schwerhoff

Leonardo de Moura Leonardo de Moura · Accepted Answer · 2013-05-08T14:22:27

The semantics of get-assignment is not intuitive. It displays the value of named subformulas. From the SMT 2.0 reference (page 62):

get-assignment is a light-weight and restricted version of get-value that asks for a truth assignment for a selected set of previously entered formulas.(29) Similarly to several other commands already discussed (e.g., get-proof), this command can be issued only if the produce-assignments option, which is false by default, is set to true (see Section 5.1.7 below). Solvers are not required to support this option. Like get-value, it can be issued only following a check- sat command that reports sat or, optionally, also one that reports unknown, without intervening assertion-set commands. The command returns a sequence of all pairs (f b) where b is either true or false and f is the label of a (sub)term of the form (t named f) in the set of all assertions, with t of sort Bool. Similarly to get-value, when the response of the most recent check-sat command was sat, and only then, the set of all assertions is guaranteed to have a model (in the logic) that agrees with the returned truth assignment.

Here is the same example using two named subformulas (also available online here):

(set-option :produce-assignments true)
(set-logic QF_UF)
(declare-fun a () Bool)
(declare-fun b () Bool)
(assert (! (= (! a :named a_val) b ) :named eq_val)) 
(check-sat)
(get-assignment)

Get-assignment in Z3

1 Answers