This makes the word decision procedures WORD_ARITH/WORD_ARITH_TAC and BITBLAST_RULE more capable in several ways:
Both BITBLAST_RULE and WORD_ARITH make more systematic reduction of word ground expressions internally.
BITBLAST_RULE now transforms "val(x) MOD n" and "val(x) DIV n" where n is (or can be transformed into) a power of 2, into bitwise equivalents so that the core procedure can handle it.
WORD_ARITH also expands "val(word n)" into "n MOD ...." after all the casewise "linear" expansions have been tried, giving it some capacity to handle multiplication by constants.
The underlying integer arithmetic procedure INT_ARITH has been enhanced so that it is never worse to use it than the natural number version, because it will infer nonnegativity of quotients introduced by div/rem elimination where possible.
Here are some word examples that work now but didn't before:
WORD_ARITH
!m n. m < 4096 /\ n <= 511 ==> word_ule (word_add (word_mul (word n) (word 0x00001000)) (word m)) (word 0x0000000001FFFFFF:int64);;
BITBLAST_RULE
word_and x (word 256):int64 = word 0 <=> val x MOD 512 < 256;;
This makes the word decision procedures WORD_ARITH/WORD_ARITH_TAC and BITBLAST_RULE more capable in several ways:
Both BITBLAST_RULE and WORD_ARITH make more systematic reduction of word ground expressions internally.
BITBLAST_RULE now transforms "val(x) MOD n" and "val(x) DIV n" where n is (or can be transformed into) a power of 2, into bitwise equivalents so that the core procedure can handle it.
WORD_ARITH also expands "val(word n)" into "n MOD ...." after all the casewise "linear" expansions have been tried, giving it some capacity to handle multiplication by constants.
The underlying integer arithmetic procedure INT_ARITH has been enhanced so that it is never worse to use it than the natural number version, because it will infer nonnegativity of quotients introduced by div/rem elimination where possible.
Here are some word examples that work now but didn't before:
WORD_ARITH
!m n. m < 4096 /\ n <= 511 ==> word_ule (word_add (word_mul (word n) (word 0x00001000)) (word m)) (word 0x0000000001FFFFFF:int64);;BITBLAST_RULE
word_and x (word 256):int64 = word 0 <=> val x MOD 512 < 256;;