mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2026-07-05 15:06:11 +00:00
Code Activity

smtbmc: support latest bitwuzla

Browse source
This commit is contained in:
Miodrag Milanovic 2026-06-22 08:40:16 +02:00
parent 5d7486115a
commit ebcbc06951
1 changed files with 24 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

25
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,29 @@ 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":
try:
help_text = subprocess.check_output([self.solver, "--help"], text=True)
except FileNotFoundError:
print("%s SMT Solver '%s' not found in path." % (self.timestamp(), self.solver), flush=True)
sys.exit(1)
if "--lang" in help_text:
self.popen_vargs = [self.solver, '--lang', 'smt2'] + self.solver_opts
self.unroll = True
if self.timeout != 0:
self.popen_vargs.append('--time-limit')
self.popen_vargs.append('%d000' % self.timeout)
else:
# Versions before 0.3
if self.noincr:
self.popen_vargs = [self.solver, '--smt2'] + self.solver_opts
else:
self.popen_vargs = [self.solver, '--smt2', '-i'] + self.solver_opts
self.unroll = True
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)]