CODEWITHSUNDEEP
pythonz3z3py
IssamLaradji
IssamLaradji

Reputation: 6865

Z3Py: Why are the following assumptions not satisfiable?

Why does the following not result in a satisfiable set of assumptions?

Doesn't the last assumption follow directly from assumptions 2 and 3?

import z3

# Initialize variables
t = z3.Int('t')
z = z3.Real("z")
y = z3.Real("y")
M = z3.Real("M")
x = z3.Function("x", z3.IntSort(), z3.RealSort())
f = z3.Function("f", z3.RealSort(), z3.RealSort())
d_f1 = z3.Function("d_f1", z3.RealSort(), z3.RealSort())

# Add assumptions
s = z3.Solver()

s.add(f(y) == f(z) + d_f1(z) *(y-z))
s.add(d_f1(z) < M)
s.add(f(x(t+1)) == f(x(t)) + d_f1(x(t)) *(x(t+1)-x(t)))

s.add(f(x(t+1)) < f(x(t)) + M *(x(t+1)-x(t)))

# Check if assumptions are satisfiable
s.check()

The result I get is,

unknown

Is there a way to encode a similar set of assumptions that are determined as satisfiable by the solver?

Upvotes: 0

Views: 107

Answers (1)

Nikolaj Bjorner
Nikolaj Bjorner

Reputation: 8359

Z3 returns "unknown", which means that it is unable to find a model for the assertions. The background is that your constraints use non-linear arithmetic over free functions (and integers). Z3 does not offer a decision procedure for the fragment your formula is in. Instead it tries an incomplete search procedure and comes up with a state where it can neither establish, nor refute the assertions.

Upvotes: 1

Related Questions