github.com/YosysHQ.yosys
1
0
Fork 0
mirror of synced 2026-04-26 04:08:28 +00:00
Code Issues Releases Wiki Activity

Merge pull request #2016 from boqwxp/qbfsat-yices

Browse Source 
qbfsat: Add `-solver` option and allow choice of Z3 or Yices, making Yices the default.
This commit is contained in:
clairexen
2020-05-29 16:21:45 +02:00
committed by GitHub
parent 626c74adbd 54570a3978
commit 1c8d5a08a0
2 changed files with 52 additions and 21 deletions
Download Patch File Download Diff File Expand all files Collapse all files

6
backends/smt2/smtio.py
View File

@@ -172,7 +172,7 @@ class SmtIo:
self.unroll = False
if self.solver == "yices":
if self.noincr:
if self.noincr or self.forall:
self.popen_vargs = ['yices-smt2'] + self.solver_opts
else:
self.popen_vargs = ['yices-smt2', '--incremental'] + self.solver_opts
@@ -232,12 +232,16 @@ class SmtIo:
if self.logic_uf: self.logic += "UF"
if self.logic_bv: self.logic += "BV"
if self.logic_dt: self.logic = "ALL"
if self.solver == "yices" and self.forall: self.logic = "BV"
self.setup_done = True
for stmt in self.info_stmts:
self.write(stmt)
if self.forall and self.solver == "yices":
self.write("(set-option :yices-ef-max-iters 1000000000)")
if self.produce_models:
self.write("(set-option :produce-models true)")