testbed
generated constraint from time and size complexity anlysis with HOSA
solver
z3
strategy
incremental templates
incremental templates with minimisation
incremental templates with minimisation and scc decomposition
z3-i
z3-im
z3-ims
Problem (all selected)
 * answer * answer * answer
append-size
 *
SUCCESS(1)
 		0.01 *
SUCCESS(1)
 		0.02 *
SUCCESS(1)
 		0.02
append-time
 *
SUCCESS(1)
 		0.03 *
SUCCESS(1)
 		0.07 *
SUCCESS(1)
 		0.05
appendtwice-size
 *
SUCCESS(1)
 		0.26 *
SUCCESS(1)
 		0.14 *
SUCCESS(1)
 		0.04
appendtwice-time
 *
SUCCESS(1)
 		0.25 *
SUCCESS(1)
 		2.05 *
SUCCESS(1)
 		0.13
dfs-flatten-size
 *
SUCCESS(1)
 		0.04 *
SUCCESS(1)
 		0.12 *
SUCCESS(1)
 		0.08
dfs-flatten-time
 *
SUCCESS(1)
 		0.96 *
SUCCESS(1)
 		0.50 *
SUCCESS(1)
 		0.30
fmap_tree-size
 *
SUCCESS(1)
 		0.06 *
SUCCESS(1)
 		0.18 *
SUCCESS(1)
 		0.12
fmap_tree-time
 *
SUCCESS(1)
 		0.33 *
SUCCESS(1)
 		0.40 *
SUCCESS(1)
 		0.37
insertsort-size
 *
TIMEOUT
 90.05 *
SUCCESS(2)
 		21.47 *
SUCCESS(1)
 		0.24
insertsort-time
 *
TIMEOUT
 90.09 *
TIMEOUT
 90.09 *
SUCCESS(3)
 		13.06
prependall-size
 *
SUCCESS(1)
 		0.03 *
SUCCESS(1)
 		0.15 *
SUCCESS(1)
 		0.09
prependall-time
 *
SUCCESS(2)
 		5.06 *
SUCCESS(2)
 		1.06 *
SUCCESS(2)
 		0.29
product-size
 *
TIMEOUT
 90.01 *
SUCCESS(2)
 		1.41 *
SUCCESS(2)
 		0.12
product-time
 *
SUCCESS(2)
 		63.21 *
SUCCESS(2)
 		13.16 *
SUCCESS(2)
 		0.74
recscheme-size
 *
SUCCESS(1)
 		0.02 *
SUCCESS(1)
 		0.03 *
SUCCESS(1)
 		0.03
recscheme-time
 *
SUCCESS(1)
 		0.14 *
SUCCESS(1)
 		0.24 *
SUCCESS(1)
 		0.13
rev-dl-contrived-size
 *
SUCCESS(1)
 		0.03 *
SUCCESS(1)
 		0.07 *
SUCCESS(1)
 		0.05
rev-dl-contrived-time
 *
SUCCESS(1)
 		0.62 *
SUCCESS(1)
 		2.82 *
SUCCESS(1)
 		1.43
rev-dl-size
 *
SUCCESS(1)
 		0.03 *
SUCCESS(1)
 		0.08 *
SUCCESS(1)
 		0.07
rev-dl-time
 *
SUCCESS(1)
 		0.44 *
SUCCESS(1)
 		4.25 *
SUCCESS(1)
 		0.68
reverse-size
 *
SUCCESS(1)
 		0.01 *
SUCCESS(1)
 		0.01 *
SUCCESS(1)
 		0.02
reverse-time
 *
SUCCESS(1)
 		0.03 *
SUCCESS(1)
 		0.05 *
SUCCESS(1)
 		0.04

Result Summary



z3-i
z3-im
z3-ims
Success "SUCCESS(1)"
 17 17 18
Success "SUCCESS(2)"
 2 4 3
Success "SUCCESS(3)"
 0 0 1
Timeout
 3 1 0

Average Times


z3-i
z3-im
z3-ims
Success "SUCCESS(1)"
 0.19 0.66 0.22
Success "SUCCESS(2)"
 34.13 9.28 0.38
Success "SUCCESS(3)"
 0.00 0.00 13.06
Timeout
 90.05 90.09 0.00
Overall
 15.53 6.29 0.82