Soundness: SetHasSize results in an incorrect `unsat` answer

[LeventErkok]

@rainoftime

This is most likely related to https://github.com/Z3Prover/z3/issues/3854

The original discussion was on stack-overflow: https://stackoverflow.com/questions/63983897/using-sets-and-sethassize-on-intersections-in-z3

For this Python program:

from z3 import *

A, B = Consts('A B', SetSort(IntSort()))
s = Solver()
s.add(SetHasSize(A, 2))
s.add(SetHasSize(B, 2))
s.add(SetHasSize(SetIntersect(A, B), 1))
print(s.sexpr())
print(s.check())

I get:

$ python a.py
(declare-fun A () (Array Int Bool))
(declare-fun B () (Array Int Bool))
(assert (set-has-size A 2))
(assert (set-has-size B 2))
(assert (set-has-size (intersection A B) 1))

unsat

which is not correct. There are many models of the problem stated.

In https://github.com/Z3Prover/z3/issues/3854, the recommendation was that set-has-size is deprecated in the SMT-Lib backend, but using it from Python or C++ should be fine. The above demonstrates perhaps that's not really the case?

[rainoftime]

The SMTLib frontend does not support set-has-size (BAPA theory). But the potential bug is still there, triggered by the Python interfaces.

As suggested by "alias" in https://stackoverflow.com/questions/63983897/using-sets-and-sethassize-on-intersections-in-z3, the users may consider changing the encoding.

Besides, CVC4 also supports set-has-size (enabled with ``sets-ext'' option). It might be more stable.

[rainoftime]

Another direction is implementing some algorithms for BAPA on top of z3 (or other SMT solvers). Here is an example: https://github.com/psuter/bapa-z3 (not sure if it still works)

which implements Philippe Suter, Robin Steiger, and Viktor Kuncak. Sets with Cardinality Constraints in Satisfiability Modulo Theories. VMCAI 2011

[NikolajBjorner]

This is not a supported feature. Do you have an actual use case for it or are you just trying to punch holes?

[LeventErkok]

@NikolajBjorner No intention of punching holes; quite the opposite actually. It'd be great if unsupported features are reported as such, as they can creep in and cause soundness issues elsewhere.

Perhaps remove SetHasSize from the Python and C++ (Java, if it supports); or at least catch what's not supported and report to the user as an error as opposed to issuing unsat? That'd be an ideal solution, but you're right that I don't have a specific use case in mind. (Except the person on stack-overflow was actually trying to solve a problem but was utterly confused by the behavior. If you consider that an actual use case.)

[NikolajBjorner]

Makes sense. Z3 will now throw if attempting to use this.

[LeventErkok]

Thanks!