Abs program loaded in 3 ms.

Rule based representation generated in 1 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*A=1,1*B+ -1*C=0],0,0)
sabu_memo_table_1(case_0,[A,B,C],[-1*B+1*C>=0,1*A>=1],0,1)
sabu_memo_table_1(apply,[A,B,C],[1*A>=1,-1*B+1*C>=0],1,0)
sabu_memo_table_1(comp,[A,B,C],[-1*B+1*C>=1,-1*A+1*C>=1,1*C>=2],0,0)
sabu_memo_table_1(case_1,[A,B],[1*B=1,1*A=1],0,0)
sabu_memo_table_1(walk,[A,B],[1*A=1,1*B=1],0,0)
sabu_memo_table_1(case_1,[A,B],[-1*A+1*B>=0,1*A>=1],1,1)
sabu_memo_table_1(walk,[A,B],[-1*A+1*B>=0,1*A>=1],2,1)
sabu_memo_table_1(rev2,[A,B],[1*B>=1,1*A>=1],0,0)
sabu_memo_table_1(start,[A,B],[1*A>=1,1*B>=1],0,0)
sabu_memo_table_1(start,[A,B],[],0,1)
:- dynamic sabu_memo_table_1/5.

sabu_memo_table_1(case_0, [C, A, B], [-1*A+1*B>=0, 1*C>=1], 0, 1).
sabu_memo_table_1(apply, [A, B, C], [1*A>=1, -1*B+1*C>=0], 1, 0).
sabu_memo_table_1(comp, [C, A, B], [-1*A+1*B>=1, -1*C+1*B>=1, 1*B>=2], 0, 0).
sabu_memo_table_1(case_1, [A, B], [-1*A+1*B>=0, 1*A>=1], 1, 1).
sabu_memo_table_1(walk, [A, B], [-1*A+1*B>=0, 1*A>=1], 2, 1).
sabu_memo_table_1(rev2, [B, A], [1*A>=1, 1*B>=1], 0, 0).
sabu_memo_table_1(start, [_, _], [], 0, 1).


Size analysis performed in 3 ms.

Cost relation system stored in /tmp/costabs/crs.crs

Generated 35 equations 

Cost relation system solved by PUBS in 25 ms.

Method start terminates?: YES

UB for start(l) = nat(l)+pow(2,c(maximize_failed))


Preprocessing Cost Relations
=====================================

#### Computed strongly connected components 
0. recursive [multiple] : [apply/2,case_0/2]
1. non_recursive  : [comp/2]
2. recursive [non_tail] : [case_1/1,walk/1]
3. non_recursive  : [rev2/1]
5. non_recursive  : [start/1]
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]

#### Obtained direct recursion through partial evaluation 
0. SCC is partially evaluated into apply/2
1. SCC is completely evaluated into other SCCs
2. SCC is partially evaluated into walk/1
3. SCC is partially evaluated into rev2/1

Control-Flow Refinement of Cost Relations
=====================================

### Specialization of cost equations apply/2 
* CE 6 is refined into CE [8] 
* CE 7 is refined into CE [9] 
* CE 5 is refined into CE [10] 
* CE 4 is refined into CE [11] 


#### Refined cost equations apply/2 
* CE 8: apply(A,B) = 4+ apply(C,B)+ apply(D,E)
     [A>=C+1,E>=B,C>=1,B>=1,A=D+1] 
* CE 9: apply(A,B) = 4+ apply(C,B)+ apply(D,E)
     [C>=D,E>=B,C>=1,B>=1,C+1=A] 
* CE 10: apply(A,B) = 5
     [B>=1,A>=2] 
* CE 11: apply(A,B) = 3
     [B>=1,A=1] 

### Cost equations --> "Loop" of apply/2 
* CEs [10] --> Loop 8 
* CEs [11] --> Loop 9 
* CEs [8] --> Loop 10 
* CEs [9] --> Loop 11 

#### Loops of apply/2 
* Loop 8: apply(A,B) [B>=1,A>=2] 
* Loop 9: apply(A,B) [B>=1,A=1] 
* Loop 10: apply(A,B)->  apply(A',B)  apply(A'2,B'2)
                  [A>=A'+1,B'2>=B,A'>=1,B>=1,A=A'2+1] 
* Loop 11: apply(A,B)->  apply(A',B)  apply(A'2,B'2)
                  [A'>=A'2,B'2>=B,A'>=1,B>=1,A'+1=A] 

### Ranking functions of CR apply(A,B) 
* RF of phase [10,11]: [A-1]

#### Partial ranking functions of CR apply(A,B) 
* Partial RF of phase [10,11]:
  - RF of loop [10:1,10:2,11:1,11:2]:
    A-1


### Resulting Chains:apply(A,B) 
* [9]
* [8]
* [multiple([10,11],[[9],[8]])]


### Specialization of cost equations walk/1 
* CE 3 is refined into CE [12] 
* CE 2 is refined into CE [13] 


#### Refined cost equations walk/1 
* CE 12: walk(A) = 7+ walk(B)
     [A>=B+1,B>=1] 
* CE 13: walk(A) = 3
     [A=1] 

### Cost equations --> "Loop" of walk/1 
* CEs [13] --> Loop 12 
* CEs [12] --> Loop 13 

#### Loops of walk/1 
* Loop 12: walk(A) [A=1] 
* Loop 13: walk(A)->  walk(A')
                  [A>=A'+1,A'>=1] 

### Ranking functions of CR walk(A) 
* RF of phase [13]: [A-1]

#### Partial ranking functions of CR walk(A) 
* Partial RF of phase [13]:
  - RF of loop [13:1]:
    A-1


### Resulting Chains:walk(A) 
* [[13],12]
* [12]


### Specialization of cost equations rev2/1 
* CE 1 is refined into CE [14,15,16,17,18] 


#### Refined cost equations rev2/1 
* CE 14: rev2(A) = 3+ walk(A):[[13],12]+ apply(B,C):[8]
     [B>=A,A>=2,C=1] 
* CE 15: rev2(A) = 3+ walk(A):[[13],12]+ apply(B,C):[multiple([10,11],[[9],[8]])]
     [B>=A,A>=2,C=1] 
* CE 16: rev2(A) = 3+ walk(B):[12]+ apply(C,D):[9]
     [D=1,C=1,B=1,A=1] 
* CE 17: rev2(A) = 3+ walk(B):[12]+ apply(C,D):[8]
     [C>=2,D=1,B=1,A=1] 
* CE 18: rev2(A) = 3+ walk(B):[12]+ apply(C,D):[multiple([10,11],[[9],[8]])]
     [C>=2,D=1,B=1,A=1] 

### Cost equations --> "Loop" of rev2/1 
* CEs [15] --> Loop 14 
* CEs [14] --> Loop 15 
* CEs [18] --> Loop 16 
* CEs [17] --> Loop 17 
* CEs [16] --> Loop 18 

#### Loops of rev2/1 
* Loop 14: rev2(A) [A>=2] 
* Loop 15: rev2(A) [A>=2] 
* Loop 16: rev2(A) [A=1] 
* Loop 17: rev2(A) [A=1] 
* Loop 18: rev2(A) [A=1] 

### Ranking functions of CR rev2(A) 

#### Partial ranking functions of CR rev2(A) 


### Resulting Chains:rev2(A) 
* [18]
* [17]
* [16]
* [15]
* [14]


Computing Bounds
=====================================

#### Cost of loops [10,11] 

 * loop 10:apply(A,B) -> [apply(A',B'),apply(A'2,B'2)] 
4
 * loop 11:apply(A,B) -> [apply(A',B'),apply(A'2,B'2)] 
4
#### Cost of phase [10,11]:apply(A,B) -> [] 
8*it(10)+5*it([8])+3*it([9])+0
#### Cost of chains of apply(A,B):
* Chain [9]: 3
  with precondition: [A=1,B>=1] 

* Chain [8]: 5
  with precondition: [A>=2,B>=1] 

* Chain [multiple([10,11],[[9],[8]])]: 8*it(10)+5*it([8])+3*it([9])+0
  with precondition: [A>=2,B>=1] 


#### Cost of loops [13] 

 * loop 13:walk(A) -> [walk(A')] 
7
#### Cost of phase [13]:walk(A) -> [walk(A')] 
7*it(13)+0
  Such that:it(13) =< A-1
it(13) =< A-A'

#### Cost of chains of walk(A):
* Chain [[13],12]: 7*it(13)+3
  Such that:it(13) =< A-1

  with precondition: [A>=2] 

* Chain [12]: 3
  with precondition: [A=1] 


#### Cost of chains of rev2(A):
* Chain [18]: 9
  with precondition: [A=1] 

* Chain [17]: 11
  with precondition: [A=1] 

* Chain [16]: 16*s(1)+6
  with precondition: [A=1] 

* Chain [15]: 7*s(4)+11
  Such that:s(4) =< A-1

  with precondition: [A>=2] 

* Chain [14]: 7*s(5)+16*s(6)+6
  Such that:s(5) =< A-1

  with precondition: [A>=2] 


Closed-form bounds of rev2(A): 
-------------------------------------
* Chain [18] with precondition: [A=1] 
    - Lower bound: 9 
    - Complexity: constant
 * Chain [17] with precondition: [A=1] 
    - Lower bound: 11 
    - Complexity: constant
 * Chain [16] with precondition: [A=1] 
    - Lower bound: 6 
    - Complexity: constant
 * Chain [15] with precondition: [A>=2] 
    - Lower bound: 11 
    - Complexity: constant
 * Chain [14] with precondition: [A>=2] 
    - Lower bound: 6 
    - Complexity: constant
 
### Partitioned lower bound of rev2(A): 
* 6 
 if [A>=1]
Possible lower bounds : [6]
Maximum lower bound complexity: constant
* Total analysis performed in 59 ms.