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 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(append,[A,B,C],[1*B+ -1*C=0,1*A=1],1,0)
sabu_memo_table_1(case_0,[A,B,C],[-1*B+1*C>=0,1*A>=1],2,1)
sabu_memo_table_1(append,[A,B,C],[-1*B+1*C>=0,1*A>=1],3,1)
sabu_memo_table_1(case_1,[A,B],[1*B=1,1*A=1],0,0)
sabu_memo_table_1(rev,[A,B],[1*A=1,1*B=1],0,0)
sabu_memo_table_1(case_1,[A,B],[1*A>=1,-1*A+1*B>=0],1,1)
sabu_memo_table_1(rev,[A,B],[-1*A+1*B>=0,1*A>=1],2,1)
sabu_memo_table_1(case_1,[A,B],[1*B>=1,1*A>=1],3,2)
sabu_memo_table_1(rev,[A,B],[1*B>=1,1*A>=1],4,2)
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], 2, 1).
sabu_memo_table_1(append, [C, A, B], [-1*A+1*B>=0, 1*C>=1], 3, 1).
sabu_memo_table_1(case_1, [B, A], [1*A>=1, 1*B>=1], 3, 2).
sabu_memo_table_1(rev, [B, A], [1*A>=1, 1*B>=1], 4, 2).
sabu_memo_table_1(start, [_, _], [], 0, 1).


Size analysis performed in 4 ms.

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

Generated 32 equations 

Cost relation system solved by PUBS in 17 ms.

Method start terminates?: YES

UB for start(xs) = nat(xs)*c(maximize_failed)


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]

#### 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 8 is refined into CE [9] 
* CE 7 is refined into CE [10] 


#### Refined cost equations append/2 
* CE 9: append(A,B) = 5+ append(C,B)
     [A>=C+1,B>=2,A>=2] 
* CE 10: append(A,B) = 2
     [B>=2,A=1] 

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

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

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

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


### Resulting Chains:append(A,B) 
* [[10],9]
* [9]


### Specialization of cost equations rev/1 
* CE 6 is refined into CE [11] 
* CE 5 is refined into CE [12,13] 
* CE 4 is refined into CE [14,15] 


#### Refined cost equations rev/1 
* CE 11: rev(A) = 3
     [A=1] 
* CE 12: rev(A) = 7+ rev(B)+ append(C,D):[[10],9]
     [A>=B+1,D>=A,B>=1,C>=2] 
* CE 13: rev(A) = 7+ rev(B)+ append(C,D):[9]
     [A>=B+1,D>=A,B>=1,C=1] 
* CE 14: rev(A) = 7+ rev(B)+ append(C,D):[[10],9]
     [D>=2,C>=2,A>=2,A=B+1] 
* CE 15: rev(A) = 7+ rev(B)+ append(C,D):[9]
     [D>=2,A>=2,A=B+1,C=1] 

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

#### Loops of rev/1 
* Loop 11: rev(A)->  rev(A')
                  [A>=A'+1,A'>=1] 
* Loop 12: rev(A)->  rev(A')
                  [A>=A'+1,A'>=1] 
* Loop 13: rev(A)->  rev(A')
                  [A>=2,A=A'+1] 
* Loop 14: rev(A)->  rev(A')
                  [A>=2,A=A'+1] 
* Loop 15: rev(A) [A=1] 

### Ranking functions of CR rev(A) 
* RF of phase [11,12,13,14]: [A-1]

#### Partial ranking functions of CR rev(A) 
* Partial RF of phase [11,12,13,14]:
  - RF of loop [11:1,12:1,13:1,14:1]:
    A-1


### Resulting Chains:rev(A) 
* [[11,12,13,14],15]
* [15]


### Specialization of cost equations case_1/1 
* CE 2 is refined into CE [16,17,18,19] 
* CE 1 is refined into CE [20,21,22,23] 
* CE 3 is refined into CE [24] 


#### Refined cost equations case_1/1 
* CE 16: case_1(A) = 6+ rev(B):[[11,12,13,14],15]+ append(C,D):[[10],9]
     [A>=B+1,D>=A,C>=2,B>=2] 
* CE 17: case_1(A) = 6+ rev(B):[[11,12,13,14],15]+ append(C,D):[9]
     [A>=B+1,D>=A,B>=2,C=1] 
* CE 18: case_1(A) = 6+ rev(B):[15]+ append(C,D):[[10],9]
     [D>=A,C>=2,A>=2,B=1] 
* CE 19: case_1(A) = 6+ rev(B):[15]+ append(C,D):[9]
     [D>=A,A>=2,C=1,B=1] 
* CE 20: case_1(A) = 6+ rev(B):[[11,12,13,14],15]+ append(C,D):[[10],9]
     [D>=2,C>=2,B>=2,B+1=A] 
* CE 21: case_1(A) = 6+ rev(B):[[11,12,13,14],15]+ append(C,D):[9]
     [D>=2,B>=2,B+1=A,C=1] 
* CE 22: case_1(A) = 6+ rev(B):[15]+ append(C,D):[[10],9]
     [D>=2,C>=2,B=1,A=2] 
* CE 23: case_1(A) = 6+ rev(B):[15]+ append(C,D):[9]
     [D>=2,C=1,B=1,A=2] 
* CE 24: case_1(A) = 2
     [A=1] 

### Cost equations --> "Loop" of case_1/1 
* CEs [21] --> Loop 16 
* CEs [20] --> Loop 17 
* CEs [17] --> Loop 18 
* CEs [16] --> Loop 19 
* CEs [19] --> Loop 20 
* CEs [18] --> Loop 21 
* CEs [23] --> Loop 22 
* CEs [22] --> Loop 23 
* CEs [24] --> Loop 24 

#### Loops of case_1/1 
* Loop 16: case_1(A) [A>=3] 
* Loop 17: case_1(A) [A>=3] 
* Loop 18: case_1(A) [A>=3] 
* Loop 19: case_1(A) [A>=3] 
* Loop 20: case_1(A) [A>=2] 
* Loop 21: case_1(A) [A>=2] 
* Loop 22: case_1(A) [A=2] 
* Loop 23: case_1(A) [A=2] 
* Loop 24: 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) 
* [24]
* [23]
* [22]
* [21]
* [20]
* [19]
* [18]
* [17]
* [16]


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

#### Cost of loops [10] 

 * loop 10:append(A,B) -> [append(A',B')] 
5
#### Cost of phase [10]:append(A,B) -> [append(A',B')] 
5*it(10)+0
  Such that:it(10) =< A-1
it(10) =< A-A'

#### Cost of chains of append(A,B):
* Chain [[10],9]: 5*it(10)+2
  Such that:it(10) =< A-1

  with precondition: [A>=2,B>=2] 

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


#### Cost of loops [11,12,13,14] 

 * loop 11:rev(A) -> [rev(A')] 
9
 * loop 12:rev(A) -> [rev(A')] 
5*s(2)+9
 * loop 13:rev(A) -> [rev(A')] 
9
 * loop 14:rev(A) -> [rev(A')] 
5*s(4)+9
#### Cost of phase [11,12,13,14]:rev(A) -> [rev(A')] 
9*it(11)+9*it(12)+9*it(13)+9*it(14)+10*s(5)+0
  Such that:it(11)+it(12)+it(13)+it(14) =< A-1
it(11)+it(12)+it(13)+it(14) =< A-A'

#### Cost of chains of rev(A):
* Chain [[11,12,13,14],15]: 9*it(11)+9*it(12)+9*it(13)+9*it(14)+10*s(5)+3
  Such that:it(11)+it(12)+it(13)+it(14) =< A-1

  with precondition: [A>=2] 

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


#### Cost of chains of case_1(A):
* Chain [24]: 2
  with precondition: [A=1] 

* Chain [23]: 5*s(7)+11
  with precondition: [A=2] 

* Chain [22]: 11
  with precondition: [A=2] 

* Chain [21]: 5*s(8)+11
  with precondition: [A>=2] 

* Chain [20]: 11
  with precondition: [A>=2] 

* Chain [19]: 9*s(9)+9*s(10)+9*s(11)+9*s(12)+15*s(13)+11
  Such that:s(9)+s(10)+s(11)+s(12) =< A-2

  with precondition: [A>=3] 

* Chain [18]: 9*s(15)+9*s(16)+9*s(17)+9*s(18)+10*s(19)+11
  Such that:s(15)+s(16)+s(17)+s(18) =< A-2

  with precondition: [A>=3] 

* Chain [17]: 9*s(20)+9*s(21)+9*s(22)+9*s(23)+15*s(24)+11
  Such that:s(20)+s(21)+s(22)+s(23) =< A-2

  with precondition: [A>=3] 

* Chain [16]: 9*s(26)+9*s(27)+9*s(28)+9*s(29)+10*s(30)+11
  Such that:s(26)+s(27)+s(28)+s(29) =< A-2

  with precondition: [A>=3] 


Closed-form bounds of case_1(A): 
-------------------------------------
* Chain [24] with precondition: [A=1] 
    - Lower bound: 2 
    - Complexity: constant
 * Chain [23] with precondition: [A=2] 
    - Lower bound: 11 
    - Complexity: constant
 * Chain [22] with precondition: [A=2] 
    - Lower bound: 11 
    - Complexity: constant
 * Chain [21] with precondition: [A>=2] 
    - Lower bound: 11 
    - Complexity: constant
 * Chain [20] with precondition: [A>=2] 
    - Lower bound: 11 
    - Complexity: constant
 * Chain [19] with precondition: [A>=3] 
    - Lower bound: 11 
    - Complexity: constant
 * Chain [18] with precondition: [A>=3] 
    - Lower bound: 11 
    - Complexity: constant
 * Chain [17] with precondition: [A>=3] 
    - Lower bound: 11 
    - Complexity: constant
 * Chain [16] with precondition: [A>=3] 
    - Lower bound: 11 
    - Complexity: constant
 
### Partitioned lower bound of case_1(A): 
* 2 
 if [A=1]
* 11 
 if [A>=2]
Possible lower bounds : [2,11]
Maximum lower bound complexity: constant
* Total analysis performed in 53 ms.