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
Size abstraction not supported for native

Abstract compilation performed in 1 ms.
sabu_memo_table_1(truncate,[],[],0,0)
sabu_memo_table_1(case_0,[A],[1*A>=0,1*A=1],0,0)
sabu_memo_table_1(eval,[A],[1*A>=0,1*A=1,1*A>=0],0,0)
sabu_memo_table_1(case_0,[A],[-1*A>= -3,1*A>=1],1,1)
sabu_memo_table_1(eval,[A],[-1*A>= -3,1*A>=1],2,1)
sabu_memo_table_1(case_0,[A],[-1*A>= -7,1*A>=1],3,2)
sabu_memo_table_1(eval,[A],[-1*A>= -7,1*A>=1],4,2)
sabu_memo_table_1(case_0,[A],[-1*A>= -15,1*A>=1],5,3)
sabu_memo_table_1(eval,[A],[-1*A>= -15,1*A>=1],6,3)
sabu_memo_table_1(case_0,[A],[1*A>=1],7,0)
sabu_memo_table_1(eval,[A],[1*A>=1],8,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(truncate, [], [], 0, 0).
sabu_memo_table_1(case_0, [A], [1*A>=1], 7, 0).
sabu_memo_table_1(eval, [A], [1*A>=1], 8, 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 3 ms.

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

Generated 30 equations 

Cost relation system solved by PUBS in 14 ms.

Method start terminates?: YES

 - e_1: size of e wrt. Exp
UB for start(e_1) = pow(2,nat(e_1))


Method start terminates?: YES

 - e_1: size of e wrt. Exp
UB for start(e_1) = pow(2,nat(e_1))


Method start terminates?: YES

UB for start(e_1) = pow(2,nat(e_1))


Method start terminates?: YES

UB for start(e_1) = pow(2,nat(e_1))


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

#### Computed strongly connected components 
0. non_recursive  : [truncate/0]
1. recursive [non_tail,multiple] : [case_0/1,eval/1]
3. non_recursive  : [start/1]
* The entry case_0/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 completely evaluated into other SCCs
1. SCC is partially evaluated into eval/1
3. SCC is partially evaluated into case_0/1

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

### Specialization of cost equations eval/1 
* CE 8 is refined into CE [9] 
* CE 5 is refined into CE [10] 
* CE 7 is refined into CE [11] 
* CE 6 is refined into CE [12] 


#### Refined cost equations eval/1 
* CE 9: eval(A) = 5
     [A=1] 
* CE 10: eval(A) = 9+ eval(B)+ eval(C)
     [C>=1,B>=1,B+C+1=A] 
* CE 11: eval(A) = 5+ eval(B)+ eval(C)
     [C>=0,B>=1,B+C+1=A] 
* CE 12: eval(A) = 6+ eval(B)+ eval(C)
     [C>=0,B>=1,B+C+1=A] 

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

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

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

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


### Resulting Chains:eval(A) 
* [12]
* [multiple([9,10,11],[[12]])]


### Specialization of cost equations case_0/1 
* CE 1 is refined into CE [13,14,15,16] 
* CE 3 is refined into CE [17,18,19,20] 
* CE 2 is refined into CE [21,22,23,24] 
* CE 4 is refined into CE [25] 


#### Refined cost equations case_0/1 
* CE 13: case_0(A) = 8+ eval(B):[12]+ eval(C):[12]
     [C=1,B=1,A=3] 
* CE 14: case_0(A) = 8+ eval(B):[12]+ eval(C):[multiple([9,10,11],[[12]])]
     [C>=3,C+2=A,B=1] 
* CE 15: case_0(A) = 8+ eval(B):[multiple([9,10,11],[[12]])]+ eval(C):[12]
     [B>=3,B+2=A,C=1] 
* CE 16: case_0(A) = 8+ eval(B):[multiple([9,10,11],[[12]])]+ eval(C):[multiple([9,10,11],[[12]])]
     [C>=3,B>=3,B+C+1=A] 
* CE 17: case_0(A) = 4+ eval(B):[12]+ eval(C):[12]
     [C=1,B=1,A=3] 
* CE 18: case_0(A) = 4+ eval(B):[12]+ eval(C):[multiple([9,10,11],[[12]])]
     [C>=3,C+2=A,B=1] 
* CE 19: case_0(A) = 4+ eval(B):[multiple([9,10,11],[[12]])]+ eval(C):[12]
     [B>=3,B+2=A,C=1] 
* CE 20: case_0(A) = 4+ eval(B):[multiple([9,10,11],[[12]])]+ eval(C):[multiple([9,10,11],[[12]])]
     [C>=3,B>=3,B+C+1=A] 
* CE 21: case_0(A) = 5+ eval(B):[12]+ eval(C):[12]
     [C=1,B=1,A=3] 
* CE 22: case_0(A) = 5+ eval(B):[12]+ eval(C):[multiple([9,10,11],[[12]])]
     [C>=3,C+2=A,B=1] 
* CE 23: case_0(A) = 5+ eval(B):[multiple([9,10,11],[[12]])]+ eval(C):[12]
     [B>=3,B+2=A,C=1] 
* CE 24: case_0(A) = 5+ eval(B):[multiple([9,10,11],[[12]])]+ eval(C):[multiple([9,10,11],[[12]])]
     [C>=3,B>=3,B+C+1=A] 
* CE 25: case_0(A) = 4
     [A=1] 

### Cost equations --> "Loop" of case_0/1 
* CEs [24] --> Loop 13 
* CEs [20] --> Loop 14 
* CEs [16] --> Loop 15 
* CEs [23] --> Loop 16 
* CEs [22] --> Loop 17 
* CEs [19] --> Loop 18 
* CEs [18] --> Loop 19 
* CEs [15] --> Loop 20 
* CEs [14] --> Loop 21 
* CEs [21] --> Loop 22 
* CEs [17] --> Loop 23 
* CEs [13] --> Loop 24 
* CEs [25] --> Loop 25 

#### Loops of case_0/1 
* Loop 13: case_0(A) [A>=7] 
* Loop 14: case_0(A) [A>=7] 
* Loop 15: case_0(A) [A>=7] 
* Loop 16: case_0(A) [A>=5] 
* Loop 17: case_0(A) [A>=5] 
* Loop 18: case_0(A) [A>=5] 
* Loop 19: case_0(A) [A>=5] 
* Loop 20: case_0(A) [A>=5] 
* Loop 21: case_0(A) [A>=5] 
* Loop 22: case_0(A) [A=3] 
* Loop 23: case_0(A) [A=3] 
* Loop 24: case_0(A) [A=3] 
* Loop 25: case_0(A) [A=1] 

### Ranking functions of CR case_0(A) 

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


### Resulting Chains:case_0(A) 
* [25]
* [24]
* [23]
* [22]
* [21]
* [20]
* [19]
* [18]
* [17]
* [16]
* [15]
* [14]
* [13]


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

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

 * loop 9:eval(A) -> [eval(A'),eval(A'2)] 
9
 * loop 10:eval(A) -> [eval(A'),eval(A'2)] 
6
 * loop 11:eval(A) -> [eval(A'),eval(A'2)] 
5
#### Cost of phase [9,10,11]:eval(A) -> [] 
9*it(9)+6*it(10)+5*it(11)+5*it([12])+0
  Such that:it(9)+it(10)+it(11) =< A/2-1/2
it([12]) =< A/2+1/2
it(9)+it(10)+it(11)+it([12]) >= A

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

* Chain [multiple([9,10,11],[[12]])]: 9*it(9)+6*it(10)+5*it(11)+5*it([12])+0
  Such that:it(9)+it(10)+it(11) =< A/2-1/2
it([12]) =< A/2+1/2
it(9)+it(10)+it(11)+it([12]) >= A

  with precondition: [A>=3] 


#### Cost of chains of case_0(A):
* Chain [25]: 4
  with precondition: [A=1] 

* Chain [24]: 18
  with precondition: [A=3] 

* Chain [23]: 14
  with precondition: [A=3] 

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

* Chain [21]: 9*s(1)+6*s(2)+5*s(3)+5*s(4)+13
  Such that:s(1)+s(2)+s(3) =< A/2-3/2
s(4) =< A/2-1/2
s(1)+s(2)+s(3)+s(4) >= A-2

  with precondition: [A>=5] 

* Chain [20]: 9*s(5)+6*s(6)+5*s(7)+5*s(8)+13
  Such that:s(5)+s(6)+s(7) =< A/2-3/2
s(8) =< A/2-1/2
s(5)+s(6)+s(7)+s(8) >= A-2

  with precondition: [A>=5] 

* Chain [19]: 9*s(9)+6*s(10)+5*s(11)+5*s(12)+9
  Such that:s(9)+s(10)+s(11) =< A/2-3/2
s(12) =< A/2-1/2
s(9)+s(10)+s(11)+s(12) >= A-2

  with precondition: [A>=5] 

* Chain [18]: 9*s(13)+6*s(14)+5*s(15)+5*s(16)+9
  Such that:s(13)+s(14)+s(15) =< A/2-3/2
s(16) =< A/2-1/2
s(13)+s(14)+s(15)+s(16) >= A-2

  with precondition: [A>=5] 

* Chain [17]: 9*s(17)+6*s(18)+5*s(19)+5*s(20)+10
  Such that:s(17)+s(18)+s(19) =< A/2-3/2
s(20) =< A/2-1/2
s(17)+s(18)+s(19)+s(20) >= A-2

  with precondition: [A>=5] 

* Chain [16]: 9*s(21)+6*s(22)+5*s(23)+5*s(24)+10
  Such that:s(21)+s(22)+s(23) =< A/2-3/2
s(24) =< A/2-1/2
s(21)+s(22)+s(23)+s(24) >= A-2

  with precondition: [A>=5] 

* Chain [15]: 9*s(25)+6*s(26)+5*s(27)+5*s(28)+9*s(29)+6*s(30)+5*s(31)+5*s(32)+8
  Such that:s(25)+s(26)+s(27)+s(29)+s(30)+s(31) =< A/2-3/2
aux(1) =< A/2-1/2
s(28) =< aux(1)
s(32) =< aux(1)
s(25)+s(26)+s(27)+s(28)+s(29)+s(30)+s(31)+s(32) >= A-1

  with precondition: [A>=7] 

* Chain [14]: 9*s(33)+6*s(34)+5*s(35)+5*s(36)+9*s(37)+6*s(38)+5*s(39)+5*s(40)+4
  Such that:s(33)+s(34)+s(35)+s(37)+s(38)+s(39) =< A/2-3/2
aux(2) =< A/2-1/2
s(36) =< aux(2)
s(40) =< aux(2)
s(33)+s(34)+s(35)+s(36)+s(37)+s(38)+s(39)+s(40) >= A-1

  with precondition: [A>=7] 

* Chain [13]: 9*s(41)+6*s(42)+5*s(43)+5*s(44)+9*s(45)+6*s(46)+5*s(47)+5*s(48)+5
  Such that:s(41)+s(42)+s(43)+s(45)+s(46)+s(47) =< A/2-3/2
aux(3) =< A/2-1/2
s(44) =< aux(3)
s(48) =< aux(3)
s(41)+s(42)+s(43)+s(44)+s(45)+s(46)+s(47)+s(48) >= A-1

  with precondition: [A>=7] 


Closed-form bounds of case_0(A): 
-------------------------------------
* Chain [25] with precondition: [A=1] 
    - Lower bound: 4 
    - Complexity: constant
 * Chain [24] with precondition: [A=3] 
    - Lower bound: 18 
    - Complexity: constant
 * Chain [23] with precondition: [A=3] 
    - Lower bound: 14 
    - Complexity: constant
 * Chain [22] with precondition: [A=3] 
    - Lower bound: 15 
    - Complexity: constant
 * Chain [21] with precondition: [A>=5] 
    - Lower bound: 5*A+3 
    - Complexity: n
 * Chain [20] with precondition: [A>=5] 
    - Lower bound: 5*A+3 
    - Complexity: n
 * Chain [19] with precondition: [A>=5] 
    - Lower bound: 5*A-1 
    - Complexity: n
 * Chain [18] with precondition: [A>=5] 
    - Lower bound: 5*A-1 
    - Complexity: n
 * Chain [17] with precondition: [A>=5] 
    - Lower bound: 5*A 
    - Complexity: n
 * Chain [16] with precondition: [A>=5] 
    - Lower bound: 5*A 
    - Complexity: n
 * Chain [15] with precondition: [A>=7] 
    - Lower bound: 5*A+3 
    - Complexity: n
 * Chain [14] with precondition: [A>=7] 
    - Lower bound: 5*A-1 
    - Complexity: n
 * Chain [13] with precondition: [A>=7] 
    - Lower bound: 5*A 
    - Complexity: n
 
### Partitioned lower bound of case_0(A): 
* 4 
 if [A=1]
* 14 
 if [A=3]
* 5*A-1 
 if [A>=5]
Possible lower bounds : [4,14,5*A-1]
Maximum lower bound complexity: n
* Total analysis performed in 77 ms.