Как мне оценить это уравнение в z3 для python - PullRequest
Новая
       11

Как мне оценить это уравнение в z3 для python

1 голос
/ 10 марта 2020

Я пытаюсь оценить простое неравенство по абсолютным значениям, как это, используя z3. 


x = Int("x")
y = Int("y")


def abs(x):
    return If(x >= 0,x,-x)

solve(abs( x / 1000 - y / 1000  ) < .01, y==1000)

Вывод не является решением каждый раз. Я знаю, что это математически возможно, я просто не могу понять, как z3 делает такие вещи.

Ответы [ 2 ]

2 голосов
/ 11 марта 2020

Это распространенная ошибка в привязках z3py. Константы «повышаются», чтобы соответствовать нужному типу, следуя обычной методологии Python. Но чаще всего это приводит к неправильному преобразованию, и вы попадаете в очень запутанную ситуацию.

Поскольку ваши переменные x и y являются Int значениями, сравнение с .01 заставляет эту константу 0 соответствовать типам, и это определенно не то, что вы хотели сказать. Общий совет - просто не смешивать и сопоставлять арифметику c следующим образом: приведите это как проблему к действительным значениям, а не к целым числам. (В общем, SMTLib не позволяет смешивать и сопоставлять типы в числах, хотя z3py делает. Я думаю, что это неверно, но это другое обсуждение.)

Чтобы решить вашу проблему, проще всего сделать следующее: быть, чтобы обернуть 0.01 в реальную константу, чтобы привязки z3py интерпретировали это правильно. Итак, у вас будет: 

from z3 import *

x = Int("x")
y = Int("y")

def abs(x):
    return If(x >= 0,x,-x)

solve(abs( x / 1000 - y / 1000  ) < RealVal(.01), y==1000)

Обратите внимание на использование RealVal. Это возвращает: 

[x = 1000, y = 1000]

Я думаю, это то, что вам нужно.

Но я бы вообще рекомендовал не использовать подобные преобразования. Вместо этого, будьте очень откровенны сами, и приведите это как проблему, например, к реальным значениям. Обратите внимание, что ваше деление / 1000 также интерпретируется в этом уравнении как целочисленное деление, то есть то, которое дает целочисленный результат. Так что, полагаю, это не совсем то, чего вы хотите. Но я надеюсь, что это поможет вам начать правильный путь.

0 голосов
/ 10 марта 2020

Int('a') < 0.01 превращается (правильно или неправильно) в Int('a') < 0, и очевидно, что абсолютное значение никогда не может быть меньше 0.

Я полагаю, что вы хотите Int('a') <= 0 здесь.

Примеры: 

solve(Int('a') < 0.01, Int('a') > -1)

no solution

solve(Int('a') <= 0.01, Int('a') > -1)

[a = 0]

Int('a') < 0.01

a < 0

...