// From the "Beautiful Code" book

// Chapter 5. Correct, Beautiful, Fast (in That Order): Lessons from Designing XML Verifiers
// by Elliotte Rusty Harold

// cbmc --trace --function check isXMLdigit.c

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

bool isXMLDigit(unsigned int c)
{
	if (c >= 0x0030 && c <= 0x0039) return true; // ASCII
	if (c >= 0x0660 && c <= 0x0669) return true; // arabic
	if (c >= 0x06F0 && c <= 0x06F9) return true; // arabic
	if (c >= 0x0966 && c <= 0x096F) return true; // Devanagari

	if (c >= 0x09E6 && c <= 0x09EF) return true;
	
	if (c >= 0x0A66 && c <= 0x0A6F) return true; // Gurmukhi?
	if (c >= 0x0AE6 && c <= 0x0AEF) return true;

	if (c >= 0x0B66 && c <= 0x0B6F) return true;
	if (c >= 0x0BE7 && c <= 0x0BEF) return true;
	if (c >= 0x0C66 && c <= 0x0C6F) return true;

	if (c >= 0x0CE6 && c <= 0x0CEF) return true;
	if (c >= 0x0D66 && c <= 0x0D6F) return true;
	if (c >= 0x0E50 && c <= 0x0E59) return true;

	if (c >= 0x0ED0 && c <= 0x0ED9) return true;
	if (c >= 0x0F20 && c <= 0x0F29) return true; // Tibetan?

	return false;
}

bool isXMLDigit_optimized(unsigned int c)
{
	if (c < 0x0030) return false; if (c <= 0x0039) return true;
	if (c < 0x0660) return false; if (c <= 0x0669) return true;
	if (c < 0x06F0) return false; if (c <= 0x06F9) return true;
	if (c < 0x0966) return false; if (c <= 0x096F) return true;

	if (c < 0x09E6) return false; if (c <= 0x09EF) return true;
	if (c < 0x0A66) return false; if (c <= 0x0A6F) return true;
	if (c < 0x0AE6) return false; if (c <= 0x0AEF) return true;

	if (c < 0x0B66) return false; if (c <= 0x0B6F) return true;
	if (c < 0x0BE7) return false; if (c <= 0x0BEF) return true;
	if (c < 0x0C66) return false; if (c <= 0x0C6F) return true;

	if (c < 0x0CE6) return false; if (c <= 0x0CEF) return true;
	if (c < 0x0D66) return false; if (c <= 0x0D6F) return true;
	if (c < 0x0E50) return false; if (c <= 0x0E59) return true;

	if (c < 0x0ED0) return false; if (c <= 0x0ED9) return true;
	if (c < 0x0F20) return false; if (c <= 0x0F29) return true;

	return false;
}

void check(unsigned int c)
{
	assert (isXMLDigit_optimized(c) == isXMLDigit(c));
};

int main()
{
	unsigned int c=3800;
	printf ("original: %d\n", isXMLDigit(c));
	printf ("optimized: %d\n", isXMLDigit_optimized(c));
}