/* UG-VI MJ-14 Unit I: exact arithmetic and Boolean checks. */
kill(all)$

bnot(x) := 1-x$
band2(x,y) := x*y$
bor2(x,y) := 1-(1-x)*(1-y)$
bxor2(x,y) := x+y-2*x*y$
bxnor2(x,y) := 1-bxor2(x,y)$
bit(n,k) := mod(quotient(n,2^k),2)$

/* 101101.101_2 = 45.625_10. */
positional_residual :
  (2^5+2^3+2^2+2^0+2^(-1)+2^(-3))-365/8$
print("positional reconstruction residual =", positional_residual)$

/* Eight-bit two's-complement encoding and subtraction. */
word_modulus : 2^8$
x : 37$
x_twos : mod(word_modulus-x,word_modulus)$
twos_complement_residual : mod(x+x_twos,word_modulus)$
subtraction_residual : mod(91+x_twos,word_modulus)-54$
print("two's-complement inverse residual =", twos_complement_residual)$
print("91 - 37 subtraction residual =", subtraction_residual)$

/* Boolean postulates and De Morgan identities over every input pair. */
identity_residuals : makelist(
  block([a:bit(n,1),b:bit(n,0)],
    [band2(a,1)-a,
     bor2(a,0)-a,
     band2(a,b)-band2(b,a),
     bor2(a,b)-bor2(b,a),
     bnot(band2(a,b))-bor2(bnot(a),bnot(b)),
     bnot(bor2(a,b))-band2(bnot(a),bnot(b)),
     bor2(a,band2(a,b))-a,
     band2(a,bor2(a,b))-a]),
  n,0,3)$
print("Boolean identity residuals =", identity_residuals)$

/* Canonical minterm and maxterm reconstruction. */
minterm(index,n) := product(bxnor2(bit(index,k),bit(n,k)),k,0,3)$
maxterm(index,n) := 1-minterm(index,n)$
ones : [1,3,7,11,15]$
zeros : [0,2,4,5,6,8,9,10,12,13,14]$
or_list(L) := 1-product(1-L[i],i,1,length(L))$
and_list(L) := product(L[i],i,1,length(L))$
sop_value(n) := or_list(makelist(minterm(ones[i],n),i,1,length(ones)))$
pos_value(n) := and_list(makelist(maxterm(zeros[i],n),i,1,length(zeros)))$
required_value(n) := if member(n,ones) then 1 else 0$
canonical_sop_residuals : makelist(sop_value(n)-required_value(n),n,0,15)$
canonical_pos_residuals : makelist(pos_value(n)-required_value(n),n,0,15)$
print("canonical SOP residuals =", canonical_sop_residuals)$
print("canonical POS residuals =", canonical_pos_residuals)$

/* K-map: F = sum m(1,3,7,11,15), d = sum d(0,2,5).
   The proposed cover is A'B' + CD; do not constrain don't-care cells. */
dont_cares : [0,2,5]$
kmap_cover(n) := block([a:bit(n,3),b:bit(n,2),c:bit(n,1),d:bit(n,0)],
  bor2(band2(bnot(a),bnot(b)),band2(c,d)))$
kmap_residuals : makelist(
  if member(n,dont_cares) then 0 else kmap_cover(n)-required_value(n),
  n,0,15)$
print("specified-cell K-map residuals =", kmap_residuals)$