In Z3, what is the simplest formula over a [String -> Bool] function that only maps certain values to True and all others to False?

Question

Continuing on from my question about set representation, if you define a set as follows:

from z3 import *
s = Solver()
string_set = Function('string_set', StringSort(), BoolSort())
s.add(string_set(StringVal('foo')))
s.add(string_set(StringVal('bar')))
s.add(string_set(StringVal('baz')))

this doesn't really specify the set {foo, bar, baz} because it says nothing about what values are not in the set; if asked to find a model, Z3 can easily come up with the function [else -> True] which satisfies all these constraints.

What is the easiest way to specify that the function is true only for those specific values? The objective is to produce the model:

[
  "foo" -> True,
  "bar" -> True,
  "baz" -> True,
  else -> False
]

do I really have to quantify over all strings that are not in that explicit set?

score 1 · Accepted Answer · answered Dec 08 '21 at 16:54

Strictly speaking, the only way to do this is to use quantification:

from z3 import *

s = Solver()

string_set = Function('string_set', StringSort(), BoolSort())
dummy = String('dummy')
s.add(ForAll([dummy], string_set(dummy) == Or( dummy == StringVal('foo')
                                             , dummy == StringVal('bar')
                                             , dummy == StringVal('baz'))))

However, I'd strongly caution against introducing quantifiers to your model, as it will no doubt cause the solver to use algorithms that are no longer decision procedures, i.e., you run the risk of getting unknown (or running forever); unnecessarily complicating the problem.

What's rather implicit in Nikolaj's answer is that if you want to model sets this way, uninterpreted functions are a good way to go so long as you don't have insertions/deletions. But then those aren't really sets, just pure functions. So, you should model them as such. That is, to answer your question more literally, i.e., what's the "simplest" formula that only yields true for these given values, you need to make it an actual function:

def string_set(x):
   return (Or(x == 'foo', x == 'bar', x == 'baz'))

Or, if you want to make it a proper function inside the solver:

from z3 import *

string_set = RecFunction("string_set", StringSort(), BoolSort())
dummy = String("dummy")
RecAddDefinition( string_set
                , [dummy]
                , Or(dummy == StringVal("foo"), dummy == StringVal("bar"), dummy == StringVal("baz"))
                )

From a modeling perspective, I think the best way to go for modeling sets is arrays, followed by functions as I described here.

Oh that seems much nicer! I ended up writing some fairly hideous quantifier constraints but will switch to this method; see here: https://github.com/gravitational/rbac-linter/blob/c9cdca2431e07b0ebce3dcdf4f1420cac33bbaf5/role_analyzer.py#L542 — ahelwer, Dec 08 '21 at 17:20

In Z3, what is the simplest formula over a [String -> Bool] function that only maps certain values to True and all others to False?

1 Answers1