1
После применения исключения квантификатора в Z3 к линейной арифметической формуле h, я получаю 30-строчную формулу. Оказывается, эта формула эквивалентна h2=And(n>2, i>=0, i<=n-2), которую я бы предпочел в качестве вывода.Упрощение целочисленных формул в Z3
Я пробовал ctx-solver-simplify; Я получаю: And(Not(n <= 2), Or(Not(i >= 1), Not(n + -1*i <= 1)), i >= 0)
Теперь Not(n<=2) можно более кратко выражается как n>=3, Not(n + -1*i <= 1) в n-i>=2, и в этой формуле i >= 1 не требуется.
Repeat(Then('nnf','ctx-solver-simplify')) делает немного лучше (избавляясь от i>=1).
Есть ли более эффективная тактика упрощения?
Аналогичным образом, есть тактика, которая преобразит Or(x==0, x==1, x==2, x==3) в And(x>=0,x<=3)?
Хороший вопрос, хотя я не думаю, что встроенный метод это сделает. Метод упрощения ctx-solver является одним из наиболее агрессивных, и он не знает, что вы намерены получить соединение. Возможно, идея состоит в том, чтобы упростить формулы по модулю набора шаблонов. Вы можете предложить литералы, извлеченные из вашего пространства шаблонов (которые вы извлекаете из самой формулы), а затем извлекаете соединение. –
К сожалению, ожидаемая формула не обязательно является конъюнкцией. В этом конкретном примере я предположил, что результат должен быть эквивалентен этой формуле 'h2' (' h' исходит из проблемы с программным анализом, и у меня была некоторая интуиция относительно того, каким должен быть конечный результат), который я проверил с Z3 ('h'⇒'h2' и' h2'⇒'h'), но в целом формула может быть более сложной. Ваша идея интересна, я мог бы, скажем, предположить, что формула состоит только из нескольких дизъюнктов ... –