Skip to content

Commit

Permalink
Check that there are not other solutions other than the first given
Browse files Browse the repository at this point in the history
  • Loading branch information
RCoeurjoly committed Jul 4, 2024
1 parent c3fbdc6 commit 752ea70
Showing 1 changed file with 12 additions and 1 deletion.
13 changes: 12 additions & 1 deletion tests/functional/single_cells/vcd_harness_smt.py
Original file line number Diff line number Diff line change
Expand Up @@ -41,7 +41,7 @@
# Load and execute the SMT file
with open(smt_file_path, 'r') as smt_file:
for line in smt_file:
smt_io.write(line.strip())
smt_io.write(line.strip())
smt_io.check_sat()
# Read and parse the SMT file line by line
with open(smt_file_path, 'r') as smt_file:
Expand Down Expand Up @@ -161,6 +161,17 @@ def hex_to_bin(value):
value = hex_to_bin(value[1:])
print(f" {output_name}: {value}")
signals[output_name].append((step, value))
smt_io.write(f'(push 1)')
smt_io.write(f'(assert (not (= ({output_name} test_outputs_step_n{step}) #{value})))')
result = smt_io.check_sat(["unsat"])
if result != 'unsat':
smt_io.p_close()
sys.exit(1)
smt_io.write(f'(pop 1)')
result = smt_io.check_sat(["sat"])
if result != 'sat':
smt_io.p_close()
sys.exit(1)

smt_io.p_close()

Expand Down

0 comments on commit 752ea70

Please sign in to comment.