`check-sat-assuming` seems broken

[LeventErkok]

For this input:

(set-option :produce-models true)
(set-logic QF_BV)
(declare-fun s0 () (_ BitVec 32))
(define-fun s1 () (_ BitVec 32) #x0000000a)
(define-fun s2 () Bool (bvugt s0 s1))
(check-sat-assuming (s2 (not s2)))
(get-unsat-assumptions)

I'm getting:

(error "line 6 column 24: invalid check-sat command, argument must be a Boolean literal")
unsupported
; get-unsat-assumptions line: 7 position: 22

I do believe the input format is correct for check-sat-assuming, so I'm curious why z3 is saying the arguments are not boolean.

Also, am I to conclude get-unsat-assumptions isn't implemented yet? That seems rather unfortunate given there seems to be support for check-sat-assuming.

[delcypher]

@LeventErkok

(error "line 6 column 24: invalid check-sat command, argument must be a Boolean literal") unsupported

Neither s2 nor (not s2) are boolean literals. They are of boolean type but they are definitely not literals.

[LeventErkok]

@delcypher You mean they are not true or false? I'm not sure what's a literal in this context.

My understanding is that the command is supposed to take variables instead of expressions. How else would one use it?

[delcypher]

Try this

(set-option :produce-models true)
(set-logic QF_BV)
(declare-fun s0 () (_ BitVec 32))
(define-fun s1 () (_ BitVec 32) #x0000000a)
(define-fun s2 () Bool (bvugt s0 s1))
(declare-const x Bool)
(assert (= x s2))
(check-sat-assuming (x (not x)))

I've not used the feature but I believe the expressions given to check-sat-assuming must be a boolean variable (e.g. x in the above example) or its negated value.

[LeventErkok]

Ah, I see.. OK.. Though It seems rather restrictive. I tried MathSAT and it actually took the original unmodified.

I'll leave this ticket here to see if you guys want to relax the restriction a bit, but feel free to close otherwise.

Re get-unsat-assumptions: Am I correct to assume it won't be supported any time soon?

[delcypher]

@LeventErkok I believe that's the smtlib standard ( see http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.5-r2015-06-28.pdf )

4.2.5 Checking Satisfiability

(check-sat-assuming (a1 · · · an))
where n ≥ 0 and a1, · · · , an are terms of sort Bool, instructs
the solver to check whether the conjunction of all the formulas in the current
context and the assumptions a1, · · · , an is satisfiable in the extension
of the current logic with all the current user-declared and user-defined symbols.
The assumptions a1, . . . , an can only have the form 
p or (not p) where p is a user-declared/defined Boolean constant,
i.e., a nullary function symbol of sort Bool

[LeventErkok]

@delcypher Thanks for the reference.. I find it very confusing and overly restrictive though. So,

(define-fun s2 () Bool (bvugt s0 s1))

does not make s2 a term of sort Bool? It looks like a "nullary function symbol of sort Bool" to me.

But this isn't hard to work around, if the limitation cannot be relaxed.

[NikolajBjorner]

define-fun acts as a macro declaration, so it represents (bvugt s0 s1). The restriction to use literals is a recurring pain. The reason is that formulas are generally pre-processed and therefore can be split or reassembled in arbitrary ways so we would not be able to track them as assumptions. One tradeoff is to allow arbitrary formulas, but forgo either that learned lemmas that are independent of the assumptions are retained or accumulate auxiliary formulas that introduce auxiliary literals on the side.

[LeventErkok]

Thanks @delcypher @NikolajBjorner . Very helpful.

Working around this isn't a big deal.

Any chance get-unsat-assumptions will work soon?

[delcypher]

@NikolajBjorner Side note. Does using check-sat-assuming offer any performance advantage in Z3? The SMTLIB reference is not very useful in this regard. It doesn't explain why anyone would use this feature.

[LeventErkok]

@delcypher I think it avoids pushing/popping a context at it "implicitly" creates one. That's the user side of things of course.

[NikolajBjorner]

get-unsat-assumptions was disabled. It is a newer feature. Z3 for a long time supported get-unsat-core based on check-sat with optional assumptions.

[LeventErkok]

Fantastic! Thanks for re-enabling it. I do agree that unsat-core's are easier to use due to :named parameters, but for completeness it's nice to have both.