Reputation: 1

Describing a function partially in Z3 or Z3py

This is my first question in Stackoverflow. So please do offer advice if I'm breaking any house rules.

I have started learning Z3Py only recently. I found myself in a situation where I know the following about an Int->Int function A that I want to describe and leave it for Z3Py to solve:

The summation of A(x) = 10000 where 0<x<100
A(x) > 10 where 0<x<100
A(x) = 0 where x>= 100
A(3) = 190
A(12) = 1200

How can these constraints be described in Z3Py (Or Z3)?

Upvotes: 0

Answers (2)

alias

Reputation: 30418

There could be multiple ways to code this example in z3py. With the constraints as you listed, you can use a symbolic array, an uninterpreted function or use separate variables for each of the 100 elements.

Using arrays

The simplest for this case would be the use of arrays: That is, model the Int -> Int function as an array:

from z3 import *

A = Array('A', IntSort(), IntSort())

s = Solver()

total = 0
for i in range(100):
    s.add(A[i] > 10)
    total = total + A[i]

s.add(total == 10000)

s.add(A[ 3] ==  190)
s.add(A[12] == 1200)

k = Int('k')
s.add(ForAll(k, (Implies(Or(k < 0, k >= 100),  A[k] == 0))))

if s.check() == sat:
    m = s.model()
    for i in range(100):
        v = m.evaluate(A[i]).as_long()
        print("%3d: %d" % (i, v))

When run, this prints:

You can sum up the values printed to ensure it indeed gives you 10000.

Using uninterpreted functions

You can also model A as an uninterpreted function. The changes required is really trivial to the above:

from z3 import *

A = Function('A', IntSort(), IntSort())

s = Solver()

total = 0
for i in range(100):
    s.add(A(i) > 10)
    total = total + A(i)

s.add(total == 10000)

s.add(A( 3) ==  190)
s.add(A(12) == 1200)

k = Int('k')
s.add(ForAll(k, (Implies(Or(k < 0, k >= 100),  A(k) == 0))))

if s.check() == sat:
    m = s.model()
    for i in range(100):
        v = m.evaluate(A(i)).as_long()
        print("%3d: %d" % (i, v))

This prints:

The model is quite different in this case, but it's easy to see that it has A(3) = 190, A(12) = 1200, A(74) = 7543, and all other entries are set to 11; giving you a total of 190 + 1200 + 7543 + 11 * 97 = 10000.

Using separate variables

Yet a third method would be to allocate 100 integer elements in a python array, and assert the constraints on individual elements separately. This would lead to the simplest model, as it would not use any quantification. Of course, this would model the fact that elements outside the range 0..99 are 0 implicitly, so only use this if this constraint does not need to be explicitly mentioned. Again, the coding is almost identical:

from z3 import *

A = [Int('A_%d' % i) for i in range(100)]

s = Solver()

total = 0
for i in range(100):
    s.add(A[i] > 10)
    total = total + A[i]

s.add(total == 10000)

s.add(A[ 3] ==  190)
s.add(A[12] == 1200)

if s.check() == sat:
    m = s.model()
    for i in range(100):
        v = m.evaluate(A[i]).as_long()
        print("%3d: %d" % (i, v))

I'm eliding the output of this for brevity. Note how we're using A as a python list in this case, instead of a symbolic array directly supported by z3py itself.

Summary

At the end of the day, the constraints you've described are simple enough that it can use all these three techniques. Which one is the best depends on what other constraints you'd want to model. (In particular, you'd want to avoid anything that makes heavy use of quantifiers, like ForAll above since SMT solvers don't do all that well for quantifiers in general. This problem is simple enough so it doesn't pose an issue, but when your constraints get complicated, it can increase solving times or lead the solver to answer unknown.)

Hope this gets you started. Best of luck!

Upvotes: 1

Malte Schwerhoff

Reputation: 12852

Below you'll find a straight-forward SMT encoding of your problem, except for the summation requirement.

(set-option :smt.mbqi true) ; also try false (e-matching instead of MBQI)

(declare-fun A (Int) Int)

(assert 
  (=
    10000
    (+ 
      (A 1)
      (A 2)
      (A 3)
      ; ...
      (A 99))))

; A(x) > 10 where 0<x<100
(assert (forall ((x Int))
  (implies
    (and (< 0 x) (< x 100))
    (> (A x) 10))))

; A(x) = 0 where x>= 100
(assert (forall ((x Int))
  (implies
    (>= x 100)
    (> (A x) 10))))

; A(3) = 190
(assert (= (A 3) 190))

; A(12) = 1200
(assert (= (A 12) 1200))

(check-sat)

A few remarks:

All SMT functions are total; if you want to encode a partial function, you'll have to explicitly model the function's domain, and make definitional axioms conditional on whether or not an argument is in the domain. Z3 will still give you a total model for the function, though.
Arbitrary summation is non-trivial to encode in SMT, since there is no sum comprehension operator. Your case is simpler, though, since your sum ranges over a statically known number of elements (0 < x < 100).
I'd not be surprised if Z3py offers a convenient source syntax to generate sums over statically-known many elements