Запуск проблем в Z3

Недавно я наблюдал несколько вариантов поведения Z3 в отношении срабатывания, которые я не понимаю. К сожалению, примеры взяты из больших файлов Boogie, поэтому я решил пока описать их абстрактно, просто чтобы посмотреть, есть ли очевидные ответы. Однако, если конкретные файлы будут лучше, я могу их прикрепить.

Есть в основном три проблемы, хотя третья вполне может быть частным случаем второй. Насколько я понимаю, ни одно из поведений не ожидается, но, возможно, я что-то упускаю. Любая помощь будет принята с благодарностью!

Во-первых:Тривиальные равенства в моей программе, кажется, игнорируются в том, что касается запуска. Например, если t1— это терм, который должен соответствовать образцу квантифицированной аксиомы, если я добавлю в свою программу в стиле буги-вуги строку вида

assert t1 == t1;

тогда t1, , а не , по-видимому, используется в качестве триггера для квантифицированных аксиом. Я добавил строку явно, чтобы предоставить t1в качестве триггера для доказывающего, что я часто делаю/делал в программах Boogie.

Если вместо этого я введу дополнительную функцию, скажем,

function f(x : same_type_as_t1) : bool
{ true }

а теперь вместо этого добавьте строку

assert f(t1);

к моей программе, тоt1кажется, что используется Z3 в качестве триггера. Я проверил Z3-перевод предыдущей программы, и (тривиальное )равенство на t1пережило перевод Boogie (т. е. это не попытка Boogie сделать что-то умное ).

Во-вторых:Вторичные шаблоны, похоже, не работают должным образом для меня. Например, у меня есть программа, в которой одна аксиома имеет вид

axiom (forall... :: {t1,t2} {t3,t4,t5}..... );

и ситуация, в которой произошли t3, t4и t5. Программа не проходит проверку, по-видимому, потому, что аксиома не реализована. Однако,если я перепишу аксиому как

axiom (forall... :: {t3,t4,t5} {t1,t2}..... );

затем программа проверяет. В обоих случаях время запуска Boogie составляет примерно 3 секунды, а шаблоны сохраняются до вывода Z3.

В-третьих:Это вполне могло быть признаком второй проблемы, но меня удивило следующее поведение:

Я написал аксиомы вида

axiom (forall.. :: {t1,t2}.... );

axiom (forall... :: {t2,t4} {t2,t3}...some expression involving t1... );

и в ситуации, когда произошли t2и t3, первая аксиома не была реализована (, я ожидал, что это произойдет, поскольку после реализации второй аксиомы происходит t1). Однако, если я перепишу как

axiom (forall.. ::  {t2,t3} {t1,t2}.... );

axiom (forall... :: {t2,t4} {t2,t3}...some expression involving t1... );

затем была реализована первая аксиома. Однако, если по какой-то причине вторичные шаблоны вообще не используются, то это также объясняет такое поведение.

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

Заранее большое спасибо за любой совет!

Алекс Саммерс

Изменить:вот пример, который частично иллюстрирует второе и третье поведение, описанные выше. Я приложил код Boogie, чтобы его было легче читать, но я также могу скопировать или отправить по электронной почте ввод Z3, если он будет более полезным. Я вырезал почти весь исходный код Boogie, но, кажется, трудно сделать его проще, не потеряв при этом поведение полностью.

Код ниже уже немного отличается от моего исходного примера, но я думаю, что он достаточно близок. В основном аксиома, обозначенная (1 )ниже, не может соответствовать своему второму набору шаблонов. Если я закомментирую аксиому (1 )и вместо этого заменю ее (в настоящее время -комментируемыми )аксиомами (2 )и (3 ), которые просто копии оригинала с каждым из двух наборов шаблонов, затем программа проверяет. На самом деле,в данном конкретном случае достаточно иметь аксиому (2 ). В моем исходном коде (, прежде чем я его сократил ), также было достаточно изменить порядок двух наборов шаблонов в аксиоме (1 ), но, похоже, это не так в моем случае. меньше репродукции больше.

type ref;
type HeapType;

function vals1(HeapType, ref) returns (ref);
function vals2(HeapType, ref) returns (ref);
function vals3(HeapType, ref) returns (ref);

function heap_trigger(HeapType) returns (bool);

function trigger1(ref) returns (bool);
function trigger2(ref) returns (bool);

axiom (forall Heap: HeapType, this: ref ::  {vals1(Heap, this)}  (vals1(Heap, this) == vals3(Heap,this)));

axiom (forall Heap: HeapType, this: ref :: {vals2(Heap, this)}  trigger2(this));

// (1)
axiom (forall Heap: HeapType, this: ref :: {vals1(Heap, this)} {trigger1(this), heap_trigger(Heap), trigger2(this)} (vals1(Heap, this) == vals2(Heap, this)));

// (2)
// axiom (forall Heap: HeapType, this: ref :: {trigger1(this), heap_trigger(Heap), trigger2(this)}  (vals1(Heap, this) == vals2(Heap, this)));
// (3)    
// axiom (forall Heap: HeapType, this: ref :: {vals1(Heap, this)} (vals1(Heap, this) == vals2(Heap, this)));

procedure test(Heap:HeapType, this:ref)
{
  assume trigger1(this); assume heap_trigger(Heap);

  assert (vals2(Heap, this) == vals3(Heap,this));
}