Dafny. Оптимизация проблем с проверкой времени - PullRequest
Новая
       9

Dafny. Оптимизация проблем с проверкой времени

0 голосов
/ 07 июня 2019

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

Метод довольно большой, но я постараюсь выбрать только соответствующий код: 

  method solve() returns (isSatisfiable : SAT_UNSAT)
    requires valid();
    requires formula.stack.size > 0 ==> |formula.stack.stack[formula.stack.size-1]| > 0;
    requires formula.stack.size <= formula.stack.stack.Length;

    modifies formula.truthAssignment, formula.stack, formula.stack.stack,
             formula.trueLiteralsCount, formula.falseLiteralsCount,
             formula.satisfiedClauses;

    ensures valid();
    ensures old(formula.stack) == formula.stack;
    ensures old(formula.stack.size) == formula.stack.size;
    ensures old(formula.stack.stack) == formula.stack.stack;
    ensures old(formula.stack.stack.Length) == formula.stack.stack.Length;
    ensures forall i :: 0 <= i < formula.stack.stack.Length ==>
      formula.stack.stack[i] == old(formula.stack.stack[i]);
    ensures old(formula.stack.contents) == formula.stack.contents;
    ensures formula.stack.size > 0 ==>
      |formula.stack.stack[formula.stack.size-1]| > 0;

    decreases *;
  {
    .....

    assert valid();
    assert old(formula.stack) == formula.stack;
    assert old(formula.stack.size) == formula.stack.size;
    assert old(formula.stack.stack) == formula.stack.stack;
    assert old(formula.stack.stack.Length) == formula.stack.stack.Length;
    assert forall i :: 0 <= i < formula.stack.stack.Length ==>
      formula.stack.stack[i] == old(formula.stack.stack[i]);
    assert old(formula.stack.contents) == formula.stack.contents;
    assert formula.stack.size > 0 ==>
              |formula.stack.stack[formula.stack.size-1]| > 0;

    return result; 
  }

Доказательство занимает 24 с в этой форме.

Странные сценарии:

  1. Если я добавлю еще assert valid(); до возвращения, это займет 50 с.вместо 24 с.Это почему?Над ним стоит assert valid();, и между ними ничего не меняется.

  2. Если я добавлю if (true) { return result; } перед возвратом, это займет 300 с.Если я добавлю if (result.SAT?) { return result; }, это займет 100 секунд.Меня смущает, почему два простых случая, которые не связаны с условиями публикации, так сильно влияют на время проверки.

Какие инструменты / методы вы рекомендуете мне использовать для оптимизациивремя прувинга?

...