veri_engine_lib/solver/encoded_ops/
clz.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 clz64(solver: &mut SolverCtx, x: SExpr, id: u32) -> SExpr {
8    // Generated code.
9    // total zeros counter
10    let ret0 = solver.declare(
11        format!("ret0_{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        ret0,
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 ret1 = solver.declare(
28        format!("ret1_{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 y32 = solver.declare(
36        format!("y32_{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 x32 = solver.declare(
44        format!("x32_{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        y32,
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                y32,
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(ret1, ret0),
69        solver.smt.eq(
70            ret1,
71            solver.smt.list(vec![
72                solver.smt.atom("bvadd"),
73                ret0,
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                y32,
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(x32, y32),
96        solver.smt.eq(x32, x),
97    ]));
98    // round 2
99    let ret2 = solver.declare(
100        format!("ret2_{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 y16 = solver.declare(
108        format!("y16_{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 x16 = solver.declare(
116        format!("x16_{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            y16,
126            solver
127                .smt
128                .bvlshr(x32, 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                y16,
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(ret2, ret1),
145        solver.smt.eq(
146            ret2,
147            solver.smt.list(vec![
148                solver.smt.atom("bvadd"),
149                ret1,
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                y16,
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(x16, y16),
172        solver.smt.eq(x16, x32),
173    ]));
174    // round 3
175    let ret3 = solver.declare(
176        format!("ret3_{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 y8 = solver.declare(
184        format!("y8_{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 x8 = solver.declare(
192        format!("x8_{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            y8,
202            solver
203                .smt
204                .bvlshr(x16, 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                y8,
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(ret3, ret2),
221        solver.smt.eq(
222            ret3,
223            solver.smt.list(vec![
224                solver.smt.atom("bvadd"),
225                ret2,
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                y8,
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(x8, y8),
248        solver.smt.eq(x8, x16),
249    ]));
250    // round 4
251    let ret4 = solver.declare(
252        format!("ret4_{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 y4 = solver.declare(
260        format!("y4_{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 x4 = solver.declare(
268        format!("x4_{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(solver.smt.eq(
276        y4,
277        solver.smt.bvlshr(x8, solver.smt.atom("#x0000000000000004")),
278    ));
279    solver.assume(solver.smt.list(vec![
280        solver.smt.atom("ite"),
281        solver.smt.list(vec![
282            solver.smt.atom("not"),
283            solver.smt.eq(
284                y4,
285                solver.smt.list(vec![
286                    solver.smt.atoms().und,
287                    solver.smt.atom("bv0"),
288                    solver.smt.numeral(64),
289                ]),
290            ),
291        ]),
292        solver.smt.eq(ret4, ret3),
293        solver.smt.eq(
294            ret4,
295            solver.smt.list(vec![
296                solver.smt.atom("bvadd"),
297                ret3,
298                solver.smt.list(vec![
299                    solver.smt.atoms().und,
300                    solver.smt.atom("bv4"),
301                    solver.smt.numeral(64),
302                ]),
303            ]),
304        ),
305    ]));
306    solver.assume(solver.smt.list(vec![
307        solver.smt.atom("ite"),
308        solver.smt.list(vec![
309            solver.smt.atom("not"),
310            solver.smt.eq(
311                y4,
312                solver.smt.list(vec![
313                    solver.smt.atoms().und,
314                    solver.smt.atom("bv0"),
315                    solver.smt.numeral(64),
316                ]),
317            ),
318        ]),
319        solver.smt.eq(x4, y4),
320        solver.smt.eq(x4, x8),
321    ]));
322    // round 5
323    let ret5 = solver.declare(
324        format!("ret5_{id}", id = id),
325        solver.smt.list(vec![
326            solver.smt.atoms().und,
327            solver.smt.atom("BitVec"),
328            solver.smt.numeral(64),
329        ]),
330    );
331    let y2 = solver.declare(
332        format!("y2_{id}", id = id),
333        solver.smt.list(vec![
334            solver.smt.atoms().und,
335            solver.smt.atom("BitVec"),
336            solver.smt.numeral(64),
337        ]),
338    );
339    let x2 = solver.declare(
340        format!("x2_{id}", id = id),
341        solver.smt.list(vec![
342            solver.smt.atoms().und,
343            solver.smt.atom("BitVec"),
344            solver.smt.numeral(64),
345        ]),
346    );
347    solver.assume(solver.smt.eq(
348        y2,
349        solver.smt.bvlshr(x4, solver.smt.atom("#x0000000000000002")),
350    ));
351    solver.assume(solver.smt.list(vec![
352        solver.smt.atom("ite"),
353        solver.smt.list(vec![
354            solver.smt.atom("not"),
355            solver.smt.eq(
356                y2,
357                solver.smt.list(vec![
358                    solver.smt.atoms().und,
359                    solver.smt.atom("bv0"),
360                    solver.smt.numeral(64),
361                ]),
362            ),
363        ]),
364        solver.smt.eq(ret5, ret4),
365        solver.smt.eq(
366            ret5,
367            solver.smt.list(vec![
368                solver.smt.atom("bvadd"),
369                ret4,
370                solver.smt.list(vec![
371                    solver.smt.atoms().und,
372                    solver.smt.atom("bv2"),
373                    solver.smt.numeral(64),
374                ]),
375            ]),
376        ),
377    ]));
378    solver.assume(solver.smt.list(vec![
379        solver.smt.atom("ite"),
380        solver.smt.list(vec![
381            solver.smt.atom("not"),
382            solver.smt.eq(
383                y2,
384                solver.smt.list(vec![
385                    solver.smt.atoms().und,
386                    solver.smt.atom("bv0"),
387                    solver.smt.numeral(64),
388                ]),
389            ),
390        ]),
391        solver.smt.eq(x2, y2),
392        solver.smt.eq(x2, x4),
393    ]));
394    // round 6
395    let ret6 = solver.declare(
396        format!("ret6_{id}", id = id),
397        solver.smt.list(vec![
398            solver.smt.atoms().und,
399            solver.smt.atom("BitVec"),
400            solver.smt.numeral(64),
401        ]),
402    );
403    let y1 = solver.declare(
404        format!("y1_{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 x1 = solver.declare(
412        format!("x1_{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    solver.assume(solver.smt.eq(
420        y1,
421        solver.smt.bvlshr(x2, solver.smt.atom("#x0000000000000001")),
422    ));
423    solver.assume(solver.smt.list(vec![
424        solver.smt.atom("ite"),
425        solver.smt.list(vec![
426            solver.smt.atom("not"),
427            solver.smt.eq(
428                y1,
429                solver.smt.list(vec![
430                    solver.smt.atoms().und,
431                    solver.smt.atom("bv0"),
432                    solver.smt.numeral(64),
433                ]),
434            ),
435        ]),
436        solver.smt.eq(ret6, ret5),
437        solver.smt.eq(
438            ret6,
439            solver.smt.list(vec![
440                solver.smt.atom("bvadd"),
441                ret5,
442                solver.smt.list(vec![
443                    solver.smt.atoms().und,
444                    solver.smt.atom("bv1"),
445                    solver.smt.numeral(64),
446                ]),
447            ]),
448        ),
449    ]));
450    solver.assume(solver.smt.list(vec![
451        solver.smt.atom("ite"),
452        solver.smt.list(vec![
453            solver.smt.atom("not"),
454            solver.smt.eq(
455                y1,
456                solver.smt.list(vec![
457                    solver.smt.atoms().und,
458                    solver.smt.atom("bv0"),
459                    solver.smt.numeral(64),
460                ]),
461            ),
462        ]),
463        solver.smt.eq(x1, y1),
464        solver.smt.eq(x1, x2),
465    ]));
466
467    // last round
468    let ret7 = solver.declare(
469        format!("ret7_{id}", id = id),
470        solver.smt.list(vec![
471            solver.smt.atoms().und,
472            solver.smt.atom("BitVec"),
473            solver.smt.numeral(64),
474        ]),
475    );
476    solver.assume(solver.smt.list(vec![
477        solver.smt.atom("ite"),
478        solver.smt.list(vec![
479            solver.smt.atom("not"),
480            solver.smt.eq(
481                x1,
482                solver.smt.list(vec![
483                    solver.smt.atoms().und,
484                    solver.smt.atom("bv0"),
485                    solver.smt.numeral(64),
486                ]),
487            ),
488        ]),
489        solver.smt.eq(ret7, ret6),
490        solver.smt.eq(
491            ret7,
492            solver.smt.list(vec![
493                solver.smt.atom("bvadd"),
494                ret6,
495                solver.smt.list(vec![
496                    solver.smt.atoms().und,
497                    solver.smt.atom("bv1"),
498                    solver.smt.numeral(64),
499                ]),
500            ]),
501        ),
502    ]));
503
504    ret7
505}
506
507pub fn clz32(solver: &mut SolverCtx, x: SExpr, id: u32) -> SExpr {
508    let x = solver.smt.extract(31, 0, x);
509
510    // Generated code.
511    // total zeros counter
512    let ret0 = solver.declare(
513        format!("ret0_{id}", id = id),
514        solver.smt.list(vec![
515            solver.smt.atoms().und,
516            solver.smt.atom("BitVec"),
517            solver.smt.numeral(32),
518        ]),
519    );
520    solver.assume(solver.smt.eq(
521        ret0,
522        solver.smt.list(vec![
523            solver.smt.atoms().und,
524            solver.smt.atom("bv0"),
525            solver.smt.numeral(32),
526        ]),
527    ));
528    // round 1
529    let ret1 = solver.declare(
530        format!("ret1_{id}", id = id),
531        solver.smt.list(vec![
532            solver.smt.atoms().und,
533            solver.smt.atom("BitVec"),
534            solver.smt.numeral(32),
535        ]),
536    );
537    let y16 = solver.declare(
538        format!("y16_{id}", id = id),
539        solver.smt.list(vec![
540            solver.smt.atoms().und,
541            solver.smt.atom("BitVec"),
542            solver.smt.numeral(32),
543        ]),
544    );
545    let x16 = solver.declare(
546        format!("x16_{id}", id = id),
547        solver.smt.list(vec![
548            solver.smt.atoms().und,
549            solver.smt.atom("BitVec"),
550            solver.smt.numeral(32),
551        ]),
552    );
553    solver.assume(
554        solver
555            .smt
556            .eq(y16, solver.smt.bvlshr(x, solver.smt.atom("#x00000010"))),
557    );
558    solver.assume(solver.smt.list(vec![
559        solver.smt.atom("ite"),
560        solver.smt.list(vec![
561            solver.smt.atom("not"),
562            solver.smt.eq(
563                y16,
564                solver.smt.list(vec![
565                    solver.smt.atoms().und,
566                    solver.smt.atom("bv0"),
567                    solver.smt.numeral(32),
568                ]),
569            ),
570        ]),
571        solver.smt.eq(ret1, ret0),
572        solver.smt.eq(
573            ret1,
574            solver.smt.list(vec![
575                solver.smt.atom("bvadd"),
576                ret0,
577                solver.smt.list(vec![
578                    solver.smt.atoms().und,
579                    solver.smt.atom("bv16"),
580                    solver.smt.numeral(32),
581                ]),
582            ]),
583        ),
584    ]));
585    solver.assume(solver.smt.list(vec![
586        solver.smt.atom("ite"),
587        solver.smt.list(vec![
588            solver.smt.atom("not"),
589            solver.smt.eq(
590                y16,
591                solver.smt.list(vec![
592                    solver.smt.atoms().und,
593                    solver.smt.atom("bv0"),
594                    solver.smt.numeral(32),
595                ]),
596            ),
597        ]),
598        solver.smt.eq(x16, y16),
599        solver.smt.eq(x16, x),
600    ]));
601    // round 2
602    let ret2 = solver.declare(
603        format!("ret2_{id}", id = id),
604        solver.smt.list(vec![
605            solver.smt.atoms().und,
606            solver.smt.atom("BitVec"),
607            solver.smt.numeral(32),
608        ]),
609    );
610    let y8 = solver.declare(
611        format!("y8_{id}", id = id),
612        solver.smt.list(vec![
613            solver.smt.atoms().und,
614            solver.smt.atom("BitVec"),
615            solver.smt.numeral(32),
616        ]),
617    );
618    let x8 = solver.declare(
619        format!("x8_{id}", id = id),
620        solver.smt.list(vec![
621            solver.smt.atoms().und,
622            solver.smt.atom("BitVec"),
623            solver.smt.numeral(32),
624        ]),
625    );
626    solver.assume(
627        solver
628            .smt
629            .eq(y8, solver.smt.bvlshr(x16, solver.smt.atom("#x00000008"))),
630    );
631    solver.assume(solver.smt.list(vec![
632        solver.smt.atom("ite"),
633        solver.smt.list(vec![
634            solver.smt.atom("not"),
635            solver.smt.eq(
636                y8,
637                solver.smt.list(vec![
638                    solver.smt.atoms().und,
639                    solver.smt.atom("bv0"),
640                    solver.smt.numeral(32),
641                ]),
642            ),
643        ]),
644        solver.smt.eq(ret2, ret1),
645        solver.smt.eq(
646            ret2,
647            solver.smt.list(vec![
648                solver.smt.atom("bvadd"),
649                ret1,
650                solver.smt.list(vec![
651                    solver.smt.atoms().und,
652                    solver.smt.atom("bv8"),
653                    solver.smt.numeral(32),
654                ]),
655            ]),
656        ),
657    ]));
658    solver.assume(solver.smt.list(vec![
659        solver.smt.atom("ite"),
660        solver.smt.list(vec![
661            solver.smt.atom("not"),
662            solver.smt.eq(
663                y8,
664                solver.smt.list(vec![
665                    solver.smt.atoms().und,
666                    solver.smt.atom("bv0"),
667                    solver.smt.numeral(32),
668                ]),
669            ),
670        ]),
671        solver.smt.eq(x8, y8),
672        solver.smt.eq(x8, x16),
673    ]));
674    // round 3
675    let ret3 = solver.declare(
676        format!("ret3_{id}", id = id),
677        solver.smt.list(vec![
678            solver.smt.atoms().und,
679            solver.smt.atom("BitVec"),
680            solver.smt.numeral(32),
681        ]),
682    );
683    let y4 = solver.declare(
684        format!("y4_{id}", id = id),
685        solver.smt.list(vec![
686            solver.smt.atoms().und,
687            solver.smt.atom("BitVec"),
688            solver.smt.numeral(32),
689        ]),
690    );
691    let x4 = solver.declare(
692        format!("x4_{id}", id = id),
693        solver.smt.list(vec![
694            solver.smt.atoms().und,
695            solver.smt.atom("BitVec"),
696            solver.smt.numeral(32),
697        ]),
698    );
699    solver.assume(
700        solver
701            .smt
702            .eq(y4, solver.smt.bvlshr(x8, solver.smt.atom("#x00000004"))),
703    );
704    solver.assume(solver.smt.list(vec![
705        solver.smt.atom("ite"),
706        solver.smt.list(vec![
707            solver.smt.atom("not"),
708            solver.smt.eq(
709                y4,
710                solver.smt.list(vec![
711                    solver.smt.atoms().und,
712                    solver.smt.atom("bv0"),
713                    solver.smt.numeral(32),
714                ]),
715            ),
716        ]),
717        solver.smt.eq(ret3, ret2),
718        solver.smt.eq(
719            ret3,
720            solver.smt.list(vec![
721                solver.smt.atom("bvadd"),
722                ret2,
723                solver.smt.list(vec![
724                    solver.smt.atoms().und,
725                    solver.smt.atom("bv4"),
726                    solver.smt.numeral(32),
727                ]),
728            ]),
729        ),
730    ]));
731    solver.assume(solver.smt.list(vec![
732        solver.smt.atom("ite"),
733        solver.smt.list(vec![
734            solver.smt.atom("not"),
735            solver.smt.eq(
736                y4,
737                solver.smt.list(vec![
738                    solver.smt.atoms().und,
739                    solver.smt.atom("bv0"),
740                    solver.smt.numeral(32),
741                ]),
742            ),
743        ]),
744        solver.smt.eq(x4, y4),
745        solver.smt.eq(x4, x8),
746    ]));
747    // round 4
748    let ret4 = solver.declare(
749        format!("ret4_{id}", id = id),
750        solver.smt.list(vec![
751            solver.smt.atoms().und,
752            solver.smt.atom("BitVec"),
753            solver.smt.numeral(32),
754        ]),
755    );
756    let y2 = solver.declare(
757        format!("y2_{id}", id = id),
758        solver.smt.list(vec![
759            solver.smt.atoms().und,
760            solver.smt.atom("BitVec"),
761            solver.smt.numeral(32),
762        ]),
763    );
764    let x2 = solver.declare(
765        format!("x2_{id}", id = id),
766        solver.smt.list(vec![
767            solver.smt.atoms().und,
768            solver.smt.atom("BitVec"),
769            solver.smt.numeral(32),
770        ]),
771    );
772    solver.assume(
773        solver
774            .smt
775            .eq(y2, solver.smt.bvlshr(x4, solver.smt.atom("#x00000002"))),
776    );
777    solver.assume(solver.smt.list(vec![
778        solver.smt.atom("ite"),
779        solver.smt.list(vec![
780            solver.smt.atom("not"),
781            solver.smt.eq(
782                y2,
783                solver.smt.list(vec![
784                    solver.smt.atoms().und,
785                    solver.smt.atom("bv0"),
786                    solver.smt.numeral(32),
787                ]),
788            ),
789        ]),
790        solver.smt.eq(ret4, ret3),
791        solver.smt.eq(
792            ret4,
793            solver.smt.list(vec![
794                solver.smt.atom("bvadd"),
795                ret3,
796                solver.smt.list(vec![
797                    solver.smt.atoms().und,
798                    solver.smt.atom("bv2"),
799                    solver.smt.numeral(32),
800                ]),
801            ]),
802        ),
803    ]));
804    solver.assume(solver.smt.list(vec![
805        solver.smt.atom("ite"),
806        solver.smt.list(vec![
807            solver.smt.atom("not"),
808            solver.smt.eq(
809                y2,
810                solver.smt.list(vec![
811                    solver.smt.atoms().und,
812                    solver.smt.atom("bv0"),
813                    solver.smt.numeral(32),
814                ]),
815            ),
816        ]),
817        solver.smt.eq(x2, y2),
818        solver.smt.eq(x2, x4),
819    ]));
820    // round 5
821    let ret5 = solver.declare(
822        format!("ret5_{id}", id = id),
823        solver.smt.list(vec![
824            solver.smt.atoms().und,
825            solver.smt.atom("BitVec"),
826            solver.smt.numeral(32),
827        ]),
828    );
829    let y1 = solver.declare(
830        format!("y1_{id}", id = id),
831        solver.smt.list(vec![
832            solver.smt.atoms().und,
833            solver.smt.atom("BitVec"),
834            solver.smt.numeral(32),
835        ]),
836    );
837    let x1 = solver.declare(
838        format!("x1_{id}", id = id),
839        solver.smt.list(vec![
840            solver.smt.atoms().und,
841            solver.smt.atom("BitVec"),
842            solver.smt.numeral(32),
843        ]),
844    );
845    solver.assume(
846        solver
847            .smt
848            .eq(y1, solver.smt.bvlshr(x2, solver.smt.atom("#x00000001"))),
849    );
850    solver.assume(solver.smt.list(vec![
851        solver.smt.atom("ite"),
852        solver.smt.list(vec![
853            solver.smt.atom("not"),
854            solver.smt.eq(
855                y1,
856                solver.smt.list(vec![
857                    solver.smt.atoms().und,
858                    solver.smt.atom("bv0"),
859                    solver.smt.numeral(32),
860                ]),
861            ),
862        ]),
863        solver.smt.eq(ret5, ret4),
864        solver.smt.eq(
865            ret5,
866            solver.smt.list(vec![
867                solver.smt.atom("bvadd"),
868                ret4,
869                solver.smt.list(vec![
870                    solver.smt.atoms().und,
871                    solver.smt.atom("bv1"),
872                    solver.smt.numeral(32),
873                ]),
874            ]),
875        ),
876    ]));
877    solver.assume(solver.smt.list(vec![
878        solver.smt.atom("ite"),
879        solver.smt.list(vec![
880            solver.smt.atom("not"),
881            solver.smt.eq(
882                y1,
883                solver.smt.list(vec![
884                    solver.smt.atoms().und,
885                    solver.smt.atom("bv0"),
886                    solver.smt.numeral(32),
887                ]),
888            ),
889        ]),
890        solver.smt.eq(x1, y1),
891        solver.smt.eq(x1, x2),
892    ]));
893
894    // last round
895    let ret6 = solver.declare(
896        format!("ret6_{id}", id = id),
897        solver.smt.list(vec![
898            solver.smt.atoms().und,
899            solver.smt.atom("BitVec"),
900            solver.smt.numeral(32),
901        ]),
902    );
903    solver.assume(solver.smt.list(vec![
904        solver.smt.atom("ite"),
905        solver.smt.list(vec![
906            solver.smt.atom("not"),
907            solver.smt.eq(
908                x1,
909                solver.smt.list(vec![
910                    solver.smt.atoms().und,
911                    solver.smt.atom("bv0"),
912                    solver.smt.numeral(32),
913                ]),
914            ),
915        ]),
916        solver.smt.eq(ret6, ret5),
917        solver.smt.eq(
918            ret6,
919            solver.smt.list(vec![
920                solver.smt.atom("bvadd"),
921                ret5,
922                solver.smt.list(vec![
923                    solver.smt.atoms().und,
924                    solver.smt.atom("bv1"),
925                    solver.smt.numeral(32),
926                ]),
927            ]),
928        ),
929    ]));
930
931    if solver.find_widths {
932        let padding = solver.new_fresh_bits(solver.bitwidth - 32);
933        solver.smt.concat(padding, ret6)
934    } else {
935        ret6
936    }
937}
938
939pub fn clz16(solver: &mut SolverCtx, x: SExpr, id: u32) -> SExpr {
940    let x = solver.smt.extract(15, 0, x);
941
942    // Generated code.
943    // total zeros counter
944    let ret1 = solver.declare(
945        format!("ret1_{id}", id = id),
946        solver.smt.list(vec![
947            solver.smt.atoms().und,
948            solver.smt.atom("BitVec"),
949            solver.smt.numeral(16),
950        ]),
951    );
952    solver.assume(solver.smt.eq(
953        ret1,
954        solver.smt.list(vec![
955            solver.smt.atoms().und,
956            solver.smt.atom("bv0"),
957            solver.smt.numeral(16),
958        ]),
959    ));
960    // round 1
961    let ret2 = solver.declare(
962        format!("ret2_{id}", id = id),
963        solver.smt.list(vec![
964            solver.smt.atoms().und,
965            solver.smt.atom("BitVec"),
966            solver.smt.numeral(16),
967        ]),
968    );
969    let y8 = solver.declare(
970        format!("y8_{id}", id = id),
971        solver.smt.list(vec![
972            solver.smt.atoms().und,
973            solver.smt.atom("BitVec"),
974            solver.smt.numeral(16),
975        ]),
976    );
977    let x8 = solver.declare(
978        format!("x8_{id}", id = id),
979        solver.smt.list(vec![
980            solver.smt.atoms().und,
981            solver.smt.atom("BitVec"),
982            solver.smt.numeral(16),
983        ]),
984    );
985    solver.assume(
986        solver
987            .smt
988            .eq(y8, solver.smt.bvlshr(x, solver.smt.atom("#x0008"))),
989    );
990    solver.assume(solver.smt.list(vec![
991        solver.smt.atom("ite"),
992        solver.smt.list(vec![
993            solver.smt.atom("not"),
994            solver.smt.eq(
995                y8,
996                solver.smt.list(vec![
997                    solver.smt.atoms().und,
998                    solver.smt.atom("bv0"),
999                    solver.smt.numeral(16),
1000                ]),
1001            ),
1002        ]),
1003        solver.smt.eq(ret2, ret1),
1004        solver.smt.eq(
1005            ret2,
1006            solver.smt.list(vec![
1007                solver.smt.atom("bvadd"),
1008                ret1,
1009                solver.smt.list(vec![
1010                    solver.smt.atoms().und,
1011                    solver.smt.atom("bv8"),
1012                    solver.smt.numeral(16),
1013                ]),
1014            ]),
1015        ),
1016    ]));
1017    solver.assume(solver.smt.list(vec![
1018        solver.smt.atom("ite"),
1019        solver.smt.list(vec![
1020            solver.smt.atom("not"),
1021            solver.smt.eq(
1022                y8,
1023                solver.smt.list(vec![
1024                    solver.smt.atoms().und,
1025                    solver.smt.atom("bv0"),
1026                    solver.smt.numeral(16),
1027                ]),
1028            ),
1029        ]),
1030        solver.smt.eq(x8, y8),
1031        solver.smt.eq(x8, x),
1032    ]));
1033    // round 2
1034    let ret3 = solver.declare(
1035        format!("ret3_{id}", id = id),
1036        solver.smt.list(vec![
1037            solver.smt.atoms().und,
1038            solver.smt.atom("BitVec"),
1039            solver.smt.numeral(16),
1040        ]),
1041    );
1042    let y4 = solver.declare(
1043        format!("y4_{id}", id = id),
1044        solver.smt.list(vec![
1045            solver.smt.atoms().und,
1046            solver.smt.atom("BitVec"),
1047            solver.smt.numeral(16),
1048        ]),
1049    );
1050    let x4 = solver.declare(
1051        format!("x4_{id}", id = id),
1052        solver.smt.list(vec![
1053            solver.smt.atoms().und,
1054            solver.smt.atom("BitVec"),
1055            solver.smt.numeral(16),
1056        ]),
1057    );
1058    solver.assume(
1059        solver
1060            .smt
1061            .eq(y4, solver.smt.bvlshr(x8, solver.smt.atom("#x0004"))),
1062    );
1063    solver.assume(solver.smt.list(vec![
1064        solver.smt.atom("ite"),
1065        solver.smt.list(vec![
1066            solver.smt.atom("not"),
1067            solver.smt.eq(
1068                y4,
1069                solver.smt.list(vec![
1070                    solver.smt.atoms().und,
1071                    solver.smt.atom("bv0"),
1072                    solver.smt.numeral(16),
1073                ]),
1074            ),
1075        ]),
1076        solver.smt.eq(ret3, ret2),
1077        solver.smt.eq(
1078            ret3,
1079            solver.smt.list(vec![
1080                solver.smt.atom("bvadd"),
1081                ret2,
1082                solver.smt.list(vec![
1083                    solver.smt.atoms().und,
1084                    solver.smt.atom("bv4"),
1085                    solver.smt.numeral(16),
1086                ]),
1087            ]),
1088        ),
1089    ]));
1090    solver.assume(solver.smt.list(vec![
1091        solver.smt.atom("ite"),
1092        solver.smt.list(vec![
1093            solver.smt.atom("not"),
1094            solver.smt.eq(
1095                y4,
1096                solver.smt.list(vec![
1097                    solver.smt.atoms().und,
1098                    solver.smt.atom("bv0"),
1099                    solver.smt.numeral(16),
1100                ]),
1101            ),
1102        ]),
1103        solver.smt.eq(x4, y4),
1104        solver.smt.eq(x4, x8),
1105    ]));
1106    // round 3
1107    let ret4 = solver.declare(
1108        format!("ret4_{id}", id = id),
1109        solver.smt.list(vec![
1110            solver.smt.atoms().und,
1111            solver.smt.atom("BitVec"),
1112            solver.smt.numeral(16),
1113        ]),
1114    );
1115    let y2 = solver.declare(
1116        format!("y2_{id}", id = id),
1117        solver.smt.list(vec![
1118            solver.smt.atoms().und,
1119            solver.smt.atom("BitVec"),
1120            solver.smt.numeral(16),
1121        ]),
1122    );
1123    let x2 = solver.declare(
1124        format!("x2_{id}", id = id),
1125        solver.smt.list(vec![
1126            solver.smt.atoms().und,
1127            solver.smt.atom("BitVec"),
1128            solver.smt.numeral(16),
1129        ]),
1130    );
1131    solver.assume(
1132        solver
1133            .smt
1134            .eq(y2, solver.smt.bvlshr(x4, solver.smt.atom("#x0002"))),
1135    );
1136    solver.assume(solver.smt.list(vec![
1137        solver.smt.atom("ite"),
1138        solver.smt.list(vec![
1139            solver.smt.atom("not"),
1140            solver.smt.eq(
1141                y2,
1142                solver.smt.list(vec![
1143                    solver.smt.atoms().und,
1144                    solver.smt.atom("bv0"),
1145                    solver.smt.numeral(16),
1146                ]),
1147            ),
1148        ]),
1149        solver.smt.eq(ret4, ret3),
1150        solver.smt.eq(
1151            ret4,
1152            solver.smt.list(vec![
1153                solver.smt.atom("bvadd"),
1154                ret3,
1155                solver.smt.list(vec![
1156                    solver.smt.atoms().und,
1157                    solver.smt.atom("bv2"),
1158                    solver.smt.numeral(16),
1159                ]),
1160            ]),
1161        ),
1162    ]));
1163    solver.assume(solver.smt.list(vec![
1164        solver.smt.atom("ite"),
1165        solver.smt.list(vec![
1166            solver.smt.atom("not"),
1167            solver.smt.eq(
1168                y2,
1169                solver.smt.list(vec![
1170                    solver.smt.atoms().und,
1171                    solver.smt.atom("bv0"),
1172                    solver.smt.numeral(16),
1173                ]),
1174            ),
1175        ]),
1176        solver.smt.eq(x2, y2),
1177        solver.smt.eq(x2, x4),
1178    ]));
1179    // round 4
1180    let ret5 = solver.declare(
1181        format!("ret5_{id}", id = id),
1182        solver.smt.list(vec![
1183            solver.smt.atoms().und,
1184            solver.smt.atom("BitVec"),
1185            solver.smt.numeral(16),
1186        ]),
1187    );
1188    let y1 = solver.declare(
1189        format!("y1_{id}", id = id),
1190        solver.smt.list(vec![
1191            solver.smt.atoms().und,
1192            solver.smt.atom("BitVec"),
1193            solver.smt.numeral(16),
1194        ]),
1195    );
1196    let x1 = solver.declare(
1197        format!("x1_{id}", id = id),
1198        solver.smt.list(vec![
1199            solver.smt.atoms().und,
1200            solver.smt.atom("BitVec"),
1201            solver.smt.numeral(16),
1202        ]),
1203    );
1204    solver.assume(
1205        solver
1206            .smt
1207            .eq(y1, solver.smt.bvlshr(x2, solver.smt.atom("#x0001"))),
1208    );
1209    solver.assume(solver.smt.list(vec![
1210        solver.smt.atom("ite"),
1211        solver.smt.list(vec![
1212            solver.smt.atom("not"),
1213            solver.smt.eq(
1214                y1,
1215                solver.smt.list(vec![
1216                    solver.smt.atoms().und,
1217                    solver.smt.atom("bv0"),
1218                    solver.smt.numeral(16),
1219                ]),
1220            ),
1221        ]),
1222        solver.smt.eq(ret5, ret4),
1223        solver.smt.eq(
1224            ret5,
1225            solver.smt.list(vec![
1226                solver.smt.atom("bvadd"),
1227                ret4,
1228                solver.smt.list(vec![
1229                    solver.smt.atoms().und,
1230                    solver.smt.atom("bv1"),
1231                    solver.smt.numeral(16),
1232                ]),
1233            ]),
1234        ),
1235    ]));
1236    solver.assume(solver.smt.list(vec![
1237        solver.smt.atom("ite"),
1238        solver.smt.list(vec![
1239            solver.smt.atom("not"),
1240            solver.smt.eq(
1241                y1,
1242                solver.smt.list(vec![
1243                    solver.smt.atoms().und,
1244                    solver.smt.atom("bv0"),
1245                    solver.smt.numeral(16),
1246                ]),
1247            ),
1248        ]),
1249        solver.smt.eq(x1, y1),
1250        solver.smt.eq(x1, x2),
1251    ]));
1252
1253    // last round
1254    let ret6 = solver.declare(
1255        format!("ret6_{id}", id = id),
1256        solver.smt.list(vec![
1257            solver.smt.atoms().und,
1258            solver.smt.atom("BitVec"),
1259            solver.smt.numeral(16),
1260        ]),
1261    );
1262    solver.assume(solver.smt.list(vec![
1263        solver.smt.atom("ite"),
1264        solver.smt.list(vec![
1265            solver.smt.atom("not"),
1266            solver.smt.eq(
1267                x1,
1268                solver.smt.list(vec![
1269                    solver.smt.atoms().und,
1270                    solver.smt.atom("bv0"),
1271                    solver.smt.numeral(16),
1272                ]),
1273            ),
1274        ]),
1275        solver.smt.eq(ret6, ret5),
1276        solver.smt.eq(
1277            ret6,
1278            solver.smt.list(vec![
1279                solver.smt.atom("bvadd"),
1280                ret5,
1281                solver.smt.list(vec![
1282                    solver.smt.atoms().und,
1283                    solver.smt.atom("bv1"),
1284                    solver.smt.numeral(16),
1285                ]),
1286            ]),
1287        ),
1288    ]));
1289
1290    if solver.find_widths {
1291        let padding = solver.new_fresh_bits(solver.bitwidth - 16);
1292        solver.smt.concat(padding, ret6)
1293    } else {
1294        ret6
1295    }
1296}
1297
1298pub fn clz8(solver: &mut SolverCtx, x: SExpr, id: u32) -> SExpr {
1299    let x = solver.smt.extract(7, 0, x);
1300
1301    // Generated code.
1302    // total zeros counter
1303    let ret0 = solver.declare(
1304        format!("ret0_{id}", id = id),
1305        solver.smt.list(vec![
1306            solver.smt.atoms().und,
1307            solver.smt.atom("BitVec"),
1308            solver.smt.numeral(8),
1309        ]),
1310    );
1311    solver.assume(solver.smt.eq(
1312        ret0,
1313        solver.smt.list(vec![
1314            solver.smt.atoms().und,
1315            solver.smt.atom("bv0"),
1316            solver.smt.numeral(8),
1317        ]),
1318    ));
1319    // round 1
1320    let ret3 = solver.declare(
1321        format!("ret3_{id}", id = id),
1322        solver.smt.list(vec![
1323            solver.smt.atoms().und,
1324            solver.smt.atom("BitVec"),
1325            solver.smt.numeral(8),
1326        ]),
1327    );
1328    let y4 = solver.declare(
1329        format!("y4_{id}", id = id),
1330        solver.smt.list(vec![
1331            solver.smt.atoms().und,
1332            solver.smt.atom("BitVec"),
1333            solver.smt.numeral(8),
1334        ]),
1335    );
1336    let x4 = solver.declare(
1337        format!("x4_{id}", id = id),
1338        solver.smt.list(vec![
1339            solver.smt.atoms().und,
1340            solver.smt.atom("BitVec"),
1341            solver.smt.numeral(8),
1342        ]),
1343    );
1344    solver.assume(
1345        solver
1346            .smt
1347            .eq(y4, solver.smt.bvlshr(x, solver.smt.atom("#x04"))),
1348    );
1349    solver.assume(solver.smt.list(vec![
1350        solver.smt.atom("ite"),
1351        solver.smt.list(vec![
1352            solver.smt.atom("not"),
1353            solver.smt.eq(
1354                y4,
1355                solver.smt.list(vec![
1356                    solver.smt.atoms().und,
1357                    solver.smt.atom("bv0"),
1358                    solver.smt.numeral(8),
1359                ]),
1360            ),
1361        ]),
1362        solver.smt.eq(ret3, ret0),
1363        solver.smt.eq(
1364            ret3,
1365            solver.smt.list(vec![
1366                solver.smt.atom("bvadd"),
1367                ret0,
1368                solver.smt.list(vec![
1369                    solver.smt.atoms().und,
1370                    solver.smt.atom("bv4"),
1371                    solver.smt.numeral(8),
1372                ]),
1373            ]),
1374        ),
1375    ]));
1376    solver.assume(solver.smt.list(vec![
1377        solver.smt.atom("ite"),
1378        solver.smt.list(vec![
1379            solver.smt.atom("not"),
1380            solver.smt.eq(
1381                y4,
1382                solver.smt.list(vec![
1383                    solver.smt.atoms().und,
1384                    solver.smt.atom("bv0"),
1385                    solver.smt.numeral(8),
1386                ]),
1387            ),
1388        ]),
1389        solver.smt.eq(x4, y4),
1390        solver.smt.eq(x4, x),
1391    ]));
1392    // round 2
1393    let ret4 = solver.declare(
1394        format!("ret4_{id}", id = id),
1395        solver.smt.list(vec![
1396            solver.smt.atoms().und,
1397            solver.smt.atom("BitVec"),
1398            solver.smt.numeral(8),
1399        ]),
1400    );
1401    let y2 = solver.declare(
1402        format!("y2_{id}", id = id),
1403        solver.smt.list(vec![
1404            solver.smt.atoms().und,
1405            solver.smt.atom("BitVec"),
1406            solver.smt.numeral(8),
1407        ]),
1408    );
1409    let x2 = solver.declare(
1410        format!("x2_{id}", id = id),
1411        solver.smt.list(vec![
1412            solver.smt.atoms().und,
1413            solver.smt.atom("BitVec"),
1414            solver.smt.numeral(8),
1415        ]),
1416    );
1417    solver.assume(
1418        solver
1419            .smt
1420            .eq(y2, solver.smt.bvlshr(x4, solver.smt.atom("#x02"))),
1421    );
1422    solver.assume(solver.smt.list(vec![
1423        solver.smt.atom("ite"),
1424        solver.smt.list(vec![
1425            solver.smt.atom("not"),
1426            solver.smt.eq(
1427                y2,
1428                solver.smt.list(vec![
1429                    solver.smt.atoms().und,
1430                    solver.smt.atom("bv0"),
1431                    solver.smt.numeral(8),
1432                ]),
1433            ),
1434        ]),
1435        solver.smt.eq(ret4, ret3),
1436        solver.smt.eq(
1437            ret4,
1438            solver.smt.list(vec![
1439                solver.smt.atom("bvadd"),
1440                ret3,
1441                solver.smt.list(vec![
1442                    solver.smt.atoms().und,
1443                    solver.smt.atom("bv2"),
1444                    solver.smt.numeral(8),
1445                ]),
1446            ]),
1447        ),
1448    ]));
1449    solver.assume(solver.smt.list(vec![
1450        solver.smt.atom("ite"),
1451        solver.smt.list(vec![
1452            solver.smt.atom("not"),
1453            solver.smt.eq(
1454                y2,
1455                solver.smt.list(vec![
1456                    solver.smt.atoms().und,
1457                    solver.smt.atom("bv0"),
1458                    solver.smt.numeral(8),
1459                ]),
1460            ),
1461        ]),
1462        solver.smt.eq(x2, y2),
1463        solver.smt.eq(x2, x4),
1464    ]));
1465    // round 3
1466    let ret5 = solver.declare(
1467        format!("ret5_{id}", id = id),
1468        solver.smt.list(vec![
1469            solver.smt.atoms().und,
1470            solver.smt.atom("BitVec"),
1471            solver.smt.numeral(8),
1472        ]),
1473    );
1474    let y1 = solver.declare(
1475        format!("y1_{id}", id = id),
1476        solver.smt.list(vec![
1477            solver.smt.atoms().und,
1478            solver.smt.atom("BitVec"),
1479            solver.smt.numeral(8),
1480        ]),
1481    );
1482    let x1 = solver.declare(
1483        format!("x1_{id}", id = id),
1484        solver.smt.list(vec![
1485            solver.smt.atoms().und,
1486            solver.smt.atom("BitVec"),
1487            solver.smt.numeral(8),
1488        ]),
1489    );
1490    solver.assume(
1491        solver
1492            .smt
1493            .eq(y1, solver.smt.bvlshr(x2, solver.smt.atom("#x01"))),
1494    );
1495    solver.assume(solver.smt.list(vec![
1496        solver.smt.atom("ite"),
1497        solver.smt.list(vec![
1498            solver.smt.atom("not"),
1499            solver.smt.eq(
1500                y1,
1501                solver.smt.list(vec![
1502                    solver.smt.atoms().und,
1503                    solver.smt.atom("bv0"),
1504                    solver.smt.numeral(8),
1505                ]),
1506            ),
1507        ]),
1508        solver.smt.eq(ret5, ret4),
1509        solver.smt.eq(
1510            ret5,
1511            solver.smt.list(vec![
1512                solver.smt.atom("bvadd"),
1513                ret4,
1514                solver.smt.list(vec![
1515                    solver.smt.atoms().und,
1516                    solver.smt.atom("bv1"),
1517                    solver.smt.numeral(8),
1518                ]),
1519            ]),
1520        ),
1521    ]));
1522    solver.assume(solver.smt.list(vec![
1523        solver.smt.atom("ite"),
1524        solver.smt.list(vec![
1525            solver.smt.atom("not"),
1526            solver.smt.eq(
1527                y1,
1528                solver.smt.list(vec![
1529                    solver.smt.atoms().und,
1530                    solver.smt.atom("bv0"),
1531                    solver.smt.numeral(8),
1532                ]),
1533            ),
1534        ]),
1535        solver.smt.eq(x1, y1),
1536        solver.smt.eq(x1, x2),
1537    ]));
1538    // last round
1539    let ret6 = solver.declare(
1540        format!("ret6_{id}", id = id),
1541        solver.smt.list(vec![
1542            solver.smt.atoms().und,
1543            solver.smt.atom("BitVec"),
1544            solver.smt.numeral(8),
1545        ]),
1546    );
1547    solver.assume(solver.smt.list(vec![
1548        solver.smt.atom("ite"),
1549        solver.smt.list(vec![
1550            solver.smt.atom("not"),
1551            solver.smt.eq(
1552                x1,
1553                solver.smt.list(vec![
1554                    solver.smt.atoms().und,
1555                    solver.smt.atom("bv0"),
1556                    solver.smt.numeral(8),
1557                ]),
1558            ),
1559        ]),
1560        solver.smt.eq(ret6, ret5),
1561        solver.smt.eq(
1562            ret6,
1563            solver.smt.list(vec![
1564                solver.smt.atom("bvadd"),
1565                ret5,
1566                solver.smt.list(vec![
1567                    solver.smt.atoms().und,
1568                    solver.smt.atom("bv1"),
1569                    solver.smt.numeral(8),
1570                ]),
1571            ]),
1572        ),
1573    ]));
1574
1575    if solver.find_widths {
1576        let padding = solver.new_fresh_bits(solver.bitwidth - 8);
1577        solver.smt.concat(padding, ret6)
1578    } else {
1579        ret6
1580    }
1581}
1582
1583pub fn clz1(solver: &mut SolverCtx, x: SExpr, id: u32) -> SExpr {
1584    let x = solver.smt.extract(0, 0, x);
1585
1586    // Generated code.
1587    let clz1ret = solver.declare(
1588        format!("clz1ret_{id}", id = id),
1589        solver.smt.list(vec![
1590            solver.smt.atoms().und,
1591            solver.smt.atom("BitVec"),
1592            solver.smt.numeral(1),
1593        ]),
1594    );
1595    solver.assume(
1596        solver
1597            .smt
1598            .eq(clz1ret, solver.smt.list(vec![solver.smt.atom("bvnot"), x])),
1599    );
1600
1601    if solver.find_widths {
1602        let padding = solver.new_fresh_bits(solver.bitwidth - 1);
1603        solver.smt.concat(padding, clz1ret)
1604    } else {
1605        clz1ret
1606    }
1607}
veri_engine_lib/solver/encoded_ops/clz.rs

veri_engine_lib/solver/encoded_ops/
clz.rs
