#60: first commit

Lollo/output.txt

@@ -0,0 +1,132 @@
+#QCIR-14
+exists(70, 71, 72, 73, 74, 75, 76, 77, 78, 79, 710, 711, 712, 713, 714, 715, 930, 716, 717, 718, 719, 720, 721, 722, 723, 724, 725, 726, 727, 728, 729, 730, 731, 931)
+forall(10, 11, 110, 111, 112, 113, 114, 115, 12, 13, 14, 15, 16, 17, 18, 19)
+
+output(90)
+
+91 = and()
+92 = or()
+
+#exact_circuit
+28 = and(110, 12)
+210 = and(111, 13)
+212 = and(112, 14)
+214 = and(113, 15)
+216 = and(114, 16)
+218 = and(115, 17)
+220 = and(10, 18)
+222 = and(11, 19)
+225 = and(-110, -12)
+227 = and(-111, -13)
+229 = and(-112, -14)
+231 = and(-113, -15)
+233 = and(-114, -16)
+235 = and(-115, -17)
+237 = and(-10, -18)
+239 = and(-11, -19)
+248 = and(-28, -225)
+249 = and(-210, -227)
+250 = and(-212, -229)
+251 = and(-214, -231)
+252 = and(-216, -233)
+253 = and(-218, -235)
+254 = and(-220, -237)
+255 = and(-222, -239)
+262 = and(255, 220)
+265 = and(-220, -255)
+266 = and(-222, -262)
+268 = and(-248, 266)
+270 = and(-262, -265)
+272 = and(248, -266)
+274 = and(-28, -272)
+275 = and(-272, -268)
+276 = and(274, -249)
+279 = and(249, -274)
+281 = and(-210, -279)
+282 = and(-279, -276)
+283 = and(-250, 281)
+286 = and(250, -281)
+288 = and(-212, -286)
+289 = and(-286, -283)
+290 = and(288, -251)
+293 = and(251, -288)
+295 = and(-293, -290)
+296 = and(-214, -293)
+297 = and(-252, 296)
+2100 = and(252, -296)
+2102 = and(-2100, -297)
+2103 = and(-216, -2100)
+2104 = and(253, 2103)
+2107 = and(-253, -2103)
+2108 = and(-2103, -235)
+2111 = and(-2107, -2104)
+2112 = and(-218, -2108)
+
+#outputs of exact circuit
+30 = and(254)
+31 = and(270)
+32 = and(275)
+33 = and(282)
+34 = and(289)
+35 = and(295)
+36 = and(2102)
+37 = and(-2111)
+38 = and(-2112)
+
+#parametrical_circuit
+400 = and(70, 71, 115)
+401 = and(70, -71, -115)
+410 = or(400, 401, -70)
+402 = and(72, 73, 17)
+403 = and(72, -73, -17)
+411 = or(402, 403, -72)
+404 = and(74, 75, -216)
+405 = and(74, -75, 216)
+412 = or(404, 405, -74)
+406 = and(76, 77, -2100)
+407 = and(76, -77, 2100)
+413 = or(406, 407, -76)
+50 = and(410, 411, 412, 413)
+408 = and(78, 79, 115)
+409 = and(78, -79, -115)
+414 = or(408, 409, -78)
+4010 = and(710, 711, 17)
+4011 = and(710, -711, -17)
+415 = or(4010, 4011, -710)
+4012 = and(712, 713, -216)
+4013 = and(712, -713, 216)
+416 = or(4012, 4013, -712)
+4014 = and(714, 715, -2100)
+4015 = and(714, -715, 2100)
+417 = or(4014, 4015, -714)
+51 = and(414, 415, 416, 417)
+600 = or(50, 51)
+610 = and(930, 600)
+4016 = and(716, 717, 115)
+4017 = and(716, -717, -115)
+418 = or(4016, 4017, -716)
+4018 = and(718, 719, 17)
+4019 = and(718, -719, -17)
+419 = or(4018, 4019, -718)
+4020 = and(720, 721, -216)
+4021 = and(720, -721, 216)
+4110 = or(4020, 4021, -720)
+4022 = and(722, 723, -2100)
+4023 = and(722, -723, 2100)
+4111 = or(4022, 4023, -722)
+52 = and(418, 419, 4110, 4111)
+4024 = and(724, 725, 115)
+4025 = and(724, -725, -115)
+4112 = or(4024, 4025, -724)
+4026 = and(726, 727, 17)
+4027 = and(726, -727, -17)
+4113 = or(4026, 4027, -726)
+4028 = and(728, 729, -216)
+4029 = and(728, -729, 216)
+4114 = or(4028, 4029, -728)
+4030 = and(730, 731, -2100)
+4031 = and(730, -731, 2100)
+4115 = or(4030, 4031, -730)
+53 = and(4112, 4113, 4114, 4115)
+601 = or(52, 53)
+611 = and(931, 601)

Lollo/test.py

@@ -0,0 +1,223 @@
+import sys
+from collections import deque
+sys.path.append("/home/lorenzospada/Documents/SubXPAT")
+#sys.path.append("/home/lorenzospada/Documents/SubXPAT/input")
+print(sys.path)
+
+from sxpat.annotatedGraph import *
+
+#I need the labels for how the not,and,or gates are called in subxpat and the labels for the name of the function of and and or in qcir
+NOT = 'not'
+AND_QCIR = 'and'
+AND_SUBXPAT = 'and'
+OR_QCIR = 'or'
+OR_SUBXPAT = 'or'
+INPUT_GATE_INITIALS = 'in'
+STANDARD_GATE_INITIALS = 'g'
+OUTPUT_GATE_INITIALS = 'out'
+CHANGE = {INPUT_GATE_INITIALS : "1", STANDARD_GATE_INITIALS : "2", OUTPUT_GATE_INITIALS : "3"} #
+
+def make_qcir_variable(var):
+    for key,value in CHANGE.items():
+        if var[:len(key)] == key:
+            return value + var[len(key):]
+    raise TypeError("received a variable that I can't convert, the variable was: " + var)
+
+#specs_obj: TemplateSpecs
+def check_sat(specs_obj: TemplateSpecs):
+    annotated = AnnotatedGraph('adder_i16_o9', is_clean=False, partitioning_percentage=1) 
+    annotated.extract_subgraph(specs_obj)
+    graph = annotated.graph
+    nodes = graph.nodes
+    print(annotated.subgraph_output_dict.values())
+    #print(annotated.subgraph_num_inputs, annotated.subgraph_num_outputs, specs_obj.ppo)
+    #print(annotated.graph.nodes)
+    print(annotated.graph.nodes['g113'])
+    print(annotated.graph.nodes['g114'])
+    #print(*annotated.graph.neighbors('g20'))
+    #print(*annotated.graph.successors('g20'))
+    #print(list(annotated.graph.predecessors('out0')))
+
+    # 1,2,3 is for the input, and, output gates of the exact circuit, 40 for intermidiate and gates of the multiplexer, 41 for the output of the multiplexer,
+    # 5 for the and gates, 60 for the or gates, 61 for the and between the or gate and p_o# (the outputs of the parametrical circuit), 7 is for the parameters p_o#_t#_i#_s/l,
+    # 90 is for the satisfability problem, 91 for false constant, 92 for true constant, 93 for the parameters p_o#
+    output = open('./Lollo/output.txt','w')
+
+    output.write('#QCIR-14\n')
+
+    #add the exist for parameters
+    output.write('exists(')
+    start = True
+    for a in range(annotated.subgraph_num_outputs):
+        for t in range(specs_obj.ppo):
+            for c in range(annotated.subgraph_num_inputs):
+                if not start:
+                    output.write(', ')
+                var = ((a * specs_obj.ppo + t) * annotated.subgraph_num_inputs + c) * 2
+                output.write('7' + str(var) + ', 7' + str(var+1))
+                start = False
+        output.write(', 93' + str(a))
+
+    output.write(')\nforall(')
+    deq = deque()
+    pres = set() #used to check if and / or gates have all their inputs arrived
+    start = True
+    for x in nodes:
+        if x[:len(INPUT_GATE_INITIALS)] != INPUT_GATE_INITIALS:
+            continue
+        for succ in graph.successors(x):
+            if nodes[succ]['label'] == NOT or succ in pres:
+                deq.append(succ)
+            else:
+                pres.add(succ)
+        if not start:
+            output.write(', ')
+        output.write(make_qcir_variable(x))
+        start = False
+    output.write(')\n\n')
+
+    output.write('output(90)\n\n')
+
+    output.write('91 = and()\n92 = or()\n\n')
+
+    output.write('#exact_circuit\n')
+    inverted = {} #key : [gate_referring_to, inverted?]
+    while len(deq) != 0:
+        cur = deq.popleft()
+        label = nodes[cur]['label']
+        if label == NOT:
+            predecessor = next(graph.predecessors(cur))
+            predecessor_label = nodes[predecessor]['label']
+            if predecessor_label == NOT:
+                inverted[cur] = [inverted[predecessor][0], not inverted[predecessor][1]]
+            else:
+                inverted[cur] = [predecessor, True]
+
+        else:
+            output.write(make_qcir_variable(cur) + ' = ' + (AND_QCIR if label == AND_SUBXPAT else OR_QCIR) + '(')
+            for i,x in enumerate(graph.predecessors(cur)):
+                if x in inverted:
+                    if inverted[x][1]:
+                        output.write('-')
+                    output.write(make_qcir_variable(inverted[x][0]))
+                else:
+                    output.write(make_qcir_variable(x))
+                output.write(', ' if i < len(list(graph.predecessors(cur))) - 1 else '')
+            output.write(')\n')
+
+        for x in graph.successors(cur):
+            if nodes[x]['label'] == NOT or x in pres:
+                deq.append(x)
+            else:
+                pres.add(x)
+
+    #add outputs
+    output.write('\n#outputs of exact circuit\n')
+    for x in nodes:
+        if x[:len(OUTPUT_GATE_INITIALS)] != OUTPUT_GATE_INITIALS:
+            continue
+        predecessor = next(graph.predecessors(x))
+        inv = False
+        if predecessor in inverted:
+            inv = inverted[predecessor][1]
+            predecessor = inverted[predecessor][0]
+        output.write(make_qcir_variable(x) + ' = and(' + ('-' if inv else '') + make_qcir_variable(predecessor) + ')\n')
+    #finished exact_circuit
+    output.write('\n')
+
+    output.write('#parametrical_circuit\n')
+    #start with parametrical_template
+    deq = deque()
+    pres = {}  # qcir_gate_name : qcir_gate_you_come_from
+    inverted = {} #key : [qcir_gate_referring_to, inverted?]
+    for x in nodes:
+        if x[:len(INPUT_GATE_INITIALS)] != INPUT_GATE_INITIALS or x in annotated.subgraph_input_dict.keys():
+            continue
+        for succ in graph.successors(x):
+            if nodes[succ]['label'] == NOT or make_qcir_variable(succ) in pres:
+                deq.append(succ)
+            else:
+                pres[make_qcir_variable(succ)] = make_qcir_variable(x)
+
+    #quasi uguale a sopra, sistemare
+    while len(deq) != 0:
+        cur = deq.popleft()
+        if cur in annotated.subgraph_input_dict.keys():
+            continue
+        label = nodes[cur]['label']
+        if label == NOT:
+            predecessor = next(graph.predecessors(cur))
+            predecessor_label = nodes[predecessor]['label']
+            if predecessor_label == NOT:
+                inverted[make_qcir_variable(cur)] = [inverted[make_qcir_variable(predecessor)][0], not inverted[make_qcir_variable(predecessor)][1]]
+            else:
+                inverted[make_qcir_variable(cur)] = [predecessor, True]
+
+        for x in graph.successors(cur):
+            if nodes[x]['label'] == NOT or x in pres:
+                deq.append(x)
+            else:
+                pres[x] = make_qcir_variable(cur)
+
+    #formula of multiplexer or( and(s,l,in), and(s, !l, !in), !s)
+    for a,out in enumerate(annotated.subgraph_output_dict.values()):
+        and_list = []
+
+        for t in range(specs_obj.ppo):
+            multi_list = []
+
+            for c,inp in enumerate(annotated.subgraph_input_dict.values()):
+                var = ((a * specs_obj.ppo + t) * annotated.subgraph_num_inputs + c) * 2
+                and1 = '40' + str(var)
+                and2 = '40' + str(var+1)
+
+                #partial and gates of the multiplexer
+                output.write(and1 + ' = and(7' + str(var) + ', 7' + str(var+1)  + ', ' + (make_qcir_variable(inp) if nodes[inp]['label'] != NOT else
+                                                                                          ('-' if inverted[make_qcir_variable(inp)][1] else '') + make_qcir_variable(inverted[make_qcir_variable(inp)][0])) + ')\n')
+
+                output.write(and2 + ' = and(7' + str(var) + ', -7' + str(var+1) + ', ' + ('-' + make_qcir_variable(inp) if nodes[inp]['label'] != NOT else
+                                                                                          ('' if inverted[make_qcir_variable(inp)][1] else '-') + make_qcir_variable(inverted[make_qcir_variable(inp)][0])) + ')\n')
+
+                #output of the multiplexer
+                multi = '41' + str(var//2)
+                output.write(multi + ' = or(' + and1 + ', ' + and2 + ', -7' + str(var) + ')\n')
+                multi_list.append(multi)
+
+            #and gates of the parametrical circuit
+            var = a * specs_obj.ppo + t
+            andg = '5' + str(var)
+            and_list.append(andg)
+            output.write(andg + ' = and(')
+            start = True
+            for m in multi_list:
+                if not start:
+                    output.write(', ')
+                start = False
+                output.write(m)
+            output.write(')\n')
+
+        #or gates of the parametrical circuit
+        org = '60' + str(a)
+        output.write(org + ' = or(')
+        start = True
+        for x in and_list:
+            if not start:
+                output.write(', ')
+            start = False
+            output.write(x)
+        output.write(')\n')
+
+        #p_o#
+        p_o = '93' + str(a)
+        #outputs of the parametrical circuit
+        outp = '61' + str(a)
+        output.write(outp + ' = and(' + p_o + ', ' + org + ')\n')
+
+    # for x in annotated.subgraph_output_dict.values():
+    #     for succ in graph.successors(x):
+    #         label = 
+
+
+
+
+#check_sat()

sxpat/xplore.py

@@ -1,5 +1,8 @@
 import csv
 import time
+
+import Lollo.test
+
 from typing import Iterable, Iterator, List, Union
 import networkx as nx
 from tabulate import tabulate