diff options
Diffstat (limited to 'backends/smt2/smtbmc.py')
| -rw-r--r-- | backends/smt2/smtbmc.py | 52 |
1 files changed, 29 insertions, 23 deletions
diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index fa4966089..bb763647c 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -35,6 +35,7 @@ dumpall = False assume_skipped = None final_only = False topmod = None +noinfo = False so = SmtOpts() @@ -60,6 +61,10 @@ yosys-smtbmc [options] <yosys_smt2_output> --smtc <constr_filename> read constraints file + --noinfo + only run the core proof, do not collect and print any + additional information (e.g. which assert failed) + --final-only only check final constraints, assume base case @@ -89,7 +94,7 @@ yosys-smtbmc [options] <yosys_smt2_output> try: opts, args = getopt.getopt(sys.argv[1:], so.shortopts + "t:igm:", so.longopts + - ["final-only", "assume-skipped=", "smtc=", "dump-vcd=", "dump-vlogtb=", "dump-smtc=", "dump-all"]) + ["final-only", "assume-skipped=", "smtc=", "dump-vcd=", "dump-vlogtb=", "dump-smtc=", "dump-all", "noinfo"]) except: usage() @@ -121,6 +126,8 @@ for o, a in opts: outconstr = a elif o == "--dump-all": dumpall = True + elif o == "--noinfo": + noinfo = True elif o == "-i": tempind = True elif o == "-g": @@ -136,11 +143,6 @@ if len(args) != 1: usage() -if tempind and len(inconstr) != 0: - print("Error: options -i and --smtc are exclusive.") - sys.exit(1) - - constr_final_start = None constr_asserts = defaultdict(list) constr_assumes = defaultdict(list) @@ -163,7 +165,8 @@ for fn in inconstr: if tokens[0] == "initial": current_states = set() - current_states.add(0) + if not tempind: + current_states.add(0) continue if tokens[0] == "final": @@ -182,20 +185,21 @@ for fn in inconstr: if tokens[0] == "state": current_states = set() - for token in tokens[1:]: - tok = token.split(":") - if len(tok) == 1: - current_states.add(int(token)) - elif len(tok) == 2: - lower = int(tok[0]) - if tok[1] == "*": - upper = num_steps + if not tempind: + for token in tokens[1:]: + tok = token.split(":") + if len(tok) == 1: + current_states.add(int(token)) + elif len(tok) == 2: + lower = int(tok[0]) + if tok[1] == "*": + upper = num_steps + else: + upper = int(tok[1]) + for i in range(lower, upper+1): + current_states.add(i) else: - upper = int(tok[1]) - for i in range(lower, upper+1): - current_states.add(i) - else: - assert 0 + assert 0 continue if tokens[0] == "always": @@ -281,12 +285,10 @@ def print_msg(msg): sys.stdout.flush() print_msg("Solver: %s" % (so.solver)) -smt.setup("QF_AUFBV") with open(args[0], "r") as f: for line in f: smt.write(line) - smt.info(line) if topmod is None: topmod = smt.topmod @@ -490,6 +492,7 @@ def print_failed_asserts_worker(mod, state, path): def print_failed_asserts(state, final=False): + if noinfo: return loc_list, expr_list, value_list = get_constr_expr(constr_asserts, state, final=final, getvalues=True) for loc, expr, value in zip(loc_list, expr_list, value_list): @@ -511,6 +514,7 @@ def print_anyconsts_worker(mod, state, path): def print_anyconsts(state): + if noinfo: return print_anyconsts_worker(topmod, "s%d" % state, topmod) @@ -522,13 +526,15 @@ if tempind: smt.write("(assert (|%s_u| s%d))" % (topmod, step)) smt.write("(assert (|%s_h| s%d))" % (topmod, step)) smt.write("(assert (not (|%s_is| s%d)))" % (topmod, step)) + smt.write("(assert %s)" % get_constr_expr(constr_assumes, step)) if step == num_steps: - smt.write("(assert (not (|%s_a| s%d)))" % (topmod, step)) + smt.write("(assert (not (and (|%s_a| s%d) %s)))" % (topmod, step, get_constr_expr(constr_asserts, step))) else: smt.write("(assert (|%s_t| s%d s%d))" % (topmod, step, step+1)) smt.write("(assert (|%s_a| s%d))" % (topmod, step)) + smt.write("(assert %s)" % get_constr_expr(constr_asserts, step)) if step > num_steps-skip_steps: print_msg("Skipping induction in step %d.." % (step)) |