- 1
Я гниль.
Нашли или выдавили из себя код, который нельзя назвать нормальным, на который без улыбки не взглянешь? Не торопитесь его удалять или рефакторить, — запостите его на говнокод.ру, посмеёмся вместе!
−103
Я гниль.
+1
https://www.youtube.com/watch?v=WT-oowiPUVQ
Черная дыра
0
https://i.redd.it/67mnaevvhlm31.jpg
Эх... А ведь так всё и было....
0
(set-logic LIA)
;(set-option :produce-proofs true)
(define-fun-rec add_via_add1 ((a Int) (b Int)) Int
(ite (= b 0) a ; if (b == 0) return a
(ite (< b 0) (- (add_via_add1 (- a) (- b))) ; if (b < 0) return add_via_add(-a,-b)
(+ (add_via_add1 a (- b 1)) 1) ; return add_via_add(a, b-1) + 1;
)
)
)
(assert
(not (forall ((a Int) (b Int))
(= (add_via_add1 a b) (+ a b))
))
)
(check-sat)
(get-model)
(exit)
Хуйня, которую SMT солверы Z3 и CVC4 доказать не могут. Надо переходить на Coq, Metamath, LEAN, Mizar или еще какую-то такую хуйню
0
███████
██ ██
██ ██
██ ██ █████ ████ ██ ██ ██████ █████ ██████ ████ ██ ██ █████ ██ ██ ██ ██ ██ █ ██ ██ ██ ████
██ ██ ██ ██ ██ ██ ██ ██ █ ██ █ ██ ██ █ ██ █ ██ ██ ██ ██ ██ ██ ██ ██ ██ ██ █ ██ ██ ██ ██
██ ██ ██ ██ ██ ██ ██ ███ ██ ██ ██ ██ █████ ██ ██ ██ ██ ██ ██ ██ ██ █ █ █ ██ ██ █████
██ ██ ██ ██ ██ ██ ██ █ ██ ██ ██ ██ ██ ██ ██ ███████ ███████ ███████ ██ ██ █████ ███████ ██ ██
██ ██ ██ ██ ██ ██ ███ ██ ██ ██ ██ ██ ██ ██ ██ ██ ██ ██ ██ ██ ██ █ █ █ ██ ██ ██ ██
██ ██ ██ ██ ██ ██ ██ ██ ██ ██ ██ ██ ██ ██ ██ ██ ██ ██ ██ ██ ██████ ██ █ ██ ██ ██ ██ ██
██ ██ █████ ███ ██ ██ ██ ████ █████ ████ ███ ██ ██ ██ █████ ██ ██ ██ ██ █ ██ ██ ██ ███ ██
██
██ ██
█████
Политота не нужна
0
static F1(jtdrr){PROLOG(0055);A df,dg,hs,*x,z;B b,ex,xop;C c,id;I fl,*hv,m;V*v;
RZ(w);
// If the input is a name, it must be from ".@'name' which turned into ".@(name+noun) - or in debug, but that's discarded
if(AT(w)&NAME){RZ(w=sfn(0,w));}
// If noun, return the value of the noun.
if(AT(w)&NOUN)R w; // no quotes needed
// Non-nouns and NMDOT names carry on
v=FAV(w); id=v->id; fl=v->flag;
I fndx=(id==CBDOT)&&!v->fgh[0]; A fs=v->fgh[fndx]; A gs=v->fgh[fndx^1]; // In verb for m b., if f is empty look to g for the left arg. It would be nice to be more general
hs=v->fgh[2]; if(id==CBOX)gs=0; // ignore gs field in BOX, there to simulate BOXATOP
if(fl&VXOPCALL)R drr(hs);
xop=1&&VXOP&fl; ex=id==CCOLON&&hs&&!xop;
b=id==CHOOK||id==CADVF; c=id==CFORK;
m=!!fs+(gs||ex);
if(!m)R spella(w);
if(evoke(w))R drr(sfne(w)); // turn nameref into string or verb; then take rep
if(fs)RZ(df=fl&VGERL?every(fxeach(fs),0L,jtdrr):drr(fs));
if(gs)RZ(dg=fl&VGERR?every(fxeach(gs),0L,jtdrr):drr(gs));
if(ex)RZ(dg=unparsem(num[0],w));
m+=!b&&!xop||hs&&xop;
GATV0(z,BOX,m,1); x=AAV(z);
RZ(x[0]=rifvs(df));
RZ(x[1]=rifvs(b||c||xop?dg:fl&VDDOP?(hv=AV(hs),link(sc(hv[0]),link(spellout(id),sc(hv[1])))):spellout(id)));
if(2<m)RZ(x[2]=rifvs(c||xop?drr(hs):dg));
EPILOG(z);
}
F1(jtdrep){A z=drr(w); R z&&AT(z)&BOX?z:ravel(box(z));}
F1(jtaro){A fs,gs,hs,s,*u,*x,y,z;B ex,xop;C id;I*hv,m;V*v;
RZ(w);
if(FUNC&AT(w)){
v=FAV(w); id=v->id;
I fndx=(id==CBDOT)&&!v->fgh[0]; fs=v->fgh[fndx]; gs=v->fgh[fndx^1]; // In verb for m b., if f is empty look to g for the left arg. It would be nice to be more general
hs=v->fgh[2]; if(id==CBOX)gs=0; // ignore gs field in BOX, there to simulate BOXATOP
if(VXOPCALL&v->flag)R aro(hs);
xop=1&&VXOP&v->flag;
ex=hs&&id==CCOLON&&!xop;
m=id==CFORK?3:!!fs+(ex||xop&&hs||!xop&&gs);
if(!m)R spella(w);
if(evoke(w)){RZ(w=sfne(w)); if(FUNC&AT(w))w=aro(w); R w;} // keep nameref as a string, UNLESS it is NMDOT, in which case use the (f.'d) verb value
}
GAT0(z,BOX,2,1); x=AAV(z);
if(NOUN&AT(w)){RZ(x[0]=rifvs(ravel(scc(CNOUN)))); if(AT(w)&NAME)RZ(w=sfn(0,w)); x[1]=INCORPNA(w); RETF(z);} // if name, must be ".@'name', format name as string
GATV0(y,BOX,m,1); u=AAV(y);
if(0<m)RZ(u[0]=rifvs(aro(fs)));
if(1<m)RZ(u[1]=rifvs(aro(ex?unparsem(num[0],w):xop?hs:gs)));
if(2<m)RZ(u[2]=rifvs(aro(hs)));
s=xop?aro(gs):VDDOP&v->flag?(hv=AV(hs),aro(foreign(sc(hv[0]),sc(hv[1])))):spellout(id);
RZ(x[0]=rifvs(s)); x[1]=INCORPNA(y);
R z;
}
F1(jtarep){R box(aro(w));}
// Create A for a string - name~, a primitive, or the boxed string
static DF1(jtfxchar){A y;C c,d,id,*s;I m,n;
n=AN(w);
ASSERT(1>=AR(w),EVRANK); // string must be an atom or list
ASSERT(n,EVLENGTH);
s=CAV(w); c=*(s+n-1);
DO(n, d=s[i]; ASSERT((C)(d-32)<(C)(127-32),EVSPELL);); // must be all ASCII
if(CA==ctype[(UC)*s]&&c!=CESC1&&c!=CESC2)R swap(w); // If name and not control word, treat as name~, create nameref
ASSERT(id=spellin(n,s),EVSPELL); // not name, must be control word or primitive. Also classify string
if(id!=CFCONS)y=ds(id); else{m=s[n-2]-'0'; y=FCONS(CSIGN!=*s?scib(m):2==n?ainf:scib(-m));} // define 0:, if it's that, using boolean for 0/1
ASSERT(y&&RHS&AT(y),EVDOMAIN); // make sure it's a noun/verb/adv/conj
if(!self || AT(y)
0
RZ(z=tail(w)); k=AN(z)<<bplg(AT(z)); // k=length of input cell in bytes
// fill in the shape, offset, and item-count of the virtual block
AN(a)=AN(z); AK(a)+=(n-1)*k; MCISH(AS(a),AS(z),r-1); // make the virtual block look like the tail, except for the offset. We start out pointing
// to the last item; the pointer is unused in the first iteration, and we then back up to the second-last item, which is the first one we
// process as a
#define ZZPOPNEVER 1 // we mustn't TPOP after copying the result atoms, because they are reused. This will leave the memory used for type-conversions unclaimed.
// if we implement the annulment of tpop pointers, we should use that to hand-free results that have been converted
// We have to dance a bit for BOXATOP verbs, because the result comes back unboxed, but it has to be put into a box
// to be fed into the next iteration. This is still a saving, because we can use the same box to point to each successive result.
// Exception: if the reusable box gets incorporated, it is no longer reusable and must be reallocated. We will use the original z box,
// which will NEVER be virtual because it is an atom whenever BOXATOP is set, as the starting pointer to the prev boxed result
A boxedz = z; z=(state&ZZFLAGBOXATOP)?AAV(z)[0]:z; // init current pointer for the temp box; if BOXATOP, use >{:y as the first (to-be-boxed) result
#define ZZDECL
#define ZZSTARTATEND 1 // build result from bottom up
#include "result.h"
ZZPARMS(1,n,2)
#define ZZINSTALLFRAME(optr) *optr++=n;
AD * RESTRICT zz=0;
for(i=0;i<n;++i){ // loop through items, noting that the first is the tail itself
if(i){RZ(z=CALL2(f2,a,z,fs));} // apply the verb to the arguments (except the first time)
#define ZZBODY
#include "result.h"
// If BOXATOP, we need to reinstate the boxing around z for the next iteration.
if(state&ZZFLAGBOXATOP){
// If boxedz itself has been incorporated into the result, we have to reallocate it. We don't need the usual check for z==boxedz, because we know we INCORPed z into
// the boxed result, so if it was the same as boxedz, the usecount of boxedz was incremented then
if(!ACIPISOK(boxedz))GAT0(boxedz,BOX,1,0); // reallocate boxedz if needed
AAV(boxedz)[0]=z; z=boxedz; // point boxedz to the previous result, and make that the new argument for next time
}
// if result happens to be the same virtual block that we passed in, we have to clone it before we change the pointer
else if(a==z){RZ(z=virtual(z,0,AR(a))); AN(z)=AN(a); MCISH(AS(z),AS(a),r-1);}
AK(a)-=k; // back up to next input
}
A jtscansp(J jt,A w,A self,AF sf){A e,ee,x,z;B*b;I f,m,j,r,t,wr;P*wp,*zp;
wr=AR(w); r=(RANKT)jt->ranks; r=wr<r?wr:r; RESETRANK; f=wr-r;
wp=PAV(w); e=SPA(wp,e); RZ(ee=over(e,e));
if(!equ(ee,CALL1(sf,ee,self))){
RZ(x=denseit(w));
R IRS1(x,self,r,sf,z);
}else{
RZ(b=bfi(wr,SPA(wp,a),1));
if(r&&b[f]){b[f]=0; RZ(w=reaxis(ifb(wr,b),w));}
j=f; m=0; DQ(wr-f, m+=!b[j++];);
}
wp=PAV(w); e=SPA(wp,e); x=SPA(wp,x);
RZ(x=IRS1(x,self,m,sf,z));
t=maxtype(AT(e),AT(x)); RZ(e=cvt(t,e)); if(TYPESNE(t,AT(x)))RZ(x=cvt(t,x));
GASPARSE(z,STYPE(t),1,wr+!m,AS(w)); if(!m)*(wr+AS(z))=1;
zp=PAV(z);
SPB(zp,e,e);
SPB(zp,x,x);
SPB(zp,i,ca(SPA(wp,i)));
SPB(zp,a,ca(SPA(wp,a)));
R z;
} /* f/\"r or f/\."r on sparse w */
static DF1(jtsscan){A y,z;I d,f,m,n,r,t,wn,wr,*ws,wt;
RZ(w);F1PREFIP;
wt=AT(w);
if(SPARSE&wt)R scansp(w,self,jtsscan);
wn=AN(w); wr=AR(w); r=(RANKT)jt->ranks; r=wr<r?wr:r; f=wr-r; ws=AS(w); RESETRANK;
PROD(m,f,ws); PROD1(d,r-1,f+ws+1); n=r?ws[f]:1; // will not be used if WN==0, so PROD ok. n is # items along the selected rank
y=FAV(self)->fgh[0]; // y is f/
if(((n-2)|(wn-1))<0){if(vaid(FAV(y)->fgh[0])){R r?RETARG(w):reshape(over(shape(w),num[1]),w);}else R IRS1(w,self,r,jtsuffix,z);} // if empty arg, or just 1 cell in selected axis, convert to f/\ which handles the short arg
//
0
Электрика / электроника #2
#1: http://govnokod.xyz/_25437/
0
IT Оффтоп #22
#1: https://govnokod.ru/18142 https://govnokod.xyz/_18142
#2: https://govnokod.ru/18378 https://govnokod.xyz/_18378
#3: https://govnokod.ru/19667 https://govnokod.xyz/_19667
#4: https://govnokod.ru/21160 https://govnokod.xyz/_21160
#5: https://govnokod.ru/21772 https://govnokod.xyz/_21772
#6: https://govnokod.ru/24063 (потёр пидор сракер) https://govnokod.xyz/_24063
#7: https://govnokod.ru/24538 https://govnokod.xyz/_24538
#8: https://govnokod.ru/24815 (потёр пидор сракер) https://govnokod.xyz/_24815
#9: https://govnokod.ru/24867 https://govnokod.xyz/_24867
#10: https://govnokod.ru/25328 https://govnokod.xyz/_25328
#11: https://govnokod.xyz/_25436 https://govnokod.ru/25436 (потёр пидор сракер)
#12: https://govnokod.xyz/_25471
#13: https://govnokod.xyz/_25590 (потёр пидор сракер)
#14: https://govnokod.xyz/_25684
#15: https://govnokod.xyz/_25694
#16: https://govnokod.xyz/_25725
#17: https://govnokod.xyz/_25731
#18: https://govnokod.xyz/_25762
#19: https://govnokod.xyz/_25767
#20: https://govnokod.xyz/_25776
#21: https://govnokod.xyz/_25798
−3
https://habr.com/ru/post/465553/
А правда, почему компилятор C++ позволяет писать такую хуету
x+= x++ + ++x;
x^=y^=x^=y;
?