key icon indicating copy to clipboard operation
key copied to clipboard

Published 20 hours ago • verified publisher icon KeYProject

Prover slows down on large sequents

Open wadoon opened this issue 2 years ago • 0 comments

This issue was created at git.key-project.org where the discussions are preserved.

  • Mantis: MT-1299
  • Submitted on: 2013-05-08 by (at)grahl
  • Updated: 2013-05-10

Description

The average time for a single rule application grows at least linear with the sequent size (which means linearly growing sequents cause at least quadratic increase in computation time).

Steps to reproduce

Load the attached Java file and try to prove the contract for foo() using the contract for bar(). Set max rule applications to 10,000. After 10,000 rule applications, press automode button again. (The complete proof takes around 132,000 steps.)

The sequent size will grow linearly. Each 10,000 next steps will take more time. The following results were obtained on i57pc7 (Core i7 with 8GB RAM):

10k   20k   30k   40k   50k   60k   70k
44s   95s  146s   n/a  265s  324s  398s

Files

Contract.java

Notes

(at)rbubel at 2013-05-10

One problem is that replacement of a formula in the sequent has a worst case of O(n) due to immutability of sequents (and the underlying list datastructure). Best case is O(1) if the first element is replaced, but I am not sure how much this contributes to the overall lines, I assume there are other reasons (with a higher constant) as well.

Associated Bugs

  • Relates to MT-1291 with

  • Relates to MT-827 with

History

  • (at)grahl -- (NEW_BUG) 2013-05-08

  • (at)grahl -- (FILE_ADDED) 2013-05-08

  • (at)grahl -- (BUG_ADD_RELATIONSHIP) 2013-05-08

  • (at)klebanov -- (BUG_ADD_RELATIONSHIP) 2013-05-08

  • (at)rbubel -- (BUGNOTE_ADDED) 2013-05-10

Attributes

  • Category: Prover Core
  • Status: NEW
  • Severity: MAJOR
  • OS:
  • Target Version:
  • Resolution: OPEN
  • Priority: NORMAL
  • Reproducibility: ALWAYS
  • Platform:
  • Commit: 6405dc35713c274f6018f61a192d4d637a450d2d
  • Build:
  • Tags []
  • Labels: ~Prover Core ~Bug ~NORMAL
  • Version: 2.0

View in Mantis

Information:

  • created_at: 2017-05-29T02:49:05.959Z
  • updated_at: 2017-05-29T02:49:06.214Z
  • closed_at: None (closed_by: )
  • milestone:
  • user_notes_count: 0

wadoon avatar Dec 23 '22 23:12 wadoon