veri_engine_lib/solver/encoded_ops/
cls.rs

1use crate::solver::SolverCtx;
2use easy_smt::SExpr;
3
4// Future work: possibly move these into the annotation language or an SMTLIB prelude
5// Adapted from https://stackoverflow.com/questions/23856596/how-to-count-leading-zeros-in-a-32-bit-unsigned-integer
6
7pub fn cls64(solver: &mut SolverCtx, x: SExpr, id: u32) -> SExpr {
8    // Generated code.
9    // total zeros counter
10    let zret0 = solver.declare(
11        format!("zret0_{id}", id = id),
12        solver.smt.list(vec![
13            solver.smt.atoms().und,
14            solver.smt.atom("BitVec"),
15            solver.smt.numeral(64),
16        ]),
17    );
18    solver.assume(solver.smt.eq(
19        zret0,
20        solver.smt.list(vec![
21            solver.smt.atoms().und,
22            solver.smt.atom("bv0"),
23            solver.smt.numeral(64),
24        ]),
25    ));
26    // round 1
27    let zret1 = solver.declare(
28        format!("zret1_{id}", id = id),
29        solver.smt.list(vec![
30            solver.smt.atoms().und,
31            solver.smt.atom("BitVec"),
32            solver.smt.numeral(64),
33        ]),
34    );
35    let zy32 = solver.declare(
36        format!("zy32_{id}", id = id),
37        solver.smt.list(vec![
38            solver.smt.atoms().und,
39            solver.smt.atom("BitVec"),
40            solver.smt.numeral(64),
41        ]),
42    );
43    let zx32 = solver.declare(
44        format!("zx32_{id}", id = id),
45        solver.smt.list(vec![
46            solver.smt.atoms().und,
47            solver.smt.atom("BitVec"),
48            solver.smt.numeral(64),
49        ]),
50    );
51    solver.assume(solver.smt.eq(
52        zy32,
53        solver.smt.bvlshr(x, solver.smt.atom("#x0000000000000020")),
54    ));
55    solver.assume(solver.smt.list(vec![
56        solver.smt.atom("ite"),
57        solver.smt.list(vec![
58            solver.smt.atom("not"),
59            solver.smt.eq(
60                zy32,
61                solver.smt.list(vec![
62                    solver.smt.atoms().und,
63                    solver.smt.atom("bv0"),
64                    solver.smt.numeral(64),
65                ]),
66            ),
67        ]),
68        solver.smt.eq(zret1, zret0),
69        solver.smt.eq(
70            zret1,
71            solver.smt.list(vec![
72                solver.smt.atom("bvadd"),
73                zret0,
74                solver.smt.list(vec![
75                    solver.smt.atoms().und,
76                    solver.smt.atom("bv32"),
77                    solver.smt.numeral(64),
78                ]),
79            ]),
80        ),
81    ]));
82    solver.assume(solver.smt.list(vec![
83        solver.smt.atom("ite"),
84        solver.smt.list(vec![
85            solver.smt.atom("not"),
86            solver.smt.eq(
87                zy32,
88                solver.smt.list(vec![
89                    solver.smt.atoms().und,
90                    solver.smt.atom("bv0"),
91                    solver.smt.numeral(64),
92                ]),
93            ),
94        ]),
95        solver.smt.eq(zx32, zy32),
96        solver.smt.eq(zx32, x),
97    ]));
98    // round 2
99    let zret2 = solver.declare(
100        format!("zret2_{id}", id = id),
101        solver.smt.list(vec![
102            solver.smt.atoms().und,
103            solver.smt.atom("BitVec"),
104            solver.smt.numeral(64),
105        ]),
106    );
107    let zy16 = solver.declare(
108        format!("zy16_{id}", id = id),
109        solver.smt.list(vec![
110            solver.smt.atoms().und,
111            solver.smt.atom("BitVec"),
112            solver.smt.numeral(64),
113        ]),
114    );
115    let zx16 = solver.declare(
116        format!("zx16_{id}", id = id),
117        solver.smt.list(vec![
118            solver.smt.atoms().und,
119            solver.smt.atom("BitVec"),
120            solver.smt.numeral(64),
121        ]),
122    );
123    solver.assume(
124        solver.smt.eq(
125            zy16,
126            solver
127                .smt
128                .bvlshr(zx32, solver.smt.atom("#x0000000000000010")),
129        ),
130    );
131    solver.assume(solver.smt.list(vec![
132        solver.smt.atom("ite"),
133        solver.smt.list(vec![
134            solver.smt.atom("not"),
135            solver.smt.eq(
136                zy16,
137                solver.smt.list(vec![
138                    solver.smt.atoms().und,
139                    solver.smt.atom("bv0"),
140                    solver.smt.numeral(64),
141                ]),
142            ),
143        ]),
144        solver.smt.eq(zret2, zret1),
145        solver.smt.eq(
146            zret2,
147            solver.smt.list(vec![
148                solver.smt.atom("bvadd"),
149                zret1,
150                solver.smt.list(vec![
151                    solver.smt.atoms().und,
152                    solver.smt.atom("bv16"),
153                    solver.smt.numeral(64),
154                ]),
155            ]),
156        ),
157    ]));
158    solver.assume(solver.smt.list(vec![
159        solver.smt.atom("ite"),
160        solver.smt.list(vec![
161            solver.smt.atom("not"),
162            solver.smt.eq(
163                zy16,
164                solver.smt.list(vec![
165                    solver.smt.atoms().und,
166                    solver.smt.atom("bv0"),
167                    solver.smt.numeral(64),
168                ]),
169            ),
170        ]),
171        solver.smt.eq(zx16, zy16),
172        solver.smt.eq(zx16, zx32),
173    ]));
174    // round 3
175    let zret3 = solver.declare(
176        format!("zret3_{id}", id = id),
177        solver.smt.list(vec![
178            solver.smt.atoms().und,
179            solver.smt.atom("BitVec"),
180            solver.smt.numeral(64),
181        ]),
182    );
183    let zy8 = solver.declare(
184        format!("zy8_{id}", id = id),
185        solver.smt.list(vec![
186            solver.smt.atoms().und,
187            solver.smt.atom("BitVec"),
188            solver.smt.numeral(64),
189        ]),
190    );
191    let zx8 = solver.declare(
192        format!("zx8_{id}", id = id),
193        solver.smt.list(vec![
194            solver.smt.atoms().und,
195            solver.smt.atom("BitVec"),
196            solver.smt.numeral(64),
197        ]),
198    );
199    solver.assume(
200        solver.smt.eq(
201            zy8,
202            solver
203                .smt
204                .bvlshr(zx16, solver.smt.atom("#x0000000000000008")),
205        ),
206    );
207    solver.assume(solver.smt.list(vec![
208        solver.smt.atom("ite"),
209        solver.smt.list(vec![
210            solver.smt.atom("not"),
211            solver.smt.eq(
212                zy8,
213                solver.smt.list(vec![
214                    solver.smt.atoms().und,
215                    solver.smt.atom("bv0"),
216                    solver.smt.numeral(64),
217                ]),
218            ),
219        ]),
220        solver.smt.eq(zret3, zret2),
221        solver.smt.eq(
222            zret3,
223            solver.smt.list(vec![
224                solver.smt.atom("bvadd"),
225                zret2,
226                solver.smt.list(vec![
227                    solver.smt.atoms().und,
228                    solver.smt.atom("bv8"),
229                    solver.smt.numeral(64),
230                ]),
231            ]),
232        ),
233    ]));
234    solver.assume(solver.smt.list(vec![
235        solver.smt.atom("ite"),
236        solver.smt.list(vec![
237            solver.smt.atom("not"),
238            solver.smt.eq(
239                zy8,
240                solver.smt.list(vec![
241                    solver.smt.atoms().und,
242                    solver.smt.atom("bv0"),
243                    solver.smt.numeral(64),
244                ]),
245            ),
246        ]),
247        solver.smt.eq(zx8, zy8),
248        solver.smt.eq(zx8, zx16),
249    ]));
250    // round 4
251    let zret4 = solver.declare(
252        format!("zret4_{id}", id = id),
253        solver.smt.list(vec![
254            solver.smt.atoms().und,
255            solver.smt.atom("BitVec"),
256            solver.smt.numeral(64),
257        ]),
258    );
259    let zy4 = solver.declare(
260        format!("zy4_{id}", id = id),
261        solver.smt.list(vec![
262            solver.smt.atoms().und,
263            solver.smt.atom("BitVec"),
264            solver.smt.numeral(64),
265        ]),
266    );
267    let zx4 = solver.declare(
268        format!("zx4_{id}", id = id),
269        solver.smt.list(vec![
270            solver.smt.atoms().und,
271            solver.smt.atom("BitVec"),
272            solver.smt.numeral(64),
273        ]),
274    );
275    solver.assume(
276        solver.smt.eq(
277            zy4,
278            solver
279                .smt
280                .bvlshr(zx8, solver.smt.atom("#x0000000000000004")),
281        ),
282    );
283    solver.assume(solver.smt.list(vec![
284        solver.smt.atom("ite"),
285        solver.smt.list(vec![
286            solver.smt.atom("not"),
287            solver.smt.eq(
288                zy4,
289                solver.smt.list(vec![
290                    solver.smt.atoms().und,
291                    solver.smt.atom("bv0"),
292                    solver.smt.numeral(64),
293                ]),
294            ),
295        ]),
296        solver.smt.eq(zret4, zret3),
297        solver.smt.eq(
298            zret4,
299            solver.smt.list(vec![
300                solver.smt.atom("bvadd"),
301                zret3,
302                solver.smt.list(vec![
303                    solver.smt.atoms().und,
304                    solver.smt.atom("bv4"),
305                    solver.smt.numeral(64),
306                ]),
307            ]),
308        ),
309    ]));
310    solver.assume(solver.smt.list(vec![
311        solver.smt.atom("ite"),
312        solver.smt.list(vec![
313            solver.smt.atom("not"),
314            solver.smt.eq(
315                zy4,
316                solver.smt.list(vec![
317                    solver.smt.atoms().und,
318                    solver.smt.atom("bv0"),
319                    solver.smt.numeral(64),
320                ]),
321            ),
322        ]),
323        solver.smt.eq(zx4, zy4),
324        solver.smt.eq(zx4, zx8),
325    ]));
326    // round 5
327    let zret5 = solver.declare(
328        format!("zret5_{id}", id = id),
329        solver.smt.list(vec![
330            solver.smt.atoms().und,
331            solver.smt.atom("BitVec"),
332            solver.smt.numeral(64),
333        ]),
334    );
335    let zy2 = solver.declare(
336        format!("zy2_{id}", id = id),
337        solver.smt.list(vec![
338            solver.smt.atoms().und,
339            solver.smt.atom("BitVec"),
340            solver.smt.numeral(64),
341        ]),
342    );
343    let zx2 = solver.declare(
344        format!("zx2_{id}", id = id),
345        solver.smt.list(vec![
346            solver.smt.atoms().und,
347            solver.smt.atom("BitVec"),
348            solver.smt.numeral(64),
349        ]),
350    );
351    solver.assume(
352        solver.smt.eq(
353            zy2,
354            solver
355                .smt
356                .bvlshr(zx4, solver.smt.atom("#x0000000000000002")),
357        ),
358    );
359    solver.assume(solver.smt.list(vec![
360        solver.smt.atom("ite"),
361        solver.smt.list(vec![
362            solver.smt.atom("not"),
363            solver.smt.eq(
364                zy2,
365                solver.smt.list(vec![
366                    solver.smt.atoms().und,
367                    solver.smt.atom("bv0"),
368                    solver.smt.numeral(64),
369                ]),
370            ),
371        ]),
372        solver.smt.eq(zret5, zret4),
373        solver.smt.eq(
374            zret5,
375            solver.smt.list(vec![
376                solver.smt.atom("bvadd"),
377                zret4,
378                solver.smt.list(vec![
379                    solver.smt.atoms().und,
380                    solver.smt.atom("bv2"),
381                    solver.smt.numeral(64),
382                ]),
383            ]),
384        ),
385    ]));
386    solver.assume(solver.smt.list(vec![
387        solver.smt.atom("ite"),
388        solver.smt.list(vec![
389            solver.smt.atom("not"),
390            solver.smt.eq(
391                zy2,
392                solver.smt.list(vec![
393                    solver.smt.atoms().und,
394                    solver.smt.atom("bv0"),
395                    solver.smt.numeral(64),
396                ]),
397            ),
398        ]),
399        solver.smt.eq(zx2, zy2),
400        solver.smt.eq(zx2, zx4),
401    ]));
402    // round 6
403    let zret6 = solver.declare(
404        format!("zret6_{id}", id = id),
405        solver.smt.list(vec![
406            solver.smt.atoms().und,
407            solver.smt.atom("BitVec"),
408            solver.smt.numeral(64),
409        ]),
410    );
411    let zy1 = solver.declare(
412        format!("zy1_{id}", id = id),
413        solver.smt.list(vec![
414            solver.smt.atoms().und,
415            solver.smt.atom("BitVec"),
416            solver.smt.numeral(64),
417        ]),
418    );
419    let zx1 = solver.declare(
420        format!("zx1_{id}", id = id),
421        solver.smt.list(vec![
422            solver.smt.atoms().und,
423            solver.smt.atom("BitVec"),
424            solver.smt.numeral(64),
425        ]),
426    );
427    solver.assume(
428        solver.smt.eq(
429            zy1,
430            solver
431                .smt
432                .bvlshr(zx2, solver.smt.atom("#x0000000000000001")),
433        ),
434    );
435    solver.assume(solver.smt.list(vec![
436        solver.smt.atom("ite"),
437        solver.smt.list(vec![
438            solver.smt.atom("not"),
439            solver.smt.eq(
440                zy1,
441                solver.smt.list(vec![
442                    solver.smt.atoms().und,
443                    solver.smt.atom("bv0"),
444                    solver.smt.numeral(64),
445                ]),
446            ),
447        ]),
448        solver.smt.eq(zret6, zret5),
449        solver.smt.eq(
450            zret6,
451            solver.smt.list(vec![
452                solver.smt.atom("bvadd"),
453                zret5,
454                solver.smt.list(vec![
455                    solver.smt.atoms().und,
456                    solver.smt.atom("bv1"),
457                    solver.smt.numeral(64),
458                ]),
459            ]),
460        ),
461    ]));
462    solver.assume(solver.smt.list(vec![
463        solver.smt.atom("ite"),
464        solver.smt.list(vec![
465            solver.smt.atom("not"),
466            solver.smt.eq(
467                zy1,
468                solver.smt.list(vec![
469                    solver.smt.atoms().und,
470                    solver.smt.atom("bv0"),
471                    solver.smt.numeral(64),
472                ]),
473            ),
474        ]),
475        solver.smt.eq(zx1, zy1),
476        solver.smt.eq(zx1, zx2),
477    ]));
478    // last round
479    let zret7 = solver.declare(
480        format!("zret7_{id}", id = id),
481        solver.smt.list(vec![
482            solver.smt.atoms().und,
483            solver.smt.atom("BitVec"),
484            solver.smt.numeral(64),
485        ]),
486    );
487    solver.assume(solver.smt.list(vec![
488        solver.smt.atom("ite"),
489        solver.smt.list(vec![
490            solver.smt.atom("not"),
491            solver.smt.eq(
492                zx1,
493                solver.smt.list(vec![
494                    solver.smt.atoms().und,
495                    solver.smt.atom("bv0"),
496                    solver.smt.numeral(64),
497                ]),
498            ),
499        ]),
500        solver.smt.eq(zret7, zret6),
501        solver.smt.eq(
502            zret7,
503            solver.smt.list(vec![
504                solver.smt.atom("bvadd"),
505                zret6,
506                solver.smt.list(vec![
507                    solver.smt.atoms().und,
508                    solver.smt.atom("bv1"),
509                    solver.smt.numeral(64),
510                ]),
511            ]),
512        ),
513    ]));
514    let clzret = solver.declare(
515        format!("clzret_{id}", id = id),
516        solver.smt.list(vec![
517            solver.smt.atoms().und,
518            solver.smt.atom("BitVec"),
519            solver.smt.numeral(64),
520        ]),
521    );
522    solver.assume(solver.smt.list(vec![
523        solver.smt.atom("ite"),
524        solver.smt.eq(
525            zret7,
526            solver.smt.list(vec![
527                solver.smt.atoms().und,
528                solver.smt.atom("bv0"),
529                solver.smt.numeral(64),
530            ]),
531        ),
532        solver.smt.eq(clzret, zret7),
533        solver.smt.eq(
534            clzret,
535            solver.smt.list(vec![
536                solver.smt.atom("bvsub"),
537                zret7,
538                solver.smt.list(vec![
539                    solver.smt.atoms().und,
540                    solver.smt.atom("bv1"),
541                    solver.smt.numeral(64),
542                ]),
543            ]),
544        ),
545    ]));
546    // total zeros counter
547    let sret0 = solver.declare(
548        format!("sret0_{id}", id = id),
549        solver.smt.list(vec![
550            solver.smt.atoms().und,
551            solver.smt.atom("BitVec"),
552            solver.smt.numeral(64),
553        ]),
554    );
555    solver.assume(solver.smt.eq(
556        sret0,
557        solver.smt.list(vec![
558            solver.smt.atoms().und,
559            solver.smt.atom("bv0"),
560            solver.smt.numeral(64),
561        ]),
562    ));
563    // round 1
564    let sret1 = solver.declare(
565        format!("sret1_{id}", id = id),
566        solver.smt.list(vec![
567            solver.smt.atoms().und,
568            solver.smt.atom("BitVec"),
569            solver.smt.numeral(64),
570        ]),
571    );
572    let sy32 = solver.declare(
573        format!("sy32_{id}", id = id),
574        solver.smt.list(vec![
575            solver.smt.atoms().und,
576            solver.smt.atom("BitVec"),
577            solver.smt.numeral(64),
578        ]),
579    );
580    let sx32 = solver.declare(
581        format!("sx32_{id}", id = id),
582        solver.smt.list(vec![
583            solver.smt.atoms().und,
584            solver.smt.atom("BitVec"),
585            solver.smt.numeral(64),
586        ]),
587    );
588    solver.assume(solver.smt.eq(
589        sy32,
590        solver.smt.bvashr(x, solver.smt.atom("#x0000000000000020")),
591    ));
592    solver.assume(solver.smt.list(vec![
593        solver.smt.atom("ite"),
594        solver.smt.list(vec![
595            solver.smt.atom("not"),
596            solver.smt.eq(
597                sy32,
598                solver.smt.list(vec![
599                    solver.smt.atoms().und,
600                    solver.smt.atom("bv18446744073709551615"),
601                    solver.smt.numeral(64),
602                ]),
603            ),
604        ]),
605        solver.smt.eq(sret1, sret0),
606        solver.smt.eq(
607            sret1,
608            solver.smt.list(vec![
609                solver.smt.atom("bvadd"),
610                sret0,
611                solver.smt.list(vec![
612                    solver.smt.atoms().und,
613                    solver.smt.atom("bv32"),
614                    solver.smt.numeral(64),
615                ]),
616            ]),
617        ),
618    ]));
619    solver.assume(solver.smt.list(vec![
620        solver.smt.atom("ite"),
621        solver.smt.list(vec![
622            solver.smt.atom("not"),
623            solver.smt.eq(
624                sy32,
625                solver.smt.list(vec![
626                    solver.smt.atoms().und,
627                    solver.smt.atom("bv18446744073709551615"),
628                    solver.smt.numeral(64),
629                ]),
630            ),
631        ]),
632        solver.smt.eq(sx32, sy32),
633        solver.smt.eq(sx32, x),
634    ]));
635    // round 2
636    let sret2 = solver.declare(
637        format!("sret2_{id}", id = id),
638        solver.smt.list(vec![
639            solver.smt.atoms().und,
640            solver.smt.atom("BitVec"),
641            solver.smt.numeral(64),
642        ]),
643    );
644    let sy16 = solver.declare(
645        format!("sy16_{id}", id = id),
646        solver.smt.list(vec![
647            solver.smt.atoms().und,
648            solver.smt.atom("BitVec"),
649            solver.smt.numeral(64),
650        ]),
651    );
652    let sx16 = solver.declare(
653        format!("sx16_{id}", id = id),
654        solver.smt.list(vec![
655            solver.smt.atoms().und,
656            solver.smt.atom("BitVec"),
657            solver.smt.numeral(64),
658        ]),
659    );
660    solver.assume(
661        solver.smt.eq(
662            sy16,
663            solver
664                .smt
665                .bvashr(sx32, solver.smt.atom("#x0000000000000010")),
666        ),
667    );
668    solver.assume(solver.smt.list(vec![
669        solver.smt.atom("ite"),
670        solver.smt.list(vec![
671            solver.smt.atom("not"),
672            solver.smt.eq(
673                sy16,
674                solver.smt.list(vec![
675                    solver.smt.atoms().und,
676                    solver.smt.atom("bv18446744073709551615"),
677                    solver.smt.numeral(64),
678                ]),
679            ),
680        ]),
681        solver.smt.eq(sret2, sret1),
682        solver.smt.eq(
683            sret2,
684            solver.smt.list(vec![
685                solver.smt.atom("bvadd"),
686                sret1,
687                solver.smt.list(vec![
688                    solver.smt.atoms().und,
689                    solver.smt.atom("bv16"),
690                    solver.smt.numeral(64),
691                ]),
692            ]),
693        ),
694    ]));
695    solver.assume(solver.smt.list(vec![
696        solver.smt.atom("ite"),
697        solver.smt.list(vec![
698            solver.smt.atom("not"),
699            solver.smt.eq(
700                sy16,
701                solver.smt.list(vec![
702                    solver.smt.atoms().und,
703                    solver.smt.atom("bv18446744073709551615"),
704                    solver.smt.numeral(64),
705                ]),
706            ),
707        ]),
708        solver.smt.eq(sx16, sy16),
709        solver.smt.eq(sx16, sx32),
710    ]));
711    // round 3
712    let sret3 = solver.declare(
713        format!("sret3_{id}", id = id),
714        solver.smt.list(vec![
715            solver.smt.atoms().und,
716            solver.smt.atom("BitVec"),
717            solver.smt.numeral(64),
718        ]),
719    );
720    let sy8 = solver.declare(
721        format!("sy8_{id}", id = id),
722        solver.smt.list(vec![
723            solver.smt.atoms().und,
724            solver.smt.atom("BitVec"),
725            solver.smt.numeral(64),
726        ]),
727    );
728    let sx8 = solver.declare(
729        format!("sx8_{id}", id = id),
730        solver.smt.list(vec![
731            solver.smt.atoms().und,
732            solver.smt.atom("BitVec"),
733            solver.smt.numeral(64),
734        ]),
735    );
736    solver.assume(
737        solver.smt.eq(
738            sy8,
739            solver
740                .smt
741                .bvashr(sx16, solver.smt.atom("#x0000000000000008")),
742        ),
743    );
744    solver.assume(solver.smt.list(vec![
745        solver.smt.atom("ite"),
746        solver.smt.list(vec![
747            solver.smt.atom("not"),
748            solver.smt.eq(
749                sy8,
750                solver.smt.list(vec![
751                    solver.smt.atoms().und,
752                    solver.smt.atom("bv18446744073709551615"),
753                    solver.smt.numeral(64),
754                ]),
755            ),
756        ]),
757        solver.smt.eq(sret3, sret2),
758        solver.smt.eq(
759            sret3,
760            solver.smt.list(vec![
761                solver.smt.atom("bvadd"),
762                sret2,
763                solver.smt.list(vec![
764                    solver.smt.atoms().und,
765                    solver.smt.atom("bv8"),
766                    solver.smt.numeral(64),
767                ]),
768            ]),
769        ),
770    ]));
771    solver.assume(solver.smt.list(vec![
772        solver.smt.atom("ite"),
773        solver.smt.list(vec![
774            solver.smt.atom("not"),
775            solver.smt.eq(
776                sy8,
777                solver.smt.list(vec![
778                    solver.smt.atoms().und,
779                    solver.smt.atom("bv18446744073709551615"),
780                    solver.smt.numeral(64),
781                ]),
782            ),
783        ]),
784        solver.smt.eq(sx8, sy8),
785        solver.smt.eq(sx8, sx16),
786    ]));
787    // round 4
788    let sret4 = solver.declare(
789        format!("sret4_{id}", id = id),
790        solver.smt.list(vec![
791            solver.smt.atoms().und,
792            solver.smt.atom("BitVec"),
793            solver.smt.numeral(64),
794        ]),
795    );
796    let sy4 = solver.declare(
797        format!("sy4_{id}", id = id),
798        solver.smt.list(vec![
799            solver.smt.atoms().und,
800            solver.smt.atom("BitVec"),
801            solver.smt.numeral(64),
802        ]),
803    );
804    let sx4 = solver.declare(
805        format!("sx4_{id}", id = id),
806        solver.smt.list(vec![
807            solver.smt.atoms().und,
808            solver.smt.atom("BitVec"),
809            solver.smt.numeral(64),
810        ]),
811    );
812    solver.assume(
813        solver.smt.eq(
814            sy4,
815            solver
816                .smt
817                .bvashr(sx8, solver.smt.atom("#x0000000000000004")),
818        ),
819    );
820    solver.assume(solver.smt.list(vec![
821        solver.smt.atom("ite"),
822        solver.smt.list(vec![
823            solver.smt.atom("not"),
824            solver.smt.eq(
825                sy4,
826                solver.smt.list(vec![
827                    solver.smt.atoms().und,
828                    solver.smt.atom("bv18446744073709551615"),
829                    solver.smt.numeral(64),
830                ]),
831            ),
832        ]),
833        solver.smt.eq(sret4, sret3),
834        solver.smt.eq(
835            sret4,
836            solver.smt.list(vec![
837                solver.smt.atom("bvadd"),
838                sret3,
839                solver.smt.list(vec![
840                    solver.smt.atoms().und,
841                    solver.smt.atom("bv4"),
842                    solver.smt.numeral(64),
843                ]),
844            ]),
845        ),
846    ]));
847    solver.assume(solver.smt.list(vec![
848        solver.smt.atom("ite"),
849        solver.smt.list(vec![
850            solver.smt.atom("not"),
851            solver.smt.eq(
852                sy4,
853                solver.smt.list(vec![
854                    solver.smt.atoms().und,
855                    solver.smt.atom("bv18446744073709551615"),
856                    solver.smt.numeral(64),
857                ]),
858            ),
859        ]),
860        solver.smt.eq(sx4, sy4),
861        solver.smt.eq(sx4, sx8),
862    ]));
863    // round 5
864    let sret5 = solver.declare(
865        format!("sret5_{id}", id = id),
866        solver.smt.list(vec![
867            solver.smt.atoms().und,
868            solver.smt.atom("BitVec"),
869            solver.smt.numeral(64),
870        ]),
871    );
872    let sy2 = solver.declare(
873        format!("sy2_{id}", id = id),
874        solver.smt.list(vec![
875            solver.smt.atoms().und,
876            solver.smt.atom("BitVec"),
877            solver.smt.numeral(64),
878        ]),
879    );
880    let sx2 = solver.declare(
881        format!("sx2_{id}", id = id),
882        solver.smt.list(vec![
883            solver.smt.atoms().und,
884            solver.smt.atom("BitVec"),
885            solver.smt.numeral(64),
886        ]),
887    );
888    solver.assume(
889        solver.smt.eq(
890            sy2,
891            solver
892                .smt
893                .bvashr(sx4, solver.smt.atom("#x0000000000000002")),
894        ),
895    );
896    solver.assume(solver.smt.list(vec![
897        solver.smt.atom("ite"),
898        solver.smt.list(vec![
899            solver.smt.atom("not"),
900            solver.smt.eq(
901                sy2,
902                solver.smt.list(vec![
903                    solver.smt.atoms().und,
904                    solver.smt.atom("bv18446744073709551615"),
905                    solver.smt.numeral(64),
906                ]),
907            ),
908        ]),
909        solver.smt.eq(sret5, sret4),
910        solver.smt.eq(
911            sret5,
912            solver.smt.list(vec![
913                solver.smt.atom("bvadd"),
914                sret4,
915                solver.smt.list(vec![
916                    solver.smt.atoms().und,
917                    solver.smt.atom("bv2"),
918                    solver.smt.numeral(64),
919                ]),
920            ]),
921        ),
922    ]));
923    solver.assume(solver.smt.list(vec![
924        solver.smt.atom("ite"),
925        solver.smt.list(vec![
926            solver.smt.atom("not"),
927            solver.smt.eq(
928                sy2,
929                solver.smt.list(vec![
930                    solver.smt.atoms().und,
931                    solver.smt.atom("bv18446744073709551615"),
932                    solver.smt.numeral(64),
933                ]),
934            ),
935        ]),
936        solver.smt.eq(sx2, sy2),
937        solver.smt.eq(sx2, sx4),
938    ]));
939    // round 6
940    let sret6 = solver.declare(
941        format!("sret6_{id}", id = id),
942        solver.smt.list(vec![
943            solver.smt.atoms().und,
944            solver.smt.atom("BitVec"),
945            solver.smt.numeral(64),
946        ]),
947    );
948    let sy1 = solver.declare(
949        format!("sy1_{id}", id = id),
950        solver.smt.list(vec![
951            solver.smt.atoms().und,
952            solver.smt.atom("BitVec"),
953            solver.smt.numeral(64),
954        ]),
955    );
956    let sx1 = solver.declare(
957        format!("sx1_{id}", id = id),
958        solver.smt.list(vec![
959            solver.smt.atoms().und,
960            solver.smt.atom("BitVec"),
961            solver.smt.numeral(64),
962        ]),
963    );
964    solver.assume(
965        solver.smt.eq(
966            sy1,
967            solver
968                .smt
969                .bvashr(sx2, solver.smt.atom("#x0000000000000001")),
970        ),
971    );
972    solver.assume(solver.smt.list(vec![
973        solver.smt.atom("ite"),
974        solver.smt.list(vec![
975            solver.smt.atom("not"),
976            solver.smt.eq(
977                sy1,
978                solver.smt.list(vec![
979                    solver.smt.atoms().und,
980                    solver.smt.atom("bv18446744073709551615"),
981                    solver.smt.numeral(64),
982                ]),
983            ),
984        ]),
985        solver.smt.eq(sret6, sret5),
986        solver.smt.eq(
987            sret6,
988            solver.smt.list(vec![
989                solver.smt.atom("bvadd"),
990                sret5,
991                solver.smt.list(vec![
992                    solver.smt.atoms().und,
993                    solver.smt.atom("bv1"),
994                    solver.smt.numeral(64),
995                ]),
996            ]),
997        ),
998    ]));
999    solver.assume(solver.smt.list(vec![
1000        solver.smt.atom("ite"),
1001        solver.smt.list(vec![
1002            solver.smt.atom("not"),
1003            solver.smt.eq(
1004                sy1,
1005                solver.smt.list(vec![
1006                    solver.smt.atoms().und,
1007                    solver.smt.atom("bv18446744073709551615"),
1008                    solver.smt.numeral(64),
1009                ]),
1010            ),
1011        ]),
1012        solver.smt.eq(sx1, sy1),
1013        solver.smt.eq(sx1, sx2),
1014    ]));
1015    // last round
1016    let sret7 = solver.declare(
1017        format!("sret7_{id}", id = id),
1018        solver.smt.list(vec![
1019            solver.smt.atoms().und,
1020            solver.smt.atom("BitVec"),
1021            solver.smt.numeral(64),
1022        ]),
1023    );
1024    solver.assume(solver.smt.list(vec![
1025        solver.smt.atom("ite"),
1026        solver.smt.list(vec![
1027            solver.smt.atom("not"),
1028            solver.smt.eq(
1029                sx1,
1030                solver.smt.list(vec![
1031                    solver.smt.atoms().und,
1032                    solver.smt.atom("bv18446744073709551615"),
1033                    solver.smt.numeral(64),
1034                ]),
1035            ),
1036        ]),
1037        solver.smt.eq(sret7, sret6),
1038        solver.smt.eq(
1039            sret7,
1040            solver.smt.list(vec![
1041                solver.smt.atom("bvadd"),
1042                sret6,
1043                solver.smt.list(vec![
1044                    solver.smt.atoms().und,
1045                    solver.smt.atom("bv1"),
1046                    solver.smt.numeral(64),
1047                ]),
1048            ]),
1049        ),
1050    ]));
1051    let clsret = solver.declare(
1052        format!("clsret_{id}", id = id),
1053        solver.smt.list(vec![
1054            solver.smt.atoms().und,
1055            solver.smt.atom("BitVec"),
1056            solver.smt.numeral(64),
1057        ]),
1058    );
1059    solver.assume(solver.smt.list(vec![
1060        solver.smt.atom("ite"),
1061        solver.smt.eq(
1062            sret7,
1063            solver.smt.list(vec![
1064                solver.smt.atoms().und,
1065                solver.smt.atom("bv0"),
1066                solver.smt.numeral(64),
1067            ]),
1068        ),
1069        solver.smt.eq(clsret, sret7),
1070        solver.smt.eq(
1071            clsret,
1072            solver.smt.list(vec![
1073                solver.smt.atom("bvsub"),
1074                sret7,
1075                solver.smt.list(vec![
1076                    solver.smt.atoms().und,
1077                    solver.smt.atom("bv1"),
1078                    solver.smt.numeral(64),
1079                ]),
1080            ]),
1081        ),
1082    ]));
1083    let cls64ret = solver.declare(
1084        format!("cls64ret_{id}", id = id),
1085        solver.smt.list(vec![
1086            solver.smt.atoms().und,
1087            solver.smt.atom("BitVec"),
1088            solver.smt.numeral(64),
1089        ]),
1090    );
1091    solver.assume(solver.smt.list(vec![
1092        solver.smt.atom("ite"),
1093        solver.smt.list(vec![
1094            solver.smt.atom("bvsle"),
1095            solver.smt.list(vec![
1096                solver.smt.atoms().und,
1097                solver.smt.atom("bv0"),
1098                solver.smt.numeral(64),
1099            ]),
1100            x,
1101        ]),
1102        solver.smt.eq(cls64ret, clzret),
1103        solver.smt.eq(cls64ret, clsret),
1104    ]));
1105
1106    cls64ret
1107}
1108
1109pub fn cls32(solver: &mut SolverCtx, x: SExpr, id: u32) -> SExpr {
1110    let x = solver.smt.extract(31, 0, x);
1111
1112    // Generated code.
1113    // total zeros counter
1114    let zret0 = solver.declare(
1115        format!("zret0_{id}", id = id),
1116        solver.smt.list(vec![
1117            solver.smt.atoms().und,
1118            solver.smt.atom("BitVec"),
1119            solver.smt.numeral(32),
1120        ]),
1121    );
1122    solver.assume(solver.smt.eq(
1123        zret0,
1124        solver.smt.list(vec![
1125            solver.smt.atoms().und,
1126            solver.smt.atom("bv0"),
1127            solver.smt.numeral(32),
1128        ]),
1129    ));
1130    // round 1
1131    let zret2 = solver.declare(
1132        format!("zret2_{id}", id = id),
1133        solver.smt.list(vec![
1134            solver.smt.atoms().und,
1135            solver.smt.atom("BitVec"),
1136            solver.smt.numeral(32),
1137        ]),
1138    );
1139    let zy16 = solver.declare(
1140        format!("zy16_{id}", id = id),
1141        solver.smt.list(vec![
1142            solver.smt.atoms().und,
1143            solver.smt.atom("BitVec"),
1144            solver.smt.numeral(32),
1145        ]),
1146    );
1147    let zx16 = solver.declare(
1148        format!("zx16_{id}", id = id),
1149        solver.smt.list(vec![
1150            solver.smt.atoms().und,
1151            solver.smt.atom("BitVec"),
1152            solver.smt.numeral(32),
1153        ]),
1154    );
1155    solver.assume(
1156        solver
1157            .smt
1158            .eq(zy16, solver.smt.bvlshr(x, solver.smt.atom("#x00000010"))),
1159    );
1160    solver.assume(solver.smt.list(vec![
1161        solver.smt.atom("ite"),
1162        solver.smt.list(vec![
1163            solver.smt.atom("not"),
1164            solver.smt.eq(
1165                zy16,
1166                solver.smt.list(vec![
1167                    solver.smt.atoms().und,
1168                    solver.smt.atom("bv0"),
1169                    solver.smt.numeral(32),
1170                ]),
1171            ),
1172        ]),
1173        solver.smt.eq(zret2, zret0),
1174        solver.smt.eq(
1175            zret2,
1176            solver.smt.list(vec![
1177                solver.smt.atom("bvadd"),
1178                zret0,
1179                solver.smt.list(vec![
1180                    solver.smt.atoms().und,
1181                    solver.smt.atom("bv16"),
1182                    solver.smt.numeral(32),
1183                ]),
1184            ]),
1185        ),
1186    ]));
1187    solver.assume(solver.smt.list(vec![
1188        solver.smt.atom("ite"),
1189        solver.smt.list(vec![
1190            solver.smt.atom("not"),
1191            solver.smt.eq(
1192                zy16,
1193                solver.smt.list(vec![
1194                    solver.smt.atoms().und,
1195                    solver.smt.atom("bv0"),
1196                    solver.smt.numeral(32),
1197                ]),
1198            ),
1199        ]),
1200        solver.smt.eq(zx16, zy16),
1201        solver.smt.eq(zx16, x),
1202    ]));
1203    // round 2
1204    let zret3 = solver.declare(
1205        format!("zret3_{id}", id = id),
1206        solver.smt.list(vec![
1207            solver.smt.atoms().und,
1208            solver.smt.atom("BitVec"),
1209            solver.smt.numeral(32),
1210        ]),
1211    );
1212    let zy8 = solver.declare(
1213        format!("zy8_{id}", id = id),
1214        solver.smt.list(vec![
1215            solver.smt.atoms().und,
1216            solver.smt.atom("BitVec"),
1217            solver.smt.numeral(32),
1218        ]),
1219    );
1220    let zx8 = solver.declare(
1221        format!("zx8_{id}", id = id),
1222        solver.smt.list(vec![
1223            solver.smt.atoms().und,
1224            solver.smt.atom("BitVec"),
1225            solver.smt.numeral(32),
1226        ]),
1227    );
1228    solver.assume(
1229        solver
1230            .smt
1231            .eq(zy8, solver.smt.bvlshr(zx16, solver.smt.atom("#x00000008"))),
1232    );
1233    solver.assume(solver.smt.list(vec![
1234        solver.smt.atom("ite"),
1235        solver.smt.list(vec![
1236            solver.smt.atom("not"),
1237            solver.smt.eq(
1238                zy8,
1239                solver.smt.list(vec![
1240                    solver.smt.atoms().und,
1241                    solver.smt.atom("bv0"),
1242                    solver.smt.numeral(32),
1243                ]),
1244            ),
1245        ]),
1246        solver.smt.eq(zret3, zret2),
1247        solver.smt.eq(
1248            zret3,
1249            solver.smt.list(vec![
1250                solver.smt.atom("bvadd"),
1251                zret2,
1252                solver.smt.list(vec![
1253                    solver.smt.atoms().und,
1254                    solver.smt.atom("bv8"),
1255                    solver.smt.numeral(32),
1256                ]),
1257            ]),
1258        ),
1259    ]));
1260    solver.assume(solver.smt.list(vec![
1261        solver.smt.atom("ite"),
1262        solver.smt.list(vec![
1263            solver.smt.atom("not"),
1264            solver.smt.eq(
1265                zy8,
1266                solver.smt.list(vec![
1267                    solver.smt.atoms().und,
1268                    solver.smt.atom("bv0"),
1269                    solver.smt.numeral(32),
1270                ]),
1271            ),
1272        ]),
1273        solver.smt.eq(zx8, zy8),
1274        solver.smt.eq(zx8, zx16),
1275    ]));
1276    // round 3
1277    let zret4 = solver.declare(
1278        format!("zret4_{id}", id = id),
1279        solver.smt.list(vec![
1280            solver.smt.atoms().und,
1281            solver.smt.atom("BitVec"),
1282            solver.smt.numeral(32),
1283        ]),
1284    );
1285    let zy4 = solver.declare(
1286        format!("zy4_{id}", id = id),
1287        solver.smt.list(vec![
1288            solver.smt.atoms().und,
1289            solver.smt.atom("BitVec"),
1290            solver.smt.numeral(32),
1291        ]),
1292    );
1293    let zx4 = solver.declare(
1294        format!("zx4_{id}", id = id),
1295        solver.smt.list(vec![
1296            solver.smt.atoms().und,
1297            solver.smt.atom("BitVec"),
1298            solver.smt.numeral(32),
1299        ]),
1300    );
1301    solver.assume(
1302        solver
1303            .smt
1304            .eq(zy4, solver.smt.bvlshr(zx8, solver.smt.atom("#x00000004"))),
1305    );
1306    solver.assume(solver.smt.list(vec![
1307        solver.smt.atom("ite"),
1308        solver.smt.list(vec![
1309            solver.smt.atom("not"),
1310            solver.smt.eq(
1311                zy4,
1312                solver.smt.list(vec![
1313                    solver.smt.atoms().und,
1314                    solver.smt.atom("bv0"),
1315                    solver.smt.numeral(32),
1316                ]),
1317            ),
1318        ]),
1319        solver.smt.eq(zret4, zret3),
1320        solver.smt.eq(
1321            zret4,
1322            solver.smt.list(vec![
1323                solver.smt.atom("bvadd"),
1324                zret3,
1325                solver.smt.list(vec![
1326                    solver.smt.atoms().und,
1327                    solver.smt.atom("bv4"),
1328                    solver.smt.numeral(32),
1329                ]),
1330            ]),
1331        ),
1332    ]));
1333    solver.assume(solver.smt.list(vec![
1334        solver.smt.atom("ite"),
1335        solver.smt.list(vec![
1336            solver.smt.atom("not"),
1337            solver.smt.eq(
1338                zy4,
1339                solver.smt.list(vec![
1340                    solver.smt.atoms().und,
1341                    solver.smt.atom("bv0"),
1342                    solver.smt.numeral(32),
1343                ]),
1344            ),
1345        ]),
1346        solver.smt.eq(zx4, zy4),
1347        solver.smt.eq(zx4, zx8),
1348    ]));
1349    // round 4
1350    let zret5 = solver.declare(
1351        format!("zret5_{id}", id = id),
1352        solver.smt.list(vec![
1353            solver.smt.atoms().und,
1354            solver.smt.atom("BitVec"),
1355            solver.smt.numeral(32),
1356        ]),
1357    );
1358    let zy2 = solver.declare(
1359        format!("zy2_{id}", id = id),
1360        solver.smt.list(vec![
1361            solver.smt.atoms().und,
1362            solver.smt.atom("BitVec"),
1363            solver.smt.numeral(32),
1364        ]),
1365    );
1366    let zx2 = solver.declare(
1367        format!("zx2_{id}", id = id),
1368        solver.smt.list(vec![
1369            solver.smt.atoms().und,
1370            solver.smt.atom("BitVec"),
1371            solver.smt.numeral(32),
1372        ]),
1373    );
1374    solver.assume(
1375        solver
1376            .smt
1377            .eq(zy2, solver.smt.bvlshr(zx4, solver.smt.atom("#x00000002"))),
1378    );
1379    solver.assume(solver.smt.list(vec![
1380        solver.smt.atom("ite"),
1381        solver.smt.list(vec![
1382            solver.smt.atom("not"),
1383            solver.smt.eq(
1384                zy2,
1385                solver.smt.list(vec![
1386                    solver.smt.atoms().und,
1387                    solver.smt.atom("bv0"),
1388                    solver.smt.numeral(32),
1389                ]),
1390            ),
1391        ]),
1392        solver.smt.eq(zret5, zret4),
1393        solver.smt.eq(
1394            zret5,
1395            solver.smt.list(vec![
1396                solver.smt.atom("bvadd"),
1397                zret4,
1398                solver.smt.list(vec![
1399                    solver.smt.atoms().und,
1400                    solver.smt.atom("bv2"),
1401                    solver.smt.numeral(32),
1402                ]),
1403            ]),
1404        ),
1405    ]));
1406    solver.assume(solver.smt.list(vec![
1407        solver.smt.atom("ite"),
1408        solver.smt.list(vec![
1409            solver.smt.atom("not"),
1410            solver.smt.eq(
1411                zy2,
1412                solver.smt.list(vec![
1413                    solver.smt.atoms().und,
1414                    solver.smt.atom("bv0"),
1415                    solver.smt.numeral(32),
1416                ]),
1417            ),
1418        ]),
1419        solver.smt.eq(zx2, zy2),
1420        solver.smt.eq(zx2, zx4),
1421    ]));
1422    // round 5
1423    let zret6 = solver.declare(
1424        format!("zret6_{id}", id = id),
1425        solver.smt.list(vec![
1426            solver.smt.atoms().und,
1427            solver.smt.atom("BitVec"),
1428            solver.smt.numeral(32),
1429        ]),
1430    );
1431    let zy1 = solver.declare(
1432        format!("zy1_{id}", id = id),
1433        solver.smt.list(vec![
1434            solver.smt.atoms().und,
1435            solver.smt.atom("BitVec"),
1436            solver.smt.numeral(32),
1437        ]),
1438    );
1439    let zx1 = solver.declare(
1440        format!("zx1_{id}", id = id),
1441        solver.smt.list(vec![
1442            solver.smt.atoms().und,
1443            solver.smt.atom("BitVec"),
1444            solver.smt.numeral(32),
1445        ]),
1446    );
1447    solver.assume(
1448        solver
1449            .smt
1450            .eq(zy1, solver.smt.bvlshr(zx2, solver.smt.atom("#x00000001"))),
1451    );
1452    solver.assume(solver.smt.list(vec![
1453        solver.smt.atom("ite"),
1454        solver.smt.list(vec![
1455            solver.smt.atom("not"),
1456            solver.smt.eq(
1457                zy1,
1458                solver.smt.list(vec![
1459                    solver.smt.atoms().und,
1460                    solver.smt.atom("bv0"),
1461                    solver.smt.numeral(32),
1462                ]),
1463            ),
1464        ]),
1465        solver.smt.eq(zret6, zret5),
1466        solver.smt.eq(
1467            zret6,
1468            solver.smt.list(vec![
1469                solver.smt.atom("bvadd"),
1470                zret5,
1471                solver.smt.list(vec![
1472                    solver.smt.atoms().und,
1473                    solver.smt.atom("bv1"),
1474                    solver.smt.numeral(32),
1475                ]),
1476            ]),
1477        ),
1478    ]));
1479    solver.assume(solver.smt.list(vec![
1480        solver.smt.atom("ite"),
1481        solver.smt.list(vec![
1482            solver.smt.atom("not"),
1483            solver.smt.eq(
1484                zy1,
1485                solver.smt.list(vec![
1486                    solver.smt.atoms().und,
1487                    solver.smt.atom("bv0"),
1488                    solver.smt.numeral(32),
1489                ]),
1490            ),
1491        ]),
1492        solver.smt.eq(zx1, zy1),
1493        solver.smt.eq(zx1, zx2),
1494    ]));
1495    // last round
1496    let zret7 = solver.declare(
1497        format!("zret7_{id}", id = id),
1498        solver.smt.list(vec![
1499            solver.smt.atoms().und,
1500            solver.smt.atom("BitVec"),
1501            solver.smt.numeral(32),
1502        ]),
1503    );
1504    solver.assume(solver.smt.list(vec![
1505        solver.smt.atom("ite"),
1506        solver.smt.list(vec![
1507            solver.smt.atom("not"),
1508            solver.smt.eq(
1509                zx1,
1510                solver.smt.list(vec![
1511                    solver.smt.atoms().und,
1512                    solver.smt.atom("bv0"),
1513                    solver.smt.numeral(32),
1514                ]),
1515            ),
1516        ]),
1517        solver.smt.eq(zret7, zret6),
1518        solver.smt.eq(
1519            zret7,
1520            solver.smt.list(vec![
1521                solver.smt.atom("bvadd"),
1522                zret6,
1523                solver.smt.list(vec![
1524                    solver.smt.atoms().und,
1525                    solver.smt.atom("bv1"),
1526                    solver.smt.numeral(32),
1527                ]),
1528            ]),
1529        ),
1530    ]));
1531    let clzret = solver.declare(
1532        format!("clzret_{id}", id = id),
1533        solver.smt.list(vec![
1534            solver.smt.atoms().und,
1535            solver.smt.atom("BitVec"),
1536            solver.smt.numeral(32),
1537        ]),
1538    );
1539    solver.assume(solver.smt.list(vec![
1540        solver.smt.atom("ite"),
1541        solver.smt.eq(
1542            zret7,
1543            solver.smt.list(vec![
1544                solver.smt.atoms().und,
1545                solver.smt.atom("bv0"),
1546                solver.smt.numeral(32),
1547            ]),
1548        ),
1549        solver.smt.eq(clzret, zret7),
1550        solver.smt.eq(
1551            clzret,
1552            solver.smt.list(vec![
1553                solver.smt.atom("bvsub"),
1554                zret7,
1555                solver.smt.list(vec![
1556                    solver.smt.atoms().und,
1557                    solver.smt.atom("bv1"),
1558                    solver.smt.numeral(32),
1559                ]),
1560            ]),
1561        ),
1562    ]));
1563    // total zeros counter
1564    let sret0 = solver.declare(
1565        format!("sret0_{id}", id = id),
1566        solver.smt.list(vec![
1567            solver.smt.atoms().und,
1568            solver.smt.atom("BitVec"),
1569            solver.smt.numeral(32),
1570        ]),
1571    );
1572    solver.assume(solver.smt.eq(
1573        sret0,
1574        solver.smt.list(vec![
1575            solver.smt.atoms().und,
1576            solver.smt.atom("bv0"),
1577            solver.smt.numeral(32),
1578        ]),
1579    ));
1580    // round 1
1581    let sret2 = solver.declare(
1582        format!("sret2_{id}", id = id),
1583        solver.smt.list(vec![
1584            solver.smt.atoms().und,
1585            solver.smt.atom("BitVec"),
1586            solver.smt.numeral(32),
1587        ]),
1588    );
1589    let sy16 = solver.declare(
1590        format!("sy16_{id}", id = id),
1591        solver.smt.list(vec![
1592            solver.smt.atoms().und,
1593            solver.smt.atom("BitVec"),
1594            solver.smt.numeral(32),
1595        ]),
1596    );
1597    let sx16 = solver.declare(
1598        format!("sx16_{id}", id = id),
1599        solver.smt.list(vec![
1600            solver.smt.atoms().und,
1601            solver.smt.atom("BitVec"),
1602            solver.smt.numeral(32),
1603        ]),
1604    );
1605    solver.assume(
1606        solver
1607            .smt
1608            .eq(sy16, solver.smt.bvashr(x, solver.smt.atom("#x00000010"))),
1609    );
1610    solver.assume(solver.smt.list(vec![
1611        solver.smt.atom("ite"),
1612        solver.smt.list(vec![
1613            solver.smt.atom("not"),
1614            solver.smt.eq(
1615                sy16,
1616                solver.smt.list(vec![
1617                    solver.smt.atoms().und,
1618                    solver.smt.atom("bv4294967295"),
1619                    solver.smt.numeral(32),
1620                ]),
1621            ),
1622        ]),
1623        solver.smt.eq(sret2, sret0),
1624        solver.smt.eq(
1625            sret2,
1626            solver.smt.list(vec![
1627                solver.smt.atom("bvadd"),
1628                sret0,
1629                solver.smt.list(vec![
1630                    solver.smt.atoms().und,
1631                    solver.smt.atom("bv16"),
1632                    solver.smt.numeral(32),
1633                ]),
1634            ]),
1635        ),
1636    ]));
1637    solver.assume(solver.smt.list(vec![
1638        solver.smt.atom("ite"),
1639        solver.smt.list(vec![
1640            solver.smt.atom("not"),
1641            solver.smt.eq(
1642                sy16,
1643                solver.smt.list(vec![
1644                    solver.smt.atoms().und,
1645                    solver.smt.atom("bv4294967295"),
1646                    solver.smt.numeral(32),
1647                ]),
1648            ),
1649        ]),
1650        solver.smt.eq(sx16, sy16),
1651        solver.smt.eq(sx16, x),
1652    ]));
1653    // round 2
1654    let sret3 = solver.declare(
1655        format!("sret3_{id}", id = id),
1656        solver.smt.list(vec![
1657            solver.smt.atoms().und,
1658            solver.smt.atom("BitVec"),
1659            solver.smt.numeral(32),
1660        ]),
1661    );
1662    let sy8 = solver.declare(
1663        format!("sy8_{id}", id = id),
1664        solver.smt.list(vec![
1665            solver.smt.atoms().und,
1666            solver.smt.atom("BitVec"),
1667            solver.smt.numeral(32),
1668        ]),
1669    );
1670    let sx8 = solver.declare(
1671        format!("sx8_{id}", id = id),
1672        solver.smt.list(vec![
1673            solver.smt.atoms().und,
1674            solver.smt.atom("BitVec"),
1675            solver.smt.numeral(32),
1676        ]),
1677    );
1678    solver.assume(
1679        solver
1680            .smt
1681            .eq(sy8, solver.smt.bvashr(sx16, solver.smt.atom("#x00000008"))),
1682    );
1683    solver.assume(solver.smt.list(vec![
1684        solver.smt.atom("ite"),
1685        solver.smt.list(vec![
1686            solver.smt.atom("not"),
1687            solver.smt.eq(
1688                sy8,
1689                solver.smt.list(vec![
1690                    solver.smt.atoms().und,
1691                    solver.smt.atom("bv4294967295"),
1692                    solver.smt.numeral(32),
1693                ]),
1694            ),
1695        ]),
1696        solver.smt.eq(sret3, sret2),
1697        solver.smt.eq(
1698            sret3,
1699            solver.smt.list(vec![
1700                solver.smt.atom("bvadd"),
1701                sret2,
1702                solver.smt.list(vec![
1703                    solver.smt.atoms().und,
1704                    solver.smt.atom("bv8"),
1705                    solver.smt.numeral(32),
1706                ]),
1707            ]),
1708        ),
1709    ]));
1710    solver.assume(solver.smt.list(vec![
1711        solver.smt.atom("ite"),
1712        solver.smt.list(vec![
1713            solver.smt.atom("not"),
1714            solver.smt.eq(
1715                sy8,
1716                solver.smt.list(vec![
1717                    solver.smt.atoms().und,
1718                    solver.smt.atom("bv4294967295"),
1719                    solver.smt.numeral(32),
1720                ]),
1721            ),
1722        ]),
1723        solver.smt.eq(sx8, sy8),
1724        solver.smt.eq(sx8, sx16),
1725    ]));
1726    // round 3
1727    let sret4 = solver.declare(
1728        format!("sret4_{id}", id = id),
1729        solver.smt.list(vec![
1730            solver.smt.atoms().und,
1731            solver.smt.atom("BitVec"),
1732            solver.smt.numeral(32),
1733        ]),
1734    );
1735    let sy4 = solver.declare(
1736        format!("sy4_{id}", id = id),
1737        solver.smt.list(vec![
1738            solver.smt.atoms().und,
1739            solver.smt.atom("BitVec"),
1740            solver.smt.numeral(32),
1741        ]),
1742    );
1743    let sx4 = solver.declare(
1744        format!("sx4_{id}", id = id),
1745        solver.smt.list(vec![
1746            solver.smt.atoms().und,
1747            solver.smt.atom("BitVec"),
1748            solver.smt.numeral(32),
1749        ]),
1750    );
1751    solver.assume(
1752        solver
1753            .smt
1754            .eq(sy4, solver.smt.bvashr(sx8, solver.smt.atom("#x00000004"))),
1755    );
1756    solver.assume(solver.smt.list(vec![
1757        solver.smt.atom("ite"),
1758        solver.smt.list(vec![
1759            solver.smt.atom("not"),
1760            solver.smt.eq(
1761                sy4,
1762                solver.smt.list(vec![
1763                    solver.smt.atoms().und,
1764                    solver.smt.atom("bv4294967295"),
1765                    solver.smt.numeral(32),
1766                ]),
1767            ),
1768        ]),
1769        solver.smt.eq(sret4, sret3),
1770        solver.smt.eq(
1771            sret4,
1772            solver.smt.list(vec![
1773                solver.smt.atom("bvadd"),
1774                sret3,
1775                solver.smt.list(vec![
1776                    solver.smt.atoms().und,
1777                    solver.smt.atom("bv4"),
1778                    solver.smt.numeral(32),
1779                ]),
1780            ]),
1781        ),
1782    ]));
1783    solver.assume(solver.smt.list(vec![
1784        solver.smt.atom("ite"),
1785        solver.smt.list(vec![
1786            solver.smt.atom("not"),
1787            solver.smt.eq(
1788                sy4,
1789                solver.smt.list(vec![
1790                    solver.smt.atoms().und,
1791                    solver.smt.atom("bv4294967295"),
1792                    solver.smt.numeral(32),
1793                ]),
1794            ),
1795        ]),
1796        solver.smt.eq(sx4, sy4),
1797        solver.smt.eq(sx4, sx8),
1798    ]));
1799    // round 4
1800    let sret5 = solver.declare(
1801        format!("sret5_{id}", id = id),
1802        solver.smt.list(vec![
1803            solver.smt.atoms().und,
1804            solver.smt.atom("BitVec"),
1805            solver.smt.numeral(32),
1806        ]),
1807    );
1808    let sy2 = solver.declare(
1809        format!("sy2_{id}", id = id),
1810        solver.smt.list(vec![
1811            solver.smt.atoms().und,
1812            solver.smt.atom("BitVec"),
1813            solver.smt.numeral(32),
1814        ]),
1815    );
1816    let sx2 = solver.declare(
1817        format!("sx2_{id}", id = id),
1818        solver.smt.list(vec![
1819            solver.smt.atoms().und,
1820            solver.smt.atom("BitVec"),
1821            solver.smt.numeral(32),
1822        ]),
1823    );
1824    solver.assume(
1825        solver
1826            .smt
1827            .eq(sy2, solver.smt.bvashr(sx4, solver.smt.atom("#x00000002"))),
1828    );
1829    solver.assume(solver.smt.list(vec![
1830        solver.smt.atom("ite"),
1831        solver.smt.list(vec![
1832            solver.smt.atom("not"),
1833            solver.smt.eq(
1834                sy2,
1835                solver.smt.list(vec![
1836                    solver.smt.atoms().und,
1837                    solver.smt.atom("bv4294967295"),
1838                    solver.smt.numeral(32),
1839                ]),
1840            ),
1841        ]),
1842        solver.smt.eq(sret5, sret4),
1843        solver.smt.eq(
1844            sret5,
1845            solver.smt.list(vec![
1846                solver.smt.atom("bvadd"),
1847                sret4,
1848                solver.smt.list(vec![
1849                    solver.smt.atoms().und,
1850                    solver.smt.atom("bv2"),
1851                    solver.smt.numeral(32),
1852                ]),
1853            ]),
1854        ),
1855    ]));
1856    solver.assume(solver.smt.list(vec![
1857        solver.smt.atom("ite"),
1858        solver.smt.list(vec![
1859            solver.smt.atom("not"),
1860            solver.smt.eq(
1861                sy2,
1862                solver.smt.list(vec![
1863                    solver.smt.atoms().und,
1864                    solver.smt.atom("bv4294967295"),
1865                    solver.smt.numeral(32),
1866                ]),
1867            ),
1868        ]),
1869        solver.smt.eq(sx2, sy2),
1870        solver.smt.eq(sx2, sx4),
1871    ]));
1872    // round 5
1873    let sret6 = solver.declare(
1874        format!("sret6_{id}", id = id),
1875        solver.smt.list(vec![
1876            solver.smt.atoms().und,
1877            solver.smt.atom("BitVec"),
1878            solver.smt.numeral(32),
1879        ]),
1880    );
1881    let sy1 = solver.declare(
1882        format!("sy1_{id}", id = id),
1883        solver.smt.list(vec![
1884            solver.smt.atoms().und,
1885            solver.smt.atom("BitVec"),
1886            solver.smt.numeral(32),
1887        ]),
1888    );
1889    let sx1 = solver.declare(
1890        format!("sx1_{id}", id = id),
1891        solver.smt.list(vec![
1892            solver.smt.atoms().und,
1893            solver.smt.atom("BitVec"),
1894            solver.smt.numeral(32),
1895        ]),
1896    );
1897    solver.assume(
1898        solver
1899            .smt
1900            .eq(sy1, solver.smt.bvashr(sx2, solver.smt.atom("#x00000001"))),
1901    );
1902    solver.assume(solver.smt.list(vec![
1903        solver.smt.atom("ite"),
1904        solver.smt.list(vec![
1905            solver.smt.atom("not"),
1906            solver.smt.eq(
1907                sy1,
1908                solver.smt.list(vec![
1909                    solver.smt.atoms().und,
1910                    solver.smt.atom("bv4294967295"),
1911                    solver.smt.numeral(32),
1912                ]),
1913            ),
1914        ]),
1915        solver.smt.eq(sret6, sret5),
1916        solver.smt.eq(
1917            sret6,
1918            solver.smt.list(vec![
1919                solver.smt.atom("bvadd"),
1920                sret5,
1921                solver.smt.list(vec![
1922                    solver.smt.atoms().und,
1923                    solver.smt.atom("bv1"),
1924                    solver.smt.numeral(32),
1925                ]),
1926            ]),
1927        ),
1928    ]));
1929    solver.assume(solver.smt.list(vec![
1930        solver.smt.atom("ite"),
1931        solver.smt.list(vec![
1932            solver.smt.atom("not"),
1933            solver.smt.eq(
1934                sy1,
1935                solver.smt.list(vec![
1936                    solver.smt.atoms().und,
1937                    solver.smt.atom("bv4294967295"),
1938                    solver.smt.numeral(32),
1939                ]),
1940            ),
1941        ]),
1942        solver.smt.eq(sx1, sy1),
1943        solver.smt.eq(sx1, sx2),
1944    ]));
1945    // last round
1946    let sret7 = solver.declare(
1947        format!("sret7_{id}", id = id),
1948        solver.smt.list(vec![
1949            solver.smt.atoms().und,
1950            solver.smt.atom("BitVec"),
1951            solver.smt.numeral(32),
1952        ]),
1953    );
1954    solver.assume(solver.smt.list(vec![
1955        solver.smt.atom("ite"),
1956        solver.smt.list(vec![
1957            solver.smt.atom("not"),
1958            solver.smt.eq(
1959                sx1,
1960                solver.smt.list(vec![
1961                    solver.smt.atoms().und,
1962                    solver.smt.atom("bv4294967295"),
1963                    solver.smt.numeral(32),
1964                ]),
1965            ),
1966        ]),
1967        solver.smt.eq(sret7, sret6),
1968        solver.smt.eq(
1969            sret7,
1970            solver.smt.list(vec![
1971                solver.smt.atom("bvadd"),
1972                sret6,
1973                solver.smt.list(vec![
1974                    solver.smt.atoms().und,
1975                    solver.smt.atom("bv1"),
1976                    solver.smt.numeral(32),
1977                ]),
1978            ]),
1979        ),
1980    ]));
1981    let clsret = solver.declare(
1982        format!("clsret_{id}", id = id),
1983        solver.smt.list(vec![
1984            solver.smt.atoms().und,
1985            solver.smt.atom("BitVec"),
1986            solver.smt.numeral(32),
1987        ]),
1988    );
1989    solver.assume(solver.smt.list(vec![
1990        solver.smt.atom("ite"),
1991        solver.smt.eq(
1992            sret7,
1993            solver.smt.list(vec![
1994                solver.smt.atoms().und,
1995                solver.smt.atom("bv0"),
1996                solver.smt.numeral(32),
1997            ]),
1998        ),
1999        solver.smt.eq(clsret, sret7),
2000        solver.smt.eq(
2001            clsret,
2002            solver.smt.list(vec![
2003                solver.smt.atom("bvsub"),
2004                sret7,
2005                solver.smt.list(vec![
2006                    solver.smt.atoms().und,
2007                    solver.smt.atom("bv1"),
2008                    solver.smt.numeral(32),
2009                ]),
2010            ]),
2011        ),
2012    ]));
2013    let cls32ret = solver.declare(
2014        format!("cls32ret_{id}", id = id),
2015        solver.smt.list(vec![
2016            solver.smt.atoms().und,
2017            solver.smt.atom("BitVec"),
2018            solver.smt.numeral(32),
2019        ]),
2020    );
2021    solver.assume(solver.smt.list(vec![
2022        solver.smt.atom("ite"),
2023        solver.smt.list(vec![
2024            solver.smt.atom("bvsle"),
2025            solver.smt.list(vec![
2026                solver.smt.atoms().und,
2027                solver.smt.atom("bv0"),
2028                solver.smt.numeral(32),
2029            ]),
2030            x,
2031        ]),
2032        solver.smt.eq(cls32ret, clzret),
2033        solver.smt.eq(cls32ret, clsret),
2034    ]));
2035
2036    if solver.find_widths {
2037        let padding = solver.new_fresh_bits(solver.bitwidth - 32);
2038        solver.smt.concat(padding, cls32ret)
2039    } else {
2040        cls32ret
2041    }
2042}
2043
2044pub fn cls16(solver: &mut SolverCtx, x: SExpr, id: u32) -> SExpr {
2045    let x = solver.smt.extract(15, 0, x);
2046
2047    // Generated code.
2048    // total zeros counter
2049    let zret0 = solver.declare(
2050        format!("zret0_{id}", id = id),
2051        solver.smt.list(vec![
2052            solver.smt.atoms().und,
2053            solver.smt.atom("BitVec"),
2054            solver.smt.numeral(16),
2055        ]),
2056    );
2057    solver.assume(solver.smt.eq(
2058        zret0,
2059        solver.smt.list(vec![
2060            solver.smt.atoms().und,
2061            solver.smt.atom("bv0"),
2062            solver.smt.numeral(16),
2063        ]),
2064    ));
2065    // round 1
2066    let zret3 = solver.declare(
2067        format!("zret3_{id}", id = id),
2068        solver.smt.list(vec![
2069            solver.smt.atoms().und,
2070            solver.smt.atom("BitVec"),
2071            solver.smt.numeral(16),
2072        ]),
2073    );
2074    let zy8 = solver.declare(
2075        format!("zy8_{id}", id = id),
2076        solver.smt.list(vec![
2077            solver.smt.atoms().und,
2078            solver.smt.atom("BitVec"),
2079            solver.smt.numeral(16),
2080        ]),
2081    );
2082    let zx8 = solver.declare(
2083        format!("zx8_{id}", id = id),
2084        solver.smt.list(vec![
2085            solver.smt.atoms().und,
2086            solver.smt.atom("BitVec"),
2087            solver.smt.numeral(16),
2088        ]),
2089    );
2090    solver.assume(
2091        solver
2092            .smt
2093            .eq(zy8, solver.smt.bvlshr(x, solver.smt.atom("#x0008"))),
2094    );
2095    solver.assume(solver.smt.list(vec![
2096        solver.smt.atom("ite"),
2097        solver.smt.list(vec![
2098            solver.smt.atom("not"),
2099            solver.smt.eq(
2100                zy8,
2101                solver.smt.list(vec![
2102                    solver.smt.atoms().und,
2103                    solver.smt.atom("bv0"),
2104                    solver.smt.numeral(16),
2105                ]),
2106            ),
2107        ]),
2108        solver.smt.eq(zret3, zret0),
2109        solver.smt.eq(
2110            zret3,
2111            solver.smt.list(vec![
2112                solver.smt.atom("bvadd"),
2113                zret0,
2114                solver.smt.list(vec![
2115                    solver.smt.atoms().und,
2116                    solver.smt.atom("bv8"),
2117                    solver.smt.numeral(16),
2118                ]),
2119            ]),
2120        ),
2121    ]));
2122    solver.assume(solver.smt.list(vec![
2123        solver.smt.atom("ite"),
2124        solver.smt.list(vec![
2125            solver.smt.atom("not"),
2126            solver.smt.eq(
2127                zy8,
2128                solver.smt.list(vec![
2129                    solver.smt.atoms().und,
2130                    solver.smt.atom("bv0"),
2131                    solver.smt.numeral(16),
2132                ]),
2133            ),
2134        ]),
2135        solver.smt.eq(zx8, zy8),
2136        solver.smt.eq(zx8, x),
2137    ]));
2138    // round 2
2139    let zret4 = solver.declare(
2140        format!("zret4_{id}", id = id),
2141        solver.smt.list(vec![
2142            solver.smt.atoms().und,
2143            solver.smt.atom("BitVec"),
2144            solver.smt.numeral(16),
2145        ]),
2146    );
2147    let zy4 = solver.declare(
2148        format!("zy4_{id}", id = id),
2149        solver.smt.list(vec![
2150            solver.smt.atoms().und,
2151            solver.smt.atom("BitVec"),
2152            solver.smt.numeral(16),
2153        ]),
2154    );
2155    let zx4 = solver.declare(
2156        format!("zx4_{id}", id = id),
2157        solver.smt.list(vec![
2158            solver.smt.atoms().und,
2159            solver.smt.atom("BitVec"),
2160            solver.smt.numeral(16),
2161        ]),
2162    );
2163    solver.assume(
2164        solver
2165            .smt
2166            .eq(zy4, solver.smt.bvlshr(zx8, solver.smt.atom("#x0004"))),
2167    );
2168    solver.assume(solver.smt.list(vec![
2169        solver.smt.atom("ite"),
2170        solver.smt.list(vec![
2171            solver.smt.atom("not"),
2172            solver.smt.eq(
2173                zy4,
2174                solver.smt.list(vec![
2175                    solver.smt.atoms().und,
2176                    solver.smt.atom("bv0"),
2177                    solver.smt.numeral(16),
2178                ]),
2179            ),
2180        ]),
2181        solver.smt.eq(zret4, zret3),
2182        solver.smt.eq(
2183            zret4,
2184            solver.smt.list(vec![
2185                solver.smt.atom("bvadd"),
2186                zret3,
2187                solver.smt.list(vec![
2188                    solver.smt.atoms().und,
2189                    solver.smt.atom("bv4"),
2190                    solver.smt.numeral(16),
2191                ]),
2192            ]),
2193        ),
2194    ]));
2195    solver.assume(solver.smt.list(vec![
2196        solver.smt.atom("ite"),
2197        solver.smt.list(vec![
2198            solver.smt.atom("not"),
2199            solver.smt.eq(
2200                zy4,
2201                solver.smt.list(vec![
2202                    solver.smt.atoms().und,
2203                    solver.smt.atom("bv0"),
2204                    solver.smt.numeral(16),
2205                ]),
2206            ),
2207        ]),
2208        solver.smt.eq(zx4, zy4),
2209        solver.smt.eq(zx4, zx8),
2210    ]));
2211    // round 3
2212    let zret5 = solver.declare(
2213        format!("zret5_{id}", id = id),
2214        solver.smt.list(vec![
2215            solver.smt.atoms().und,
2216            solver.smt.atom("BitVec"),
2217            solver.smt.numeral(16),
2218        ]),
2219    );
2220    let zy2 = solver.declare(
2221        format!("zy2_{id}", id = id),
2222        solver.smt.list(vec![
2223            solver.smt.atoms().und,
2224            solver.smt.atom("BitVec"),
2225            solver.smt.numeral(16),
2226        ]),
2227    );
2228    let zx2 = solver.declare(
2229        format!("zx2_{id}", id = id),
2230        solver.smt.list(vec![
2231            solver.smt.atoms().und,
2232            solver.smt.atom("BitVec"),
2233            solver.smt.numeral(16),
2234        ]),
2235    );
2236    solver.assume(
2237        solver
2238            .smt
2239            .eq(zy2, solver.smt.bvlshr(zx4, solver.smt.atom("#x0002"))),
2240    );
2241    solver.assume(solver.smt.list(vec![
2242        solver.smt.atom("ite"),
2243        solver.smt.list(vec![
2244            solver.smt.atom("not"),
2245            solver.smt.eq(
2246                zy2,
2247                solver.smt.list(vec![
2248                    solver.smt.atoms().und,
2249                    solver.smt.atom("bv0"),
2250                    solver.smt.numeral(16),
2251                ]),
2252            ),
2253        ]),
2254        solver.smt.eq(zret5, zret4),
2255        solver.smt.eq(
2256            zret5,
2257            solver.smt.list(vec![
2258                solver.smt.atom("bvadd"),
2259                zret4,
2260                solver.smt.list(vec![
2261                    solver.smt.atoms().und,
2262                    solver.smt.atom("bv2"),
2263                    solver.smt.numeral(16),
2264                ]),
2265            ]),
2266        ),
2267    ]));
2268    solver.assume(solver.smt.list(vec![
2269        solver.smt.atom("ite"),
2270        solver.smt.list(vec![
2271            solver.smt.atom("not"),
2272            solver.smt.eq(
2273                zy2,
2274                solver.smt.list(vec![
2275                    solver.smt.atoms().und,
2276                    solver.smt.atom("bv0"),
2277                    solver.smt.numeral(16),
2278                ]),
2279            ),
2280        ]),
2281        solver.smt.eq(zx2, zy2),
2282        solver.smt.eq(zx2, zx4),
2283    ]));
2284    // round 4
2285    let zret6 = solver.declare(
2286        format!("zret6_{id}", id = id),
2287        solver.smt.list(vec![
2288            solver.smt.atoms().und,
2289            solver.smt.atom("BitVec"),
2290            solver.smt.numeral(16),
2291        ]),
2292    );
2293    let zy1 = solver.declare(
2294        format!("zy1_{id}", id = id),
2295        solver.smt.list(vec![
2296            solver.smt.atoms().und,
2297            solver.smt.atom("BitVec"),
2298            solver.smt.numeral(16),
2299        ]),
2300    );
2301    let zx1 = solver.declare(
2302        format!("zx1_{id}", id = id),
2303        solver.smt.list(vec![
2304            solver.smt.atoms().und,
2305            solver.smt.atom("BitVec"),
2306            solver.smt.numeral(16),
2307        ]),
2308    );
2309    solver.assume(
2310        solver
2311            .smt
2312            .eq(zy1, solver.smt.bvlshr(zx2, solver.smt.atom("#x0001"))),
2313    );
2314    solver.assume(solver.smt.list(vec![
2315        solver.smt.atom("ite"),
2316        solver.smt.list(vec![
2317            solver.smt.atom("not"),
2318            solver.smt.eq(
2319                zy1,
2320                solver.smt.list(vec![
2321                    solver.smt.atoms().und,
2322                    solver.smt.atom("bv0"),
2323                    solver.smt.numeral(16),
2324                ]),
2325            ),
2326        ]),
2327        solver.smt.eq(zret6, zret5),
2328        solver.smt.eq(
2329            zret6,
2330            solver.smt.list(vec![
2331                solver.smt.atom("bvadd"),
2332                zret5,
2333                solver.smt.list(vec![
2334                    solver.smt.atoms().und,
2335                    solver.smt.atom("bv1"),
2336                    solver.smt.numeral(16),
2337                ]),
2338            ]),
2339        ),
2340    ]));
2341    solver.assume(solver.smt.list(vec![
2342        solver.smt.atom("ite"),
2343        solver.smt.list(vec![
2344            solver.smt.atom("not"),
2345            solver.smt.eq(
2346                zy1,
2347                solver.smt.list(vec![
2348                    solver.smt.atoms().und,
2349                    solver.smt.atom("bv0"),
2350                    solver.smt.numeral(16),
2351                ]),
2352            ),
2353        ]),
2354        solver.smt.eq(zx1, zy1),
2355        solver.smt.eq(zx1, zx2),
2356    ]));
2357    // last round
2358    let zret7 = solver.declare(
2359        format!("zret7_{id}", id = id),
2360        solver.smt.list(vec![
2361            solver.smt.atoms().und,
2362            solver.smt.atom("BitVec"),
2363            solver.smt.numeral(16),
2364        ]),
2365    );
2366    solver.assume(solver.smt.list(vec![
2367        solver.smt.atom("ite"),
2368        solver.smt.list(vec![
2369            solver.smt.atom("not"),
2370            solver.smt.eq(
2371                zx1,
2372                solver.smt.list(vec![
2373                    solver.smt.atoms().und,
2374                    solver.smt.atom("bv0"),
2375                    solver.smt.numeral(16),
2376                ]),
2377            ),
2378        ]),
2379        solver.smt.eq(zret7, zret6),
2380        solver.smt.eq(
2381            zret7,
2382            solver.smt.list(vec![
2383                solver.smt.atom("bvadd"),
2384                zret6,
2385                solver.smt.list(vec![
2386                    solver.smt.atoms().und,
2387                    solver.smt.atom("bv1"),
2388                    solver.smt.numeral(16),
2389                ]),
2390            ]),
2391        ),
2392    ]));
2393    let clzret = solver.declare(
2394        format!("clzret_{id}", id = id),
2395        solver.smt.list(vec![
2396            solver.smt.atoms().und,
2397            solver.smt.atom("BitVec"),
2398            solver.smt.numeral(16),
2399        ]),
2400    );
2401    solver.assume(solver.smt.list(vec![
2402        solver.smt.atom("ite"),
2403        solver.smt.eq(
2404            zret7,
2405            solver.smt.list(vec![
2406                solver.smt.atoms().und,
2407                solver.smt.atom("bv0"),
2408                solver.smt.numeral(16),
2409            ]),
2410        ),
2411        solver.smt.eq(clzret, zret7),
2412        solver.smt.eq(
2413            clzret,
2414            solver.smt.list(vec![
2415                solver.smt.atom("bvsub"),
2416                zret7,
2417                solver.smt.list(vec![
2418                    solver.smt.atoms().und,
2419                    solver.smt.atom("bv1"),
2420                    solver.smt.numeral(16),
2421                ]),
2422            ]),
2423        ),
2424    ]));
2425    // total zeros counter
2426    let sret0 = solver.declare(
2427        format!("sret0_{id}", id = id),
2428        solver.smt.list(vec![
2429            solver.smt.atoms().und,
2430            solver.smt.atom("BitVec"),
2431            solver.smt.numeral(16),
2432        ]),
2433    );
2434    solver.assume(solver.smt.eq(
2435        sret0,
2436        solver.smt.list(vec![
2437            solver.smt.atoms().und,
2438            solver.smt.atom("bv0"),
2439            solver.smt.numeral(16),
2440        ]),
2441    ));
2442    // round 1
2443    let sret3 = solver.declare(
2444        format!("sret3_{id}", id = id),
2445        solver.smt.list(vec![
2446            solver.smt.atoms().und,
2447            solver.smt.atom("BitVec"),
2448            solver.smt.numeral(16),
2449        ]),
2450    );
2451    let sy8 = solver.declare(
2452        format!("sy8_{id}", id = id),
2453        solver.smt.list(vec![
2454            solver.smt.atoms().und,
2455            solver.smt.atom("BitVec"),
2456            solver.smt.numeral(16),
2457        ]),
2458    );
2459    let sx8 = solver.declare(
2460        format!("sx8_{id}", id = id),
2461        solver.smt.list(vec![
2462            solver.smt.atoms().und,
2463            solver.smt.atom("BitVec"),
2464            solver.smt.numeral(16),
2465        ]),
2466    );
2467    solver.assume(
2468        solver
2469            .smt
2470            .eq(sy8, solver.smt.bvashr(x, solver.smt.atom("#x0008"))),
2471    );
2472    solver.assume(solver.smt.list(vec![
2473        solver.smt.atom("ite"),
2474        solver.smt.list(vec![
2475            solver.smt.atom("not"),
2476            solver.smt.eq(
2477                sy8,
2478                solver.smt.list(vec![
2479                    solver.smt.atoms().und,
2480                    solver.smt.atom("bv65535"),
2481                    solver.smt.numeral(16),
2482                ]),
2483            ),
2484        ]),
2485        solver.smt.eq(sret3, sret0),
2486        solver.smt.eq(
2487            sret3,
2488            solver.smt.list(vec![
2489                solver.smt.atom("bvadd"),
2490                sret0,
2491                solver.smt.list(vec![
2492                    solver.smt.atoms().und,
2493                    solver.smt.atom("bv8"),
2494                    solver.smt.numeral(16),
2495                ]),
2496            ]),
2497        ),
2498    ]));
2499    solver.assume(solver.smt.list(vec![
2500        solver.smt.atom("ite"),
2501        solver.smt.list(vec![
2502            solver.smt.atom("not"),
2503            solver.smt.eq(
2504                sy8,
2505                solver.smt.list(vec![
2506                    solver.smt.atoms().und,
2507                    solver.smt.atom("bv65535"),
2508                    solver.smt.numeral(16),
2509                ]),
2510            ),
2511        ]),
2512        solver.smt.eq(sx8, sy8),
2513        solver.smt.eq(sx8, x),
2514    ]));
2515    // round 2
2516    let sret4 = solver.declare(
2517        format!("sret4_{id}", id = id),
2518        solver.smt.list(vec![
2519            solver.smt.atoms().und,
2520            solver.smt.atom("BitVec"),
2521            solver.smt.numeral(16),
2522        ]),
2523    );
2524    let sy4 = solver.declare(
2525        format!("sy4_{id}", id = id),
2526        solver.smt.list(vec![
2527            solver.smt.atoms().und,
2528            solver.smt.atom("BitVec"),
2529            solver.smt.numeral(16),
2530        ]),
2531    );
2532    let sx4 = solver.declare(
2533        format!("sx4_{id}", id = id),
2534        solver.smt.list(vec![
2535            solver.smt.atoms().und,
2536            solver.smt.atom("BitVec"),
2537            solver.smt.numeral(16),
2538        ]),
2539    );
2540    solver.assume(
2541        solver
2542            .smt
2543            .eq(sy4, solver.smt.bvashr(sx8, solver.smt.atom("#x0004"))),
2544    );
2545    solver.assume(solver.smt.list(vec![
2546        solver.smt.atom("ite"),
2547        solver.smt.list(vec![
2548            solver.smt.atom("not"),
2549            solver.smt.eq(
2550                sy4,
2551                solver.smt.list(vec![
2552                    solver.smt.atoms().und,
2553                    solver.smt.atom("bv65535"),
2554                    solver.smt.numeral(16),
2555                ]),
2556            ),
2557        ]),
2558        solver.smt.eq(sret4, sret3),
2559        solver.smt.eq(
2560            sret4,
2561            solver.smt.list(vec![
2562                solver.smt.atom("bvadd"),
2563                sret3,
2564                solver.smt.list(vec![
2565                    solver.smt.atoms().und,
2566                    solver.smt.atom("bv4"),
2567                    solver.smt.numeral(16),
2568                ]),
2569            ]),
2570        ),
2571    ]));
2572    solver.assume(solver.smt.list(vec![
2573        solver.smt.atom("ite"),
2574        solver.smt.list(vec![
2575            solver.smt.atom("not"),
2576            solver.smt.eq(
2577                sy4,
2578                solver.smt.list(vec![
2579                    solver.smt.atoms().und,
2580                    solver.smt.atom("bv65535"),
2581                    solver.smt.numeral(16),
2582                ]),
2583            ),
2584        ]),
2585        solver.smt.eq(sx4, sy4),
2586        solver.smt.eq(sx4, sx8),
2587    ]));
2588    // round 3
2589    let sret5 = solver.declare(
2590        format!("sret5_{id}", id = id),
2591        solver.smt.list(vec![
2592            solver.smt.atoms().und,
2593            solver.smt.atom("BitVec"),
2594            solver.smt.numeral(16),
2595        ]),
2596    );
2597    let sy2 = solver.declare(
2598        format!("sy2_{id}", id = id),
2599        solver.smt.list(vec![
2600            solver.smt.atoms().und,
2601            solver.smt.atom("BitVec"),
2602            solver.smt.numeral(16),
2603        ]),
2604    );
2605    let sx2 = solver.declare(
2606        format!("sx2_{id}", id = id),
2607        solver.smt.list(vec![
2608            solver.smt.atoms().und,
2609            solver.smt.atom("BitVec"),
2610            solver.smt.numeral(16),
2611        ]),
2612    );
2613    solver.assume(
2614        solver
2615            .smt
2616            .eq(sy2, solver.smt.bvashr(sx4, solver.smt.atom("#x0002"))),
2617    );
2618    solver.assume(solver.smt.list(vec![
2619        solver.smt.atom("ite"),
2620        solver.smt.list(vec![
2621            solver.smt.atom("not"),
2622            solver.smt.eq(
2623                sy2,
2624                solver.smt.list(vec![
2625                    solver.smt.atoms().und,
2626                    solver.smt.atom("bv65535"),
2627                    solver.smt.numeral(16),
2628                ]),
2629            ),
2630        ]),
2631        solver.smt.eq(sret5, sret4),
2632        solver.smt.eq(
2633            sret5,
2634            solver.smt.list(vec![
2635                solver.smt.atom("bvadd"),
2636                sret4,
2637                solver.smt.list(vec![
2638                    solver.smt.atoms().und,
2639                    solver.smt.atom("bv2"),
2640                    solver.smt.numeral(16),
2641                ]),
2642            ]),
2643        ),
2644    ]));
2645    solver.assume(solver.smt.list(vec![
2646        solver.smt.atom("ite"),
2647        solver.smt.list(vec![
2648            solver.smt.atom("not"),
2649            solver.smt.eq(
2650                sy2,
2651                solver.smt.list(vec![
2652                    solver.smt.atoms().und,
2653                    solver.smt.atom("bv65535"),
2654                    solver.smt.numeral(16),
2655                ]),
2656            ),
2657        ]),
2658        solver.smt.eq(sx2, sy2),
2659        solver.smt.eq(sx2, sx4),
2660    ]));
2661    // round 4
2662    let sret6 = solver.declare(
2663        format!("sret6_{id}", id = id),
2664        solver.smt.list(vec![
2665            solver.smt.atoms().und,
2666            solver.smt.atom("BitVec"),
2667            solver.smt.numeral(16),
2668        ]),
2669    );
2670    let sy1 = solver.declare(
2671        format!("sy1_{id}", id = id),
2672        solver.smt.list(vec![
2673            solver.smt.atoms().und,
2674            solver.smt.atom("BitVec"),
2675            solver.smt.numeral(16),
2676        ]),
2677    );
2678    let sx1 = solver.declare(
2679        format!("sx1_{id}", id = id),
2680        solver.smt.list(vec![
2681            solver.smt.atoms().und,
2682            solver.smt.atom("BitVec"),
2683            solver.smt.numeral(16),
2684        ]),
2685    );
2686    solver.assume(
2687        solver
2688            .smt
2689            .eq(sy1, solver.smt.bvashr(sx2, solver.smt.atom("#x0001"))),
2690    );
2691    solver.assume(solver.smt.list(vec![
2692        solver.smt.atom("ite"),
2693        solver.smt.list(vec![
2694            solver.smt.atom("not"),
2695            solver.smt.eq(
2696                sy1,
2697                solver.smt.list(vec![
2698                    solver.smt.atoms().und,
2699                    solver.smt.atom("bv65535"),
2700                    solver.smt.numeral(16),
2701                ]),
2702            ),
2703        ]),
2704        solver.smt.eq(sret6, sret5),
2705        solver.smt.eq(
2706            sret6,
2707            solver.smt.list(vec![
2708                solver.smt.atom("bvadd"),
2709                sret5,
2710                solver.smt.list(vec![
2711                    solver.smt.atoms().und,
2712                    solver.smt.atom("bv1"),
2713                    solver.smt.numeral(16),
2714                ]),
2715            ]),
2716        ),
2717    ]));
2718    solver.assume(solver.smt.list(vec![
2719        solver.smt.atom("ite"),
2720        solver.smt.list(vec![
2721            solver.smt.atom("not"),
2722            solver.smt.eq(
2723                sy1,
2724                solver.smt.list(vec![
2725                    solver.smt.atoms().und,
2726                    solver.smt.atom("bv65535"),
2727                    solver.smt.numeral(16),
2728                ]),
2729            ),
2730        ]),
2731        solver.smt.eq(sx1, sy1),
2732        solver.smt.eq(sx1, sx2),
2733    ]));
2734    // last round
2735    let sret7 = solver.declare(
2736        format!("sret7_{id}", id = id),
2737        solver.smt.list(vec![
2738            solver.smt.atoms().und,
2739            solver.smt.atom("BitVec"),
2740            solver.smt.numeral(16),
2741        ]),
2742    );
2743    solver.assume(solver.smt.list(vec![
2744        solver.smt.atom("ite"),
2745        solver.smt.list(vec![
2746            solver.smt.atom("not"),
2747            solver.smt.eq(
2748                sx1,
2749                solver.smt.list(vec![
2750                    solver.smt.atoms().und,
2751                    solver.smt.atom("bv65535"),
2752                    solver.smt.numeral(16),
2753                ]),
2754            ),
2755        ]),
2756        solver.smt.eq(sret7, sret6),
2757        solver.smt.eq(
2758            sret7,
2759            solver.smt.list(vec![
2760                solver.smt.atom("bvadd"),
2761                sret6,
2762                solver.smt.list(vec![
2763                    solver.smt.atoms().und,
2764                    solver.smt.atom("bv1"),
2765                    solver.smt.numeral(16),
2766                ]),
2767            ]),
2768        ),
2769    ]));
2770    let clsret = solver.declare(
2771        format!("clsret_{id}", id = id),
2772        solver.smt.list(vec![
2773            solver.smt.atoms().und,
2774            solver.smt.atom("BitVec"),
2775            solver.smt.numeral(16),
2776        ]),
2777    );
2778    solver.assume(solver.smt.list(vec![
2779        solver.smt.atom("ite"),
2780        solver.smt.eq(
2781            sret7,
2782            solver.smt.list(vec![
2783                solver.smt.atoms().und,
2784                solver.smt.atom("bv0"),
2785                solver.smt.numeral(16),
2786            ]),
2787        ),
2788        solver.smt.eq(clsret, sret7),
2789        solver.smt.eq(
2790            clsret,
2791            solver.smt.list(vec![
2792                solver.smt.atom("bvsub"),
2793                sret7,
2794                solver.smt.list(vec![
2795                    solver.smt.atoms().und,
2796                    solver.smt.atom("bv1"),
2797                    solver.smt.numeral(16),
2798                ]),
2799            ]),
2800        ),
2801    ]));
2802    let cls16ret = solver.declare(
2803        format!("cls16ret_{id}", id = id),
2804        solver.smt.list(vec![
2805            solver.smt.atoms().und,
2806            solver.smt.atom("BitVec"),
2807            solver.smt.numeral(16),
2808        ]),
2809    );
2810    solver.assume(solver.smt.list(vec![
2811        solver.smt.atom("ite"),
2812        solver.smt.list(vec![
2813            solver.smt.atom("bvsle"),
2814            solver.smt.list(vec![
2815                solver.smt.atoms().und,
2816                solver.smt.atom("bv0"),
2817                solver.smt.numeral(16),
2818            ]),
2819            x,
2820        ]),
2821        solver.smt.eq(cls16ret, clzret),
2822        solver.smt.eq(cls16ret, clsret),
2823    ]));
2824
2825    if solver.find_widths {
2826        let padding = solver.new_fresh_bits(solver.bitwidth - 16);
2827        solver.smt.concat(padding, cls16ret)
2828    } else {
2829        cls16ret
2830    }
2831}
2832
2833pub fn cls8(solver: &mut SolverCtx, x: SExpr, id: u32) -> SExpr {
2834    let x = solver.smt.extract(7, 0, x);
2835
2836    // Generated code.
2837    // total zeros counter
2838    let zret0 = solver.declare(
2839        format!("zret0_{id}", id = id),
2840        solver.smt.list(vec![
2841            solver.smt.atoms().und,
2842            solver.smt.atom("BitVec"),
2843            solver.smt.numeral(8),
2844        ]),
2845    );
2846    solver.assume(solver.smt.eq(
2847        zret0,
2848        solver.smt.list(vec![
2849            solver.smt.atoms().und,
2850            solver.smt.atom("bv0"),
2851            solver.smt.numeral(8),
2852        ]),
2853    ));
2854    // round 1
2855    let zret4 = solver.declare(
2856        format!("zret4_{id}", id = id),
2857        solver.smt.list(vec![
2858            solver.smt.atoms().und,
2859            solver.smt.atom("BitVec"),
2860            solver.smt.numeral(8),
2861        ]),
2862    );
2863    let zy4 = solver.declare(
2864        format!("zy4_{id}", id = id),
2865        solver.smt.list(vec![
2866            solver.smt.atoms().und,
2867            solver.smt.atom("BitVec"),
2868            solver.smt.numeral(8),
2869        ]),
2870    );
2871    let zx4 = solver.declare(
2872        format!("zx4_{id}", id = id),
2873        solver.smt.list(vec![
2874            solver.smt.atoms().und,
2875            solver.smt.atom("BitVec"),
2876            solver.smt.numeral(8),
2877        ]),
2878    );
2879    solver.assume(
2880        solver
2881            .smt
2882            .eq(zy4, solver.smt.bvlshr(x, solver.smt.atom("#x04"))),
2883    );
2884    solver.assume(solver.smt.list(vec![
2885        solver.smt.atom("ite"),
2886        solver.smt.list(vec![
2887            solver.smt.atom("not"),
2888            solver.smt.eq(
2889                zy4,
2890                solver.smt.list(vec![
2891                    solver.smt.atoms().und,
2892                    solver.smt.atom("bv0"),
2893                    solver.smt.numeral(8),
2894                ]),
2895            ),
2896        ]),
2897        solver.smt.eq(zret4, zret0),
2898        solver.smt.eq(
2899            zret4,
2900            solver.smt.list(vec![
2901                solver.smt.atom("bvadd"),
2902                zret0,
2903                solver.smt.list(vec![
2904                    solver.smt.atoms().und,
2905                    solver.smt.atom("bv4"),
2906                    solver.smt.numeral(8),
2907                ]),
2908            ]),
2909        ),
2910    ]));
2911    solver.assume(solver.smt.list(vec![
2912        solver.smt.atom("ite"),
2913        solver.smt.list(vec![
2914            solver.smt.atom("not"),
2915            solver.smt.eq(
2916                zy4,
2917                solver.smt.list(vec![
2918                    solver.smt.atoms().und,
2919                    solver.smt.atom("bv0"),
2920                    solver.smt.numeral(8),
2921                ]),
2922            ),
2923        ]),
2924        solver.smt.eq(zx4, zy4),
2925        solver.smt.eq(zx4, x),
2926    ]));
2927    // round 2
2928    let zret5 = solver.declare(
2929        format!("zret5_{id}", id = id),
2930        solver.smt.list(vec![
2931            solver.smt.atoms().und,
2932            solver.smt.atom("BitVec"),
2933            solver.smt.numeral(8),
2934        ]),
2935    );
2936    let zy2 = solver.declare(
2937        format!("zy2_{id}", id = id),
2938        solver.smt.list(vec![
2939            solver.smt.atoms().und,
2940            solver.smt.atom("BitVec"),
2941            solver.smt.numeral(8),
2942        ]),
2943    );
2944    let zx2 = solver.declare(
2945        format!("zx2_{id}", id = id),
2946        solver.smt.list(vec![
2947            solver.smt.atoms().und,
2948            solver.smt.atom("BitVec"),
2949            solver.smt.numeral(8),
2950        ]),
2951    );
2952    solver.assume(
2953        solver
2954            .smt
2955            .eq(zy2, solver.smt.bvlshr(zx4, solver.smt.atom("#x02"))),
2956    );
2957    solver.assume(solver.smt.list(vec![
2958        solver.smt.atom("ite"),
2959        solver.smt.list(vec![
2960            solver.smt.atom("not"),
2961            solver.smt.eq(
2962                zy2,
2963                solver.smt.list(vec![
2964                    solver.smt.atoms().und,
2965                    solver.smt.atom("bv0"),
2966                    solver.smt.numeral(8),
2967                ]),
2968            ),
2969        ]),
2970        solver.smt.eq(zret5, zret4),
2971        solver.smt.eq(
2972            zret5,
2973            solver.smt.list(vec![
2974                solver.smt.atom("bvadd"),
2975                zret4,
2976                solver.smt.list(vec![
2977                    solver.smt.atoms().und,
2978                    solver.smt.atom("bv2"),
2979                    solver.smt.numeral(8),
2980                ]),
2981            ]),
2982        ),
2983    ]));
2984    solver.assume(solver.smt.list(vec![
2985        solver.smt.atom("ite"),
2986        solver.smt.list(vec![
2987            solver.smt.atom("not"),
2988            solver.smt.eq(
2989                zy2,
2990                solver.smt.list(vec![
2991                    solver.smt.atoms().und,
2992                    solver.smt.atom("bv0"),
2993                    solver.smt.numeral(8),
2994                ]),
2995            ),
2996        ]),
2997        solver.smt.eq(zx2, zy2),
2998        solver.smt.eq(zx2, zx4),
2999    ]));
3000    // round 3
3001    let zret6 = solver.declare(
3002        format!("zret6_{id}", id = id),
3003        solver.smt.list(vec![
3004            solver.smt.atoms().und,
3005            solver.smt.atom("BitVec"),
3006            solver.smt.numeral(8),
3007        ]),
3008    );
3009    let zy1 = solver.declare(
3010        format!("zy1_{id}", id = id),
3011        solver.smt.list(vec![
3012            solver.smt.atoms().und,
3013            solver.smt.atom("BitVec"),
3014            solver.smt.numeral(8),
3015        ]),
3016    );
3017    let zx1 = solver.declare(
3018        format!("zx1_{id}", id = id),
3019        solver.smt.list(vec![
3020            solver.smt.atoms().und,
3021            solver.smt.atom("BitVec"),
3022            solver.smt.numeral(8),
3023        ]),
3024    );
3025    solver.assume(
3026        solver
3027            .smt
3028            .eq(zy1, solver.smt.bvlshr(zx2, solver.smt.atom("#x01"))),
3029    );
3030    solver.assume(solver.smt.list(vec![
3031        solver.smt.atom("ite"),
3032        solver.smt.list(vec![
3033            solver.smt.atom("not"),
3034            solver.smt.eq(
3035                zy1,
3036                solver.smt.list(vec![
3037                    solver.smt.atoms().und,
3038                    solver.smt.atom("bv0"),
3039                    solver.smt.numeral(8),
3040                ]),
3041            ),
3042        ]),
3043        solver.smt.eq(zret6, zret5),
3044        solver.smt.eq(
3045            zret6,
3046            solver.smt.list(vec![
3047                solver.smt.atom("bvadd"),
3048                zret5,
3049                solver.smt.list(vec![
3050                    solver.smt.atoms().und,
3051                    solver.smt.atom("bv1"),
3052                    solver.smt.numeral(8),
3053                ]),
3054            ]),
3055        ),
3056    ]));
3057    solver.assume(solver.smt.list(vec![
3058        solver.smt.atom("ite"),
3059        solver.smt.list(vec![
3060            solver.smt.atom("not"),
3061            solver.smt.eq(
3062                zy1,
3063                solver.smt.list(vec![
3064                    solver.smt.atoms().und,
3065                    solver.smt.atom("bv0"),
3066                    solver.smt.numeral(8),
3067                ]),
3068            ),
3069        ]),
3070        solver.smt.eq(zx1, zy1),
3071        solver.smt.eq(zx1, zx2),
3072    ]));
3073    // last round
3074    let zret7 = solver.declare(
3075        format!("zret7_{id}", id = id),
3076        solver.smt.list(vec![
3077            solver.smt.atoms().und,
3078            solver.smt.atom("BitVec"),
3079            solver.smt.numeral(8),
3080        ]),
3081    );
3082    solver.assume(solver.smt.list(vec![
3083        solver.smt.atom("ite"),
3084        solver.smt.list(vec![
3085            solver.smt.atom("not"),
3086            solver.smt.eq(
3087                zx1,
3088                solver.smt.list(vec![
3089                    solver.smt.atoms().und,
3090                    solver.smt.atom("bv0"),
3091                    solver.smt.numeral(8),
3092                ]),
3093            ),
3094        ]),
3095        solver.smt.eq(zret7, zret6),
3096        solver.smt.eq(
3097            zret7,
3098            solver.smt.list(vec![
3099                solver.smt.atom("bvadd"),
3100                zret6,
3101                solver.smt.list(vec![
3102                    solver.smt.atoms().und,
3103                    solver.smt.atom("bv1"),
3104                    solver.smt.numeral(8),
3105                ]),
3106            ]),
3107        ),
3108    ]));
3109    let clzret = solver.declare(
3110        format!("clzret_{id}", id = id),
3111        solver.smt.list(vec![
3112            solver.smt.atoms().und,
3113            solver.smt.atom("BitVec"),
3114            solver.smt.numeral(8),
3115        ]),
3116    );
3117    solver.assume(solver.smt.list(vec![
3118        solver.smt.atom("ite"),
3119        solver.smt.eq(
3120            zret7,
3121            solver.smt.list(vec![
3122                solver.smt.atoms().und,
3123                solver.smt.atom("bv0"),
3124                solver.smt.numeral(8),
3125            ]),
3126        ),
3127        solver.smt.eq(clzret, zret7),
3128        solver.smt.eq(
3129            clzret,
3130            solver.smt.list(vec![
3131                solver.smt.atom("bvsub"),
3132                zret7,
3133                solver.smt.list(vec![
3134                    solver.smt.atoms().und,
3135                    solver.smt.atom("bv1"),
3136                    solver.smt.numeral(8),
3137                ]),
3138            ]),
3139        ),
3140    ]));
3141    // total zeros counter
3142    let sret0 = solver.declare(
3143        format!("sret0_{id}", id = id),
3144        solver.smt.list(vec![
3145            solver.smt.atoms().und,
3146            solver.smt.atom("BitVec"),
3147            solver.smt.numeral(8),
3148        ]),
3149    );
3150    solver.assume(solver.smt.eq(
3151        sret0,
3152        solver.smt.list(vec![
3153            solver.smt.atoms().und,
3154            solver.smt.atom("bv0"),
3155            solver.smt.numeral(8),
3156        ]),
3157    ));
3158    // round 1
3159    let sret4 = solver.declare(
3160        format!("sret4_{id}", id = id),
3161        solver.smt.list(vec![
3162            solver.smt.atoms().und,
3163            solver.smt.atom("BitVec"),
3164            solver.smt.numeral(8),
3165        ]),
3166    );
3167    let sy4 = solver.declare(
3168        format!("sy4_{id}", id = id),
3169        solver.smt.list(vec![
3170            solver.smt.atoms().und,
3171            solver.smt.atom("BitVec"),
3172            solver.smt.numeral(8),
3173        ]),
3174    );
3175    let sx4 = solver.declare(
3176        format!("sx4_{id}", id = id),
3177        solver.smt.list(vec![
3178            solver.smt.atoms().und,
3179            solver.smt.atom("BitVec"),
3180            solver.smt.numeral(8),
3181        ]),
3182    );
3183    solver.assume(
3184        solver
3185            .smt
3186            .eq(sy4, solver.smt.bvashr(x, solver.smt.atom("#x04"))),
3187    );
3188    solver.assume(solver.smt.list(vec![
3189        solver.smt.atom("ite"),
3190        solver.smt.list(vec![
3191            solver.smt.atom("not"),
3192            solver.smt.eq(
3193                sy4,
3194                solver.smt.list(vec![
3195                    solver.smt.atoms().und,
3196                    solver.smt.atom("bv255"),
3197                    solver.smt.numeral(8),
3198                ]),
3199            ),
3200        ]),
3201        solver.smt.eq(sret4, sret0),
3202        solver.smt.eq(
3203            sret4,
3204            solver.smt.list(vec![
3205                solver.smt.atom("bvadd"),
3206                sret0,
3207                solver.smt.list(vec![
3208                    solver.smt.atoms().und,
3209                    solver.smt.atom("bv4"),
3210                    solver.smt.numeral(8),
3211                ]),
3212            ]),
3213        ),
3214    ]));
3215    solver.assume(solver.smt.list(vec![
3216        solver.smt.atom("ite"),
3217        solver.smt.list(vec![
3218            solver.smt.atom("not"),
3219            solver.smt.eq(
3220                sy4,
3221                solver.smt.list(vec![
3222                    solver.smt.atoms().und,
3223                    solver.smt.atom("bv255"),
3224                    solver.smt.numeral(8),
3225                ]),
3226            ),
3227        ]),
3228        solver.smt.eq(sx4, sy4),
3229        solver.smt.eq(sx4, x),
3230    ]));
3231    // round 2
3232    let sret5 = solver.declare(
3233        format!("sret5_{id}", id = id),
3234        solver.smt.list(vec![
3235            solver.smt.atoms().und,
3236            solver.smt.atom("BitVec"),
3237            solver.smt.numeral(8),
3238        ]),
3239    );
3240    let sy2 = solver.declare(
3241        format!("sy2_{id}", id = id),
3242        solver.smt.list(vec![
3243            solver.smt.atoms().und,
3244            solver.smt.atom("BitVec"),
3245            solver.smt.numeral(8),
3246        ]),
3247    );
3248    let sx2 = solver.declare(
3249        format!("sx2_{id}", id = id),
3250        solver.smt.list(vec![
3251            solver.smt.atoms().und,
3252            solver.smt.atom("BitVec"),
3253            solver.smt.numeral(8),
3254        ]),
3255    );
3256    solver.assume(
3257        solver
3258            .smt
3259            .eq(sy2, solver.smt.bvashr(sx4, solver.smt.atom("#x02"))),
3260    );
3261    solver.assume(solver.smt.list(vec![
3262        solver.smt.atom("ite"),
3263        solver.smt.list(vec![
3264            solver.smt.atom("not"),
3265            solver.smt.eq(
3266                sy2,
3267                solver.smt.list(vec![
3268                    solver.smt.atoms().und,
3269                    solver.smt.atom("bv255"),
3270                    solver.smt.numeral(8),
3271                ]),
3272            ),
3273        ]),
3274        solver.smt.eq(sret5, sret4),
3275        solver.smt.eq(
3276            sret5,
3277            solver.smt.list(vec![
3278                solver.smt.atom("bvadd"),
3279                sret4,
3280                solver.smt.list(vec![
3281                    solver.smt.atoms().und,
3282                    solver.smt.atom("bv2"),
3283                    solver.smt.numeral(8),
3284                ]),
3285            ]),
3286        ),
3287    ]));
3288    solver.assume(solver.smt.list(vec![
3289        solver.smt.atom("ite"),
3290        solver.smt.list(vec![
3291            solver.smt.atom("not"),
3292            solver.smt.eq(
3293                sy2,
3294                solver.smt.list(vec![
3295                    solver.smt.atoms().und,
3296                    solver.smt.atom("bv255"),
3297                    solver.smt.numeral(8),
3298                ]),
3299            ),
3300        ]),
3301        solver.smt.eq(sx2, sy2),
3302        solver.smt.eq(sx2, sx4),
3303    ]));
3304    // round 3
3305    let sret6 = solver.declare(
3306        format!("sret6_{id}", id = id),
3307        solver.smt.list(vec![
3308            solver.smt.atoms().und,
3309            solver.smt.atom("BitVec"),
3310            solver.smt.numeral(8),
3311        ]),
3312    );
3313    let sy1 = solver.declare(
3314        format!("sy1_{id}", id = id),
3315        solver.smt.list(vec![
3316            solver.smt.atoms().und,
3317            solver.smt.atom("BitVec"),
3318            solver.smt.numeral(8),
3319        ]),
3320    );
3321    let sx1 = solver.declare(
3322        format!("sx1_{id}", id = id),
3323        solver.smt.list(vec![
3324            solver.smt.atoms().und,
3325            solver.smt.atom("BitVec"),
3326            solver.smt.numeral(8),
3327        ]),
3328    );
3329    solver.assume(
3330        solver
3331            .smt
3332            .eq(sy1, solver.smt.bvashr(sx2, solver.smt.atom("#x01"))),
3333    );
3334    solver.assume(solver.smt.list(vec![
3335        solver.smt.atom("ite"),
3336        solver.smt.list(vec![
3337            solver.smt.atom("not"),
3338            solver.smt.eq(
3339                sy1,
3340                solver.smt.list(vec![
3341                    solver.smt.atoms().und,
3342                    solver.smt.atom("bv255"),
3343                    solver.smt.numeral(8),
3344                ]),
3345            ),
3346        ]),
3347        solver.smt.eq(sret6, sret5),
3348        solver.smt.eq(
3349            sret6,
3350            solver.smt.list(vec![
3351                solver.smt.atom("bvadd"),
3352                sret5,
3353                solver.smt.list(vec![
3354                    solver.smt.atoms().und,
3355                    solver.smt.atom("bv1"),
3356                    solver.smt.numeral(8),
3357                ]),
3358            ]),
3359        ),
3360    ]));
3361    solver.assume(solver.smt.list(vec![
3362        solver.smt.atom("ite"),
3363        solver.smt.list(vec![
3364            solver.smt.atom("not"),
3365            solver.smt.eq(
3366                sy1,
3367                solver.smt.list(vec![
3368                    solver.smt.atoms().und,
3369                    solver.smt.atom("bv255"),
3370                    solver.smt.numeral(8),
3371                ]),
3372            ),
3373        ]),
3374        solver.smt.eq(sx1, sy1),
3375        solver.smt.eq(sx1, sx2),
3376    ]));
3377    // last round
3378    let sret7 = solver.declare(
3379        format!("sret7_{id}", id = id),
3380        solver.smt.list(vec![
3381            solver.smt.atoms().und,
3382            solver.smt.atom("BitVec"),
3383            solver.smt.numeral(8),
3384        ]),
3385    );
3386    solver.assume(solver.smt.list(vec![
3387        solver.smt.atom("ite"),
3388        solver.smt.list(vec![
3389            solver.smt.atom("not"),
3390            solver.smt.eq(
3391                sx1,
3392                solver.smt.list(vec![
3393                    solver.smt.atoms().und,
3394                    solver.smt.atom("bv255"),
3395                    solver.smt.numeral(8),
3396                ]),
3397            ),
3398        ]),
3399        solver.smt.eq(sret7, sret6),
3400        solver.smt.eq(
3401            sret7,
3402            solver.smt.list(vec![
3403                solver.smt.atom("bvadd"),
3404                sret6,
3405                solver.smt.list(vec![
3406                    solver.smt.atoms().und,
3407                    solver.smt.atom("bv1"),
3408                    solver.smt.numeral(8),
3409                ]),
3410            ]),
3411        ),
3412    ]));
3413    let clsret = solver.declare(
3414        format!("clsret_{id}", id = id),
3415        solver.smt.list(vec![
3416            solver.smt.atoms().und,
3417            solver.smt.atom("BitVec"),
3418            solver.smt.numeral(8),
3419        ]),
3420    );
3421    solver.assume(solver.smt.list(vec![
3422        solver.smt.atom("ite"),
3423        solver.smt.eq(
3424            sret7,
3425            solver.smt.list(vec![
3426                solver.smt.atoms().und,
3427                solver.smt.atom("bv0"),
3428                solver.smt.numeral(8),
3429            ]),
3430        ),
3431        solver.smt.eq(clsret, sret7),
3432        solver.smt.eq(
3433            clsret,
3434            solver.smt.list(vec![
3435                solver.smt.atom("bvsub"),
3436                sret7,
3437                solver.smt.list(vec![
3438                    solver.smt.atoms().und,
3439                    solver.smt.atom("bv1"),
3440                    solver.smt.numeral(8),
3441                ]),
3442            ]),
3443        ),
3444    ]));
3445    let cls8ret = solver.declare(
3446        format!("cls8ret_{id}", id = id),
3447        solver.smt.list(vec![
3448            solver.smt.atoms().und,
3449            solver.smt.atom("BitVec"),
3450            solver.smt.numeral(8),
3451        ]),
3452    );
3453    solver.assume(solver.smt.list(vec![
3454        solver.smt.atom("ite"),
3455        solver.smt.list(vec![
3456            solver.smt.atom("bvsle"),
3457            solver.smt.list(vec![
3458                solver.smt.atoms().und,
3459                solver.smt.atom("bv0"),
3460                solver.smt.numeral(8),
3461            ]),
3462            x,
3463        ]),
3464        solver.smt.eq(cls8ret, clzret),
3465        solver.smt.eq(cls8ret, clsret),
3466    ]));
3467
3468    if solver.find_widths {
3469        let padding = solver.new_fresh_bits(solver.bitwidth - 8);
3470        solver.smt.concat(padding, cls8ret)
3471    } else {
3472        cls8ret
3473    }
3474}
3475
3476pub fn cls1(solver: &mut SolverCtx, id: u32) -> SExpr {
3477    // Generated code.
3478    let cls1ret = solver.declare(
3479        format!("cls1ret_{id}", id = id),
3480        solver.smt.list(vec![
3481            solver.smt.atoms().und,
3482            solver.smt.atom("BitVec"),
3483            solver.smt.numeral(1),
3484        ]),
3485    );
3486    solver.assume(solver.smt.eq(
3487        cls1ret,
3488        solver.smt.list(vec![
3489            solver.smt.atoms().und,
3490            solver.smt.atom("bv0"),
3491            solver.smt.numeral(1),
3492        ]),
3493    ));
3494
3495    if solver.find_widths {
3496        let padding = solver.new_fresh_bits(solver.bitwidth - 1);
3497        solver.smt.concat(padding, cls1ret)
3498    } else {
3499        cls1ret
3500    }
3501}
veri_engine_lib/solver/encoded_ops/cls.rs

veri_engine_lib/solver/encoded_ops/
cls.rs
