(Z3Py) işlevini

Question

ilan bazı belirli bir sonuç/x çiftleri için basit bir "sonuç x = * t + c" formülündeki C ve T katsayıları bulmak istiyoruz:

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 

... ama sonuç açıkça yanlıştır. Muhtemelen fonksiyon argümanlarını nasıl haritalayacağımı bulmalıyım.

İşlev nasıl doğru tanımlamalıyım?

Answer 1

iddia f(x) == x*t + c tüm x için işlevini f tanımlayan değil olduğunu. Sadece için f değerinin verilenx değerinin x*t + c olduğunu söylüyor. Z3 evrensel niceleyicileri destekler. Bununla birlikte, bunlar çok pahalıdır ve problemin kararsız hale gelmesinden beri bir dizi kısıtlama evrensel niceleyicileri içerdiğinde Z3 tamamlanmamıştır. Yani, Z3 bu tür bir sorun için unknown'u döndürebilir.

Not: f kodunuzda bir "makro" olduğunu unutmayın. Bu "makro" kodlamak için bir Z3 işlevi kullanmak yerine, hile yapan bir Python işlevi oluşturabiliriz. Yani, bir Z3 ifadesi verilen yeni bir Z3 ifadesi döndüren bir Python işlevi. İşte yeni bir senaryo. 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)]) 

Açıklama: http://rise4fun.com/Z3Py/Yoi İşte c ve tReal yerine Int olan script başka versiyonudur: Senaryo altındadır çevrimiçi kullanılabilir SMT 2.0 ön uç olarak, makro kullanılarak tanımlanabilir define-fun komutu.