Skip to content

Commit 010e345

Browse files
ckirschckirsch
committed
PBVDDs -> PDDs
1 parent 3729dc6 commit 010e345

File tree

4 files changed

+237
-216
lines changed

4 files changed

+237
-216
lines changed

‎tools/bitme.py‎

Lines changed: 8 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -29,6 +29,8 @@
2929
import bvdd as BVDD
3030
import cflobvdd as CFLOBVDD
3131

32+
import pdd as PDD
33+
3234
import ctypes
3335

3436
try:
@@ -90,7 +92,7 @@ def __init__(self, sid_line, value, var_line = None, bvdd = None, cflobvdd = Non
9092
assert sid_line.is_unsigned_value(value)
9193

9294
if Values.BVDD:
93-
self.bvdd = BVDD.PBVDD.constant(value)
95+
self.bvdd = PDD.PDD.constant(value, BVDD.BVDD)
9496
if Values.CFLOBVDD:
9597
self.cflobvdd = CFLOBVDD.CFLOBVDD.byte_constant(
9698
Values.CFLOBVDD_level,
@@ -102,7 +104,7 @@ def __init__(self, sid_line, value, var_line = None, bvdd = None, cflobvdd = Non
102104
Values.total_number_of_constants += 1
103105
elif isinstance(var_line, Variable):
104106
if Values.BVDD:
105-
self.bvdd = BVDD.PBVDD.projection(var_line.input_index)
107+
self.bvdd = PDD.PDD.projection(var_line.input_index, BVDD.BVDD)
106108
if Values.CFLOBVDD:
107109
self.cflobvdd = CFLOBVDD.CFLOBVDD.byte_projection(
108110
Values.CFLOBVDD_level,
@@ -1409,7 +1411,7 @@ def print_inputs(self, inputs, step, level):
14091411
self.bitwuzla_solver.print_inputs(inputs, step, level)
14101412
else:
14111413
if Values.BVDD:
1412-
print(self.constraint.bvdd.get_printed_BVDD(True))
1414+
print(self.constraint.bvdd.get_printed_inputs(True))
14131415
if Values.CFLOBVDD:
14141416
print(self.constraint.cflobvdd.get_printed_CFLOBVDD(True))
14151417

@@ -1799,9 +1801,10 @@ def main():
17991801
bmc(bitwuzla_solver, kmin, kmax, args)
18001802

18011803
if Values.BVDD:
1802-
BVDD.PBVDD.print_profile()
1804+
BVDD.BVDD.print_profile()
1805+
PDD.PDD.print_profile()
18031806
if Values.CFLOBVDD:
1804-
BVDD.PBVDD.print_profile()
1807+
BVDD.BVDD.print_profile()
18051808
CFLOBVDD.CFLOBVDD.print_profile()
18061809

18071810
print_separator('#')

‎tools/bvdd.py‎

Lines changed: 3 additions & 210 deletions
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@
1010

1111
# selfie.cs.uni-salzburg.at
1212

13-
# Bitvector decision diagrams (BVDDs)
13+
# Bitvector Decision Diagrams (BVDDs)
1414

1515
# Given an n-bit bitvector (currently for n == 8 only),
1616
# we use 2**n-bit unsigned integers to represent
@@ -195,7 +195,7 @@ def compute_ite(self, bvdd2, bvdd3, op_id):
195195
assert type(bvdd3) is type(self)
196196
return self.compute_ternary(lambda x, y, z: y if x else z, bvdd2, bvdd3, op_id)
197197

198-
# for partitioned BVDDs
198+
# for PDDs
199199

200200
def op_union(output1, output2):
201201
return output1 if output2 is None else output2
@@ -367,7 +367,7 @@ def extract(self, output_value):
367367
# BVDD may be incomplete, only use for printing
368368
return new_bvdd
369369

370-
def get_printed_BVDD(self, output_value):
370+
def get_printed_inputs(self, output_value):
371371
return (f"{type(self).__name__}:\n" +
372372
f"{self.number_of_connections()} connections\n" +
373373
f"{self.number_of_outputs()} output values\n" +
@@ -905,211 +905,4 @@ def print_profile():
905905
print(f"ternary operators: {utilization(BVDD_cached.compute_ternary_hits, len(BVDD_cached.compute_ternary_cache))}")
906906

907907
class BVDD(BVDD_cached):
908-
pass
909-
910-
class PBVDD_uncached:
911-
def __init__(self, o2b):
912-
self.o2b = o2b
913-
914-
def __str__(self):
915-
return "PBVDD: " + ", ".join([f"{bvdd} -> {output_value}"
916-
for output_value, bvdd in self.o2b.items()])
917-
918-
def is_consistent(self):
919-
for output1_value in self.o2b:
920-
bvdd1 = self.o2b[output1_value]
921-
if len(self.o2b) == 1:
922-
if not bvdd1.is_constant() or bvdd1.get_dont_care_output() is None:
923-
return False
924-
for output2_value in self.o2b:
925-
if output1_value != output2_value:
926-
bvdd2 = self.o2b[output2_value]
927-
if bvdd1.intersection(bvdd2).is_not_empty():
928-
return False
929-
return True
930-
931-
def number_of_connections(self):
932-
return sum([self.o2b[output_value].number_of_connections() for output_value in self.o2b])
933-
934-
def number_of_outputs(self):
935-
return len(self.o2b)
936-
937-
def number_of_distinct_inputs(self):
938-
return sum([self.o2b[output_value].number_of_distinct_inputs(0) for output_value in self.o2b])
939-
940-
def is_always_false(self):
941-
return len(self.o2b) == 1 and False in self.o2b
942-
943-
def is_always_true(self):
944-
return len(self.o2b) == 1 and True in self.o2b
945-
946-
def constant(output_value):
947-
assert isinstance(output_value, bool) or isinstance(output_value, int)
948-
return PBVDD({output_value:BVDD.constant(0)})
949-
950-
def projection(index, offset = 0):
951-
return PBVDD(dict([(input_value + offset, BVDD.projection(index, offset, input_value))
952-
for input_value in range(256)]))
953-
954-
def map(self, inputs, output_value):
955-
if output_value not in self.o2b:
956-
self.o2b[output_value] = inputs
957-
else:
958-
self.o2b[output_value] = self.o2b[output_value].union(inputs)
959-
960-
def compute_unary(self, op, op_id = None):
961-
new_bvdd = PBVDD({})
962-
for output_value in self.o2b:
963-
new_bvdd.map(self.o2b[output_value], op(output_value))
964-
return new_bvdd
965-
966-
def compute_binary(self, op, bvdd2, op_id = None):
967-
assert type(bvdd2) is type(self)
968-
bvdd1 = self
969-
new_bvdd = PBVDD({})
970-
for output1_value in bvdd1.o2b:
971-
for output2_value in bvdd2.o2b:
972-
intersection = bvdd1.o2b[output1_value].intersection(bvdd2.o2b[output2_value])
973-
if intersection.is_not_empty():
974-
new_bvdd.map(intersection, op(output1_value, output2_value))
975-
return new_bvdd
976-
977-
def compute_ite(self, bvdd2, bvdd3, op_id):
978-
assert type(bvdd2) is type(self)
979-
assert type(bvdd3) is type(self)
980-
bvdd1 = self
981-
new_bvdd = PBVDD({})
982-
for output1_value in bvdd1.o2b:
983-
assert isinstance(output1_value, bool)
984-
if output1_value:
985-
for output2_value in bvdd2.o2b:
986-
intersection = bvdd1.o2b[output1_value].intersection(bvdd2.o2b[output2_value])
987-
if intersection.is_not_empty():
988-
new_bvdd.map(intersection, output2_value)
989-
else:
990-
for output3_value in bvdd3.o2b:
991-
intersection = bvdd1.o2b[output1_value].intersection(bvdd3.o2b[output3_value])
992-
if intersection.is_not_empty():
993-
new_bvdd.map(intersection, output3_value)
994-
return new_bvdd
995-
996-
def compute_ternary(self, op, bvdd2, bvdd3, op_id = None):
997-
assert type(bvdd2) is type(self)
998-
assert type(bvdd3) is type(self)
999-
bvdd1 = self
1000-
new_bvdd = PBVDD({})
1001-
for output1_value in bvdd1.o2b:
1002-
for output2_value in bvdd2.o2b:
1003-
for output3_value in bvdd3.o2b:
1004-
intersection = bvdd1.o2b[output1_value].intersection(
1005-
bvdd2.o2b[output2_value],
1006-
bvdd3.o2b[output3_value])
1007-
if intersection.is_not_empty():
1008-
new_bvdd.map(intersection,
1009-
op(output1_value, output2_value, output3_value))
1010-
return new_bvdd
1011-
1012-
def compute_ite_slow(self, bvdd2, bvdd3, op_id):
1013-
assert type(bvdd2) is type(self)
1014-
assert type(bvdd3) is type(self)
1015-
return self.compute_ternary(lambda x, y, z: y if x else z, bvdd2, bvdd3, op_id)
1016-
1017-
def get_printed_BVDD(self, output_value):
1018-
return (f"{type(self).__name__}:" +
1019-
f"{self.o2b[output_value].get_printed_BVDD(0)} -> {output_value}")
1020-
1021-
class PBVDD_cached(PBVDD_uncached):
1022-
compute_unary_lock = threading.Lock()
1023-
compute_unary_cache = {}
1024-
compute_unary_hits = 0
1025-
1026-
def compute_unary(self, op, op_id = None, unary = None):
1027-
if op_id is None:
1028-
return super().compute_unary(op)
1029-
elif (op_id, self) in PBVDD_cached.compute_unary_cache:
1030-
# assert (super().compute_unary(op, op_id) ==
1031-
# PBVDD_cached.compute_unary_cache[(op_id, self)])
1032-
PBVDD_cached.compute_unary_hits += 1
1033-
elif unary:
1034-
# lock is acquired
1035-
PBVDD_cached.compute_unary_cache[(op_id, self)] = unary
1036-
else:
1037-
# concurrent without acquiring lock
1038-
unary = super().compute_unary(op, op_id)
1039-
with PBVDD_cached.compute_unary_lock:
1040-
return self.compute_unary(op, op_id, unary)
1041-
return PBVDD_cached.compute_unary_cache[(op_id, self)]
1042-
1043-
compute_binary_lock = threading.Lock()
1044-
compute_binary_cache = {}
1045-
compute_binary_hits = 0
1046-
1047-
def compute_binary(self, op, bvdd2, op_id = None, binary = None):
1048-
if op_id is None:
1049-
return super().compute_binary(op, bvdd2)
1050-
elif (op_id, self, bvdd2) in PBVDD_cached.compute_binary_cache:
1051-
# assert (super().compute_binary(op, bvdd2, op_id) ==
1052-
# PBVDD_cached.compute_binary_cache[(op_id, self, bvdd2)])
1053-
PBVDD_cached.compute_binary_hits += 1
1054-
elif binary:
1055-
# lock is acquired
1056-
PBVDD_cached.compute_binary_cache[(op_id, self, bvdd2)] = binary
1057-
else:
1058-
# concurrent without acquiring lock
1059-
binary = super().compute_binary(op, bvdd2, op_id)
1060-
with PBVDD_cached.compute_binary_lock:
1061-
return self.compute_binary(op, bvdd2, op_id, binary)
1062-
return PBVDD_cached.compute_binary_cache[(op_id, self, bvdd2)]
1063-
1064-
compute_ite_lock = threading.Lock()
1065-
compute_ite_cache = {}
1066-
compute_ite_hits = 0
1067-
1068-
def compute_ite(self, bvdd2, bvdd3, op_id = None, ite = None):
1069-
if op_id is None:
1070-
return super().compute_ite(bvdd2, bvdd3)
1071-
elif (op_id, self, bvdd2, bvdd3) in PBVDD_cached.compute_ite_cache:
1072-
# assert (super().compute_ite(bvdd2, bvdd3, op_id) ==
1073-
# PBVDD_cached.compute_ite_cache[(op_id, self, bvdd2, bvdd3)])
1074-
PBVDD_cached.compute_ite_hits += 1
1075-
elif ite:
1076-
# lock is acquired
1077-
PBVDD_cached.compute_ite_cache[(op_id, self, bvdd2, bvdd3)] = ite
1078-
else:
1079-
# concurrent without acquiring lock
1080-
ite = super().compute_ite(bvdd2, bvdd3, op_id)
1081-
with PBVDD_cached.compute_ite_lock:
1082-
return self.compute_ite(bvdd2, bvdd3, op_id, ite)
1083-
return PBVDD_cached.compute_ite_cache[(op_id, self, bvdd2, bvdd3)]
1084-
1085-
compute_ternary_lock = threading.Lock()
1086-
compute_ternary_cache = {}
1087-
compute_ternary_hits = 0
1088-
1089-
def compute_ternary(self, op, bvdd2, bvdd3, op_id = None, ternary = None):
1090-
if op_id is None:
1091-
return super().compute_ternary(op, bvdd2, bvdd3)
1092-
elif (op_id, self, bvdd2, bvdd3) in PBVDD_cached.compute_ternary_cache:
1093-
# assert (super().compute_ternary(op, bvdd2, bvdd3, op_id) ==
1094-
# PBVDD_cached.compute_ternary_cache[(op_id, self, bvdd2, bvdd3)])
1095-
PBVDD_cached.compute_ternary_hits += 1
1096-
elif ternary:
1097-
# lock is acquired
1098-
PBVDD_cached.compute_ternary_cache[(op_id, self, bvdd2, bvdd3)] = ternary
1099-
else:
1100-
# concurrent without acquiring lock
1101-
ternary = super().compute_ternary(op, bvdd2, bvdd3, op_id)
1102-
with PBVDD_cached.compute_ternary_lock:
1103-
return self.compute_ternary(op, bvdd2, bvdd3, op_id, ternary)
1104-
return PBVDD_cached.compute_ternary_cache[(op_id, self, bvdd2, bvdd3)]
1105-
1106-
def print_profile():
1107-
BVDD.print_profile()
1108-
print("PBVDD cache profile:")
1109-
print(f"unary operators: {utilization(PBVDD_cached.compute_unary_hits, len(PBVDD_cached.compute_unary_cache))}")
1110-
print(f"binary operators: {utilization(PBVDD_cached.compute_binary_hits, len(PBVDD_cached.compute_binary_cache))}")
1111-
print(f"ite operators: {utilization(PBVDD_cached.compute_ite_hits, len(PBVDD_cached.compute_ite_cache))}")
1112-
print(f"ternary operators: {utilization(PBVDD_cached.compute_ternary_hits, len(PBVDD_cached.compute_ternary_cache))}")
1113-
1114-
class PBVDD(PBVDD_cached):
1115908
pass

‎tools/cflobvdd.py‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@
1010

1111
# selfie.cs.uni-salzburg.at
1212

13-
# Context-free language ordered bitvector decision diagrams (CFLOBVDDs)
13+
# Context-free Language Ordered Bitvector Decision Diagrams (CFLOBVDDs)
1414

1515
# CFLOBVDDs generalize CFLOBDDs in two ways:
1616

0 commit comments

Comments
 (0)