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 (deftype integer-with-a-bite-out (s bite)
298 (cond ((eq s '*) 'integer)
299 ((and (integerp s) (> s 1))
300 (let ((bound (ash 1 s)))
301 `(integer 0 ,(- bound bite 1))))
303 (error "Bad size specified for SIGNED-BYTE type specifier: ~S." s))))
305 (define-vop (fast-conditional/fixnum fast-conditional)
306 (:args (x :scs (any-reg))
308 (:arg-types tagged-num tagged-num)
309 (:note "inline fixnum comparison"))
311 (define-vop (fast-conditional-c/fixnum fast-conditional/fixnum)
312 (:args (x :scs (any-reg)))
313 (:arg-types tagged-num (:constant (integer-with-a-bite-out 6 4)))
314 (:info target not-p y))
316 (define-vop (fast-conditional/signed fast-conditional)
317 (:args (x :scs (signed-reg))
318 (y :scs (signed-reg)))
319 (:arg-types signed-num signed-num)
320 (:note "inline (signed-byte 32) comparison"))
322 (define-vop (fast-conditional-c/signed fast-conditional/signed)
323 (:args (x :scs (signed-reg)))
324 (:arg-types signed-num (:constant (integer-with-a-bite-out 8 1)))
325 (:info target not-p y))
327 (define-vop (fast-conditional/unsigned fast-conditional)
328 (:args (x :scs (unsigned-reg))
329 (y :scs (unsigned-reg)))
330 (:arg-types unsigned-num unsigned-num)
331 (:note "inline (unsigned-byte 32) comparison"))
333 (define-vop (fast-conditional-c/unsigned fast-conditional/unsigned)
334 (:args (x :scs (unsigned-reg)))
335 (:arg-types unsigned-num (:constant (integer-with-a-bite-out 8 1)))
336 (:info target not-p y))
339 (defmacro define-conditional-vop (translate &rest generator)
341 ,@(mapcar #'(lambda (suffix cost signed)
342 (unless (and (member suffix '(/fixnum -c/fixnum))
344 `(define-vop (,(intern (format nil "~:@(FAST-IF-~A~A~)"
347 (format nil "~:@(FAST-CONDITIONAL~A~)"
349 (:translate ,translate)
351 (let* ((signed ,signed)
352 (-c/fixnum ,(eq suffix '-c/fixnum))
353 (y (if -c/fixnum (fixnumize y) y)))
355 '(/fixnum -c/fixnum /signed -c/signed /unsigned -c/unsigned)
357 '(t t t t nil nil))))
359 (define-conditional-vop <
360 (cond ((and signed (eql y 0))
363 (inst blt x target)))
366 (inst cmplt x y temp)
367 (inst cmpult x y temp))
369 (inst beq temp target)
370 (inst bne temp target)))))
372 (define-conditional-vop >
373 (cond ((and signed (eql y 0))
376 (inst bgt x target)))
378 (let ((y (+ y (if -c/fixnum (fixnumize 1) 1))))
380 (inst cmplt x y temp)
381 (inst cmpult x y temp))
383 (inst bne temp target)
384 (inst beq temp target))))
387 (inst cmplt y x temp)
388 (inst cmpult y x temp))
390 (inst beq temp target)
391 (inst bne temp target)))))
393 ;;; EQL/FIXNUM is funny because the first arg can be of any type, not
394 ;;; just a known fixnum.
396 (define-conditional-vop eql
397 (declare (ignore signed))
401 (inst cmpeq x y temp)
403 (inst beq temp target)
404 (inst bne temp target)))
406 ;;; These versions specify a fixnum restriction on their first arg. We
407 ;;; have also generic-eql/fixnum VOPs which are the same, but have no
408 ;;; restriction on the first arg and a higher cost. The reason for
409 ;;; doing this is to prevent fixnum specific operations from being
410 ;;; used on word integers, spuriously consing the argument.
411 (define-vop (fast-eql/fixnum fast-conditional)
412 (:args (x :scs (any-reg))
414 (:arg-types tagged-num tagged-num)
415 (:note "inline fixnum comparison")
418 (cond ((equal y zero-tn)
421 (inst beq x target)))
423 (inst cmpeq x y temp)
425 (inst beq temp target)
426 (inst bne temp target))))))
429 (define-vop (generic-eql/fixnum fast-eql/fixnum)
430 (:args (x :scs (any-reg descriptor-reg))
432 (:arg-types * tagged-num)
435 (define-vop (fast-eql-c/fixnum fast-conditional/fixnum)
436 (:args (x :scs (any-reg)))
437 (:arg-types tagged-num (:constant (signed-byte 6)))
438 (:temporary (:scs (non-descriptor-reg)) temp)
439 (:info target not-p y)
442 (let ((y (cond ((eql y 0) zero-tn)
444 (inst li (fixnumize y) temp)
446 (inst cmpeq x y temp)
448 (inst beq temp target)
449 (inst bne temp target)))))
451 (define-vop (generic-eql-c/fixnum fast-eql-c/fixnum)
452 (:args (x :scs (any-reg descriptor-reg)))
453 (:arg-types * (:constant (signed-byte 6)))
457 ;;;; 32-bit logical operations
459 (define-vop (merge-bits)
460 (:translate merge-bits)
461 (:args (shift :scs (signed-reg unsigned-reg))
462 (prev :scs (unsigned-reg))
463 (next :scs (unsigned-reg)))
464 (:arg-types tagged-num unsigned-num unsigned-num)
465 (:temporary (:scs (unsigned-reg) :to (:result 0)) temp)
466 (:temporary (:scs (unsigned-reg) :to (:result 0) :target result) res)
467 (:results (result :scs (unsigned-reg)))
468 (:result-types unsigned-num)
471 (let ((done (gen-label)))
472 (inst srl next shift res)
473 (inst beq shift done)
474 (inst subq zero-tn shift temp)
475 (inst sll prev temp temp)
476 (inst bis res temp res)
481 (define-vop (32bit-logical)
482 (:args (x :scs (unsigned-reg))
483 (y :scs (unsigned-reg)))
484 (:arg-types unsigned-num unsigned-num)
485 (:results (r :scs (unsigned-reg)))
486 (:result-types unsigned-num)
487 (:policy :fast-safe))
489 (define-vop (32bit-logical-not 32bit-logical)
490 (:translate 32bit-logical-not)
491 (:args (x :scs (unsigned-reg)))
492 (:arg-types unsigned-num)
497 (define-vop (32bit-logical-and 32bit-logical)
498 (:translate 32bit-logical-and)
502 (deftransform 32bit-logical-nand ((x y) (* *))
503 '(32bit-logical-not (32bit-logical-and x y)))
505 (define-vop (32bit-logical-or 32bit-logical)
506 (:translate 32bit-logical-or)
510 (define-vop (32bit-logical-nor 32bit-logical)
511 (:translate 32bit-logical-nor)
516 (define-vop (32bit-logical-xor 32bit-logical)
517 (:translate 32bit-logical-xor)
521 (deftransform 32bit-logical-eqv ((x y) (* *))
522 '(32bit-logical-not (32bit-logical-xor x y)))
524 (deftransform 32bit-logical-andc1 ((x y) (* *))
525 '(32bit-logical-and (32bit-logical-not x) y))
527 (deftransform 32bit-logical-andc2 ((x y) (* *))
528 '(32bit-logical-and x (32bit-logical-not y)))
530 (deftransform 32bit-logical-orc1 ((x y) (* *))
531 '(32bit-logical-or (32bit-logical-not x) y))
533 (deftransform 32bit-logical-orc2 ((x y) (* *))
534 '(32bit-logical-or x (32bit-logical-not y)))
537 (define-vop (shift-towards-someplace)
539 (:args (num :scs (unsigned-reg))
540 (amount :scs (signed-reg)))
541 (:arg-types unsigned-num tagged-num)
542 (:results (r :scs (unsigned-reg)))
543 (:result-types unsigned-num))
545 (define-vop (shift-towards-start shift-towards-someplace)
546 (:translate shift-towards-start)
547 (:note "SHIFT-TOWARDS-START")
548 (:temporary (:sc non-descriptor-reg) temp)
550 (inst and amount #x1f temp)
551 (inst srl num temp r)))
553 (define-vop (shift-towards-end shift-towards-someplace)
554 (:translate shift-towards-end)
555 (:note "SHIFT-TOWARDS-END")
556 (:temporary (:sc non-descriptor-reg) temp)
558 (inst and amount #x1f temp)
559 (inst sll num temp r)))
563 (define-vop (bignum-length get-header-data)
564 (:translate sb!bignum::%bignum-length)
565 (:policy :fast-safe))
567 (define-vop (bignum-set-length set-header-data)
568 (:translate sb!bignum::%bignum-set-length)
569 (:policy :fast-safe))
571 (define-full-reffer bignum-ref * bignum-digits-offset other-pointer-lowtag
572 (unsigned-reg) unsigned-num sb!bignum::%bignum-ref)
574 (define-full-setter bignum-set * bignum-digits-offset other-pointer-lowtag
575 (unsigned-reg) unsigned-num sb!bignum::%bignum-set #+gengc nil)
577 (define-vop (digit-0-or-plus)
578 (:translate sb!bignum::%digit-0-or-plusp)
580 (:args (digit :scs (unsigned-reg)))
581 (:arg-types unsigned-num)
582 (:temporary (:sc non-descriptor-reg) temp)
586 (inst sll digit 32 temp)
588 (inst blt temp target)
589 (inst bge temp target))))
591 (define-vop (add-w/carry)
592 (:translate sb!bignum::%add-with-carry)
594 (:args (a :scs (unsigned-reg))
595 (b :scs (unsigned-reg))
596 (c :scs (unsigned-reg)))
597 (:arg-types unsigned-num unsigned-num positive-fixnum)
598 (:results (result :scs (unsigned-reg) :from :load)
599 (carry :scs (unsigned-reg) :from :eval))
600 (:result-types unsigned-num positive-fixnum)
602 (inst addq a b result)
603 (inst addq result c result)
604 (inst sra result 32 carry)
605 (inst mskll result 4 result)))
607 (define-vop (sub-w/borrow)
608 (:translate sb!bignum::%subtract-with-borrow)
610 (:args (a :scs (unsigned-reg))
611 (b :scs (unsigned-reg))
612 (c :scs (unsigned-reg)))
613 (:arg-types unsigned-num unsigned-num positive-fixnum)
614 (:results (result :scs (unsigned-reg) :from :load)
615 (borrow :scs (unsigned-reg) :from :eval))
616 (:result-types unsigned-num positive-fixnum)
618 (inst xor c 1 result)
619 (inst subq a result result)
620 (inst subq result b result)
621 (inst srl result 63 borrow)
622 (inst xor borrow 1 borrow)
623 (inst mskll result 4 result)))
625 (define-vop (bignum-mult-and-add-3-arg)
626 (:translate sb!bignum::%multiply-and-add)
628 (:args (x :scs (unsigned-reg))
629 (y :scs (unsigned-reg))
630 (carry-in :scs (unsigned-reg) :to :save))
631 (:arg-types unsigned-num unsigned-num unsigned-num)
632 (:results (hi :scs (unsigned-reg))
633 (lo :scs (unsigned-reg)))
634 (:result-types unsigned-num unsigned-num)
637 (inst addq lo carry-in lo)
639 (inst mskll lo 4 lo)))
642 (define-vop (bignum-mult-and-add-4-arg)
643 (:translate sb!bignum::%multiply-and-add)
645 (:args (x :scs (unsigned-reg))
646 (y :scs (unsigned-reg))
647 (prev :scs (unsigned-reg))
648 (carry-in :scs (unsigned-reg) :to :save))
649 (:arg-types unsigned-num unsigned-num unsigned-num unsigned-num)
650 (:results (hi :scs (unsigned-reg))
651 (lo :scs (unsigned-reg)))
652 (:result-types unsigned-num unsigned-num)
655 (inst addq lo prev lo)
656 (inst addq lo carry-in lo)
658 (inst mskll lo 4 lo)))
660 (define-vop (bignum-mult)
661 (:translate sb!bignum::%multiply)
663 (:args (x :scs (unsigned-reg))
664 (y :scs (unsigned-reg)))
665 (:arg-types unsigned-num unsigned-num)
666 (:results (hi :scs (unsigned-reg))
667 (lo :scs (unsigned-reg)))
668 (:result-types unsigned-num unsigned-num)
672 (inst mskll lo 4 lo)))
674 (define-vop (bignum-lognot)
675 (:translate sb!bignum::%lognot)
677 (:args (x :scs (unsigned-reg)))
678 (:arg-types unsigned-num)
679 (:results (r :scs (unsigned-reg)))
680 (:result-types unsigned-num)
685 (define-vop (fixnum-to-digit)
686 (:translate sb!bignum::%fixnum-to-digit)
688 (:args (fixnum :scs (any-reg)))
689 (:arg-types tagged-num)
690 (:results (digit :scs (unsigned-reg)))
691 (:result-types unsigned-num)
693 (inst sra fixnum 2 digit)))
695 (define-vop (bignum-floor)
696 (:translate sb!bignum::%floor)
698 (:args (num-high :scs (unsigned-reg))
699 (num-low :scs (unsigned-reg))
700 (denom-arg :scs (unsigned-reg) :target denom))
701 (:arg-types unsigned-num unsigned-num unsigned-num)
702 (:temporary (:scs (unsigned-reg) :from (:argument 2)) denom)
703 (:temporary (:scs (unsigned-reg) :from (:eval 0)) temp)
704 (:results (quo :scs (unsigned-reg) :from (:eval 0))
705 (rem :scs (unsigned-reg) :from (:argument 0)))
706 (:result-types unsigned-num unsigned-num)
707 (:generator 325 ; number of inst assuming targeting works.
708 (inst sll num-high 32 rem)
709 (inst bis rem num-low rem)
710 (inst sll denom-arg 32 denom)
711 (inst cmpule denom rem quo)
712 (inst beq quo shift1)
713 (inst subq rem denom rem)
716 (let ((shift2 (gen-label)))
717 (inst srl denom 1 denom)
718 (inst cmpule denom rem temp)
720 (inst beq temp shift2)
721 (inst subq rem denom rem)
723 (emit-label shift2)))))
725 (define-vop (signify-digit)
726 (:translate sb!bignum::%fixnum-digit-with-correct-sign)
728 (:args (digit :scs (unsigned-reg) :target res))
729 (:arg-types unsigned-num)
730 (:results (res :scs (any-reg signed-reg)))
731 (:result-types signed-num)
735 (inst sll digit 34 res)
736 (inst sra res 32 res))
738 (inst sll digit 32 res)
739 (inst sra res 32 res)))))
742 (define-vop (digit-ashr)
743 (:translate sb!bignum::%ashr)
745 (:args (digit :scs (unsigned-reg))
746 (count :scs (unsigned-reg)))
747 (:arg-types unsigned-num positive-fixnum)
748 (:results (result :scs (unsigned-reg) :from (:argument 0)))
749 (:result-types unsigned-num)
751 (inst sll digit 32 result)
752 (inst sra result count result)
753 (inst srl result 32 result)))
755 (define-vop (digit-lshr digit-ashr)
756 (:translate sb!bignum::%digit-logical-shift-right)
758 (inst srl digit count result)))
760 (define-vop (digit-ashl digit-ashr)
761 (:translate sb!bignum::%ashl)
763 (inst sll digit count result)))
765 ;;;; static functions
767 (define-static-fun two-arg-gcd (x y) :translate gcd)
768 (define-static-fun two-arg-lcm (x y) :translate lcm)
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 *)
773 (define-static-fun two-arg-/ (x y) :translate /)
775 (define-static-fun two-arg-< (x y) :translate <)
776 (define-static-fun two-arg-<= (x y) :translate <=)
777 (define-static-fun two-arg-> (x y) :translate >)
778 (define-static-fun two-arg->= (x y) :translate >=)
779 (define-static-fun two-arg-= (x y) :translate =)
780 (define-static-fun two-arg-/= (x y) :translate /=)
782 (define-static-fun %negate (x) :translate %negate)
784 (define-static-fun two-arg-and (x y) :translate logand)
785 (define-static-fun two-arg-ior (x y) :translate logior)
786 (define-static-fun two-arg-xor (x y) :translate logxor)