Geek asks and answers

(Z3Py) declaring a function

I would like to find the coefficients c and t in the simple formula "result = x * t + c" for some given pairs of / x results:

from z3 import *

x=Int('x')
c=Int('c')
t=Int('t')

s=Solver()

f = Function('f', IntSort(), IntSort())

# x*t+c = result
# x, result = [(1,55), (12,34), (13,300)]

s.add (f(x)==(x*t+c))
s.add (f(1)==55, f(12)==34, f(13)==300)

t=s.check()
if t==sat:
    print s.model()
else:
   print t

... but the result is clearly wrong. I probably need to figure out how to match function arguments.

How to determine the function?

+5
source share
1 answer

An assertion f(x) == x*t + cdoes not define a function ffor everyone x. He simply says that the value ffor this xis x*t + c. Z3 supports universal quantifiers. However, they are very expensive, and Z3 is not complete when the set of constraints contains universal quantifiers, since the problem becomes unsolvable. That is, Z3 may return unknownfor this problem.

, f "" script. Z3 "" Python, . , Python, , Z3, Z3. script. script : http://rise4fun.com/Z3Py/Yoi script, c t Real Int: http://rise4fun.com/Z3Py/uZl

from z3 import *

c=Int('c')
t=Int('t')

def f(x):
    return x*t + c

# data is a list of pairs (x, r)
def find(data):
    s=Solver()
    s.add([ f(x) == r for (x, r) in data ])
    t = s.check()
    if s.check() == sat:
        print s.model()
    else:
        print t

find([(1, 55)])
find([(1, 55), (12, 34)])
find([(1, 55), (12, 34), (13, 300)])

. SMT 2.0 define-fun.

+6

More articles:


All Articles