API tools faq
paste
Advertisement
KittehKing

Untitled

KittehKing
Jul 24th, 2024 (edited)
107
0
Never
Add comment
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
Python 11.64 KB | None | 0 0
raw download clone embed print report
  1. import numpy as np
  2. from z3 import *
  3. import matplotlib.pyplot as plt
  4. import time
  5.  
  6. class bitshift():
  7.     def __init__(self, out, wordlength, verbose=False):
  8.         self.wordlength = wordlength
  9.         self.out = out
  10.         self.N = 10
  11.         self.verbose = verbose
  12.  
  13.  
  14.         #input multiplexer
  15.         c=[[Bool(f'c{i}{w}') for w in range(self.wordlength)] for i in range(self.N+1)]
  16.         l=[[Bool(f'l{i}{w}') for w in range(self.wordlength)] for i in range(1, self.N+1)]
  17.         r=[[Bool(f'r{i}{w}') for w in range(self.wordlength)] for i in range(1, self.N+1)]
  18.  
  19.  
  20.         alpha = [[Bool(f'alpha{i}{a}') for a in range(i)] for i in range(1, self.N+1)]
  21.         beta =[[ Bool(f'Beta{i}{a}') for a in range(i)] for i in range(1, self.N+1)]
  22.  
  23.         solver = Solver()
  24.  
  25.  
  26.         #c0,w is always 0 except w=0
  27.         for w in range(1,self.wordlength):
  28.             solver.add(Not(c[0][w]))
  29.  
  30.         solver.add(c[0][0])
  31.  
  32.  
  33.         #input multiplexer
  34.         for i in range(1, self.N+1):
  35.             alpha_sum = []
  36.             beta_sum = []
  37.             for a in range(i):
  38.                 for word in range(self.wordlength):
  39.                     clause1_1 = Or(Not(alpha[i-1][a]), Not(c[a][word]), l[i-1][word])
  40.                     clause1_2 = Or(Not(alpha[i-1][a]), c[a][word], Not(l[i-1][word]))
  41.                     solver.add(And(clause1_1, clause1_2))
  42.  
  43.                     clause2_1 = Or(Not(beta[i-1][a]), Not(c[a][word]), r[i-1][word])
  44.                     clause2_2 = Or(Not(beta[i-1][a]), c[a][word], Not(r[i-1][word]))
  45.                     solver.add(And(clause2_1, clause2_2))
  46.  
  47.                 #make a pair for pbeq with a weight of 1 for later
  48.                 alpha_sum.append((alpha[i-1][a], 1))
  49.                 beta_sum.append((beta[i-1][a], 1))
  50.  
  51.            
  52.             solver.add(PbEq(alpha_sum,1))
  53.             solver.add(PbEq(beta_sum,1))
  54.  
  55.         #Left Shifter
  56.         #k is the shift selector
  57.         gamma = [[Bool(f'gamma{i}{k}') for k in range(self.wordlength-1)] for i in range(1, self.N+1)]
  58.         s     = [[Bool(f's{i}{w}') for w in range(self.wordlength)] for i in range(1, self.N+1)]
  59.  
  60.  
  61.         for i in range(1, self.N+1):
  62.             gamma_sum = []
  63.             for k in range(self.wordlength-1):
  64.                 for j in range(self.wordlength-1-k):
  65.                     clause3_1 = Or(Not(gamma[i-1][k]),Not(l[i-1][j]),s[i-1][j+k])
  66.                     clause3_2 = Or(Not(gamma[i-1][k]),l[i-1][j],Not(s[i-1][j+k]))
  67.                     solver.add(And(clause3_1, clause3_2))
  68.  
  69.                 gamma_sum.append((gamma[i-1][k], 1))
  70.            
  71.             solver.add(PbEq(gamma_sum,1))
  72.  
  73.  
  74.             for kf in range(1,self.wordlength-1):
  75.                 for b in range(kf):
  76.                     clause4 = Or(Not(gamma[i-1][kf]),Not(s[i-1][b]))
  77.                     clause5 = Or(Not(gamma[i-1][kf]), Not(l[i-1][self.wordlength-1]), l[i-1][self.wordlength-2-b])
  78.                     clause6 = Or(Not(gamma[i-1][kf]), l[i-1][self.wordlength-1], Not(l[i-1][self.wordlength-2-b]))
  79.                     solver.add(clause4)
  80.                     solver.add(clause5)
  81.                     solver.add(clause6)
  82.  
  83.             clause7_1= Or(Not(l[i-1][self.wordlength-1]), s[i-1][self.wordlength-1])
  84.             clause7_2= Or(l[i-1][self.wordlength-1], Not(s[i-1][self.wordlength-1]))
  85.             solver.add(And(clause7_1, clause7_2))
  86.  
  87.  
  88.         delta = [Bool(f'delta{i}') for i in range(1, self.N+1)]
  89.         w     = [[Bool(f'w{i}{w}') for w in range(self.wordlength)] for i in range(1, self.N+1)]
  90.         x     = [[Bool(f'x{i}{w}') for w in range(self.wordlength)] for i in range(1, self.N+1)]
  91.  
  92.    
  93.    
  94.         #delta selector
  95.         for i in range(1, self.N+1):
  96.             for word in range(self.wordlength):
  97.                 clause8_1 = Or(Not(delta[i-1]),Not(s[i-1][word]),x[i-1][word])
  98.                 clause8_2 = Or(Not(delta[i-1]),s[i-1][word],Not(x[i-1][word]))
  99.                 solver.add(And(clause8_1, clause8_2))
  100.                
  101.                 clause9_1 = Or(Not(delta[i-1]),Not(r[i-1][word]),w[i-1][word])
  102.                 clause9_2 = Or(Not(delta[i-1]),r[i-1][word],Not(w[i-1][word]))
  103.                 solver.add(And(clause9_1, clause9_2))
  104.  
  105.                 clause10_1 = Or(delta[i-1],Not(s[i-1][word]),w[i-1][word])
  106.                 clause10_2 = Or(delta[i-1],s[i-1][word],Not(w[i-1][word]))
  107.                 solver.add(And(clause10_1, clause10_2))
  108.  
  109.                 clause11_1 = Or(delta[i-1],Not(r[i-1][word]),x[i-1][word])
  110.                 clause11_2 = Or(delta[i-1],r[i-1][word],Not(x[i-1][word]))
  111.                 solver.add(And(clause11_1, clause11_2))
  112.                
  113.         epsilon = [Bool(f'epsilon{i}') for i in range(1, self.N+1)]
  114.         y     = [[Bool(f'y{i}{w}') for w in range(self.wordlength)] for i in range(1, self.N+1)]
  115.  
  116.  
  117.         #xor
  118.         for i in range(1, self.N+1):
  119.             for word in range(self.wordlength):
  120.                 clause12 = Or(w[i-1][word], epsilon[i-1], Not(y[i-1][word]))
  121.                 clause13 = Or(w[i-1][word], Not(epsilon[i-1]), y[i-1][word])
  122.                 clause14 = Or(Not(w[i-1][word]), epsilon[i-1], y[i-1][word])
  123.                 clause15 = Or(Not(w[i-1][word]), Not(epsilon[i-1]), Not(y[i-1][word]))
  124.                 solver.add(clause12)
  125.                 solver.add(clause13)
  126.                 solver.add(clause14)
  127.                 solver.add(clause15)
  128.  
  129.        
  130.        
  131.        
  132.  
  133.         #ripple carry
  134.         z     = [[Bool(f'z{i}{w}') for w in range(self.wordlength)] for i in range(1, self.N+1)]
  135.         cout  = [[Bool(f'z{i}{w}') for w in range(self.wordlength)] for i in range(1, self.N+1)]
  136.  
  137.        
  138.         for i in range(1, self.N+1):
  139.             # Clauses for sum = a ⊕ b ⊕ cin at 0
  140.             clause16 = Or(x[i-1][0], y[i-1][0], epsilon[i-1], Not(z[i-1][0]))
  141.             clause17 = Or(x[i-1][0], y[i-1][0], Not(epsilon[i-1]), z[i-1][0])
  142.             clause18 = Or(x[i-1][0], Not(y[i-1][0]), epsilon[i-1], z[i-1][0])
  143.             clause19 = Or(Not(x[i-1][0]), y[i-1][0], epsilon[i-1], z[i-1][0])
  144.             clause20 = Or(Not(x[i-1][0]), Not(y[i-1][0]), Not(epsilon[i-1]), z[i-1][0])
  145.             clause21 = Or(Not(x[i-1][0]), Not(y[i-1][0]), epsilon[i-1], Not(z[i-1][0]))
  146.             clause22 = Or(Not(x[i-1][0]), y[i-1][0], Not(epsilon[i-1]), Not(z[i-1][0]))
  147.             clause23 = Or(x[i-1][0], Not(y[i-1][0]), Not(epsilon[i-1]), Not(z[i-1][0]))
  148.  
  149.             solver.add(clause16)
  150.             solver.add(clause17)
  151.             solver.add(clause18)
  152.             solver.add(clause19)
  153.             solver.add(clause20)
  154.             solver.add(clause21)
  155.             solver.add(clause22)
  156.             solver.add(clause23)
  157.  
  158.             # Clauses for cout = (a AND b) OR (cin AND (a ⊕ b))
  159.             clause24 = Or(Not(x[i-1][0]), Not(y[i-1][0]), cout[i-1][0])
  160.             clause25 = Or(x[i-1][0], y[i-1][0], Not(cout[i-1][0]))
  161.             clause26 = Or(Not(x[i-1][0]), Not(epsilon[i-1]), cout[i-1][0])
  162.             clause27 = Or(x[i-1][0], epsilon[i-1], Not(cout[i-1][0]))
  163.             clause28 = Or(Not(y[i-1][0]), Not(epsilon[i-1]), cout[i-1][0])
  164.             clause29 = Or(y[i-1][0], epsilon[i-1], Not(cout[i-1][0]))
  165.  
  166.             solver.add(clause24)
  167.             solver.add(clause25)
  168.             solver.add(clause26)
  169.             solver.add(clause27)
  170.             solver.add(clause28)
  171.             solver.add(clause29)
  172.  
  173.             for kf in range(1, self.wordlength):
  174.                 # Clauses for sum = a ⊕ b ⊕ cin at kf
  175.                 clause30 = Or(x[i-1][kf], y[i-1][kf], cout[i-1][kf-1], Not(z[i-1][kf]))
  176.                 clause31 = Or(x[i-1][kf], y[i-1][kf], Not(cout[i-1][kf-1]), z[i-1][kf])
  177.                 clause32 = Or(x[i-1][kf], Not(y[i-1][kf]), cout[i-1][kf-1], z[i-1][kf])
  178.                 clause33 = Or(Not(x[i-1][kf]), y[i-1][kf], cout[i-1][kf-1], z[i-1][kf])
  179.                 clause34 = Or(Not(x[i-1][kf]), Not(y[i-1][kf]), Not(cout[i-1][kf-1]), z[i-1][kf])
  180.                 clause35 = Or(Not(x[i-1][kf]), Not(y[i-1][kf]), cout[i-1][kf-1], Not(z[i-1][kf]))
  181.                 clause36 = Or(Not(x[i-1][kf]), y[i-1][kf], Not(cout[i-1][kf-1]), Not(z[i-1][kf]))
  182.                 clause37 = Or(x[i-1][kf], Not(y[i-1][kf]), Not(cout[i-1][kf-1]), Not(z[i-1][kf]))
  183.  
  184.                 solver.add(clause30)
  185.                 solver.add(clause31)
  186.                 solver.add(clause32)
  187.                 solver.add(clause33)
  188.                 solver.add(clause34)
  189.                 solver.add(clause35)
  190.                 solver.add(clause36)
  191.                 solver.add(clause37)
  192.  
  193.                 # Clauses for cout = (a AND b) OR (cin AND (a ⊕ b)) at kf
  194.                 clause38 = Or(Not(x[i-1][kf]), Not(y[i-1][kf]), cout[i-1][kf])
  195.                 clause39 = Or(x[i-1][kf], y[i-1][kf], Not(cout[i-1][kf]))
  196.                 clause40 = Or(Not(x[i-1][kf]), Not(cout[i-1][kf-1]), cout[i-1][kf])
  197.                 clause41 = Or(x[i-1][kf], cout[i-1][kf-1], Not(cout[i-1][kf]))
  198.                 clause42 = Or(Not(y[i-1][kf]), Not(cout[i-1][kf-1]), cout[i-1][kf])
  199.                 clause43 = Or(y[i-1][kf], cout[i-1][kf-1], Not(cout[i-1][kf]))
  200.  
  201.                 solver.add(clause38)
  202.                 solver.add(clause39)
  203.                 solver.add(clause40)
  204.                 solver.add(clause41)
  205.                 solver.add(clause42)
  206.                 solver.add(clause43)
  207.  
  208.             clause44 = Or(epsilon[i-1], x[i-1][self.wordlength-1], w[i-1][self.wordlength-1], Not(z[i-1][self.wordlength-1]))
  209.             clause45 = Or(epsilon[i-1], Not(x[i-1][self.wordlength-1]), Not(w[i-1][self.wordlength-1]), z[i-1][self.wordlength-1])
  210.             clause46 = Or(Not(epsilon[i-1]), x[i-1][self.wordlength-1], Not(w[i-1][self.wordlength-1]), Not(z[i-1][self.wordlength-1]))
  211.             clause47 = Or(Not(epsilon[i-1]), Not(x[i-1][self.wordlength-1]), w[i-1][self.wordlength-1], z[i-1][self.wordlength-1])
  212.  
  213.             solver.add(clause44)
  214.             solver.add(clause45)
  215.             solver.add(clause46)
  216.             solver.add(clause47)
  217.  
  218.  
  219.         #right shift
  220.         zeta = [[Bool(f'zeta{i}{k}') for k in range(self.wordlength-1)] for i in range(1, self.N+1)]
  221.  
  222.  
  223.  
  224.         for i in range(1, self.N+1):
  225.             zeta_sum = []
  226.             for k in range(self.wordlength-1):
  227.                 for j in range(self.wordlength-1-k):
  228.                     clause48_1 = Or(Not(zeta[i-1][k]),Not(z[i-1][j+k]),c[i][j])
  229.                     clause48_2 = Or(Not(zeta[i-1][k]),z[i-1][j+k],Not(c[i][j]))
  230.                     solver.add(And(clause48_1, clause48_2))
  231.  
  232.                 zeta_sum.append((zeta[i-1][k], 1))
  233.            
  234.             solver.add(PbEq(zeta_sum,1))
  235.  
  236.  
  237.             for kf in range(1,self.wordlength-1):
  238.                 for b in range(kf):
  239.                     clause49_1 = Or(Not(zeta[i-1][kf]), Not(z[i-1][self.wordlength-1]), c[i][self.wordlength-2-b])
  240.                     clause49_2 = Or(Not(zeta[i-1][kf]), z[i-1][self.wordlength-1], Not(c[i][self.wordlength-2-b]))
  241.                     solver.add(clause49_1)
  242.                     solver.add(clause49_2)
  243.  
  244.                     clause50 = Or(Not(zeta[i-1][kf]), Not(z[i-1][b]))
  245.                     solver.add(clause50)
  246.            
  247.             clause51_1 = Or(Not(z[i-1][self.wordlength-1]), c[i][self.wordlength-1])
  248.             clause51_2 = Or(z[i-1][self.wordlength-1], Not(c[i][self.wordlength-1]))
  249.             solver.add(And(clause51_1, clause51_2))
  250.  
  251.      
  252.             #bound ci,0 to be odd number
  253.             # solver.add(c[i-1][0])
  254.        
  255.  
  256.  
  257.         if solver.check() == sat:
  258.             print("its sat")
  259.             model = solver.model()
  260.             print(model)
  261.         else:
  262.             print("No solution")
  263.        
  264.  
  265.  
  266.  
  267.  
  268. if __name__ == '__main__':
  269.     hm = (25, 23, 11,25,75)
  270.     wordlength = 20 #min wordlength would be 2
  271.     bitshift(hm, wordlength, verbose=True)
  272.  
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement
Public Pastes
Advertisement
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy.  OK, I Understand
Not a member of Pastebin yet?
Sign Up, it unlocks many cool features!