(Z3Py) समारोह

Question

घोषित मैं कुछ दिया परिणाम/एक्स जोड़े के लिए सरल "परिणाम = एक्स * टी + स" सूत्र में सी और टी गुणांक प्राप्त करना चाहते हैं:

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 

... लेकिन परिणाम जाहिर है गलत है। मुझे शायद फ़ंक्शन तर्कों को मैप करने का तरीका जानने की आवश्यकता है।

मुझे कार्य को सही तरीके से परिभाषित कैसे करना चाहिए?

Answer 1

अभिकथन f(x) == x*t + cनहीं सब x के लिए समारोह f को परिभाषित है। यह सिर्फ यह कह रहा है कि f का मान के लिए दिया गयाxx*t + c है। जेड 3 सार्वभौमिक क्वांटिफायर का समर्थन करता है। हालांकि, वे बहुत महंगा हैं, और ज़ेड 3 पूर्ण नहीं होता है जब बाधाओं के एक सेट में सार्वभौमिक क्वांटिफायर होते हैं क्योंकि समस्या अनावश्यक हो जाती है। यही है, Z3 इस तरह की समस्या के लिए unknown वापस कर सकता है।

ध्यान दें कि f आपकी लिपि में अनिवार्य रूप से "मैक्रो" है। इस "मैक्रो" को एन्कोड करने के लिए Z3 फ़ंक्शन का उपयोग करने के बजाय, हम एक पायथन फ़ंक्शन बना सकते हैं जो चाल करता है। यही है, एक पायथन समारोह है कि, एक Z3 अभिव्यक्ति दिया, एक नई Z3 अभिव्यक्ति देता है। यहां एक नई लिपि है। 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)]) 

टिप्पणी: http://rise4fun.com/Z3Py/Yoi यहाँ स्क्रिप्ट का एक और संस्करण जहां c और tReal बजाय Int हैं: स्क्रिप्ट पर भी ऑनलाइन उपलब्ध है श्रीमती 2.0 सामने के अंत में, मैक्रो का उपयोग कर परिभाषित किया जा सकता आदेश define-fun।