WORST_CASE(?,O(n^2)) proof of input_o3a9YGu4n1.trs # AProVE Commit ID: aff8ecad908e01718a4c36e68d2e55d5e0f16e15 fuhs 20220216 unpublished The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^2). (0) CpxTRS (1) RelTrsToWeightedTrsProof [UPPER BOUND(ID), 0 ms] (2) CpxWeightedTrs (3) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms] (4) CpxTypedWeightedTrs (5) CompletionProof [UPPER BOUND(ID), 0 ms] (6) CpxTypedWeightedCompleteTrs (7) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms] (8) CpxRNTS (9) CompleteCoflocoProof [FINISHED, 921 ms] (10) BOUNDS(1, n^2) ---------------------------------------- (0) Obligation: The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^2). The TRS R consists of the following rules: if(true, t, e) -> t if(false, t, e) -> e member(x, nil) -> false member(x, cons(y, ys)) -> if(eq(x, y), true, member(x, ys)) eq(nil, nil) -> true eq(O(x), 0(y)) -> eq(x, y) eq(0(x), 1(y)) -> false eq(1(x), 0(y)) -> false eq(1(x), 1(y)) -> eq(x, y) negate(0(x)) -> 1(x) negate(1(x)) -> 0(x) choice(cons(x, xs)) -> x choice(cons(x, xs)) -> choice(xs) guess(nil) -> nil guess(cons(clause, cnf)) -> cons(choice(clause), guess(cnf)) verify(nil) -> true verify(cons(l, ls)) -> if(member(negate(l), ls), false, verify(ls)) sat(cnf) -> satck(cnf, guess(cnf)) satck(cnf, assign) -> if(verify(assign), assign, unsat) S is empty. Rewrite Strategy: PARALLEL_INNERMOST ---------------------------------------- (1) RelTrsToWeightedTrsProof (UPPER BOUND(ID)) Transformed relative TRS to weighted TRS ---------------------------------------- (2) Obligation: The Runtime Complexity (innermost) of the given CpxWeightedTrs could be proven to be BOUNDS(1, n^2). The TRS R consists of the following rules: if(true, t, e) -> t [1] if(false, t, e) -> e [1] member(x, nil) -> false [1] member(x, cons(y, ys)) -> if(eq(x, y), true, member(x, ys)) [1] eq(nil, nil) -> true [1] eq(O(x), 0(y)) -> eq(x, y) [1] eq(0(x), 1(y)) -> false [1] eq(1(x), 0(y)) -> false [1] eq(1(x), 1(y)) -> eq(x, y) [1] negate(0(x)) -> 1(x) [1] negate(1(x)) -> 0(x) [1] choice(cons(x, xs)) -> x [1] choice(cons(x, xs)) -> choice(xs) [1] guess(nil) -> nil [1] guess(cons(clause, cnf)) -> cons(choice(clause), guess(cnf)) [1] verify(nil) -> true [1] verify(cons(l, ls)) -> if(member(negate(l), ls), false, verify(ls)) [1] sat(cnf) -> satck(cnf, guess(cnf)) [1] satck(cnf, assign) -> if(verify(assign), assign, unsat) [1] Rewrite Strategy: INNERMOST ---------------------------------------- (3) TypeInferenceProof (BOTH BOUNDS(ID, ID)) Infered types. ---------------------------------------- (4) Obligation: Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: if(true, t, e) -> t [1] if(false, t, e) -> e [1] member(x, nil) -> false [1] member(x, cons(y, ys)) -> if(eq(x, y), true, member(x, ys)) [1] eq(nil, nil) -> true [1] eq(O(x), 0(y)) -> eq(x, y) [1] eq(0(x), 1(y)) -> false [1] eq(1(x), 0(y)) -> false [1] eq(1(x), 1(y)) -> eq(x, y) [1] negate(0(x)) -> 1(x) [1] negate(1(x)) -> 0(x) [1] choice(cons(x, xs)) -> x [1] choice(cons(x, xs)) -> choice(xs) [1] guess(nil) -> nil [1] guess(cons(clause, cnf)) -> cons(choice(clause), guess(cnf)) [1] verify(nil) -> true [1] verify(cons(l, ls)) -> if(member(negate(l), ls), false, verify(ls)) [1] sat(cnf) -> satck(cnf, guess(cnf)) [1] satck(cnf, assign) -> if(verify(assign), assign, unsat) [1] The TRS has the following type information: if :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat true :: true:false:nil:cons:O:0:1:unsat false :: true:false:nil:cons:O:0:1:unsat member :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat nil :: true:false:nil:cons:O:0:1:unsat cons :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat eq :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat O :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat 0 :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat 1 :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat negate :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat choice :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat guess :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat verify :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat sat :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat satck :: true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat -> true:false:nil:cons:O:0:1:unsat unsat :: true:false:nil:cons:O:0:1:unsat Rewrite Strategy: INNERMOST ---------------------------------------- (5) CompletionProof (UPPER BOUND(ID)) The TRS is a completely defined constructor system, as every type has a constant constructor and the following rules were added: if(v0, v1, v2) -> null_if [0] member(v0, v1) -> null_member [0] eq(v0, v1) -> null_eq [0] negate(v0) -> null_negate [0] choice(v0) -> null_choice [0] guess(v0) -> null_guess [0] verify(v0) -> null_verify [0] And the following fresh constants: null_if, null_member, null_eq, null_negate, null_choice, null_guess, null_verify ---------------------------------------- (6) Obligation: Runtime Complexity Weighted TRS where all functions are completely defined. The underlying TRS is: Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: if(true, t, e) -> t [1] if(false, t, e) -> e [1] member(x, nil) -> false [1] member(x, cons(y, ys)) -> if(eq(x, y), true, member(x, ys)) [1] eq(nil, nil) -> true [1] eq(O(x), 0(y)) -> eq(x, y) [1] eq(0(x), 1(y)) -> false [1] eq(1(x), 0(y)) -> false [1] eq(1(x), 1(y)) -> eq(x, y) [1] negate(0(x)) -> 1(x) [1] negate(1(x)) -> 0(x) [1] choice(cons(x, xs)) -> x [1] choice(cons(x, xs)) -> choice(xs) [1] guess(nil) -> nil [1] guess(cons(clause, cnf)) -> cons(choice(clause), guess(cnf)) [1] verify(nil) -> true [1] verify(cons(l, ls)) -> if(member(negate(l), ls), false, verify(ls)) [1] sat(cnf) -> satck(cnf, guess(cnf)) [1] satck(cnf, assign) -> if(verify(assign), assign, unsat) [1] if(v0, v1, v2) -> null_if [0] member(v0, v1) -> null_member [0] eq(v0, v1) -> null_eq [0] negate(v0) -> null_negate [0] choice(v0) -> null_choice [0] guess(v0) -> null_guess [0] verify(v0) -> null_verify [0] The TRS has the following type information: if :: true:false:nil:cons:O:0:1:unsat:null_if:null_member:null_eq:null_negate:null_choice:null_guess:null_verify -> true:false:nil:cons:O:0:1:unsat:null_if:null_member:null_eq:null_negate:null_choice:null_guess:null_verify -> true:false:nil:cons:O:0:1:unsat:null_if:null_member:null_eq:null_negate:null_choice:null_guess:null_verify -> true:false:nil:cons:O:0:1:unsat:null_if:null_member:null_eq:null_negate:null_choice:null_guess:null_verify true :: true:false:nil:cons:O:0:1:unsat:null_if:null_member:null_eq:null_negate:null_choice:null_guess:null_verify false :: true:false:nil:cons:O:0:1:unsat:null_if:null_member:null_eq:null_negate:null_choice:null_guess:null_verify member :: true:false:nil:cons:O:0:1:unsat:null_if:null_member:null_eq:null_negate:null_choice:null_guess:null_verify -> true:false:nil:cons:O:0:1:unsat:null_if:null_member:null_eq:null_negate:null_choice:null_guess:null_verify -> true:false:nil:cons:O:0:1:unsat:null_if:null_member:null_eq:null_negate:null_choice:null_guess:null_verify nil :: true:false:nil:cons:O:0:1:unsat:null_if:null_member:null_eq:null_negate:null_choice:null_guess:null_verify cons :: true:false:nil:cons:O:0:1:unsat:null_if:null_member:null_eq:null_negate:null_choice:null_guess:null_verify -> true:false:nil:cons:O:0:1:unsat:null_if:null_member:null_eq:null_negate:null_choice:null_guess:null_verify -> true:false:nil:cons:O:0:1:unsat:null_if:null_member:null_eq:null_negate:null_choice:null_guess:null_verify eq :: true:false:nil:cons:O:0:1:unsat:null_if:null_member:null_eq:null_negate:null_choice:null_guess:null_verify -> true:false:nil:cons:O:0:1:unsat:null_if:null_member:null_eq:null_negate:null_choice:null_guess:null_verify -> true:false:nil:cons:O:0:1:unsat:null_if:null_member:null_eq:null_negate:null_choice:null_guess:null_verify O :: true:false:nil:cons:O:0:1:unsat:null_if:null_member:null_eq:null_negate:null_choice:null_guess:null_verify -> true:false:nil:cons:O:0:1:unsat:null_if:null_member:null_eq:null_negate:null_choice:null_guess:null_verify 0 :: true:false:nil:cons:O:0:1:unsat:null_if:null_member:null_eq:null_negate:null_choice:null_guess:null_verify -> true:false:nil:cons:O:0:1:unsat:null_if:null_member:null_eq:null_negate:null_choice:null_guess:null_verify 1 :: true:false:nil:cons:O:0:1:unsat:null_if:null_member:null_eq:null_negate:null_choice:null_guess:null_verify -> true:false:nil:cons:O:0:1:unsat:null_if:null_member:null_eq:null_negate:null_choice:null_guess:null_verify negate :: true:false:nil:cons:O:0:1:unsat:null_if:null_member:null_eq:null_negate:null_choice:null_guess:null_verify -> true:false:nil:cons:O:0:1:unsat:null_if:null_member:null_eq:null_negate:null_choice:null_guess:null_verify choice :: true:false:nil:cons:O:0:1:unsat:null_if:null_member:null_eq:null_negate:null_choice:null_guess:null_verify -> true:false:nil:cons:O:0:1:unsat:null_if:null_member:null_eq:null_negate:null_choice:null_guess:null_verify guess :: true:false:nil:cons:O:0:1:unsat:null_if:null_member:null_eq:null_negate:null_choice:null_guess:null_verify -> true:false:nil:cons:O:0:1:unsat:null_if:null_member:null_eq:null_negate:null_choice:null_guess:null_verify verify :: true:false:nil:cons:O:0:1:unsat:null_if:null_member:null_eq:null_negate:null_choice:null_guess:null_verify -> true:false:nil:cons:O:0:1:unsat:null_if:null_member:null_eq:null_negate:null_choice:null_guess:null_verify sat :: true:false:nil:cons:O:0:1:unsat:null_if:null_member:null_eq:null_negate:null_choice:null_guess:null_verify -> true:false:nil:cons:O:0:1:unsat:null_if:null_member:null_eq:null_negate:null_choice:null_guess:null_verify satck :: true:false:nil:cons:O:0:1:unsat:null_if:null_member:null_eq:null_negate:null_choice:null_guess:null_verify -> true:false:nil:cons:O:0:1:unsat:null_if:null_member:null_eq:null_negate:null_choice:null_guess:null_verify -> true:false:nil:cons:O:0:1:unsat:null_if:null_member:null_eq:null_negate:null_choice:null_guess:null_verify unsat :: true:false:nil:cons:O:0:1:unsat:null_if:null_member:null_eq:null_negate:null_choice:null_guess:null_verify null_if :: true:false:nil:cons:O:0:1:unsat:null_if:null_member:null_eq:null_negate:null_choice:null_guess:null_verify null_member :: true:false:nil:cons:O:0:1:unsat:null_if:null_member:null_eq:null_negate:null_choice:null_guess:null_verify null_eq :: true:false:nil:cons:O:0:1:unsat:null_if:null_member:null_eq:null_negate:null_choice:null_guess:null_verify null_negate :: true:false:nil:cons:O:0:1:unsat:null_if:null_member:null_eq:null_negate:null_choice:null_guess:null_verify null_choice :: true:false:nil:cons:O:0:1:unsat:null_if:null_member:null_eq:null_negate:null_choice:null_guess:null_verify null_guess :: true:false:nil:cons:O:0:1:unsat:null_if:null_member:null_eq:null_negate:null_choice:null_guess:null_verify null_verify :: true:false:nil:cons:O:0:1:unsat:null_if:null_member:null_eq:null_negate:null_choice:null_guess:null_verify Rewrite Strategy: INNERMOST ---------------------------------------- (7) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID)) Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction. The constant constructors are abstracted as follows: true => 2 false => 0 nil => 1 unsat => 3 null_if => 0 null_member => 0 null_eq => 0 null_negate => 0 null_choice => 0 null_guess => 0 null_verify => 0 ---------------------------------------- (8) Obligation: Complexity RNTS consisting of the following rules: choice(z) -{ 1 }-> x :|: z = 1 + x + xs, xs >= 0, x >= 0 choice(z) -{ 1 }-> choice(xs) :|: z = 1 + x + xs, xs >= 0, x >= 0 choice(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0 eq(z, z') -{ 1 }-> eq(x, y) :|: z' = 1 + y, x >= 0, y >= 0, z = 1 + x eq(z, z') -{ 1 }-> 2 :|: z = 1, z' = 1 eq(z, z') -{ 1 }-> 0 :|: z' = 1 + y, x >= 0, y >= 0, z = 1 + x eq(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 guess(z) -{ 1 }-> 1 :|: z = 1 guess(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0 guess(z) -{ 1 }-> 1 + choice(clause) + guess(cnf) :|: cnf >= 0, z = 1 + clause + cnf, clause >= 0 if(z, z', z'') -{ 1 }-> e :|: z' = t, t >= 0, e >= 0, z = 0, z'' = e if(z, z', z'') -{ 1 }-> t :|: z = 2, z' = t, t >= 0, e >= 0, z'' = e if(z, z', z'') -{ 0 }-> 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0 member(z, z') -{ 1 }-> if(eq(x, y), 2, member(x, ys)) :|: ys >= 0, x >= 0, y >= 0, z = x, z' = 1 + y + ys member(z, z') -{ 1 }-> 0 :|: x >= 0, z' = 1, z = x member(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1 negate(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0 negate(z) -{ 1 }-> 1 + x :|: x >= 0, z = 1 + x sat(z) -{ 1 }-> satck(cnf, guess(cnf)) :|: cnf >= 0, z = cnf satck(z, z') -{ 1 }-> if(verify(assign), assign, 3) :|: cnf >= 0, z' = assign, z = cnf, assign >= 0 verify(z) -{ 1 }-> if(member(negate(l), ls), 0, verify(ls)) :|: l >= 0, ls >= 0, z = 1 + l + ls verify(z) -{ 1 }-> 2 :|: z = 1 verify(z) -{ 0 }-> 0 :|: v0 >= 0, z = v0 Only complete derivations are relevant for the runtime complexity. ---------------------------------------- (9) CompleteCoflocoProof (FINISHED) Transformed the RNTS (where only complete derivations are relevant) into cost relations for CoFloCo: eq(start(V3, V1, V4),0,[if(V3, V1, V4, Out)],[V3 >= 0,V1 >= 0,V4 >= 0]). eq(start(V3, V1, V4),0,[member(V3, V1, Out)],[V3 >= 0,V1 >= 0]). eq(start(V3, V1, V4),0,[eq(V3, V1, Out)],[V3 >= 0,V1 >= 0]). eq(start(V3, V1, V4),0,[negate(V3, Out)],[V3 >= 0]). eq(start(V3, V1, V4),0,[choice(V3, Out)],[V3 >= 0]). eq(start(V3, V1, V4),0,[guess(V3, Out)],[V3 >= 0]). eq(start(V3, V1, V4),0,[verify(V3, Out)],[V3 >= 0]). eq(start(V3, V1, V4),0,[sat(V3, Out)],[V3 >= 0]). eq(start(V3, V1, V4),0,[satck(V3, V1, Out)],[V3 >= 0,V1 >= 0]). eq(if(V3, V1, V4, Out),1,[],[Out = V2,V3 = 2,V1 = V2,V2 >= 0,V >= 0,V4 = V]). eq(if(V3, V1, V4, Out),1,[],[Out = V5,V1 = V6,V6 >= 0,V5 >= 0,V3 = 0,V4 = V5]). eq(member(V3, V1, Out),1,[],[Out = 0,V7 >= 0,V1 = 1,V3 = V7]). eq(member(V3, V1, Out),1,[eq(V8, V10, Ret0),member(V8, V9, Ret2),if(Ret0, 2, Ret2, Ret)],[Out = Ret,V9 >= 0,V8 >= 0,V10 >= 0,V3 = V8,V1 = 1 + V10 + V9]). eq(eq(V3, V1, Out),1,[],[Out = 2,V3 = 1,V1 = 1]). eq(eq(V3, V1, Out),1,[eq(V11, V12, Ret1)],[Out = Ret1,V1 = 1 + V12,V11 >= 0,V12 >= 0,V3 = 1 + V11]). eq(eq(V3, V1, Out),1,[],[Out = 0,V1 = 1 + V14,V13 >= 0,V14 >= 0,V3 = 1 + V13]). eq(negate(V3, Out),1,[],[Out = 1 + V15,V15 >= 0,V3 = 1 + V15]). eq(choice(V3, Out),1,[],[Out = V16,V3 = 1 + V16 + V17,V17 >= 0,V16 >= 0]). eq(choice(V3, Out),1,[choice(V19, Ret3)],[Out = Ret3,V3 = 1 + V18 + V19,V19 >= 0,V18 >= 0]). eq(guess(V3, Out),1,[],[Out = 1,V3 = 1]). eq(guess(V3, Out),1,[choice(V20, Ret01),guess(V21, Ret11)],[Out = 1 + Ret01 + Ret11,V21 >= 0,V3 = 1 + V20 + V21,V20 >= 0]). eq(verify(V3, Out),1,[],[Out = 2,V3 = 1]). eq(verify(V3, Out),1,[negate(V23, Ret00),member(Ret00, V22, Ret02),verify(V22, Ret21),if(Ret02, 0, Ret21, Ret4)],[Out = Ret4,V23 >= 0,V22 >= 0,V3 = 1 + V22 + V23]). eq(sat(V3, Out),1,[guess(V24, Ret12),satck(V24, Ret12, Ret5)],[Out = Ret5,V24 >= 0,V3 = V24]). eq(satck(V3, V1, Out),1,[verify(V25, Ret03),if(Ret03, V25, 3, Ret6)],[Out = Ret6,V26 >= 0,V1 = V25,V3 = V26,V25 >= 0]). eq(if(V3, V1, V4, Out),0,[],[Out = 0,V28 >= 0,V4 = V29,V27 >= 0,V3 = V28,V1 = V27,V29 >= 0]). eq(member(V3, V1, Out),0,[],[Out = 0,V31 >= 0,V30 >= 0,V3 = V31,V1 = V30]). eq(eq(V3, V1, Out),0,[],[Out = 0,V33 >= 0,V32 >= 0,V3 = V33,V1 = V32]). eq(negate(V3, Out),0,[],[Out = 0,V34 >= 0,V3 = V34]). eq(choice(V3, Out),0,[],[Out = 0,V35 >= 0,V3 = V35]). eq(guess(V3, Out),0,[],[Out = 0,V36 >= 0,V3 = V36]). eq(verify(V3, Out),0,[],[Out = 0,V37 >= 0,V3 = V37]). input_output_vars(if(V3,V1,V4,Out),[V3,V1,V4],[Out]). input_output_vars(member(V3,V1,Out),[V3,V1],[Out]). input_output_vars(eq(V3,V1,Out),[V3,V1],[Out]). input_output_vars(negate(V3,Out),[V3],[Out]). input_output_vars(choice(V3,Out),[V3],[Out]). input_output_vars(guess(V3,Out),[V3],[Out]). input_output_vars(verify(V3,Out),[V3],[Out]). input_output_vars(sat(V3,Out),[V3],[Out]). input_output_vars(satck(V3,V1,Out),[V3,V1],[Out]). CoFloCo proof output: Preprocessing Cost Relations ===================================== #### Computed strongly connected components 0. recursive : [choice/2] 1. recursive : [eq/3] 2. recursive : [guess/2] 3. non_recursive : [if/4] 4. recursive [non_tail] : [member/3] 5. non_recursive : [negate/2] 6. recursive [non_tail] : [verify/2] 7. non_recursive : [satck/3] 8. non_recursive : [sat/2] 9. non_recursive : [start/3] #### Obtained direct recursion through partial evaluation 0. SCC is partially evaluated into choice/2 1. SCC is partially evaluated into eq/3 2. SCC is partially evaluated into guess/2 3. SCC is partially evaluated into if/4 4. SCC is partially evaluated into member/3 5. SCC is partially evaluated into negate/2 6. SCC is partially evaluated into verify/2 7. SCC is partially evaluated into satck/3 8. SCC is partially evaluated into sat/2 9. SCC is partially evaluated into start/3 Control-Flow Refinement of Cost Relations ===================================== ### Specialization of cost equations choice/2 * CE 22 is refined into CE [33] * CE 24 is refined into CE [34] * CE 23 is refined into CE [35] ### Cost equations --> "Loop" of choice/2 * CEs [35] --> Loop 23 * CEs [33] --> Loop 24 * CEs [34] --> Loop 25 ### Ranking functions of CR choice(V3,Out) * RF of phase [23]: [V3] #### Partial ranking functions of CR choice(V3,Out) * Partial RF of phase [23]: - RF of loop [23:1]: V3 ### Specialization of cost equations eq/3 * CE 18 is refined into CE [36] * CE 19 is refined into CE [37] * CE 16 is refined into CE [38] * CE 17 is refined into CE [39] ### Cost equations --> "Loop" of eq/3 * CEs [39] --> Loop 26 * CEs [36,37] --> Loop 27 * CEs [38] --> Loop 28 ### Ranking functions of CR eq(V3,V1,Out) * RF of phase [26]: [V1,V3] #### Partial ranking functions of CR eq(V3,V1,Out) * Partial RF of phase [26]: - RF of loop [26:1]: V1 V3 ### Specialization of cost equations guess/2 * CE 27 is refined into CE [40] * CE 25 is refined into CE [41] * CE 26 is refined into CE [42,43] ### Cost equations --> "Loop" of guess/2 * CEs [43] --> Loop 29 * CEs [42] --> Loop 30 * CEs [40] --> Loop 31 * CEs [41] --> Loop 32 ### Ranking functions of CR guess(V3,Out) * RF of phase [29,30]: [V3] #### Partial ranking functions of CR guess(V3,Out) * Partial RF of phase [29,30]: - RF of loop [29:1]: V3-1 - RF of loop [30:1]: V3 ### Specialization of cost equations if/4 * CE 12 is refined into CE [44] * CE 10 is refined into CE [45] * CE 11 is refined into CE [46] ### Cost equations --> "Loop" of if/4 * CEs [44] --> Loop 33 * CEs [45] --> Loop 34 * CEs [46] --> Loop 35 ### Ranking functions of CR if(V3,V1,V4,Out) #### Partial ranking functions of CR if(V3,V1,V4,Out) ### Specialization of cost equations member/3 * CE 13 is refined into CE [47] * CE 15 is refined into CE [48] * CE 14 is refined into CE [49,50,51,52,53,54] ### Cost equations --> "Loop" of member/3 * CEs [51] --> Loop 36 * CEs [53] --> Loop 37 * CEs [54] --> Loop 38 * CEs [49] --> Loop 39 * CEs [50,52] --> Loop 40 * CEs [47,48] --> Loop 41 ### Ranking functions of CR member(V3,V1,Out) * RF of phase [36,37,38,39,40]: [V1] #### Partial ranking functions of CR member(V3,V1,Out) * Partial RF of phase [36,37,38,39,40]: - RF of loop [36:1,40:1]: V1 - RF of loop [37:1,38:1]: V1/3-2/3 -V3/3+V1/3 - RF of loop [39:1]: V1/2-1/2 ### Specialization of cost equations negate/2 * CE 20 is refined into CE [55] * CE 21 is refined into CE [56] ### Cost equations --> "Loop" of negate/2 * CEs [55] --> Loop 42 * CEs [56] --> Loop 43 ### Ranking functions of CR negate(V3,Out) #### Partial ranking functions of CR negate(V3,Out) ### Specialization of cost equations verify/2 * CE 30 is refined into CE [57] * CE 28 is refined into CE [58] * CE 29 is refined into CE [59,60,61,62,63,64,65,66,67] ### Cost equations --> "Loop" of verify/2 * CEs [59,61,63,65] --> Loop 44 * CEs [60,62,64,66,67] --> Loop 45 * CEs [57] --> Loop 46 * CEs [58] --> Loop 47 ### Ranking functions of CR verify(V3,Out) * RF of phase [44,45]: [V3] #### Partial ranking functions of CR verify(V3,Out) * Partial RF of phase [44,45]: - RF of loop [44:1,45:1]: V3 ### Specialization of cost equations satck/3 * CE 32 is refined into CE [68,69,70,71,72,73,74] ### Cost equations --> "Loop" of satck/3 * CEs [73] --> Loop 48 * CEs [70,72] --> Loop 49 * CEs [68] --> Loop 50 * CEs [69,71,74] --> Loop 51 ### Ranking functions of CR satck(V3,V1,Out) #### Partial ranking functions of CR satck(V3,V1,Out) ### Specialization of cost equations sat/2 * CE 31 is refined into CE [75,76,77,78,79,80] ### Cost equations --> "Loop" of sat/2 * CEs [78] --> Loop 52 * CEs [77,80] --> Loop 53 * CEs [75] --> Loop 54 * CEs [76,79] --> Loop 55 ### Ranking functions of CR sat(V3,Out) #### Partial ranking functions of CR sat(V3,Out) ### Specialization of cost equations start/3 * CE 1 is refined into CE [81,82,83] * CE 2 is refined into CE [84,85] * CE 3 is refined into CE [86,87,88] * CE 4 is refined into CE [89,90] * CE 5 is refined into CE [91,92] * CE 6 is refined into CE [93,94] * CE 7 is refined into CE [95,96,97] * CE 8 is refined into CE [98,99,100,101] * CE 9 is refined into CE [102,103,104,105] ### Cost equations --> "Loop" of start/3 * CEs [88] --> Loop 56 * CEs [102] --> Loop 57 * CEs [82] --> Loop 58 * CEs [86,95] --> Loop 59 * CEs [81,83,84,85,87,89,90,91,92,93,94,96,97,98,99,100,101,103,104,105] --> Loop 60 ### Ranking functions of CR start(V3,V1,V4) #### Partial ranking functions of CR start(V3,V1,V4) Computing Bounds ===================================== #### Cost of chains of choice(V3,Out): * Chain [[23],25]: 1*it(23)+0 Such that:it(23) =< V3 with precondition: [Out=0,V3>=1] * Chain [[23],24]: 1*it(23)+1 Such that:it(23) =< V3-Out with precondition: [Out>=0,V3>=Out+2] * Chain [25]: 0 with precondition: [Out=0,V3>=0] * Chain [24]: 1 with precondition: [Out>=0,V3>=Out+1] #### Cost of chains of eq(V3,V1,Out): * Chain [[26],28]: 1*it(26)+1 Such that:it(26) =< V3 with precondition: [Out=2,V3=V1,V3>=2] * Chain [[26],27]: 1*it(26)+1 Such that:it(26) =< V1 with precondition: [Out=0,V3>=1,V1>=1] * Chain [28]: 1 with precondition: [V3=1,V1=1,Out=2] * Chain [27]: 1 with precondition: [Out=0,V3>=0,V1>=0] #### Cost of chains of guess(V3,Out): * Chain [[29,30],32]: 5*it(29)+1 Such that:aux(3) =< V3 it(29) =< aux(3) with precondition: [Out>=2,V3>=Out] * Chain [[29,30],31]: 5*it(29)+0 Such that:aux(4) =< V3 it(29) =< aux(4) with precondition: [Out>=1,V3>=Out] * Chain [32]: 1 with precondition: [V3=1,Out=1] * Chain [31]: 0 with precondition: [Out=0,V3>=0] #### Cost of chains of if(V3,V1,V4,Out): * Chain [35]: 1 with precondition: [V3=0,V4=Out,V1>=0,V4>=0] * Chain [34]: 1 with precondition: [V3=2,V1=Out,V1>=0,V4>=0] * Chain [33]: 0 with precondition: [Out=0,V3>=0,V1>=0,V4>=0] #### Cost of chains of member(V3,V1,Out): * Chain [[36,37,38,39,40],41]: 9*it(36)+5*it(37)+3*it(39)+1 Such that:aux(6) =< -V3/3+V1/3 it(39) =< V1/2 aux(12) =< V1 aux(13) =< V1/3 it(37) =< aux(6) it(37) =< aux(13) it(36) =< aux(12) it(37) =< aux(12) it(39) =< aux(12) with precondition: [2>=Out,Out>=0,2*V3>=Out,2*V1>=Out+2] * Chain [41]: 1 with precondition: [Out=0,V3>=0,V1>=0] #### Cost of chains of negate(V3,Out): * Chain [43]: 0 with precondition: [Out=0,V3>=0] * Chain [42]: 1 with precondition: [V3=Out,V3>=1] #### Cost of chains of verify(V3,Out): * Chain [[44,45],47]: 8*it(44)+15*s(72)+10*s(73)+45*s(74)+5*s(75)+10*s(83)+1 Such that:aux(23) =< V3/3 aux(33) =< V3 it(44) =< aux(33) aux(24) =< aux(23)*3 aux(27) =< aux(23) s(78) =< it(44)*aux(23) aux(25) =< it(44)*aux(24) s(86) =< it(44)*aux(27) s(77) =< aux(25)*(1/3) s(79) =< aux(25)*(1/2) s(72) =< s(79) s(83) =< s(86) s(83) =< s(77) s(74) =< aux(25) s(83) =< aux(25) s(72) =< aux(25) s(73) =< s(77) s(73) =< aux(25) s(75) =< s(78) s(75) =< s(77) s(75) =< aux(25) with precondition: [2>=Out,V3>=2,Out>=0] * Chain [[44,45],46]: 8*it(44)+15*s(72)+10*s(73)+45*s(74)+5*s(75)+10*s(83)+0 Such that:aux(23) =< V3/3 aux(34) =< V3 it(44) =< aux(34) aux(24) =< aux(23)*3 aux(27) =< aux(23) s(78) =< it(44)*aux(23) aux(25) =< it(44)*aux(24) s(86) =< it(44)*aux(27) s(77) =< aux(25)*(1/3) s(79) =< aux(25)*(1/2) s(72) =< s(79) s(83) =< s(86) s(83) =< s(77) s(74) =< aux(25) s(83) =< aux(25) s(72) =< aux(25) s(73) =< s(77) s(73) =< aux(25) s(75) =< s(78) s(75) =< s(77) s(75) =< aux(25) with precondition: [Out=0,V3>=1] * Chain [47]: 1 with precondition: [V3=1,Out=2] * Chain [46]: 0 with precondition: [Out=0,V3>=0] #### Cost of chains of satck(V3,V1,Out): * Chain [51]: 16*s(105)+30*s(113)+20*s(114)+90*s(115)+20*s(116)+10*s(117)+2 Such that:aux(35) =< V1 aux(36) =< V1/3 s(105) =< aux(35) s(106) =< aux(36)*3 s(107) =< aux(36) s(108) =< s(105)*aux(36) s(109) =< s(105)*s(106) s(110) =< s(105)*s(107) s(111) =< s(109)*(1/3) s(112) =< s(109)*(1/2) s(113) =< s(112) s(114) =< s(110) s(114) =< s(111) s(115) =< s(109) s(114) =< s(109) s(113) =< s(109) s(116) =< s(111) s(116) =< s(109) s(117) =< s(108) s(117) =< s(111) s(117) =< s(109) with precondition: [Out=0,V3>=0,V1>=0] * Chain [50]: 3 with precondition: [V1=1,Out=1,V3>=0] * Chain [49]: 16*s(135)+30*s(143)+20*s(144)+90*s(145)+20*s(146)+10*s(147)+3 Such that:aux(37) =< V1 aux(38) =< V1/3 s(135) =< aux(37) s(136) =< aux(38)*3 s(137) =< aux(38) s(138) =< s(135)*aux(38) s(139) =< s(135)*s(136) s(140) =< s(135)*s(137) s(141) =< s(139)*(1/3) s(142) =< s(139)*(1/2) s(143) =< s(142) s(144) =< s(140) s(144) =< s(141) s(145) =< s(139) s(144) =< s(139) s(143) =< s(139) s(146) =< s(141) s(146) =< s(139) s(147) =< s(138) s(147) =< s(141) s(147) =< s(139) with precondition: [Out=3,V3>=0,V1>=0] * Chain [48]: 8*s(165)+15*s(173)+10*s(174)+45*s(175)+10*s(176)+5*s(177)+3 Such that:s(164) =< V1 s(163) =< V1/3 s(165) =< s(164) s(166) =< s(163)*3 s(167) =< s(163) s(168) =< s(165)*s(163) s(169) =< s(165)*s(166) s(170) =< s(165)*s(167) s(171) =< s(169)*(1/3) s(172) =< s(169)*(1/2) s(173) =< s(172) s(174) =< s(170) s(174) =< s(171) s(175) =< s(169) s(174) =< s(169) s(173) =< s(169) s(176) =< s(171) s(176) =< s(169) s(177) =< s(168) s(177) =< s(171) s(177) =< s(169) with precondition: [V1=Out,V3>=0,V1>=2] #### Cost of chains of sat(V3,Out): * Chain [55]: 26*s(179)+30*s(190)+20*s(191)+90*s(192)+20*s(193)+10*s(194)+4 Such that:aux(39) =< V3 s(181) =< V3/3 s(179) =< aux(39) s(183) =< s(181)*3 s(184) =< s(181) s(185) =< s(179)*s(181) s(186) =< s(179)*s(183) s(187) =< s(179)*s(184) s(188) =< s(186)*(1/3) s(189) =< s(186)*(1/2) s(190) =< s(189) s(191) =< s(187) s(191) =< s(188) s(192) =< s(186) s(191) =< s(186) s(190) =< s(186) s(193) =< s(188) s(193) =< s(186) s(194) =< s(185) s(194) =< s(188) s(194) =< s(186) with precondition: [Out=0,V3>=0] * Chain [54]: 10*s(211)+5 Such that:s(210) =< V3 s(211) =< s(210) with precondition: [Out=1,V3>=1] * Chain [53]: 26*s(213)+30*s(224)+20*s(225)+90*s(226)+20*s(227)+10*s(228)+5 Such that:aux(41) =< V3 s(215) =< V3/3 s(213) =< aux(41) s(217) =< s(215)*3 s(218) =< s(215) s(219) =< s(213)*s(215) s(220) =< s(213)*s(217) s(221) =< s(213)*s(218) s(222) =< s(220)*(1/3) s(223) =< s(220)*(1/2) s(224) =< s(223) s(225) =< s(221) s(225) =< s(222) s(226) =< s(220) s(225) =< s(220) s(224) =< s(220) s(227) =< s(222) s(227) =< s(220) s(228) =< s(219) s(228) =< s(222) s(228) =< s(220) with precondition: [Out=3,V3>=0] * Chain [52]: 18*s(245)+15*s(256)+10*s(257)+45*s(258)+10*s(259)+5*s(260)+5 Such that:s(247) =< V3/3 aux(43) =< V3 s(245) =< aux(43) s(249) =< s(247)*3 s(250) =< s(247) s(251) =< s(245)*s(247) s(252) =< s(245)*s(249) s(253) =< s(245)*s(250) s(254) =< s(252)*(1/3) s(255) =< s(252)*(1/2) s(256) =< s(255) s(257) =< s(253) s(257) =< s(254) s(258) =< s(252) s(257) =< s(252) s(256) =< s(252) s(259) =< s(254) s(259) =< s(252) s(260) =< s(251) s(260) =< s(254) s(260) =< s(252) with precondition: [Out>=2,V3>=Out] #### Cost of chains of start(V3,V1,V4): * Chain [60]: 3*s(262)+5*s(265)+50*s(266)+108*s(268)+105*s(282)+70*s(283)+315*s(284)+70*s(285)+35*s(286)+75*s(359)+50*s(360)+225*s(361)+50*s(362)+25*s(363)+5 Such that:s(261) =< -V3/3+V1/3 s(262) =< V1/2 aux(44) =< V3 aux(45) =< V3/3 aux(46) =< V1 aux(47) =< V1/3 s(268) =< aux(44) s(266) =< aux(46) s(275) =< aux(45)*3 s(276) =< aux(45) s(277) =< s(268)*aux(45) s(278) =< s(268)*s(275) s(279) =< s(268)*s(276) s(280) =< s(278)*(1/3) s(281) =< s(278)*(1/2) s(282) =< s(281) s(283) =< s(279) s(283) =< s(280) s(284) =< s(278) s(283) =< s(278) s(282) =< s(278) s(285) =< s(280) s(285) =< s(278) s(286) =< s(277) s(286) =< s(280) s(286) =< s(278) s(265) =< s(261) s(265) =< aux(47) s(265) =< aux(46) s(262) =< aux(46) s(352) =< aux(47)*3 s(353) =< aux(47) s(354) =< s(266)*aux(47) s(355) =< s(266)*s(352) s(356) =< s(266)*s(353) s(357) =< s(355)*(1/3) s(358) =< s(355)*(1/2) s(359) =< s(358) s(360) =< s(356) s(360) =< s(357) s(361) =< s(355) s(360) =< s(355) s(359) =< s(355) s(362) =< s(357) s(362) =< s(355) s(363) =< s(354) s(363) =< s(357) s(363) =< s(355) with precondition: [V3>=0] * Chain [59]: 1 with precondition: [V3=1] * Chain [58]: 1 with precondition: [V3=2,V1>=0,V4>=0] * Chain [57]: 3 with precondition: [V1=1,V3>=0] * Chain [56]: 1*s(394)+1 Such that:s(394) =< V1 with precondition: [V3=V1,V3>=2] Closed-form bounds of start(V3,V1,V4): ------------------------------------- * Chain [60] with precondition: [V3>=0] - Upper bound: 108*V3+5+V3/3*(2555/2*V3)+nat(V1)*50+1825/2*nat(V1)*nat(V1/3)+nat(-V3/3+V1/3)*5+nat(V1/2)*3 - Complexity: n^2 * Chain [59] with precondition: [V3=1] - Upper bound: 1 - Complexity: constant * Chain [58] with precondition: [V3=2,V1>=0,V4>=0] - Upper bound: 1 - Complexity: constant * Chain [57] with precondition: [V1=1,V3>=0] - Upper bound: 3 - Complexity: constant * Chain [56] with precondition: [V3=V1,V3>=2] - Upper bound: V1+1 - Complexity: n ### Maximum cost of start(V3,V1,V4): max([2,108*V3+4+V3/3*(2555/2*V3)+nat(V1)*49+1825/2*nat(V1)*nat(V1/3)+nat(-V3/3+V1/3)*5+nat(V1/2)*3+nat(V1)])+1 Asymptotic class: n^2 * Total analysis performed in 732 ms. ---------------------------------------- (10) BOUNDS(1, n^2)