Проверить выражения числовых ограничений на эквивалентность/подмножество допустимых значений

У меня есть AST, представляющий такие выражения:

  • (<=10 && >=3) || ==0
  • ==1 || ==2 || ==3
  • ==1 && !=1

Существуют числовые, а также логические (||, &&) и числовые (<, <=, ==, !=, >=, >) операторы. При необходимости в AST можно добавить логический оператор not. Эти выражения используются для ограничения возможных числовых входных значений (обратите внимание, что последнее ничего не разрешает).

Я ищу способ сравнения двух выражений. Мне нужно знать, допускают ли они один и тот же набор чисел (эквивалентны) или допускает ли одно выражение подмножество другого.


expression algorithm haskell equivalence
person snøreven    schedule 19.04.2016    source источник

Ответы (2)


arrow_upward
2
arrow_downward

Вы можете написать функцию

evaluate :: Expression -> ValueSet

который оценивает выражение в набор значений, где оно истинно. Этот набор значений может быть чем-то вроде

data Value = MinusInfinity | Finite Integer | PositiveInfinity
type Range = (Value, Value)
type ValueSet = [Range]

где ValueSet — отсортированный список закрытых непересекающихся диапазонов. Затем вы можете реализовать случаи evaluate один за другим, используя логику, напоминающую отсортированное слияние.

person David Eisenstat    schedule 19.04.2016
comment
Он также должен был работать с дробными значениями, поэтому мне нужны были как открытые, так и закрытые интервальные границы, что все усложняло, но подход работал. Спасибо! - person snøreven; 07.05.2017

arrow_upward
1
arrow_downward

Эта задача является NP-трудной. Во всяком случае, так кажется.

Но может быть надежда. Как уже говорилось, ваш язык выражений чертовски ограничен. Например, вы не упомянули оператор not, что означает, что && никогда не может быть преобразовано в ||.

Вот схема ответа:

  1. Нормализуйте операторы сравнения: пройдитесь по деревьям, преобразуя все ‹= в > путем замены операндов. В то же время преобразуйте >= в ‹.
  2. Свернуть повторяющиеся и и или в "узел дерева с несколькими операндами". Например, переписать A || ( B || C ) так, чтобы это был один узел дерева с тремя операндами or(A,B,C). Узел может быть свернут, если он является тем же оператором, что и его родительский узел.
  3. Отсортируйте операнды ||, &&, or и and, используя стабильную сортировку, чтобы C || (B || A) также сворачивалось в or(A,B,C). И B || A и `А
  4. Теперь, когда деревья нормализованы, работает рекурсивное сравнение деревьев.

Этот ответ не учитывает перекрывающиеся наборы. Например, он не будет отображать выражение

person J Ward    schedule 19.04.2016