From 898886d5627c4f6124f5de52da7dc7b52201a5ea Mon Sep 17 00:00:00 2001 From: herbelin Date: Mon, 19 Apr 2010 12:29:42 +0000 Subject: Reduced the complexity of evar instantiations from O(n^3) to less than O(n^2). Reasoning modulo variable aliases induced an extra lookup in the environment at each inversion of the components of the evar instances: precomputing the aliases map allowed to gain a factor n. Moreover, solve_evar_evar_l2r was recomputing the evar substitution from the evar instance n more times than needed. Function solve_evar_evar_l2r is still on O(n^2) but it does not seem to be used so often actually. The trivial case has been optimized (linear time) but the general case could probably be also cut down to O(n*log(n)) if needed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12954 85f007b7-540e-0410-9357-904b9bb8a0f7 --- test-suite/complexity/evar_instance.v | 78 +++++++++++++++++++++++++++++++++++ 1 file changed, 78 insertions(+) create mode 100644 test-suite/complexity/evar_instance.v (limited to 'test-suite') diff --git a/test-suite/complexity/evar_instance.v b/test-suite/complexity/evar_instance.v new file mode 100644 index 000000000..97a66c95c --- /dev/null +++ b/test-suite/complexity/evar_instance.v @@ -0,0 +1,78 @@ +(* Checks behavior of unification with respect to the size of evar instances *) +(* Expected time < 2.00s *) + +(* Note that the exact example chosen is not important as soon as it + involves a few of each part of the unification algorithme (and especially + evar-evar unification and evar-term instantiation) *) + +(* In 8.2, the example was in O(n^3) in the number of section variables; + From current commit it is in O(n^2) *) + +(* For the record: with coqtop.byte on a Dual Core 2: + + Nb of extra T i m e + variables 8.1 8.2 8.3beta current + 800 1.6s 188s 185s 1.6s + 400 0.5s 24s 24s 0.43s + 200 0.17s 3s 3.2s 0.12s + 100 0.06s 0.5s 0.48s 0.04s + 50 0.02s 0.08s 0.08s 0.016s + n 12*a*n^2 a*n^3 a*n^3 8*a*n^2 +*) + +Set Implicit Arguments. +Parameter t:Set->Set. +Parameter map:forall elt elt' : Set, (elt -> elt') -> t elt -> t elt'. +Parameter avl: forall elt : Set, t elt -> Prop. +Parameter bst: forall elt : Set, t elt -> Prop. +Parameter map_avl: forall (elt elt' : Set) (f : elt -> elt') (m : t elt), + avl m -> avl (map f m). +Parameter map_bst: forall (elt elt' : Set) (f : elt -> elt') (m : t elt), + bst m -> bst (map f m). +Record bbst (elt:Set) : Set := + Bbst {this :> t elt; is_bst : bst this; is_avl: avl this}. +Definition t' := bbst. +Section B. + +Variables + a b c d e f g h i j k m n o p q r s u v w x y z + a0 b0 c0 d0 e0 f0 g0 h0 i0 j0 k0 m0 n0 o0 p0 q0 r0 s0 u0 v0 w0 x0 y0 z0 + a1 b1 c1 d1 e1 f1 g1 h1 i1 j1 k1 m1 n1 o1 p1 q1 r1 s1 u1 v1 w1 x1 y1 z1 + a2 b2 c2 d2 e2 f2 g2 h2 i2 j2 k2 m2 n2 o2 p2 q2 r2 s2 u2 v2 w2 x2 y2 z2 + a3 b3 c3 d3 e3 f3 g3 h3 i3 j3 k3 m3 n3 o3 p3 q3 r3 s3 u3 v3 w3 x3 y3 z3 + a4 b4 c4 d4 e4 f4 g4 h4 i4 j4 k4 m4 n4 o4 p4 q4 r4 s4 u4 v4 w4 x4 y4 z4 + a5 b5 c5 d5 e5 f5 g5 h5 i5 j5 k5 m5 n5 o5 p5 q5 r5 s5 u5 v5 w5 x5 y5 z5 + a6 b6 c6 d6 e6 f6 g6 h6 i6 j6 k6 m6 n6 o6 p6 q6 r6 s6 u6 v6 w6 x6 y6 z6 + + a7 b7 c7 d7 e7 f7 g7 h7 i7 j7 k7 m7 n7 o7 p7 q7 r7 s7 u7 v7 w7 x7 y7 z7 + a8 b8 c8 d8 e8 f8 g8 h8 i8 j8 k8 m8 n8 o8 p8 q8 r8 s8 u8 v8 w8 x8 y8 z8 + a9 b9 c9 d9 e9 f9 g9 h9 i9 j9 k9 m9 n9 o9 p9 q9 r9 s9 u9 v9 w9 x9 y9 z9 + aA bA cA dA eA fA gA hA iA jA kA mA nA oA pA qA rA sA uA vA wA xA yA zA + aB bB cB dB eB fB gB hB iB jB kB mB nB oB pB qB rB sB uB vB wB xB yB zB + aC bC cC dC eC fC gC hC iC jC kC mC nC oC pC qC rC sC uC vC wC xC yC zC + aD bD cD dD eD fD gD hD iD jD kD mD nD oD pD qD rD sD uD vD wD xD yD zD + aE bE cE dE eE fE gE hE iE jE kE mE nE oE pE qE rE sE uE vE wE xE yE zE + + aF bF cF dF eF fF gF hF iF jF kF mF nF oF pF qF rF sF uF vF wF xF yF zF + aG bG cG dG eG fG gG hG iG jG kG mG nG oG pG qG rG sG uG vG wG xG yG zG + aH bH cH dH eH fH gH hH iH jH kH mH nH oH pH qH rH sH uH vH wH xH yH zH + aI bI cI dI eI fI gI hI iI jI kI mI nI oI pI qI rI sI uI vI wI xI yI zI + aJ bJ cJ dJ eJ fJ gJ hJ iJ jJ kJ mJ nJ oJ pJ qJ rJ sJ uJ vJ wJ xJ yJ zJ + aK bK cK dK eK fK gK hK iK jK kK mK nK oK pK qK rK sK uK vK wK xK yK zK + aL bL cL dL eL fL gL hL iL jL kL mL nL oL pL qL rL sL uL vL wL xL yL zL + aM bM cM dM eM fM gM hM iM jM kM mM nM oM pM qM rM sM uM vM wM xM yM zM + + aN bN cN dN eN fN gN hN iN jN kN mN nN oN pN qN rN sN uN vN wN xN yN zN + aO bO cO dO eO fO gO hO iO jO kO mO nO oO pO qO rO sO uO vO wO xO yO zO + aP bP cP dP eP fP gP hP iP jP kP mP nP oP pP qP rP sP uP vP wP xP yP zP + aQ bQ cQ dQ eQ fQ gQ hQ iQ jQ kQ mQ nQ oQ pQ qQ rQ sQ uQ vQ wQ xQ yQ zQ + aR bR cR dR eR fR gR hR iR jR kR mR nR oR pR qR rR sR uR vR wR xR yR zR + aS bS cS dS eS fS gS hS iS jS kS mS nS oS pS qS rS sS uS vS wS xS yS zS + aT bT cT dT eT fT gT hT iT jT kT mT nT oT pT qT rT sT uT vT wT xT yT zT + aU bU cU dU eU fU gU hU iU jU kU mU nU oU pU qU rU sU uU vU wU xU yU zU + + : nat . + +Variables elt elt': Set. +Timeout 5 Time Definition map' f (m:t' elt) : t' elt' := + Bbst (map_bst f m.(is_bst)) (map_avl f m.(is_avl)). -- cgit v1.2.3