Abs program loaded in 4 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 2 ms.
sabu_memo_table_1(case_0,[A],[1*A>=0,1*A=1],0,0)
sabu_memo_table_1(apply,[A],[1*A>=0,1*A=1,1*A>=0],1,0)
sabu_memo_table_1(case_0,[A],[-1*A>= -3,1*A>=1],2,1)
sabu_memo_table_1(apply,[A],[-1*A>= -3,1*A>=1],3,1)
sabu_memo_table_1(case_0,[A],[-1*A>= -7,1*A>=1],4,2)
sabu_memo_table_1(apply,[A],[-1*A>= -7,1*A>=1],5,2)
sabu_memo_table_1(case_0,[A],[-1*A>= -15,1*A>=1],6,3)
sabu_memo_table_1(apply,[A],[-1*A>= -15,1*A>=1],7,3)
sabu_memo_table_1(case_0,[A],[1*A>=1],8,0)
sabu_memo_table_1(apply,[A],[1*A>=1],9,0)
sabu_memo_table_1(comp,[A,B,C],[1*B>=0,1*A>=0,1*A>=0,1*B>=0,1*A+1*B+ -1*C= -1],0,0)
sabu_memo_table_1(case_1,[A,B],[1*A>=0,1*B=1,1*A=1],0,0)
sabu_memo_table_1(walk,[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>= -3,1*B>=1,2*A+ -1*B=1],1,1)
sabu_memo_table_1(walk,[A,B],[-1*B>= -3,1*B>=1,2*A+ -1*B=1],2,1)
sabu_memo_table_1(case_1,[A,B],[-1*A>= -3,1*A>=1,2*A+ -1*B=1],3,2)
sabu_memo_table_1(walk,[A,B],[-1*A>= -3,1*A>=1,2*A+ -1*B=1],4,2)
sabu_memo_table_1(case_1,[A,B],[-1*A>= -4,1*A>=1,2*A+ -1*B=1],5,3)
sabu_memo_table_1(walk,[A,B],[-1*A>= -4,1*A>=1,2*A+ -1*B=1],6,3)
sabu_memo_table_1(case_1,[A,B],[2*A+ -1*B=1,1*A>=1],7,0)
sabu_memo_table_1(walk,[A,B],[2*A+ -1*B=1,1*A>=1],8,0)
sabu_memo_table_1(rev2,[A],[1*A>=1],0,0)
sabu_memo_table_1(start,[A],[1*A>=0,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], [1*A>=1], 8, 0).
sabu_memo_table_1(apply, [A], [1*A>=1], 9, 0).
sabu_memo_table_1(comp, [B, A, C], [1*A>=0, 1*B>=0, 1*B>=0, 1*A>=0, 1*B+1*A+ -1*C= -1], 0, 0).
sabu_memo_table_1(case_1, [A, B], [2*A+ -1*B=1, 1*A>=1], 7, 0).
sabu_memo_table_1(walk, [A, B], [2*A+ -1*B=1, 1*A>=1], 8, 0).
sabu_memo_table_1(rev2, [A], [1*A>=1], 0, 0).
sabu_memo_table_1(start, [A], [1*A>=0, 1*A>=1], 0, 0).
sabu_memo_table_1(start, [], [], 0, 0).


Size analysis performed in 6 ms.

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

Generated 33 equations 

Cost relation system solved by PUBS in 13 ms.

Method start terminates?: YES

 - l_1: size of l wrt. List<A>
UB for start(l_1) = nat(l_1)+pow(4,nat(l_1))


Method start terminates?: YES

 - l_1: size of l wrt. List<A>
UB for start(l_1) = nat(l_1)+pow(4,nat(l_1))


Method start terminates?: YES

UB for start(l_1) = nat(l_1)+pow(4,nat(l_1))


Method start terminates?: YES

UB for start(l_1) = nat(l_1)+pow(4,nat(l_1))


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

#### Computed strongly connected components 
0. recursive [multiple] : [apply/1,case_0/1]
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,start/0]

#### Obtained direct recursion through partial evaluation 
0. SCC is partially evaluated into apply/1
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/1 
* CE 6 is refined into CE [7] 
* CE 5 is refined into CE [8] 
* CE 4 is refined into CE [9] 


#### Refined cost equations apply/1 
* CE 7: apply(A) = 4+ apply(B)+ apply(C)
     [C>=0,B>=1,B+C+1=A] 
* CE 8: apply(A) = 5
     [A=1] 
* CE 9: apply(A) = 3
     [A=1] 

### Cost equations --> "Loop" of apply/1 
* CEs [9] --> Loop 7 
* CEs [8] --> Loop 8 
* CEs [7] --> Loop 9 

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

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

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


### Resulting Chains:apply(A) 
* [8]
* [7]
* [multiple([9],[[8],[7]])]


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


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

### Cost equations --> "Loop" of walk/1 
* CEs [11] --> Loop 10 
* CEs [10] --> Loop 11 

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

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

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


### Resulting Chains:walk(A) 
* [[11],10]
* [10]


### Specialization of cost equations rev2/1 
* CE 1 is refined into CE [12,13,14] 


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

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

#### Loops of rev2/1 
* Loop 12: rev2(A) [A>=2] 
* Loop 13: rev2(A) [A=1] 
* Loop 14: rev2(A) [A=1] 

### Ranking functions of CR rev2(A) 

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


### Resulting Chains:rev2(A) 
* [14]
* [13]
* [12]


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

#### Cost of loops [9] 

 * loop 9:apply(A) -> [apply(A'),apply(A'2)] 
4
#### Cost of phase [9]:apply(A) -> [] 
4*it(9)+3*it([7])+5*it([8])+0
  Such that:it(9) =< A/2-1/2
it([7])+it([8]) =< A/2+1/2
it(9)+it([7])+it([8]) >= A

#### Cost of chains of apply(A):
* Chain [8]: 5
  with precondition: [A=1] 

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

* Chain [multiple([9],[[8],[7]])]: 4*it(9)+3*it([7])+5*it([8])+0
  Such that:it(9) =< A/2-1/2
it([7])+it([8]) =< A/2+1/2
it(9)+it([7])+it([8]) >= A

  with precondition: [A>=3] 


#### Cost of loops [11] 

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

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

  with precondition: [A>=2] 

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


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

* Chain [13]: 9
  with precondition: [A=1] 

* Chain [12]: 7*s(1)+4*s(2)+3*s(3)+5*s(4)+6
  Such that:s(3)+s(4) =< A
aux(1) =< A-1
s(1) =< aux(1)
s(2) =< aux(1)
s(1) >= A-1
s(2)+s(3)+s(4) >= 2*A-1

  with precondition: [A>=2] 


Closed-form bounds of rev2(A): 
-------------------------------------
* Chain [14] with precondition: [A=1] 
    - Lower bound: 11 
    - Complexity: constant
 * Chain [13] with precondition: [A=1] 
    - Lower bound: 9 
    - Complexity: constant
 * Chain [12] with precondition: [A>=2] 
    - Lower bound: 13*A-4 
    - Complexity: n
 
### Partitioned lower bound of rev2(A): 
* 9 
 if [A=1]
* 13*A-4 
 if [A>=2]
Possible lower bounds : [9,13*A-4]
Maximum lower bound complexity: n
* Total analysis performed in 39 ms.