1 ;;;; the VM definition arithmetic VOPs for the Alpha
3 ;;;; This software is part of the SBCL system. See the README file for
6 ;;;; This software is derived from the CMU CL system, which was
7 ;;;; written at Carnegie Mellon University and released into the
8 ;;;; public domain. The software is in the public domain and is
9 ;;;; provided with absolutely no warranty. See the COPYING and CREDITS
10 ;;;; files for more information.
16 (define-vop (fixnum-unop)
17 (:args (x :scs (any-reg)))
18 (:results (res :scs (any-reg)))
19 (:note "inline fixnum arithmetic")
20 (:arg-types tagged-num)
21 (:result-types tagged-num)
24 (define-vop (signed-unop)
25 (:args (x :scs (signed-reg)))
26 (:results (res :scs (signed-reg)))
27 (:note "inline (signed-byte 32) arithmetic")
28 (:arg-types signed-num)
29 (:result-types signed-num)
32 (define-vop (fast-negate/fixnum fixnum-unop)
35 (inst subq zero-tn x res)))
37 (define-vop (fast-negate/signed signed-unop)
40 (inst subq zero-tn x res)))
42 (define-vop (fast-lognot/fixnum fixnum-unop)
45 (inst eqv x zero-tn res)))
47 (define-vop (fast-lognot/signed signed-unop)
52 ;;;; binary fixnum operations
54 ;;; Assume that any constant operand is the second arg...
56 (define-vop (fast-fixnum-binop)
57 (:args (x :target r :scs (any-reg))
58 (y :target r :scs (any-reg)))
59 (:arg-types tagged-num tagged-num)
60 (:results (r :scs (any-reg)))
61 (:result-types tagged-num)
62 (:note "inline fixnum arithmetic")
67 (define-vop (fast-unsigned-binop)
68 (:args (x :target r :scs (unsigned-reg))
69 (y :target r :scs (unsigned-reg)))
70 (:arg-types unsigned-num unsigned-num)
71 (:results (r :scs (unsigned-reg)))
72 (:result-types unsigned-num)
73 (:note "inline (unsigned-byte 32) arithmetic")
78 (define-vop (fast-signed-binop)
79 (:args (x :target r :scs (signed-reg))
80 (y :target r :scs (signed-reg)))
81 (:arg-types signed-num signed-num)
82 (:results (r :scs (signed-reg)))
83 (:result-types signed-num)
84 (:note "inline (signed-byte 32) arithmetic")
89 (define-vop (fast-fixnum-c-binop fast-fixnum-binop)
90 (:args (x :target r :scs (any-reg)))
92 (:arg-types tagged-num (:constant integer)))
94 (define-vop (fast-signed-c-binop fast-signed-binop)
95 (:args (x :target r :scs (signed-reg)))
97 (:arg-types tagged-num (:constant integer)))
99 (define-vop (fast-unsigned-c-binop fast-unsigned-binop)
100 (:args (x :target r :scs (unsigned-reg)))
102 (:arg-types tagged-num (:constant integer)))
104 (defmacro define-binop (translate cost untagged-cost op
105 tagged-type untagged-type)
107 (define-vop (,(symbolicate "FAST-" translate "/FIXNUM=>FIXNUM")
109 (:args (x :target r :scs (any-reg))
110 (y :target r :scs (any-reg)))
111 (:translate ,translate)
112 (:generator ,(1+ cost)
114 (define-vop (,(symbolicate "FAST-" translate "/SIGNED=>SIGNED")
116 (:args (x :target r :scs (signed-reg))
117 (y :target r :scs (signed-reg)))
118 (:translate ,translate)
119 (:generator ,(1+ untagged-cost)
121 (define-vop (,(symbolicate "FAST-" translate "/UNSIGNED=>UNSIGNED")
123 (:args (x :target r :scs (unsigned-reg))
124 (y :target r :scs (unsigned-reg)))
125 (:translate ,translate)
126 (:generator ,(1+ untagged-cost)
129 `((define-vop (,(symbolicate "FAST-" translate "-C/FIXNUM=>FIXNUM")
131 (:arg-types tagged-num (:constant ,tagged-type))
132 (:translate ,translate)
134 (inst ,op x (fixnumize y) r)))))
135 ,@(when untagged-type
136 `((define-vop (,(symbolicate "FAST-" translate "-C/SIGNED=>SIGNED")
138 (:arg-types signed-num (:constant ,untagged-type))
139 (:translate ,translate)
140 (:generator ,untagged-cost
142 (define-vop (,(symbolicate "FAST-" translate
143 "-C/UNSIGNED=>UNSIGNED")
144 fast-unsigned-c-binop)
145 (:arg-types unsigned-num (:constant ,untagged-type))
146 (:translate ,translate)
147 (:generator ,untagged-cost
148 (inst ,op x y r)))))))
150 (define-binop + 1 5 addq (unsigned-byte 6) (unsigned-byte 8))
151 (define-binop - 1 5 subq (unsigned-byte 6) (unsigned-byte 8))
152 (define-binop logior 1 3 bis (unsigned-byte 6) (unsigned-byte 8))
153 (define-binop lognor 1 3 ornot (unsigned-byte 6) (unsigned-byte 8))
154 (define-binop logand 1 3 and (unsigned-byte 6) (unsigned-byte 8))
155 (define-binop logxor 1 3 xor (unsigned-byte 6) (unsigned-byte 8))
159 (define-vop (fast-ash)
161 (:args (number :scs (signed-reg unsigned-reg) :to :save)
162 (amount :scs (signed-reg)))
163 (:arg-types (:or signed-num unsigned-num) signed-num)
164 (:results (result :scs (signed-reg unsigned-reg)))
165 (:result-types (:or signed-num unsigned-num))
168 (:temporary (:sc non-descriptor-reg) ndesc)
169 (:temporary (:sc non-descriptor-reg :to :eval) temp)
171 (inst bge amount positive)
172 (inst subq zero-tn amount ndesc)
173 (inst cmplt ndesc 31 temp)
175 (signed-reg (inst sra number ndesc result))
176 (unsigned-reg (inst srl number ndesc result)))
179 (signed-reg (inst sra number 31 result))
180 (unsigned-reg (inst srl number 31 result)))
181 (inst br zero-tn done)
184 ;; The result-type assures us that this shift will not overflow.
185 (inst sll number amount result)
189 (define-vop (fast-ash-c)
193 (:args (number :scs (signed-reg unsigned-reg)))
195 (:arg-types (:or signed-num unsigned-num) (:constant integer))
196 (:results (result :scs (signed-reg unsigned-reg)))
197 (:result-types (:or signed-num unsigned-num))
200 ;; It is a right shift.
202 (signed-reg (inst sra number (- count) result))
203 (unsigned-reg (inst srl number (- count) result))))
205 ;; It is a left shift.
206 (inst sll number count result))
208 ;; Count=0? Shouldn't happen, but it's easy:
209 (move number result)))))
211 (define-vop (signed-byte-32-len)
212 (:translate integer-length)
213 (:note "inline (signed-byte 32) integer-length")
215 (:args (arg :scs (signed-reg) :to (:argument 1)))
216 (:arg-types signed-num)
217 (:results (res :scs (any-reg)))
218 (:result-types positive-fixnum)
219 (:temporary (:scs (non-descriptor-reg) :from (:argument 0)) shift)
222 (inst cmovge arg arg shift)
223 (inst subq zero-tn 4 res)
224 (inst sll shift 1 shift)
226 (inst addq res (fixnumize 1) res)
227 (inst srl shift 1 shift)
228 (inst bne shift loop)))
230 (define-vop (unsigned-byte-32-count)
231 (:translate logcount)
232 (:note "inline (unsigned-byte 32) logcount")
234 (:args (arg :scs (unsigned-reg) :target num))
235 (:arg-types unsigned-num)
236 (:results (res :scs (unsigned-reg)))
237 (:result-types positive-fixnum)
238 (:temporary (:scs (non-descriptor-reg) :from (:argument 0) :to (:result 0)
240 (:temporary (:scs (non-descriptor-reg)) mask temp)
242 (inst li #x55555555 mask)
243 (inst srl arg 1 temp)
244 (inst and arg mask num)
245 (inst and temp mask temp)
246 (inst addq num temp num)
247 (inst li #x33333333 mask)
248 (inst srl num 2 temp)
249 (inst and num mask num)
250 (inst and temp mask temp)
251 (inst addq num temp num)
252 (inst li #x0f0f0f0f mask)
253 (inst srl num 4 temp)
254 (inst and num mask num)
255 (inst and temp mask temp)
256 (inst addq num temp num)
257 (inst li #x00ff00ff mask)
258 (inst srl num 8 temp)
259 (inst and num mask num)
260 (inst and temp mask temp)
261 (inst addq num temp num)
262 (inst li #x0000ffff mask)
263 (inst srl num 16 temp)
264 (inst and num mask num)
265 (inst and temp mask temp)
266 (inst addq num temp res)))
270 (define-vop (fast-*/fixnum=>fixnum fast-fixnum-binop)
271 (:temporary (:scs (non-descriptor-reg)) temp)
275 (inst mulq x temp r)))
277 (define-vop (fast-*/signed=>signed fast-signed-binop)
282 (define-vop (fast-*/unsigned=>unsigned fast-unsigned-binop)
287 ;;;; binary conditional VOPs
289 (define-vop (fast-conditional)
294 (:temporary (:scs (non-descriptor-reg)) temp)
295 (:policy :fast-safe))
297 (define-vop (fast-conditional/fixnum fast-conditional)
298 (:args (x :scs (any-reg))
300 (:arg-types tagged-num tagged-num)
301 (:note "inline fixnum comparison"))
303 (define-vop (fast-conditional-c/fixnum fast-conditional/fixnum)
304 (:args (x :scs (any-reg)))
305 (:arg-types tagged-num (:constant (unsigned-byte-with-a-bite-out 6 4)))
306 (:info target not-p y))
308 (define-vop (fast-conditional/signed fast-conditional)
309 (:args (x :scs (signed-reg))
310 (y :scs (signed-reg)))
311 (:arg-types signed-num signed-num)
312 (:note "inline (signed-byte 32) comparison"))
314 (define-vop (fast-conditional-c/signed fast-conditional/signed)
315 (:args (x :scs (signed-reg)))
316 (:arg-types signed-num (:constant (unsigned-byte-with-a-bite-out 8 1)))
317 (:info target not-p y))
319 (define-vop (fast-conditional/unsigned fast-conditional)
320 (:args (x :scs (unsigned-reg))
321 (y :scs (unsigned-reg)))
322 (:arg-types unsigned-num unsigned-num)
323 (:note "inline (unsigned-byte 32) comparison"))
325 (define-vop (fast-conditional-c/unsigned fast-conditional/unsigned)
326 (:args (x :scs (unsigned-reg)))
327 (:arg-types unsigned-num (:constant (unsigned-byte-with-a-bite-out 8 1)))
328 (:info target not-p y))
331 (defmacro define-conditional-vop (translate &rest generator)
333 ,@(mapcar (lambda (suffix cost signed)
334 (unless (and (member suffix '(/fixnum -c/fixnum))
336 `(define-vop (,(intern (format nil "~:@(FAST-IF-~A~A~)"
339 (format nil "~:@(FAST-CONDITIONAL~A~)"
341 (:translate ,translate)
343 (let* ((signed ,signed)
344 (-c/fixnum ,(eq suffix '-c/fixnum))
345 (y (if -c/fixnum (fixnumize y) y)))
347 '(/fixnum -c/fixnum /signed -c/signed /unsigned -c/unsigned)
349 '(t t t t nil nil))))
351 (define-conditional-vop <
352 (cond ((and signed (eql y 0))
355 (inst blt x target)))
358 (inst cmplt x y temp)
359 (inst cmpult x y temp))
361 (inst beq temp target)
362 (inst bne temp target)))))
364 (define-conditional-vop >
365 (cond ((and signed (eql y 0))
368 (inst bgt x target)))
370 (let ((y (+ y (if -c/fixnum (fixnumize 1) 1))))
372 (inst cmplt x y temp)
373 (inst cmpult x y temp))
375 (inst bne temp target)
376 (inst beq temp target))))
379 (inst cmplt y x temp)
380 (inst cmpult y x temp))
382 (inst beq temp target)
383 (inst bne temp target)))))
385 ;;; EQL/FIXNUM is funny because the first arg can be of any type, not
386 ;;; just a known fixnum.
388 (define-conditional-vop eql
389 (declare (ignore signed))
393 (inst cmpeq x y temp)
395 (inst beq temp target)
396 (inst bne temp target)))
398 ;;; These versions specify a fixnum restriction on their first arg. We
399 ;;; have also generic-eql/fixnum VOPs which are the same, but have no
400 ;;; restriction on the first arg and a higher cost. The reason for
401 ;;; doing this is to prevent fixnum specific operations from being
402 ;;; used on word integers, spuriously consing the argument.
403 (define-vop (fast-eql/fixnum fast-conditional)
404 (:args (x :scs (any-reg))
406 (:arg-types tagged-num tagged-num)
407 (:note "inline fixnum comparison")
410 (cond ((equal y zero-tn)
413 (inst beq x target)))
415 (inst cmpeq x y temp)
417 (inst beq temp target)
418 (inst bne temp target))))))
421 (define-vop (generic-eql/fixnum fast-eql/fixnum)
422 (:args (x :scs (any-reg descriptor-reg))
424 (:arg-types * tagged-num)
427 (define-vop (fast-eql-c/fixnum fast-conditional/fixnum)
428 (:args (x :scs (any-reg)))
429 (:arg-types tagged-num (:constant (signed-byte 6)))
430 (:temporary (:scs (non-descriptor-reg)) temp)
431 (:info target not-p y)
434 (let ((y (cond ((eql y 0) zero-tn)
436 (inst li (fixnumize y) temp)
438 (inst cmpeq x y temp)
440 (inst beq temp target)
441 (inst bne temp target)))))
443 (define-vop (generic-eql-c/fixnum fast-eql-c/fixnum)
444 (:args (x :scs (any-reg descriptor-reg)))
445 (:arg-types * (:constant (signed-byte 6)))
449 ;;;; 32-bit logical operations
451 (define-vop (merge-bits)
452 (:translate merge-bits)
453 (:args (shift :scs (signed-reg unsigned-reg))
454 (prev :scs (unsigned-reg))
455 (next :scs (unsigned-reg)))
456 (:arg-types tagged-num unsigned-num unsigned-num)
457 (:temporary (:scs (unsigned-reg) :to (:result 0)) temp)
458 (:temporary (:scs (unsigned-reg) :to (:result 0) :target result) res)
459 (:results (result :scs (unsigned-reg)))
460 (:result-types unsigned-num)
463 (let ((done (gen-label)))
464 (inst srl next shift res)
465 (inst beq shift done)
466 (inst subq zero-tn shift temp)
467 (inst sll prev temp temp)
468 (inst bis res temp res)
473 (define-vop (32bit-logical)
474 (:args (x :scs (unsigned-reg))
475 (y :scs (unsigned-reg)))
476 (:arg-types unsigned-num unsigned-num)
477 (:results (r :scs (unsigned-reg)))
478 (:result-types unsigned-num)
479 (:policy :fast-safe))
481 (define-vop (32bit-logical-not 32bit-logical)
482 (:translate 32bit-logical-not)
483 (:args (x :scs (unsigned-reg)))
484 (:arg-types unsigned-num)
489 (define-vop (32bit-logical-and 32bit-logical)
490 (:translate 32bit-logical-and)
494 (deftransform 32bit-logical-nand ((x y) (* *))
495 '(32bit-logical-not (32bit-logical-and x y)))
497 (define-vop (32bit-logical-or 32bit-logical)
498 (:translate 32bit-logical-or)
502 (define-vop (32bit-logical-nor 32bit-logical)
503 (:translate 32bit-logical-nor)
508 (define-vop (32bit-logical-xor 32bit-logical)
509 (:translate 32bit-logical-xor)
513 (deftransform 32bit-logical-eqv ((x y) (* *))
514 '(32bit-logical-not (32bit-logical-xor x y)))
516 (deftransform 32bit-logical-andc1 ((x y) (* *))
517 '(32bit-logical-and (32bit-logical-not x) y))
519 (deftransform 32bit-logical-andc2 ((x y) (* *))
520 '(32bit-logical-and x (32bit-logical-not y)))
522 (deftransform 32bit-logical-orc1 ((x y) (* *))
523 '(32bit-logical-or (32bit-logical-not x) y))
525 (deftransform 32bit-logical-orc2 ((x y) (* *))
526 '(32bit-logical-or x (32bit-logical-not y)))
529 (define-vop (shift-towards-someplace)
531 (:args (num :scs (unsigned-reg))
532 (amount :scs (signed-reg)))
533 (:arg-types unsigned-num tagged-num)
534 (:results (r :scs (unsigned-reg)))
535 (:result-types unsigned-num))
537 (define-vop (shift-towards-start shift-towards-someplace)
538 (:translate shift-towards-start)
539 (:note "SHIFT-TOWARDS-START")
540 (:temporary (:sc non-descriptor-reg) temp)
542 (inst and amount #x1f temp)
543 (inst srl num temp r)))
545 (define-vop (shift-towards-end shift-towards-someplace)
546 (:translate shift-towards-end)
547 (:note "SHIFT-TOWARDS-END")
548 (:temporary (:sc non-descriptor-reg) temp)
550 (inst and amount #x1f temp)
551 (inst sll num temp r)))
555 (define-vop (bignum-length get-header-data)
556 (:translate sb!bignum::%bignum-length)
557 (:policy :fast-safe))
559 (define-vop (bignum-set-length set-header-data)
560 (:translate sb!bignum::%bignum-set-length)
561 (:policy :fast-safe))
563 (define-full-reffer bignum-ref * bignum-digits-offset other-pointer-lowtag
564 (unsigned-reg) unsigned-num sb!bignum::%bignum-ref)
566 (define-full-setter bignum-set * bignum-digits-offset other-pointer-lowtag
567 (unsigned-reg) unsigned-num sb!bignum::%bignum-set #!+gengc nil)
569 (define-vop (digit-0-or-plus)
570 (:translate sb!bignum::%digit-0-or-plusp)
572 (:args (digit :scs (unsigned-reg)))
573 (:arg-types unsigned-num)
574 (:temporary (:sc non-descriptor-reg) temp)
578 (inst sll digit 32 temp)
580 (inst blt temp target)
581 (inst bge temp target))))
583 (define-vop (add-w/carry)
584 (:translate sb!bignum::%add-with-carry)
586 (:args (a :scs (unsigned-reg))
587 (b :scs (unsigned-reg))
588 (c :scs (unsigned-reg)))
589 (:arg-types unsigned-num unsigned-num positive-fixnum)
590 (:results (result :scs (unsigned-reg) :from :load)
591 (carry :scs (unsigned-reg) :from :eval))
592 (:result-types unsigned-num positive-fixnum)
594 (inst addq a b result)
595 (inst addq result c result)
596 (inst sra result 32 carry)
597 (inst mskll result 4 result)))
599 (define-vop (sub-w/borrow)
600 (:translate sb!bignum::%subtract-with-borrow)
602 (:args (a :scs (unsigned-reg))
603 (b :scs (unsigned-reg))
604 (c :scs (unsigned-reg)))
605 (:arg-types unsigned-num unsigned-num positive-fixnum)
606 (:results (result :scs (unsigned-reg) :from :load)
607 (borrow :scs (unsigned-reg) :from :eval))
608 (:result-types unsigned-num positive-fixnum)
610 (inst xor c 1 result)
611 (inst subq a result result)
612 (inst subq result b result)
613 (inst srl result 63 borrow)
614 (inst xor borrow 1 borrow)
615 (inst mskll result 4 result)))
617 (define-vop (bignum-mult-and-add-3-arg)
618 (:translate sb!bignum::%multiply-and-add)
620 (:args (x :scs (unsigned-reg))
621 (y :scs (unsigned-reg))
622 (carry-in :scs (unsigned-reg) :to :save))
623 (:arg-types unsigned-num unsigned-num unsigned-num)
624 (:results (hi :scs (unsigned-reg))
625 (lo :scs (unsigned-reg)))
626 (:result-types unsigned-num unsigned-num)
629 (inst addq lo carry-in lo)
631 (inst mskll lo 4 lo)))
634 (define-vop (bignum-mult-and-add-4-arg)
635 (:translate sb!bignum::%multiply-and-add)
637 (:args (x :scs (unsigned-reg))
638 (y :scs (unsigned-reg))
639 (prev :scs (unsigned-reg))
640 (carry-in :scs (unsigned-reg) :to :save))
641 (:arg-types unsigned-num unsigned-num unsigned-num unsigned-num)
642 (:results (hi :scs (unsigned-reg))
643 (lo :scs (unsigned-reg)))
644 (:result-types unsigned-num unsigned-num)
647 (inst addq lo prev lo)
648 (inst addq lo carry-in lo)
650 (inst mskll lo 4 lo)))
652 (define-vop (bignum-mult)
653 (:translate sb!bignum::%multiply)
655 (:args (x :scs (unsigned-reg))
656 (y :scs (unsigned-reg)))
657 (:arg-types unsigned-num unsigned-num)
658 (:results (hi :scs (unsigned-reg))
659 (lo :scs (unsigned-reg)))
660 (:result-types unsigned-num unsigned-num)
664 (inst mskll lo 4 lo)))
666 (define-vop (bignum-lognot)
667 (:translate sb!bignum::%lognot)
669 (:args (x :scs (unsigned-reg)))
670 (:arg-types unsigned-num)
671 (:results (r :scs (unsigned-reg)))
672 (:result-types unsigned-num)
677 (define-vop (fixnum-to-digit)
678 (:translate sb!bignum::%fixnum-to-digit)
680 (:args (fixnum :scs (any-reg)))
681 (:arg-types tagged-num)
682 (:results (digit :scs (unsigned-reg)))
683 (:result-types unsigned-num)
685 (inst sra fixnum 2 digit)))
687 (define-vop (bignum-floor)
688 (:translate sb!bignum::%floor)
690 (:args (num-high :scs (unsigned-reg))
691 (num-low :scs (unsigned-reg))
692 (denom-arg :scs (unsigned-reg) :target denom))
693 (:arg-types unsigned-num unsigned-num unsigned-num)
694 (:temporary (:scs (unsigned-reg) :from (:argument 2)) denom)
695 (:temporary (:scs (unsigned-reg) :from (:eval 0)) temp)
696 (:results (quo :scs (unsigned-reg) :from (:eval 0))
697 (rem :scs (unsigned-reg) :from (:argument 0)))
698 (:result-types unsigned-num unsigned-num)
699 (:generator 325 ; number of inst assuming targeting works.
700 (inst sll num-high 32 rem)
701 (inst bis rem num-low rem)
702 (inst sll denom-arg 32 denom)
703 (inst cmpule denom rem quo)
704 (inst beq quo shift1)
705 (inst subq rem denom rem)
708 (let ((shift2 (gen-label)))
709 (inst srl denom 1 denom)
710 (inst cmpule denom rem temp)
712 (inst beq temp shift2)
713 (inst subq rem denom rem)
715 (emit-label shift2)))))
717 (define-vop (signify-digit)
718 (:translate sb!bignum::%fixnum-digit-with-correct-sign)
720 (:args (digit :scs (unsigned-reg) :target res))
721 (:arg-types unsigned-num)
722 (:results (res :scs (any-reg signed-reg)))
723 (:result-types signed-num)
727 (inst sll digit 34 res)
728 (inst sra res 32 res))
730 (inst sll digit 32 res)
731 (inst sra res 32 res)))))
734 (define-vop (digit-ashr)
735 (:translate sb!bignum::%ashr)
737 (:args (digit :scs (unsigned-reg))
738 (count :scs (unsigned-reg)))
739 (:arg-types unsigned-num positive-fixnum)
740 (:results (result :scs (unsigned-reg) :from (:argument 0)))
741 (:result-types unsigned-num)
743 (inst sll digit 32 result)
744 (inst sra result count result)
745 (inst srl result 32 result)))
747 (define-vop (digit-lshr digit-ashr)
748 (:translate sb!bignum::%digit-logical-shift-right)
750 (inst srl digit count result)))
752 (define-vop (digit-ashl digit-ashr)
753 (:translate sb!bignum::%ashl)
755 (inst sll digit count result)))
757 ;;;; static functions
759 (define-static-fun two-arg-gcd (x y) :translate gcd)
760 (define-static-fun two-arg-lcm (x y) :translate lcm)
762 (define-static-fun two-arg-+ (x y) :translate +)
763 (define-static-fun two-arg-- (x y) :translate -)
764 (define-static-fun two-arg-* (x y) :translate *)
765 (define-static-fun two-arg-/ (x y) :translate /)
767 (define-static-fun two-arg-< (x y) :translate <)
768 (define-static-fun two-arg-<= (x y) :translate <=)
769 (define-static-fun two-arg-> (x y) :translate >)
770 (define-static-fun two-arg->= (x y) :translate >=)
771 (define-static-fun two-arg-= (x y) :translate =)
772 (define-static-fun two-arg-/= (x y) :translate /=)
774 (define-static-fun %negate (x) :translate %negate)
776 (define-static-fun two-arg-and (x y) :translate logand)
777 (define-static-fun two-arg-ior (x y) :translate logior)
778 (define-static-fun two-arg-xor (x y) :translate logxor)