Abs program loaded in 3 ms.
Rule based representation generated in 0 ms.
Rule based representation stored in /tmp/costabs/rbr.rbr
RBR properties stored in /tmp/costabs/rbr.properties
Class invariants generated and loaded in 0 ms.
Size abstraction not supported for native
Abstract compilation performed in 1 ms.
sabu_memo_table_1(case_0,[A,B,C],[1*C>=0,1*A>=0,1*A=1,1*B+ -1*C=0],0,0)
sabu_memo_table_1(append,[A,B,C],[1*B>=0,1*A>=0,1*B+ -1*C=0,1*A=1,1*A>=0,1*C>=0],1,0)
sabu_memo_table_1(case_0,[A,B,C],[1*B>=0,1*B+ -1*C>= -1,-1*B+1*C>=0,1*A+1*B+ -1*C=1],2,1)
sabu_memo_table_1(append,[A,B,C],[1*B>=0,1*B+ -1*C>= -1,-1*B+1*C>=0,1*A+1*B+ -1*C=1],3,1)
sabu_memo_table_1(case_0,[A,B,C],[-1*A>= -3,1*A>=1,1*B>=0,1*A+1*B+ -1*C=1],4,2)
sabu_memo_table_1(append,[A,B,C],[-1*A>= -3,1*A>=1,1*B>=0,1*A+1*B+ -1*C=1],5,2)
sabu_memo_table_1(case_0,[A,B,C],[-1*A>= -4,1*A>=1,1*B>=0,1*A+1*B+ -1*C=1],6,3)
sabu_memo_table_1(append,[A,B,C],[-1*A>= -4,1*A>=1,1*B>=0,1*A+1*B+ -1*C=1],7,3)
sabu_memo_table_1(case_0,[A,B,C],[1*A+1*B+ -1*C=1,1*B>=0,1*A>=1],8,0)
sabu_memo_table_1(append,[A,B,C],[1*A+1*B+ -1*C=1,1*B>=0,1*A>=1],9,0)
sabu_memo_table_1(case_1,[A,B],[1*A>=0,1*B=1,1*A=1],0,0)
sabu_memo_table_1(rev,[A,B],[1*A>=0,1*A=1,1*B=1,1*A>=0],0,0)
sabu_memo_table_1(case_1,[A,B],[-1*B>= -2,1*B>=1,1*A+ -1*B=0],1,1)
sabu_memo_table_1(rev,[A,B],[-1*B>= -2,1*B>=1,1*A+ -1*B=0],2,1)
sabu_memo_table_1(case_1,[A,B],[-1*A>= -3,1*A>=1,1*A+ -1*B=0],3,2)
sabu_memo_table_1(rev,[A,B],[-1*A>= -3,1*A>=1,1*A+ -1*B=0],4,2)
sabu_memo_table_1(case_1,[A,B],[-1*A>= -4,1*A>=1,1*A+ -1*B=0],5,3)
sabu_memo_table_1(rev,[A,B],[-1*A>= -4,1*A>=1,1*A+ -1*B=0],6,3)
sabu_memo_table_1(case_1,[A,B],[1*A+ -1*B=0,1*A>=1],7,0)
sabu_memo_table_1(rev,[A,B],[1*A+ -1*B=0,1*A>=1],8,0)
sabu_memo_table_1(start,[A],[1*A>=1],0,0)
sabu_memo_table_1(start,[],[],0,0)
:- dynamic sabu_memo_table_1/5.
sabu_memo_table_1(case_0, [A, B, C], [1*A+1*B+ -1*C=1, 1*B>=0, 1*A>=1], 8, 0).
sabu_memo_table_1(append, [A, B, C], [1*A+1*B+ -1*C=1, 1*B>=0, 1*A>=1], 9, 0).
sabu_memo_table_1(case_1, [A, B], [1*A+ -1*B=0, 1*A>=1], 7, 0).
sabu_memo_table_1(rev, [A, B], [1*A+ -1*B=0, 1*A>=1], 8, 0).
sabu_memo_table_1(start, [A], [1*A>=1], 0, 0).
sabu_memo_table_1(start, [], [], 0, 0).
Size analysis performed in 7 ms.
Cost relation system stored in /tmp/costabs/crs.crs
Generated 30 equations
Cost relation system solved by PUBS in 13 ms.
Method start terminates?: YES
- xs_1: size of xs wrt. List
UB for start(xs_1) = pow(nat(xs_1),2)
Method start terminates?: YES
- xs_1: size of xs wrt. List
UB for start(xs_1) = pow(nat(xs_1),2)
Method start terminates?: YES
UB for start(xs_1) = pow(nat(xs_1),2)
Method start terminates?: YES
UB for start(xs_1) = pow(nat(xs_1),2)
Preprocessing Cost Relations
=====================================
#### Computed strongly connected components
0. recursive : [append/2,case_0/2]
1. recursive [non_tail] : [case_1/1,rev/1]
3. non_recursive : [start/1]
* The entry case_1/1 is not a cutpoint so it becomes a new SCC 3
Warning: the following predicates are never called:[and_op/2,eq/2,geq/2,gt/2,leq/2,lt/2,maxNorm/2,neg/1,neq/2,or/2,start/0]
#### Obtained direct recursion through partial evaluation
0. SCC is partially evaluated into append/2
1. SCC is partially evaluated into rev/1
3. SCC is partially evaluated into case_1/1
Control-Flow Refinement of Cost Relations
=====================================
### Specialization of cost equations append/2
* CE 6 is refined into CE [7]
* CE 5 is refined into CE [8]
#### Refined cost equations append/2
* CE 7: append(A,B) = 5+ append(C,D)
[C>=0,C+1=A,D=2,B=2]
* CE 8: append(A,B) = 2
[B=2,A=1]
### Cost equations --> "Loop" of append/2
* CEs [8] --> Loop 7
* CEs [7] --> Loop 8
#### Loops of append/2
* Loop 7: append(A,B) [B=2,A=1]
* Loop 8: append(A,B)-> append(A',B')
[A'>=0,A'+1=A,B'=2,B=2]
### Ranking functions of CR append(A,B)
* RF of phase [8]: [A]
#### Partial ranking functions of CR append(A,B)
* Partial RF of phase [8]:
- RF of loop [8:1]:
A
### Resulting Chains:append(A,B)
* [[8],7]
* [7]
### Specialization of cost equations rev/1
* CE 4 is refined into CE [9]
* CE 3 is refined into CE [10,11]
#### Refined cost equations rev/1
* CE 9: rev(A) = 3
[A=1]
* CE 10: rev(A) = 7+ rev(B)+ append(B,C):[[8],7]
[B>=2,B+1=A,C=2]
* CE 11: rev(A) = 7+ rev(B)+ append(C,D):[7]
[B=1,D=2,C=1,A=2]
### Cost equations --> "Loop" of rev/1
* CEs [10] --> Loop 9
* CEs [11] --> Loop 10
* CEs [9] --> Loop 11
#### Loops of rev/1
* Loop 9: rev(A)-> rev(A')
[A'>=2,A'+1=A]
* Loop 10: rev(A)-> rev(A')
[A'=1,A=2]
* Loop 11: rev(A) [A=1]
### Ranking functions of CR rev(A)
* RF of phase [9]: [A-2]
#### Partial ranking functions of CR rev(A)
* Partial RF of phase [9]:
- RF of loop [9:1]:
A-2
### Resulting Chains:rev(A)
* [[9],10,11]
* [11]
* [10,11]
### Specialization of cost equations case_1/1
* CE 1 is refined into CE [12,13,14]
* CE 2 is refined into CE [15]
#### Refined cost equations case_1/1
* CE 12: case_1(A) = 6+ rev(B):[[9],10,11]+ append(B,C):[[8],7]
[B>=3,B+1=A,C=2]
* CE 13: case_1(A) = 6+ rev(B):[11]+ append(C,D):[7]
[D=2,C=1,B=1,A=2]
* CE 14: case_1(A) = 6+ rev(B):[10,11]+ append(C,D):[[8],7]
[D=2,C=2,B=2,A=3]
* CE 15: case_1(A) = 2
[A=1]
### Cost equations --> "Loop" of case_1/1
* CEs [12] --> Loop 12
* CEs [14] --> Loop 13
* CEs [13] --> Loop 14
* CEs [15] --> Loop 15
#### Loops of case_1/1
* Loop 12: case_1(A) [A>=4]
* Loop 13: case_1(A) [A=3]
* Loop 14: case_1(A) [A=2]
* Loop 15: case_1(A) [A=1]
### Ranking functions of CR case_1(A)
#### Partial ranking functions of CR case_1(A)
### Resulting Chains:case_1(A)
* [15]
* [14]
* [13]
* [12]
Computing Bounds
=====================================
#### Cost of loops [8]
* loop 8:append(A,B) -> [append(A',B')]
5
#### Cost of phase [8]:append(A,B) -> [append(A',B')]
5*it(8)+0
Such that:it(8) =< A
it(8) =< A-A'
it(8) >= A-A'
#### Cost of chains of append(A,B):
* Chain [[8],7]: 5*it(8)+2
Such that:it(8) =< A-1
it(8) >= A-1
with precondition: [B=2,A>=2]
* Chain [7]: 2
with precondition: [A=1,B=2]
#### Cost of loops [9]
* loop 9:rev(A) -> [rev(A')]
5*s(2)+9
Such that:s(2) =< A'-1
s(2) >= A'-1
#### Cost of phase [9]:rev(A) -> [rev(A')]
9*it(9)+5*s(3)+0
Such that:it(9) =< A-A'
aux(4) =< A-2
it(9) =< aux(4)
s(3) =< it(9)*aux(4)
aux(1) =< it(9)
aux(2) >= A-2
it(9) >= A-A'
aux(1) >= it(9)
s(3) >= aux(1)*aux(2)+aux(1)*(1/2)-aux(1)*aux(1)*(1/2)
#### Cost of chains of rev(A):
* Chain [[9],10,11]: 9*it(9)+5*s(3)+12
Such that:aux(5) =< A-2
it(9) =< aux(5)
s(3) =< it(9)*aux(5)
aux(1) =< it(9)
aux(6) >= A-2
aux(6) >= aux(6)
it(9) >= aux(6)
aux(1) >= it(9)
s(3) >= aux(1)*aux(6)+aux(1)*(1/2)-aux(1)*aux(1)*(1/2)
with precondition: [A>=3]
* Chain [11]: 3
with precondition: [A=1]
* Chain [10,11]: 12
with precondition: [A=2]
#### Cost of chains of case_1(A):
* Chain [15]: 2
with precondition: [A=1]
* Chain [14]: 11
with precondition: [A=2]
* Chain [13]: 5*s(4)+20
Such that:s(4) =< 1
s(4) >= 1
with precondition: [A=3]
* Chain [12]: 9*s(7)+5*s(8)+5*s(10)+20
Such that:s(5) =< A-3
s(10) =< A-2
s(7) =< s(5)
s(8) =< s(7)*s(5)
s(9) =< s(7)
s(6) >= A-3
s(10) >= A-2
s(6) >= s(6)
s(7) >= s(6)
s(9) >= s(7)
s(8) >= s(9)*s(6)+s(9)*(1/2)-s(9)*s(9)*(1/2)
with precondition: [A>=4]
Closed-form bounds of case_1(A):
-------------------------------------
* Chain [15] with precondition: [A=1]
- Lower bound: 2
- Complexity: constant
* Chain [14] with precondition: [A=2]
- Lower bound: 11
- Complexity: constant
* Chain [13] with precondition: [A=3]
- Lower bound: 25
- Complexity: constant
* Chain [12] with precondition: [A>=4]
- Lower bound: 33/2*A-49/2+(5/2*A-15/2)*(A-3)
- Complexity: n^2
### Partitioned lower bound of case_1(A):
* 2
if [A=1]
* 11
if [A=2]
* 25
if [A=3]
* 33/2*A-49/2+(5/2*A-15/2)*(A-3)
if [A>=4]
Possible lower bounds : [2,11,25,33/2*A-49/2+(5/2*A-15/2)*(A-3)]
Maximum lower bound complexity: n^2
* Total analysis performed in 39 ms.