mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-04-24 01:25:33 +00:00
Code Activity

qbfsat: Add -solver option and allow choice of Z3 or Yices, making Yices the default.

Browse source 
Ensures that "BV" is the logic whenever solving an exists-forall problem with Yices, moves the "(set-logic ...)" directive above any non-info line, sets the `ef-max-iters` parameter to a very high number when using Yices in exists-forall mode so as not to prematurely abandon difficult problems, and does not provide the incompatible "--incremental" Yices argument when in exists-forall mode.
This commit is contained in:
Alberto Gonzalez 2020-04-30 21:27:18 +00:00
parent 59b355fb85
commit 903456c267
No known key found for this signature in database
GPG key ID: 8395A8BA109708B2
2 changed files with 54 additions and 23 deletions
Download patch file Download diff file Expand all files Collapse all files

10
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,17 +232,21 @@ 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)")
self.write("(set-logic %s)" % self.logic)
for stmt in self.info_stmts:
self.write(stmt)
def timestamp(self):
secs = int(time() - self.start_time)
return "## %3d:%02d:%02d " % (secs // (60*60), (secs // 60) % 60, secs % 60)