Skip to content

Commit

Permalink
[format] Code format
Browse files Browse the repository at this point in the history
  • Loading branch information
xumingkuan committed Jan 18, 2025
1 parent 6907cfb commit a3f0f51
Show file tree
Hide file tree
Showing 2 changed files with 14 additions and 16 deletions.
26 changes: 13 additions & 13 deletions src/python/verifier/verifier.py
Original file line number Diff line number Diff line change
Expand Up @@ -235,7 +235,7 @@ def search_phase_factor_to_check_equivalence(
current_param_id,
current_phase_factor_symbolic,
current_phase_factor_for_fingerprint,
timeout
timeout,
):
if current_param_id == num_parameters:
# Search for constants
Expand Down Expand Up @@ -267,7 +267,7 @@ def search_phase_factor_to_check_equivalence(
current_param_id + 1,
new_phase_factor_symbolic,
new_phase_factor_for_fingerprint,
timeout
timeout,
):
return True
return False
Expand Down Expand Up @@ -386,7 +386,7 @@ def search_phase_factor_to_check_equivalence(
current_param_id + 1,
new_phase_factor_symbolic,
new_phase_factor_for_fingerprint,
timeout
timeout,
):
return True
return False
Expand All @@ -401,7 +401,7 @@ def equivalent(
do_not_invoke_smt_solver=False,
check_phase_shift_in_smt_solver=False,
phase_shift_id=None,
timeout=30000 # timeout for each z3 invocation in 30s
timeout=30000, # timeout for each z3 invocation in 30s
):
dag1_meta = dag1[0]
dag2_meta = dag2[0]
Expand Down Expand Up @@ -466,7 +466,7 @@ def equivalent(
current_param_id=0,
current_phase_factor_symbolic=(z3.RealVal(1), z3.RealVal(0)),
current_phase_factor_for_fingerprint=0,
timeout=timeout
timeout=timeout,
)
if not result:
print(
Expand Down Expand Up @@ -498,7 +498,7 @@ def equivalent(
current_param_id=0,
current_phase_factor_symbolic=(z3.RealVal(1), z3.RealVal(0)),
current_phase_factor_for_fingerprint=0,
timeout=timeout
timeout=timeout,
)
if not result:
print(
Expand Down Expand Up @@ -535,7 +535,7 @@ def find_equivalences_helper(
check_phase_shift_in_smt_solver,
verbose,
do_not_invoke_smt_solver,
timeout
timeout,
):
output_dict = {}
equivalent_called = 0
Expand Down Expand Up @@ -564,7 +564,7 @@ def find_equivalences_helper(
parameters_for_fingerprint,
do_not_invoke_smt_solver,
check_phase_shift_in_smt_solver,
timeout
timeout,
):
current_tag = hashtag + "_" + str(i)
assert current_tag in output_dict.keys()
Expand Down Expand Up @@ -616,7 +616,7 @@ def find_equivalences(
check_equivalence_with_different_hash=True,
check_phase_shift_in_smt_solver=False,
do_not_invoke_smt_solver=False,
timeout=30000 # timeout for each z3 invocation in 30s
timeout=30000, # timeout for each z3 invocation in 30s
):
input_file_data = load_json(input_file)
data = input_file_data[1]
Expand Down Expand Up @@ -661,7 +661,7 @@ def find_equivalences(
parameters_for_fingerprint,
do_not_invoke_smt_solver,
check_phase_shift_in_smt_solver,
timeout
timeout,
):
current_tag = hashtag + "_" + str(i)
assert current_tag in output_dict.keys()
Expand Down Expand Up @@ -711,7 +711,7 @@ def find_equivalences(
check_phase_shift_in_smt_solver,
verbose,
do_not_invoke_smt_solver,
timeout
timeout,
)
for hashtag, dags in data.items()
if len(dags) > 1
Expand Down Expand Up @@ -798,7 +798,7 @@ def find_equivalences(
do_not_invoke_smt_solver,
check_phase_shift_in_smt_solver,
None,
timeout
timeout,
):
equivalence_verified = True
if not equivalence_verified:
Expand Down Expand Up @@ -836,7 +836,7 @@ def find_equivalences(
do_not_invoke_smt_solver,
check_phase_shift_in_smt_solver,
phase_shift_id,
timeout
timeout,
):
equivalence_verified = True
num_equivalences_under_phase_shift += 1
Expand Down
4 changes: 1 addition & 3 deletions src/python/verifier/verify_equivalences.py
Original file line number Diff line number Diff line change
Expand Up @@ -43,7 +43,5 @@
check_phase_shift_in_smt_solver=(
False if len(sys.argv) <= 7 else ast.literal_eval(sys.argv[7])
),
timeout=(
30000 if len(sys.argv) <= 8 else ast.literal_eval(sys.argv[8])
)
timeout=(30000 if len(sys.argv) <= 8 else ast.literal_eval(sys.argv[8])),
)

0 comments on commit a3f0f51

Please sign in to comment.