Skip to content

Commit

Permalink
Add code from report (#16)
Browse files Browse the repository at this point in the history 
Adds the code written for the report of the practical work:
- scripts for profiling and plotting quantifier instantiations and
execution time
- Gobra files that were evaluated (experiments)
  • Loading branch information
@dnezam
dnezam authored Apr 29, 2024
1 parent 0a35a36 commit 9ac60d0
Show file tree
Hide file tree
Showing 90 changed files with 4,295 additions and 0 deletions.
69 changes: 69 additions & 0 deletions evaluation/README.md
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,69 @@
# Overview
`evaluation/` contains Gobra files and scripts that can be used to
evaluate and plot, for example, the effect of using `opaque` in the
standard library or using the standard library on the execution time
and number of quantifier instantiations.

## `scripts/`
Contains scripts to
- measure execution time and the number of quantifier instantiations
and store the results in a csv file (`profile.py`)
- plot the data from one or more csv files (`plot.py`)
- profile and plot every file in `experiments/` (`profile-all.sh`)

### Dependencies and Usage
plot.py has the following dependencies:
- pandas
- numpy
- seaborn
- matplotlib
Install these packages using your favorite package manager
for Python packages (e.g., apt, pacman, nix, pip, conda, etc.).

profile.py requires the path to the following files:
- silicon.sh
- Z3 (version 4.8.7)
- Gobra jar
We have only tested Z3 4.8.7; newer versions may not work as they produce
errors and different output. Additionally, in case you get errors of
the form
```
metadata["silicon_version"] = command_stdout.splitlines()[0].split()[-1][1:-2]
~~~~~~~~~~~~~~~~~~~~~~~~~~~^^^
IndexError: list index out of range
```
there may be an issue with Silicon. In this case, consider pulling Silicon's
source again, followed by building its jar.

Examples for the usage of plot.py can be found in
selected_plots/used_commands.md and profile-all.sh.
For the usage of profile.py, please take a look at its usage in
profile-all.sh. Finally, profile-all.sh contains comments describing its usage.

## `selected_plots/`
Contains plots comparing the results from different experiments.

## `experiments/`
### `program_proofs_example_10_2/`
We use the proof for `InsertCorrect` from [chapter 10.2 of Program Proofs encoded in Gobra](https://github.com/viperproject/program-proofs-gobra/blob/main/chapter10/examples_10.2.gobra)
to investigate the effect of "assisting" the verifier on execution time
and quantifier instantiations by means of intermediate assertions.

### `standard_library/`
We use parts of the standard library to investigate the effect of
making lemmas `opaque` on execution time and quantifier
instantiations.

### `synthetic_set/`
We create a synthetic example using sets that exhibits a relatively
high number of quantifier instantiations to investigate the effect of
- disabling set axiomatization and using the standard library to
manually prove all proof obligations
- "assisting" the verifier by calling lemmas from the standard library
that may be useful to prove the proof obligations

on execution time and quantifier instantiations.

Note that `fully_assisted/` is used for both types of experiments; the
difference is that in one case we disable set axiomatization by
passing the corresponding flag, while in the other case we do not.
31 changes: 31 additions & 0 deletions ...t_half/first_half-rand-iter_30-gran_1-sil_ver_0608ac9-z3_ver_4_8_7-gobra_ver_0608ac92.csv
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,31 @@
qi-k!542,qi-k!553,qi-k!587,qi-k!565,qi-quant-u-8,qi-quant-u-9,qi-$Multiset[Int]_prog.card_non_negative,qi-$Multiset[Int]_prog.card_empty,qi-quant-u-27,qi-quant-u-2,qi-quant-u-26,qi-quant-u-3,qi-quant-u-0,qi-quant-u-24,qi-quant-u-1,qi-quant-u-10,qi-quant-u-11,qi-quant-u-35,qi-quant-u-34,qi-quant-u-4,qi-quant-u-28,qi-quant-u-5,qi-quant-u-43,qi-quant-u-18,qi-quant-u-42,qi-quant-u-19,qi-quant-u-33,qi-quant-u-32,qi-quant-u-41,qi-quant-u-16,qi-quant-u-40,qi-quant-u-17,qi-quant-u-6,qi-quant-u-30,qi-quant-u-7,qi-quant-u-12,qi-quant-u-36,qi-quant-u-13,qi-$Multiset[Int]_prog.count_card,qi-$Multiset[Int]_prog.singleton_unionone,qi-$Multiset[Int]_prog.card_union,qi-$Multiset[Int]_prog.count_union,qi-$Multiset[Int]_prog.card_unionone,qi-$Multiset[Int]_prog.count_singleton,qi-$Multiset[Int]_prog.count_unionone,qi-$Multiset[Int]_prog.count_empty,qi-quant-u-14,qi-quant-u-38,qi-quant-u-15,qi-$Multiset[Int]_prog.equal_count,qi-quant-u-22,qi-quant-u-45,qi-quant-u-23,qi-quant-u-44,qi-$Multiset[Int]_prog.native_equality,qi-prog.getter_over_tuple2,qi-quant-u-20,qi-quant-u-21,qi-prog.integer_ax_dec,qi-k!569,qi-k!593,qi-k!599,qi-prog.integer_ax_bound,execution_time
1,50,43,9,13,24,29,29,21,20,21,24,20,20,20,7,15,7,7,20,20,18,2,2,2,2,13,13,3,3,3,12,3,3,3,1,1,1,21,2,5,7,2,6,6,4,1,1,1,12,1,1,1,1,1,3,2,1,9,50,26,26,6,10.57454514503479
1,50,43,9,13,24,29,29,21,20,21,24,20,20,20,7,15,7,7,20,20,18,2,2,2,2,13,13,3,3,3,12,3,3,3,1,1,1,21,2,5,7,2,6,6,4,1,1,1,12,1,1,1,1,1,3,2,1,9,50,26,26,6,10.84791350364685
1,50,43,9,13,24,29,29,21,20,21,24,20,20,20,7,15,7,7,20,20,18,2,2,2,2,13,13,3,3,3,12,3,3,3,1,1,1,21,2,5,7,2,6,6,4,1,1,1,12,1,1,1,1,1,3,2,1,9,50,26,26,6,10.858602523803711
1,50,43,9,13,24,29,29,21,20,21,24,20,20,20,7,15,7,7,20,20,18,2,2,2,2,13,13,3,3,3,12,3,3,3,1,1,1,21,2,5,7,2,6,6,4,1,1,1,12,1,1,1,1,1,3,2,1,9,50,26,26,6,10.771847009658813
1,50,43,9,13,24,29,29,21,20,21,24,20,20,20,7,15,7,7,20,20,18,2,2,2,2,13,13,3,3,3,12,3,3,3,1,1,1,21,2,5,7,2,6,6,4,1,1,1,12,1,1,1,1,1,3,2,1,9,50,26,26,6,11.01976990699768
1,50,43,9,13,24,29,29,21,20,21,24,20,20,20,7,15,7,7,20,20,18,2,2,2,2,13,13,3,3,3,12,3,3,3,1,1,1,21,2,5,7,2,6,6,4,1,1,1,12,1,1,1,1,1,3,2,1,9,50,26,26,6,10.935436010360718
1,50,43,9,13,24,29,29,21,20,21,24,20,20,20,7,15,7,7,20,20,18,2,2,2,2,13,13,3,3,3,12,3,3,3,1,1,1,21,2,5,7,2,6,6,4,1,1,1,12,1,1,1,1,1,3,2,1,9,50,26,26,6,10.75414776802063
1,50,43,9,13,24,29,29,21,20,21,24,20,20,20,7,15,7,7,20,20,18,2,2,2,2,13,13,3,3,3,12,3,3,3,1,1,1,21,2,5,7,2,6,6,4,1,1,1,12,1,1,1,1,1,3,2,1,9,50,26,26,6,11.120795011520386
1,50,43,9,13,24,29,29,21,20,21,24,20,20,20,7,15,7,7,20,20,18,2,2,2,2,13,13,3,3,3,12,3,3,3,1,1,1,21,2,5,7,2,6,6,4,1,1,1,12,1,1,1,1,1,3,2,1,9,50,26,26,6,10.82166314125061
1,50,43,9,13,24,29,29,21,20,21,24,20,20,20,7,15,7,7,20,20,18,2,2,2,2,13,13,3,3,3,12,3,3,3,1,1,1,21,2,5,7,2,6,6,4,1,1,1,12,1,1,1,1,1,3,2,1,9,50,26,26,6,11.02254605293274
1,50,43,9,13,24,29,29,21,20,21,24,20,20,20,7,15,7,7,20,20,18,2,2,2,2,13,13,3,3,3,12,3,3,3,1,1,1,21,2,5,7,2,6,6,4,1,1,1,12,1,1,1,1,1,3,2,1,9,50,26,26,6,11.238065481185913
1,50,43,9,13,24,29,29,21,20,21,24,20,20,20,7,15,7,7,20,20,18,2,2,2,2,13,13,3,3,3,12,3,3,3,1,1,1,21,2,5,7,2,6,6,4,1,1,1,12,1,1,1,1,1,3,2,1,9,50,26,26,6,11.151848554611206
1,50,43,9,13,24,29,29,21,20,21,24,20,20,20,7,15,7,7,20,20,18,2,2,2,2,13,13,3,3,3,12,3,3,3,1,1,1,21,2,5,7,2,6,6,4,1,1,1,12,1,1,1,1,1,3,2,1,9,50,26,26,6,10.836472272872925
1,50,43,9,13,24,29,29,21,20,21,24,20,20,20,7,15,7,7,20,20,18,2,2,2,2,13,13,3,3,3,12,3,3,3,1,1,1,21,2,5,7,2,6,6,4,1,1,1,12,1,1,1,1,1,3,2,1,9,50,26,26,6,10.892492055892944
1,50,43,9,13,24,29,29,21,20,21,24,20,20,20,7,15,7,7,20,20,18,2,2,2,2,13,13,3,3,3,12,3,3,3,1,1,1,21,2,5,7,2,6,6,4,1,1,1,12,1,1,1,1,1,3,2,1,9,50,26,26,6,10.741572380065918
1,50,43,9,13,24,29,29,21,20,21,24,20,20,20,7,15,7,7,20,20,18,2,2,2,2,13,13,3,3,3,12,3,3,3,1,1,1,21,2,5,7,2,6,6,4,1,1,1,12,1,1,1,1,1,3,2,1,9,50,26,26,6,11.007696628570557
1,50,43,9,13,24,29,29,21,20,21,24,20,20,20,7,15,7,7,20,20,18,2,2,2,2,13,13,3,3,3,12,3,3,3,1,1,1,21,2,5,7,2,6,6,4,1,1,1,12,1,1,1,1,1,3,2,1,9,50,26,26,6,10.838359117507935
1,50,43,9,13,24,29,29,21,20,21,24,20,20,20,7,15,7,7,20,20,18,2,2,2,2,13,13,3,3,3,12,3,3,3,1,1,1,21,2,5,7,2,6,6,4,1,1,1,12,1,1,1,1,1,3,2,1,9,50,26,26,6,10.95261025428772
1,62,45,25,13,32,85,85,31,30,31,52,30,30,30,7,17,7,7,20,20,18,2,2,2,2,13,13,3,3,3,12,3,3,3,1,1,1,192,13,27,52,13,45,45,15,1,1,1,12,1,1,1,1,1,3,2,1,9,82,44,44,6,10.821515798568726
1,50,43,9,13,24,29,29,21,20,21,24,20,20,20,7,15,7,7,20,20,18,2,2,2,2,13,13,3,3,3,12,3,3,3,1,1,1,21,2,5,7,2,6,6,4,1,1,1,12,1,1,1,1,1,3,2,1,9,50,26,26,6,10.83070993423462
1,50,43,9,13,24,29,29,21,20,21,24,20,20,20,7,15,7,7,20,20,18,2,2,2,2,13,13,3,3,3,12,3,3,3,1,1,1,21,2,5,7,2,6,6,4,1,1,1,12,1,1,1,1,1,3,2,1,9,50,26,26,6,10.751307964324951
1,50,43,9,13,24,29,29,21,20,21,24,20,20,20,7,15,7,7,20,20,18,2,2,2,2,13,13,3,3,3,12,3,3,3,1,1,1,21,2,5,7,2,6,6,4,1,1,1,12,1,1,1,1,1,3,2,1,9,50,26,26,6,10.833659172058105
1,50,43,9,13,24,29,29,21,20,21,24,20,20,20,7,15,7,7,20,20,18,2,2,2,2,13,13,3,3,3,12,3,3,3,1,1,1,21,2,5,7,2,6,6,4,1,1,1,12,1,1,1,1,1,3,2,1,9,50,26,26,6,10.8695068359375
1,50,43,9,13,24,29,29,21,20,21,24,20,20,20,7,15,7,7,20,20,18,2,2,2,2,13,13,3,3,3,12,3,3,3,1,1,1,21,2,5,7,2,6,6,4,1,1,1,12,1,1,1,1,1,3,2,1,9,50,26,26,6,11.117118120193481
1,50,43,9,13,24,29,29,21,20,21,24,20,20,20,7,15,7,7,20,20,18,2,2,2,2,13,13,3,3,3,12,3,3,3,1,1,1,21,2,5,7,2,6,6,4,1,1,1,12,1,1,1,1,1,3,2,1,9,50,26,26,6,10.845272064208984
1,50,43,9,13,24,29,29,21,20,21,24,20,20,20,7,15,7,7,20,20,18,2,2,2,2,13,13,3,3,3,12,3,3,3,1,1,1,21,2,5,7,2,6,6,4,1,1,1,12,1,1,1,1,1,3,2,1,9,50,26,26,6,11.208571195602417
1,50,43,9,13,24,29,29,21,20,21,24,20,20,20,7,15,7,7,20,20,18,2,2,2,2,13,13,3,3,3,12,3,3,3,1,1,1,21,2,5,7,2,6,6,4,1,1,1,12,1,1,1,1,1,3,2,1,9,50,26,26,6,10.688027620315552
1,50,43,9,13,24,29,29,21,20,21,24,20,20,20,7,15,7,7,20,20,18,2,2,2,2,13,13,3,3,3,12,3,3,3,1,1,1,21,2,5,7,2,6,6,4,1,1,1,12,1,1,1,1,1,3,2,1,9,50,26,26,6,10.872260570526123
1,50,43,9,13,24,29,29,21,20,21,24,20,20,20,7,15,7,7,20,20,18,2,2,2,2,13,13,3,3,3,12,3,3,3,1,1,1,21,2,5,7,2,6,6,4,1,1,1,12,1,1,1,1,1,3,2,1,9,50,26,26,6,11.039685249328613
1,50,43,9,13,24,29,29,21,20,21,24,20,20,20,7,15,7,7,20,20,18,2,2,2,2,13,13,3,3,3,12,3,3,3,1,1,1,21,2,5,7,2,6,6,4,1,1,1,12,1,1,1,1,1,3,2,1,9,50,26,26,6,10.644623517990112
Binary file added ...er_30-gran_1-sil_ver_0608ac9-z3_ver_4_8_7-gobra_ver_0608ac92.execution_time.png
View file
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
Binary file added ...half-rand-iter_30-gran_1-sil_ver_0608ac9-z3_ver_4_8_7-gobra_ver_0608ac92.qi.png
View file
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
104 changes: 104 additions & 0 deletions evaluation/experiments/program_proofs_example_10_2/first_half/first_half.gobra
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,104 @@
// This package contains the first half of the proof for InsertCorrect from
// https://github.com/viperproject/program-proofs-gobra/blob/main/chapter10/examples_10.2.gobra
package first_half

ghost
requires pq.Valid()
ensures let pqPrime := pq.Insert(y) in
pqPrime.Valid() &&
pqPrime.Elements() == pq.Elements() union mset[int]{y}
decreases len(pq)
pure func (pq PQueue) InsertCorrect(y int) Unit {
return match pq {
case Leaf{}:
Unit{}
case Node{?x, ?l, ?r}:
let pqPrime := pq.Insert(y) in
let min := y < x ? y : x in
let max := y < x ? x : y in
let newRight := r.Insert(max) in
let _ := asserting(pqPrime == Node{min, newRight, l}) in
let _ := asserting(
let L := len(l.Elements()) in
let R := len(r.Elements()) in
L == R || L == R + 1) in
r.InsertCorrect(max)
}
}

ghost
decreases len(pq)
pure func (pq PQueue) Valid() bool {
return pq.IsBinaryHeap() && pq.IsBalanced()
}

ghost
decreases len(pq)
pure func (pq PQueue) Insert(y int) PQueue {
return match pq {
case Leaf{}:
Node{y, Leaf{}, Leaf{}}
case Node{?x, ?left, ?right}:
y < x ? Node{y, right.Insert(x), left} : Node{x, right.Insert(y), left}
}
}

ghost
decreases len(pq)
pure func (pq PQueue) Elements() mset[int] {
return match pq {
case Leaf{}:
mset[int]{}
case Node{?x, ?left, ?right}:
mset[int]{x} union left.Elements() union right.Elements()
}
}

ghost
decreases len(pq)
pure func (pq PQueue) IsBalanced() (res bool) {
return match pq {
case Leaf{}:
true
case Node{_, ?left, ?right}:
left.IsBalanced() && right.IsBalanced() &&
(let L := len(left.Elements()) in
let R := len(right.Elements()) in
L == R || L == R + 1)
}
}

ghost
decreases len(pq)
pure func (pq PQueue) IsBinaryHeap() bool {
return match pq {
case Leaf{}:
true
case Node{?x, ?left, ?right}:
left.IsBinaryHeap() && right.IsBinaryHeap() &&
(left == Leaf{} || x <= left.x) &&
(right == Leaf{} || x <= right.x)
}
}


type Unit struct{}

ghost
requires b
decreases
pure func asserting(b bool) Unit {
return Unit{}
}

type PQueue = BraunTree

type BraunTree adt {
Leaf {}

Node {
x int
left BraunTree
right BraunTree
}
}
31 changes: 31 additions & 0 deletions ...le_10_2/full/full-rand-iter_30-gran_1-sil_ver_0608ac9-z3_ver_4_8_7-gobra_ver_0608ac92.csv
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,31 @@
qi-k!601,qi-k!544,qi-k!578,qi-k!556,qi-quant-u-8,qi-quant-u-9,qi-$Multiset[Int]_prog.card_non_negative,qi-$Multiset[Int]_prog.card_empty,qi-quant-u-27,qi-quant-u-2,qi-quant-u-26,qi-quant-u-3,qi-quant-u-0,qi-quant-u-24,qi-quant-u-1,qi-quant-u-10,qi-quant-u-11,qi-quant-u-35,qi-quant-u-34,qi-quant-u-4,qi-quant-u-28,qi-quant-u-5,qi-quant-u-43,qi-quant-u-18,qi-quant-u-42,qi-quant-u-19,qi-quant-u-33,qi-quant-u-32,qi-quant-u-41,qi-quant-u-16,qi-quant-u-40,qi-quant-u-17,qi-quant-u-6,qi-quant-u-30,qi-quant-u-7,qi-quant-u-12,qi-quant-u-36,qi-quant-u-13,qi-$Multiset[Int]_prog.count_card,qi-$Multiset[Int]_prog.singleton_unionone,qi-$Multiset[Int]_prog.card_union,qi-$Multiset[Int]_prog.count_union,qi-$Multiset[Int]_prog.card_unionone,qi-$Multiset[Int]_prog.count_singleton,qi-$Multiset[Int]_prog.count_unionone,qi-$Multiset[Int]_prog.count_empty,qi-quant-u-22,qi-quant-u-45,qi-quant-u-23,qi-quant-u-44,qi-$Multiset[Int]_prog.equal_count,qi-$Multiset[Int]_prog.native_equality,qi-quant-u-14,qi-quant-u-38,qi-quant-u-15,qi-prog.getter_over_tuple2,qi-quant-u-20,qi-quant-u-21,qi-prog.integer_ax_dec,qi-k!560,qi-k!584,qi-k!590,qi-prog.integer_ax_bound,qi-quant-u-47,qi-quant-u-46,execution_time
1,73,56,17,18,41,110,110,44,43,44,53,43,43,36,9,22,10,10,27,27,23,3,5,5,5,20,20,3,3,3,12,3,3,3,1,1,1,178,17,44,69,22,57,62,35,1,1,1,1,1,1,1,1,1,3,2,1,9,80,43,43,6,1,1,11.179346323013306
1,79,58,17,18,45,118,117,50,49,50,55,49,49,35,9,18,10,10,27,27,23,3,5,5,5,20,20,3,3,3,12,3,3,3,1,1,1,184,18,47,68,19,60,64,39,1,1,1,1,1,1,1,1,1,3,2,1,9,76,41,41,6,1,1,11.277501106262207
1,73,56,16,18,39,104,104,44,43,44,51,43,43,36,9,22,10,10,27,27,23,3,5,5,5,20,20,3,3,3,12,3,3,3,1,1,1,155,16,41,62,16,48,50,33,1,1,1,1,1,1,1,1,1,3,2,1,9,78,42,42,6,1,1,11.028146505355835
1,75,56,15,18,41,112,112,46,45,46,53,45,45,36,9,18,10,10,27,27,23,3,5,5,5,20,20,3,3,3,12,3,3,3,1,1,1,174,17,44,67,18,53,56,35,1,1,1,1,1,1,1,1,1,3,2,1,9,76,41,41,6,1,1,10.955808639526367
1,73,57,15,18,41,106,106,44,43,44,51,43,43,35,9,18,10,10,27,27,23,3,5,5,5,20,20,3,3,3,12,3,3,3,1,1,1,168,16,42,65,17,51,53,35,1,1,1,1,1,1,1,1,1,3,2,1,9,74,40,40,6,1,1,10.909290790557861
1,73,57,17,18,41,106,106,44,43,44,51,43,43,35,9,22,10,10,27,27,23,3,5,5,5,20,20,3,3,3,12,3,3,3,1,1,1,171,16,42,63,18,54,57,37,1,1,1,1,1,1,1,1,1,3,2,1,9,78,42,42,6,1,1,11.280102014541626
1,75,58,18,18,43,112,112,46,45,46,53,45,45,35,9,22,10,10,27,27,23,3,5,5,5,20,20,3,3,3,12,3,3,3,1,1,1,177,17,44,67,19,56,59,37,1,1,1,1,1,1,1,1,1,3,2,1,9,80,43,43,6,1,1,10.99258542060852
1,75,57,15,18,41,108,108,46,45,46,51,45,45,35,9,18,10,10,27,27,23,3,5,5,5,20,20,3,3,3,12,3,3,3,1,1,1,171,16,42,65,21,55,60,35,1,1,1,1,1,1,1,1,1,3,2,1,9,74,40,40,6,1,1,11.316591262817383
1,79,58,19,18,45,120,120,50,49,50,55,49,49,35,9,22,10,10,27,27,23,3,5,5,5,20,20,3,3,3,12,3,3,3,1,1,1,187,18,47,71,20,59,63,39,1,1,1,1,1,1,1,1,1,3,2,1,9,81,44,44,6,1,1,11.092773675918579
1,73,57,15,18,41,106,106,44,43,44,51,43,43,35,9,18,10,10,27,27,23,3,5,5,5,20,20,3,3,3,12,3,3,3,1,1,1,172,16,42,65,18,54,57,37,1,1,1,1,1,1,1,1,1,3,2,1,9,74,40,40,6,1,1,10.966804027557373
1,71,56,14,18,39,102,102,42,41,42,51,41,41,36,9,18,10,10,27,27,23,3,5,5,5,20,20,3,3,3,12,3,3,3,1,1,1,156,16,41,63,19,50,54,33,1,1,1,1,1,1,1,1,1,3,2,1,9,74,40,40,6,1,1,11.277849435806274
1,79,58,17,18,45,118,118,50,49,50,55,49,49,35,9,18,10,10,27,27,23,3,5,5,5,20,20,3,3,3,12,3,3,3,1,1,1,184,18,47,69,19,58,62,39,1,1,1,1,1,1,1,1,1,3,2,1,9,76,42,41,6,1,1,11.119897603988647
1,73,56,17,18,41,106,106,44,43,44,51,43,43,35,9,22,10,10,27,27,23,3,5,5,5,20,20,3,3,3,12,3,3,3,1,1,1,167,16,42,63,17,51,53,35,1,1,1,1,1,1,1,1,1,3,2,1,9,78,42,42,6,1,1,11.036255598068237
1,77,56,16,18,43,118,118,48,47,48,55,47,47,36,9,18,10,10,27,27,23,3,5,5,5,20,20,3,3,3,12,3,3,3,1,1,1,184,18,47,71,19,57,59,37,1,1,1,1,1,1,1,1,1,3,2,1,9,78,42,42,6,1,1,11.181584358215332
1,77,58,18,18,43,112,112,48,47,48,53,47,47,35,9,22,10,10,27,27,23,3,5,5,5,20,20,3,3,3,12,3,3,3,1,1,1,176,17,44,67,18,56,60,37,1,1,1,1,1,1,1,1,1,3,2,1,9,78,42,42,6,1,1,11.176728963851929
1,77,58,16,18,43,114,114,48,47,48,53,47,47,35,9,18,10,10,27,27,23,3,5,5,5,20,20,3,3,3,12,3,3,3,1,1,1,178,17,44,65,19,58,62,37,1,1,1,1,1,1,1,1,1,3,2,1,9,76,41,41,6,1,1,11.077479124069214
1,75,56,17,18,41,112,112,46,45,46,53,45,45,36,9,22,10,10,27,27,23,3,5,5,5,20,20,3,3,3,12,3,3,3,1,1,1,176,17,44,69,18,53,55,35,1,1,1,1,1,1,1,1,1,3,2,1,9,80,43,43,6,1,1,11.237483501434326
1,73,56,14,18,39,104,104,44,43,44,51,43,43,36,9,18,10,10,27,27,23,3,5,5,5,20,20,3,3,3,12,3,3,3,1,1,1,155,16,41,62,16,48,50,33,1,1,1,1,1,1,1,1,1,3,2,1,9,74,40,40,6,1,1,11.1346595287323
1,75,58,18,18,43,112,112,46,45,46,53,45,45,35,9,22,10,10,27,27,23,3,5,5,5,20,20,3,3,3,12,3,3,3,1,1,1,180,17,45,69,19,57,60,38,1,1,1,1,1,1,1,1,1,3,2,1,9,80,43,43,6,1,1,11.248454809188843
1,73,57,18,18,43,112,112,46,45,46,53,43,43,35,9,22,10,10,27,27,23,3,5,5,5,20,20,3,3,3,12,3,3,3,1,1,1,184,17,45,69,23,60,66,39,1,1,1,1,1,1,1,1,1,3,2,1,9,80,43,43,6,1,1,10.912991523742676
1,77,58,17,18,45,118,118,48,47,48,55,47,47,35,9,18,10,10,27,27,23,3,5,5,5,20,20,3,3,3,12,3,3,3,1,1,1,186,18,47,71,20,58,61,39,1,1,1,1,1,1,1,1,1,3,2,1,9,78,42,42,6,1,1,11.0569589138031
1,73,56,16,18,39,103,103,44,43,44,51,43,43,36,9,22,10,10,27,27,23,3,5,5,5,20,20,3,3,3,12,3,3,3,1,1,1,155,16,41,62,16,48,50,33,1,1,1,1,1,1,1,1,1,3,2,1,9,78,42,42,6,1,1,11.097052335739136
1,77,58,16,18,43,114,114,48,47,48,53,47,47,35,9,18,10,10,27,27,23,3,5,5,5,20,20,3,3,3,12,3,3,3,1,1,1,180,17,45,67,19,57,60,39,1,1,1,1,1,1,1,1,1,3,2,1,9,76,41,41,6,1,1,10.960843324661255
1,73,57,17,18,41,106,106,44,43,44,51,43,43,35,9,22,10,10,27,27,23,3,5,5,5,20,20,3,3,3,12,3,3,3,1,1,1,172,16,42,65,18,54,57,37,1,1,1,1,1,1,1,1,1,3,2,1,9,78,42,42,6,1,1,10.877399682998657
1,73,57,16,18,43,110,110,44,43,44,53,43,43,35,9,18,10,10,27,27,23,3,5,5,5,20,20,3,3,3,12,3,3,3,1,1,1,181,17,45,69,22,58,63,38,1,1,1,1,1,1,1,1,1,3,2,1,9,76,41,41,6,1,1,11.189347743988037
1,77,58,17,18,45,118,118,48,47,48,55,47,47,35,9,18,10,10,27,27,23,3,5,5,5,20,20,3,3,3,12,3,3,3,1,1,1,189,18,48,73,20,59,62,40,1,1,1,1,1,1,1,1,1,3,2,1,9,78,42,42,6,1,1,11.10829496383667
1,77,58,18,18,47,122,122,48,47,48,57,47,47,35,9,18,10,10,27,27,23,3,5,5,5,20,20,3,3,3,12,3,3,3,1,1,1,200,19,50,75,26,66,73,41,1,1,1,1,1,1,1,1,1,3,2,1,9,78,43,43,6,1,1,10.972086906433105
1,87,59,34,18,51,168,168,56,55,56,81,55,55,45,9,24,10,10,27,27,23,3,5,5,5,20,20,3,3,3,12,3,3,3,1,1,1,352,28,67,114,30,95,98,50,1,1,1,1,1,1,1,1,1,3,2,1,9,112,61,61,6,1,1,11.038999795913696
1,75,56,18,18,43,116,116,46,45,46,55,45,45,36,9,22,10,10,27,27,23,3,5,5,5,20,20,3,3,3,12,3,3,3,1,1,1,190,18,47,73,24,61,67,37,1,1,1,1,1,1,1,1,1,3,2,1,9,82,44,44,6,1,1,10.882302045822144
1,79,58,17,18,45,118,118,50,49,50,55,49,49,35,9,18,10,10,27,27,23,3,5,5,5,20,20,3,3,3,12,3,3,3,1,1,1,182,18,47,69,19,58,62,39,1,1,1,1,1,1,1,1,1,3,2,1,9,76,41,41,6,1,1,10.89523458480835
Binary file added ...er_30-gran_1-sil_ver_0608ac9-z3_ver_4_8_7-gobra_ver_0608ac92.execution_time.png
View file
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
Binary file added ...full-rand-iter_30-gran_1-sil_ver_0608ac9-z3_ver_4_8_7-gobra_ver_0608ac92.qi.png
View file
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
Loading

0 comments on commit 9ac60d0

Please sign in to comment.