diff --git a/Lollo/output.txt b/Lollo/output.txt new file mode 100644 index 000000000..56d85b58a --- /dev/null +++ b/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) diff --git a/Lollo/test.py b/Lollo/test.py new file mode 100644 index 000000000..4c092cdd9 --- /dev/null +++ b/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() \ No newline at end of file diff --git a/sxpat/xplore.py b/sxpat/xplore.py index e5b345d75..c3196a6d2 100644 --- a/sxpat/xplore.py +++ b/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