mirrors/sby
3
0
Fork 0
mirror of https://github.com/YosysHQ/sby.git synced 2025-10-31 13:02:28 +00:00
Code Activity

run() -> init().

Browse source 
Signed-off-by: William D. Jones <thor0505@comcast.net>
This commit is contained in:
William D. Jones 2019-03-29 03:57:47 -04:00 • committed by Ed Bordin
parent 009a8194dd
commit 826cd1a6f2
9 changed files with 22 additions and 22 deletions
Download patch file Download diff file Expand all files Collapse all files

8
sbysrc/sby_core.py
View file

@ -623,19 +623,19 @@ class SbyJob:
if self.opt_mode == "bmc":
import sby_mode_bmc
sby_mode_bmc.run(self)
sby_mode_bmc.init(self)
elif self.opt_mode == "prove":
import sby_mode_prove
sby_mode_prove.run(self)
sby_mode_prove.init(self)
elif self.opt_mode == "live":
import sby_mode_live
sby_mode_live.run(self)
sby_mode_live.init(self)
elif self.opt_mode == "cover":
import sby_mode_cover
sby_mode_cover.run(self)
sby_mode_cover.init(self)
else:
assert False

2
sbysrc/sby_engine_abc.py
View file

@ -19,7 +19,7 @@
import re, os, getopt
from sby_core import SbyTask
def run(mode, job, engine_idx, engine):
def init(mode, job, engine_idx, engine):
abc_opts, abc_command = getopt.getopt(engine[1:], "", [])
if len(abc_command) == 0:

2
sbysrc/sby_engine_aiger.py
View file

@ -19,7 +19,7 @@
import re, os, getopt
from sby_core import SbyTask
def run(mode, job, engine_idx, engine):
def init(mode, job, engine_idx, engine):
opts, solver_args = getopt.getopt(engine[1:], "", [])
if len(solver_args) == 0:

2
sbysrc/sby_engine_btor.py
View file

@ -20,7 +20,7 @@ import re, os, getopt
from types import SimpleNamespace
from sby_core import SbyTask
def run(mode, job, engine_idx, engine):
def init(mode, job, engine_idx, engine):
random_seed = None
opts, solver_args = getopt.getopt(engine[1:], "", ["seed="])

6
sbysrc/sby_engine_smtbmc.py
View file

@ -19,7 +19,7 @@
import re, os, getopt
from sby_core import SbyTask
def run(mode, job, engine_idx, engine):
def init(mode, job, engine_idx, engine):
smtbmc_opts = []
nomem_opt = False
presat_opt = True
@ -102,9 +102,9 @@ def run(mode, job, engine_idx, engine):
if mode == "prove":
if not induction_only:
run("prove_basecase", job, engine_idx, engine)
init("prove_basecase", job, engine_idx, engine)
if not basecase_only:
run("prove_induction", job, engine_idx, engine)
init("prove_induction", job, engine_idx, engine)
return
taskname = "engine_{}".format(engine_idx)

8
sbysrc/sby_mode_bmc.py
View file

@ -19,7 +19,7 @@
import re, os, getopt
from sby_core import SbyTask
def run(job):
def init(job):
job.handle_int_option("depth", 20)
job.handle_int_option("append", 0)
job.handle_str_option("aigsmt", "yices")
@ -33,15 +33,15 @@ def run(job):
if engine[0] == "smtbmc":
import sby_engine_smtbmc
sby_engine_smtbmc.run("bmc", job, engine_idx, engine)
sby_engine_smtbmc.init("bmc", job, engine_idx, engine)
elif engine[0] == "abc":
import sby_engine_abc
sby_engine_abc.run("bmc", job, engine_idx, engine)
sby_engine_abc.init("bmc", job, engine_idx, engine)
elif engine[0] == "btor":
import sby_engine_btor
sby_engine_btor.run("bmc", job, engine_idx, engine)
sby_engine_btor.init("bmc", job, engine_idx, engine)
else:
job.error("Invalid engine '{}' for bmc mode.".format(engine[0]))

4
sbysrc/sby_mode_cover.py
View file

@ -19,7 +19,7 @@
import re, os, getopt
from sby_core import SbyTask
def run(job):
def init(job):
job.handle_int_option("depth", 20)
job.handle_int_option("append", 0)
@ -32,7 +32,7 @@ def run(job):
if engine[0] == "smtbmc":
import sby_engine_smtbmc
sby_engine_smtbmc.run("cover", job, engine_idx, engine)
sby_engine_smtbmc.init("cover", job, engine_idx, engine)
elif engine[0] == "btor":
import sby_engine_btor

4
sbysrc/sby_mode_live.py
View file

@ -19,7 +19,7 @@
import re, os, getopt
from sby_core import SbyTask
def run(job):
def init(job):
job.handle_str_option("aigsmt", "yices")
job.status = "UNKNOWN"
@ -33,7 +33,7 @@ def run(job):
if engine[0] == "aiger":
import sby_engine_aiger
sby_engine_aiger.run("live", job, engine_idx, engine)
sby_engine_aiger.init("live", job, engine_idx, engine)
else:
job.error("Invalid engine '{}' for live mode.".format(engine[0]))

8
sbysrc/sby_mode_prove.py
View file

@ -19,7 +19,7 @@
import re, os, getopt
from sby_core import SbyTask
def run(job):
def init(job):
job.handle_int_option("depth", 20)
job.handle_int_option("append", 0)
job.handle_str_option("aigsmt", "yices")
@ -40,15 +40,15 @@ def run(job):
if engine[0] == "smtbmc":
import sby_engine_smtbmc
sby_engine_smtbmc.run("prove", job, engine_idx, engine)
sby_engine_smtbmc.init("prove", job, engine_idx, engine)
elif engine[0] == "aiger":
import sby_engine_aiger
sby_engine_aiger.run("prove", job, engine_idx, engine)
sby_engine_aiger.init("prove", job, engine_idx, engine)
elif engine[0] == "abc":
import sby_engine_abc
sby_engine_abc.run("prove", job, engine_idx, engine)
sby_engine_abc.init("prove", job, engine_idx, engine)
else:
job.error("Invalid engine '{}' for prove mode.".format(engine[0]))