Как проверить основные отношения целочисленного порядка в Sympy? - PullRequest
Новая
       61

Как проверить основные отношения целочисленного порядка в Sympy?

1 голос
/ 01 мая 2019

У меня есть (возможно, относительно большой) набор предположений о множественных целых числах , подобных {x > -1, x < 5, x != 2, y > 0, x-2 < y}, и я хотел бы проверить, являются ли некоторые другие предложения, такие как {x > -5, x == 3, ...}, истинными, ложными или могут быть обоими.

В документах говорится, что явные отношения, такие как Q.is_true(x < 3), не поддерживаются, поэтому я попытался использовать свойство .positive, но безуспешно, например, 

#    x > -1 => x > -3   - ?
x = sympy.Symbol('x')
with sympy.assuming(sympy.Q.positive(x+1), sympy.Q.integer(x)):
  print(sympy.ask(sympy.Q.positive(x+3)))

1012 * производит *

None

Это означает, что контролер отказался от проверки.

Уточнение также, похоже, не очень помогает (вероятно, использует предположения в любом случае) 

sympy.refine(x > 0, sympy.Q.is_true(x > -1))

Если есть другая библиотека, которая может это проверить, это тоже работает!

1 Ответ

2 голосов
/ 01 мая 2019

Я обнаружил, что привязки Python для решателя z3 лучше всего подходят для моей задачи. Можно просто загрузить бинарный выпуск со страницы github и добавить включенную папку в $PYTHONPATH, например, 

LD_LIBRARY_PATH=${Z3FOLDER}/bin PYTHONPATH=${Z3FOLDER}/bin/python python

тогда эти отношения можно проверить как 

from z3 import *
x = Int('x')
s = Solver()
s.add(x > 10)
s.add(x > 12)
print(s)           // [x > 10, x > 12]
print(s.check())   // sat
print(s.model())   // [x = 13]
...