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 0 ms.
sabu_memo_table_1(case_0,[A,B],[1*B=1,1*A=1],0,0)
sabu_memo_table_1(case_1,[A,B],[1*B=0,1*A=1],0,0)
sabu_memo_table_1(even,[A,B],[1*A=1,1*B=1],0,0)
sabu_memo_table_1(odd,[A,B],[1*A=1,1*B=0],0,0)
sabu_memo_table_1(case_0,[A,B],[1*B>=0,-1*B>= -1,1*A+1*B=2],1,1)
sabu_memo_table_1(case_1,[A,B],[-1*B>= -1,1*B>=0,1*A+ -1*B=1],1,1)
sabu_memo_table_1(even,[A,B],[1*B>=0,-1*B>= -1,1*A+1*B=2],2,1)
sabu_memo_table_1(odd,[A,B],[-1*B>= -1,1*B>=0,1*A+ -1*B=1],2,1)
sabu_memo_table_1(case_0,[A,B],[-1*A+1*B>= -2,-1*B>= -1,1*A+1*B>=2],3,2)
sabu_memo_table_1(case_1,[A,B],[1*B>=0,-1*A+ -1*B>= -3,1*A+ -1*B>=1],3,2)
sabu_memo_table_1(even,[A,B],[-1*A+1*B>= -2,-1*B>= -1,1*A+1*B>=2],4,2)
sabu_memo_table_1(odd,[A,B],[1*B>=0,-1*A+ -1*B>= -3,1*A+ -1*B>=1],4,2)
sabu_memo_table_1(case_0,[A,B],[1*B>=0,-1*A+ -1*B>= -4,-1*B>= -1,1*A+1*B>=2],5,3)
sabu_memo_table_1(case_1,[A,B],[-1*A+1*B>= -3,-1*B>= -1,1*A+ -1*B>=1,1*B>=0],5,3)
sabu_memo_table_1(even,[A,B],[1*B>=0,-1*A+ -1*B>= -4,-1*B>= -1,1*A+1*B>=2],6,3)
sabu_memo_table_1(odd,[A,B],[-1*A+1*B>= -3,-1*B>= -1,1*A+ -1*B>=1,1*B>=0],6,3)
sabu_memo_table_1(case_0,[A,B],[-1*B>= -1,1*B>=0,1*A+1*B>=2],7,0)
sabu_memo_table_1(case_1,[A,B],[1*B>=0,-1*B>= -1,1*A+ -1*B>=1],7,0)
sabu_memo_table_1(even,[A,B],[1*B>=0,-1*B>= -1,1*A+1*B>=2],8,0)
sabu_memo_table_1(odd,[A,B],[1*B>=0,-1*B>= -1,1*A+ -1*B>=1],8,0)
sabu_memo_table_1(start,[A,B],[1*A+1*B>=2,-1*B>= -1,1*B>=0],0,0)
sabu_memo_table_1(start,[A,B],[],0,1)
:- dynamic sabu_memo_table_1/5.

sabu_memo_table_1(case_0, [B, A], [-1*A>= -1, 1*A>=0, 1*B+1*A>=2], 7, 0).
sabu_memo_table_1(case_1, [B, A], [1*A>=0, -1*A>= -1, 1*B+ -1*A>=1], 7, 0).
sabu_memo_table_1(even, [B, A], [1*A>=0, -1*A>= -1, 1*B+1*A>=2], 8, 0).
sabu_memo_table_1(odd, [B, A], [1*A>=0, -1*A>= -1, 1*B+ -1*A>=1], 8, 0).
sabu_memo_table_1(start, [_, _], [], 0, 1).


Size analysis performed in 6 ms.

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

Generated 30 equations 

Cost relation system solved by PUBS in 8 ms.

Method start terminates?: YES

UB for start(x) = nat(x)


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

#### Computed strongly connected components 
0. recursive  : [case_0/1,case_1/1,even/1,odd/1]
1. 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 even/1
1. SCC is partially evaluated into start/1

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

### Specialization of cost equations even/1 
* CE 5 is refined into CE [6] 
* CE 3 is refined into CE [7] 
* CE 4 is refined into CE [8] 


#### Refined cost equations even/1 
* CE 6: even(A) = 7
     [A=2] 
* CE 7: even(A) = 3
     [A=1] 
* CE 8: even(A) = 8+ even(B)
     [A>=3,A=B+2] 

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

#### Loops of even/1 
* Loop 6: even(A)->  even(A')
                  [A>=3,A=A'+2] 
* Loop 7: even(A) [A=2] 
* Loop 8: even(A) [A=1] 

### Ranking functions of CR even(A) 
* RF of phase [6]: [A/2-1]

#### Partial ranking functions of CR even(A) 
* Partial RF of phase [6]:
  - RF of loop [6:1]:
    A/2-1


### Resulting Chains:even(A) 
* [[6],8]
* [[6],7]
* [8]
* [7]


### Specialization of cost equations start/1 
* CE 2 is refined into CE [9,10,11,12] 
* CE 1 is refined into CE [13] 


#### Refined cost equations start/1 
* CE 9: start(A) = 1+ even(A):[[6],8]
     [A>=3] 
* CE 10: start(A) = 1+ even(A):[[6],7]
     [A>=4] 
* CE 11: start(A) = 1+ even(B):[8]
     [B=1,A=1] 
* CE 12: start(A) = 1+ even(B):[7]
     [B=2,A=2] 
* CE 13: start(A) = 1
     [] 

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

#### Loops of start/1 
* Loop 9: start(A) [A>=4] 
* Loop 10: start(A) [A>=3] 
* Loop 11: start(A) [A=2] 
* Loop 12: start(A) [A=1] 
* Loop 13: start(A) [] 

### Ranking functions of CR start(A) 

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


### Resulting Chains:start(A) 
* [13]
* [12]
* [11]
* [10]
* [9]


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

#### Cost of loops [6] 

 * loop 6:even(A) -> [even(A')] 
8
#### Cost of phase [6]:even(A) -> [even(A')] 
8*it(6)+0
  Such that:it(6) =< A/2-1
it(6) =< A/2-A'/2
it(6) >= A/2-A'/2

#### Cost of phase [6]:even(A) -> [even(A')] 
8*it(6)+0
  Such that:it(6) =< A/2-1
it(6) =< A/2-A'/2
it(6) >= A/2-A'/2

#### Cost of chains of even(A):
* Chain [[6],8]: 8*it(6)+3
  Such that:it(6) =< A/2-1
it(6) >= A/2-1/2

  with precondition: [A>=3] 

* Chain [[6],7]: 8*it(6)+7
  Such that:it(6) =< A/2-1
it(6) >= A/2-1

  with precondition: [A>=4] 

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

* Chain [7]: 7
  with precondition: [A=2] 


#### Cost of chains of start(A):
* Chain [13]: 1
  with precondition: [] 

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

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

* Chain [10]: 8*s(1)+4
  Such that:s(1) =< A/2-1
s(1) >= A/2-1/2

  with precondition: [A>=3] 

* Chain [9]: 8*s(2)+8
  Such that:s(2) =< A/2-1
s(2) >= A/2-1

  with precondition: [A>=4] 


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