(Z3Py) समीकरण के लिए सभी समाधानों की जांच

Question

Z3Py में, मैं कैसे जांच सकता हूं कि दिए गए बाधाओं के समीकरण में केवल एक समाधान है या नहीं?

यदि एक से अधिक समाधान हैं, तो मैं उन्हें कैसे समझा सकता हूं?

Answer 1

आप एक नई बाधा डालकर ऐसा कर सकते हैं जो Z3 द्वारा लौटाए गए मॉडल को अवरुद्ध करता है। उदाहरण के लिए, मान लीजिए कि जेड 3 द्वारा लौटाए गए मॉडल में हमारे पास x = 0 और y = 1 है। फिर, हम इस मॉडल को बाधा Or(x != 0, y != 1) जोड़कर अवरुद्ध कर सकते हैं। निम्न स्क्रिप्ट चाल करता है। आप इसे ऑनलाइन आजमा सकते हैं: http://rise4fun.com/Z3Py/4blB

ध्यान दें कि निम्न स्क्रिप्ट में कुछ सीमाएं हैं। इनपुट सूत्र में अनियंत्रित फ़ंक्शन, सरणी या अनियंत्रित प्रकार शामिल नहीं हो सकते हैं।

from z3 import * 

# Return the first "M" models of formula list of formulas F 
def get_models(F, M): 
    result = [] 
    s = Solver() 
    s.add(F) 
    while len(result) < M and s.check() == sat: 
     m = s.model() 
     result.append(m) 
     # Create a new constraint the blocks the current model 
     block = [] 
     for d in m: 
      # d is a declaration 
      if d.arity() > 0: 
       raise Z3Exception("uninterpreted functions are not supported") 
      # create a constant from declaration 
      c = d() 
      if is_array(c) or c.sort().kind() == Z3_UNINTERPRETED_SORT: 
       raise Z3Exception("arrays and uninterpreted sorts are not supported") 
      block.append(c != m[d]) 
     s.add(Or(block)) 
    return result 

# Return True if F has exactly one model. 
def exactly_one_model(F): 
    return len(get_models(F, 2)) == 1 

x, y = Ints('x y') 
s = Solver() 
F = [x >= 0, x <= 1, y >= 0, y <= 2, y == 2*x] 
print get_models(F, 10) 
print exactly_one_model(F) 
print exactly_one_model([x >= 0, x <= 1, y >= 0, y <= 2, 2*y == x]) 

# Demonstrate unsupported features 
try: 
    a = Array('a', IntSort(), IntSort()) 
    b = Array('b', IntSort(), IntSort()) 
    print get_models(a==b, 10) 
except Z3Exception as ex: 
    print "Error: ", ex 

try: 
    f = Function('f', IntSort(), IntSort()) 
    print get_models(f(x) == x, 10) 
except Z3Exception as ex: 
    print "Error: ", ex