riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

smt2: fix bitwuzla invocation 

Bitwuzla no longer shares options in common with Boolector. It now
requires "--lang smt2", and always runs incrementally by default.
This commit is contained in:
Matt Young 2024-09-09 01:26:55 +10:00
parent dcf9f58315
commit c1228fec23
1 changed files with 10 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

11
backends/smt2/smtio.py
View File

@ -226,7 +226,7 @@ class SmtIo:
print('timeout option is not supported for mathsat.') print('timeout option is not supported for mathsat.')
sys.exit(1) sys.exit(1)
if self.solver in ["boolector", "bitwuzla"]: if self.solver == "boolector":
if self.noincr: if self.noincr:
self.popen_vargs = [self.solver, '--smt2'] + self.solver_opts self.popen_vargs = [self.solver, '--smt2'] + self.solver_opts
else: else:
@ -236,6 +236,15 @@ class SmtIo:
print('timeout option is not supported for %s.' % self.solver) print('timeout option is not supported for %s.' % self.solver)
sys.exit(1) sys.exit(1)
if self.solver == "bitwuzla":
self.popen_vargs = [self.solver, '--lang', 'smt2'] + self.solver_opts
self.unroll = True
# Bitwuzla always uses incremental solving
self.noincr = False
if self.timeout != 0:
print('timeout option is not supported for %s.' % self.solver)
sys.exit(1)
if self.solver == "abc": if self.solver == "abc":
if len(self.solver_opts) > 0: if len(self.solver_opts) > 0:
self.popen_vargs = ['yosys-abc', '-S', '; '.join(self.solver_opts)] self.popen_vargs = ['yosys-abc', '-S', '; '.join(self.solver_opts)]