rygorous

from collections import defaultdict
import re

# copied from Khronos Data Format spec bptc.txt table-bptcblockformat
BC6H_BIT_TABLE = '''
^.^|  0     ^.^| M^1..0^, _G_~2~^4^, _B_~2~^4^, _B_~3~^4^, _R_~0~^9..0^, _G_~0~^9..0^, _B_~0~^9..0^, _R_~1~^4..0^,
         _G_~3~^4^, _G_~2~^3..0^, _G_~1~^4..0^, _B_~3~^0^, _G_~3~^3..0^, _B_~1~^4..0^, _B_~3~^1^, _B_~2~^3..0^,
         _R_~2~^4..0^, _B_~3~^2^, _R_~3~^4..0^, _B_~3~^3^, PB^4..0^
^.^|  1     ^.^| M^1..0^, _G_~2~^5^, _G_~3~^4^, _G_~3~^5^, _R_~0~^6..0^, _B_~3~^0^, _B_~3~^1^, _B_~2~^4^,
         _G_~0~^6..0^, _B_~2~^5^, _B_~3~^2^, _G_~2~^4^, _B_~0~^6..0^, _B_~3~^3^, _B_~3~^5^, _B_~3~^4^,

rygorous

static U64 remove_anchor_bit(U64 idxs, U64 anchor_bit)
{
	// anchor bit must have been forced to zero on entry
	RR_ASSERT((idxs & anchor_bit) == 0);
	U64 lo = anchor_bit - 1ull; // bits below anchor_bit
	return idxs - ((idxs >> 1) & ~lo);
}

// in endpoint encode:

rygorous

	// Place bits in first word approximately where they need to go; specifically, keep the
	// fields contiguous, so the low bits go where they're supposed to go and the high
	// bits may be off, we can fix that cheaply all at once later!
	//
	// The code that follows is exhaustively verified for all possible combinations of Q0 and Qh.r
	// to generate the correct output.
	//
	// R/G/B are Q0.r/g/b, r is Qh.r
	//
	// 31 30 29 28 27 26 25 24 23 22 21 20 19 18 17 16 15 14 13 12 11 10 09 08 07 06 05 04 03 02 01 00

rygorous

int
fillscan(Filldata *f, Point p0, int scanxmax)
{
	int x, x0, x1, y;
	uchar *b;

	x = p0.x;
	y = p0.y;
	b = f->bmask + y*f->wmask;
	if(b[x/8] & 0x80>>(x%8)) {

rygorous

0x00 0 cost=10
0x01 BCAX(A, 0xf5, 0x0c) cost=30
0x02 BIC(0x0a, B) cost=20
0x03 EOR(A, 0xf3) cost=20
0x04 BIC(B, 0xfa) cost=20
0x05 EOR(A, 0xf5) cost=20
0x06 BCAX(0x0a, B, A) cost=20
0x07 EOR(A, 0xf7) cost=30
0x08 BCAX(B, B, 0x0a) cost=20
0x09 EOR3(A, 0x0a, 0xf3) cost=30

rygorous

import functools
from typing import Optional

class BddContext:
    def __init__(self):
        # 0/1 leaf nodes, it's convenient to just refer to them as 0 and 1
        # a node is a (var id, lo_node, hi_node) tuple
        self.nodes = []
        self.vars = []
        self.node_dict = {}

rygorous

// The FFT alg used here was designed to be very FMA-friendly, but because we can't assume FMAs are present on
// all target HW and want consistent results everywhere, we're using FMA-less algorithms for this application.

// Notation throughout this file:
//
// Let z = a + bi. Then conj(z) = a - bi.
//
// We can swap the real and imaginary parts of z to yield s(z) = b + ai ("swap").
// Now because
//

rygorous

static size_t const kMaxN = 2048; // This is the largest straight FFT we support

struct complexf
{
    float re;
    float im;

    complexf() {}
    complexf(float r) : re(r), im(0.0f) {}
    complexf(float r, float i) : re(r), im(i) {}

rygorous

#include <immintrin.h>
#include <stdio.h>
#include <stdint.h>
#include <assert.h>

typedef uint32_t uint32;
typedef __m128i Vec128_U32;

// "Insert" two 0 bits after each of the 11 low bits of x
static uint32 Part1By2(uint32 x)

rygorous

//===================================================================
// constraint validation for preserve extremes mode

// Cold part of are_endpoitns_permitted: the actual constraint validation
static RADNOINLINE bool are_endpoints_permitted_cold(const BC7BlockState & st, const bc7rd_blockinfo& info)
{
	const BC7Flags flags = info.flags;

	if (st.mode <= 3)
	{