float_adders_demand_test.py (1787B)
1 #!/usr/bin/env python3 2 """Flat-domain Boolean checks for the full-adder source forms. 3 4 The Boolean model supplements the lazy-tricu demand probes, which inspect actual 5 sum trees under selected partial-input observations. 6 """ 7 import itertools 8 import unittest 9 10 11 class Bottom(Exception): 12 pass 13 14 15 def observe(expression, values): 16 def force(value): 17 if value is None: 18 raise Bottom() 19 return value 20 a,b,c = [lambda value=value: force(value) for value in values] 21 try: 22 return expression(a,b,c) 23 except Bottom: 24 return None 25 26 27 def native_carry(a,b,c): 28 return (a() and b()) or (c() and (a() or b())) 29 30 31 def original_mux_carry(a,b,c): 32 return (b() or c()) if a() else (b() and c()) 33 34 35 def ordered_carry(a,b,c): 36 return (b() or c()) if a() else (c() and b()) 37 38 39 def native_sum(a,b,c): 40 first = (not b()) if a() else b() 41 return (not c()) if first else c() 42 43 44 def mux_sum(a,b,c): 45 return (c() if b() else not c()) if a() else ((not c()) if b() else c()) 46 47 48 class AdderDemandTests(unittest.TestCase): 49 def test_ordered_carry_all_partial_booleans(self): 50 for values in itertools.product([False,True,None],repeat=3): 51 self.assertIs(observe(native_carry,values),observe(ordered_carry,values),values) 52 53 def test_sum_all_partial_booleans(self): 54 for values in itertools.product([False,True,None],repeat=3): 55 self.assertIs(observe(native_sum,values),observe(mux_sum,values),values) 56 57 def test_original_mux_counterexample(self): 58 values = (False,None,False) 59 self.assertIs(observe(native_carry,values),False) 60 self.assertIs(observe(original_mux_carry,values),None) 61 self.assertIs(observe(ordered_carry,values),False) 62 63 64 if __name__=='__main__': 65 unittest.main()