mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-04-13 04:28:18 +00:00
Code Activity

Add support for the Bitwuzla solver

Browse source
This commit is contained in:
GCHQDeveloper560 2021-06-16 13:19:43 +01:00 committed by Marcelina Kościelnicka
parent 0565c642a0
commit 4379375d89
1 changed files with 5 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
backends/smt2/smtio.py
View file

@ -203,14 +203,14 @@ 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 == "boolector": if self.solver in ["boolector", "bitwuzla"]:
if self.noincr: if self.noincr:
self.popen_vargs = ['boolector', '--smt2'] + self.solver_opts self.popen_vargs = [self.solver, '--smt2'] + self.solver_opts
else: else:
self.popen_vargs = ['boolector', '--smt2', '-i'] + self.solver_opts self.popen_vargs = [self.solver, '--smt2', '-i'] + self.solver_opts
self.unroll = True self.unroll = True
if self.timeout != 0: if self.timeout != 0:
print('timeout option is not supported for boolector.') print('timeout option is not supported for %s.' % self.solver)
sys.exit(1) sys.exit(1)
if self.solver == "abc": if self.solver == "abc":
@ -1010,7 +1010,7 @@ class SmtOpts:
def helpmsg(self): def helpmsg(self):
return """ return """
-s <solver> -s <solver>
set SMT solver: z3, yices, boolector, cvc4, mathsat, dummy set SMT solver: z3, yices, boolector, bitwuzla, cvc4, mathsat, dummy
default: yices default: yices
-S <opt> -S <opt>