W Z3Py, jak mogę sprawdzić, czy równanie dla danych ograniczeń ma tylko jedno rozwiązanie?(Z3Py) sprawdzanie wszystkich rozwiązań dla równania
Jeśli istnieje więcej niż jedno rozwiązanie, jak mogę je wymienić?
W Z3Py, jak mogę sprawdzić, czy równanie dla danych ograniczeń ma tylko jedno rozwiązanie?(Z3Py) sprawdzanie wszystkich rozwiązań dla równania
Jeśli istnieje więcej niż jedno rozwiązanie, jak mogę je wymienić?
Możesz to zrobić, dodając nowe ograniczenie, które blokuje model zwracany przez Z3. Załóżmy na przykład, że w modelu zwróconym przez Z3 mamy te x = 0
i y = 1
. Następnie możemy zablokować ten model, dodając ograniczenie Or(x != 0, y != 1)
. Poniższy skrypt wykonuje lewę. Możesz wypróbować online pod adresem: http://rise4fun.com/Z3Py/4blB
Należy zauważyć, że poniższy skrypt ma kilka ograniczeń. Formuła wejściowa nie może zawierać nieinterpretowanych funkcji, tablic ani nieinterpretowanych sortowań.
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
Chciałbym również zapytać, czy to samo możliwe w rozszerzeniu językowym ZT SMT? –
Nie, nie jest. Jednak myślę, że warto dodać to polecenie w interfejsie SMT 2.0. –
Czy możesz dodać notatkę, aby wyjaśnić, dlaczego nieinterpretowane funkcje i tablice nie są obsługiwane za pomocą tej metody? Czy jest to przypadkowe ograniczenie (struktury danych to nie ExprRefs, czy coś w tym stylu) czy bardziej fundamentalne? – EfForEffort