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

Run solver in non-incremental mode whem smtio.py is configured for non-incremental solving

Browse source 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
This commit is contained in:
Clifford Wolf 2018-11-06 11:11:05 +01:00
parent 60ecc5c70c
commit f6c4485a3a
1 changed files with 12 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

15
backends/smt2/smtio.py
View file

@ -163,19 +163,28 @@ class SmtIo:
self.unroll = False self.unroll = False
if self.solver == "yices": if self.solver == "yices":
self.popen_vargs = ['yices-smt2', '--incremental'] + self.solver_opts if self.noincr:
self.popen_vargs = ['yices-smt2'] + self.solver_opts
else:
self.popen_vargs = ['yices-smt2', '--incremental'] + self.solver_opts
if self.solver == "z3": if self.solver == "z3":
self.popen_vargs = ['z3', '-smt2', '-in'] + self.solver_opts self.popen_vargs = ['z3', '-smt2', '-in'] + self.solver_opts
if self.solver == "cvc4": if self.solver == "cvc4":
self.popen_vargs = ['cvc4', '--incremental', '--lang', 'smt2.6' if self.logic_dt else 'smt2'] + self.solver_opts if self.noincr:
self.popen_vargs = ['cvc4', '--lang', 'smt2.6' if self.logic_dt else 'smt2'] + self.solver_opts
else:
self.popen_vargs = ['cvc4', '--incremental', '--lang', 'smt2.6' if self.logic_dt else 'smt2'] + self.solver_opts
if self.solver == "mathsat": if self.solver == "mathsat":
self.popen_vargs = ['mathsat'] + self.solver_opts self.popen_vargs = ['mathsat'] + self.solver_opts
if self.solver == "boolector": if self.solver == "boolector":
self.popen_vargs = ['boolector', '--smt2', '-i'] + self.solver_opts if self.noincr:
self.popen_vargs = ['boolector', '--smt2'] + self.solver_opts
else:
self.popen_vargs = ['boolector', '--smt2', '-i'] + self.solver_opts
self.unroll = True self.unroll = True
if self.solver == "abc": if self.solver == "abc":