From fa5565b606bf58de1e1150c937afe014fcd928b6 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Sat, 3 Sep 2016 14:26:00 +0200 Subject: [PATCH] Added boolector support to yosys-smtbmc --- backends/smt2/smt2.cc | 30 +++++++++++++++++++--------- backends/smt2/smtbmc.py | 44 ++++++++++++++++++++--------------------- backends/smt2/smtio.py | 17 ++++++++++++++-- 3 files changed, 58 insertions(+), 33 deletions(-) diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc index 30a6bb19c..b881f0154 100644 --- a/backends/smt2/smt2.cc +++ b/backends/smt2/smt2.cc @@ -751,27 +751,39 @@ struct Smt2Worker string assert_expr = assert_list.empty() ? "true" : "(and"; if (!assert_list.empty()) { - for (auto &str : assert_list) - assert_expr += stringf("\n %s", str.c_str()); - assert_expr += "\n)"; + if (GetSize(assert_list) == 1) { + assert_expr = assert_list.front(); + } else { + for (auto &str : assert_list) + assert_expr += stringf("\n %s", str.c_str()); + assert_expr += "\n)"; + } } decls.push_back(stringf("(define-fun |%s_a| ((state |%s_s|)) Bool %s)\n", get_id(module), get_id(module), assert_expr.c_str())); string assume_expr = assume_list.empty() ? "true" : "(and"; if (!assume_list.empty()) { - for (auto &str : assume_list) - assume_expr += stringf("\n %s", str.c_str()); - assume_expr += "\n)"; + if (GetSize(assume_list) == 1) { + assume_expr = assume_list.front(); + } else { + for (auto &str : assume_list) + assume_expr += stringf("\n %s", str.c_str()); + assume_expr += "\n)"; + } } decls.push_back(stringf("(define-fun |%s_u| ((state |%s_s|)) Bool %s)\n", get_id(module), get_id(module), assume_expr.c_str())); string init_expr = init_list.empty() ? "true" : "(and"; if (!init_list.empty()) { - for (auto &str : init_list) - init_expr += stringf("\n %s", str.c_str()); - init_expr += "\n)"; + if (GetSize(init_list) == 1) { + init_expr = init_list.front(); + } else { + for (auto &str : init_list) + init_expr += stringf("\n %s", str.c_str()); + init_expr += "\n)"; + } } decls.push_back(stringf("(define-fun |%s_i| ((state |%s_s|)) Bool %s)\n", get_id(module), get_id(module), init_expr.c_str())); diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index 1de0b2a30..22d48d886 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -514,17 +514,17 @@ if tempind: retstatus = False skip_counter = step_size for step in range(num_steps, -1, -1): - smt.write("(declare-fun s%d () %s_s)" % (step, topmod)) - 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("(declare-fun s%d () |%s_s|)" % (step, topmod)) + 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)) if step == num_steps: - smt.write("(assert (not (%s_a s%d)))" % (topmod, step)) + smt.write("(assert (not (|%s_a| s%d)))" % (topmod, 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_t| s%d s%d))" % (topmod, step, step+1)) + smt.write("(assert (|%s_a| s%d))" % (topmod, step)) if step > num_steps-skip_steps: print("%s Skipping induction in step %d.." % (smt.timestamp(), step)) @@ -560,23 +560,23 @@ else: # not tempind step = 0 retstatus = True while step < num_steps: - smt.write("(declare-fun s%d () %s_s)" % (step, topmod)) - smt.write("(assert (%s_u s%d))" % (topmod, step)) - smt.write("(assert (%s_h s%d))" % (topmod, step)) + smt.write("(declare-fun s%d () |%s_s|)" % (step, topmod)) + smt.write("(assert (|%s_u| s%d))" % (topmod, step)) + smt.write("(assert (|%s_h| s%d))" % (topmod, step)) smt.write("(assert %s)" % get_constr_expr(constr_assumes, step)) if step == 0: - smt.write("(assert (%s_i s0))" % (topmod)) - smt.write("(assert (%s_is s0))" % (topmod)) + smt.write("(assert (|%s_i| s0))" % (topmod)) + smt.write("(assert (|%s_is| s0))" % (topmod)) else: - smt.write("(assert (%s_t s%d s%d))" % (topmod, step-1, step)) - smt.write("(assert (not (%s_is s%d)))" % (topmod, step)) + smt.write("(assert (|%s_t| s%d s%d))" % (topmod, step-1, step)) + smt.write("(assert (not (|%s_is| s%d)))" % (topmod, step)) if step < skip_steps: if assume_skipped is not None and step >= assume_skipped: print("%s Skipping step %d (and assuming pass).." % (smt.timestamp(), step)) - smt.write("(assert (%s_a s%d))" % (topmod, step)) + smt.write("(assert (|%s_a| s%d))" % (topmod, step)) smt.write("(assert %s)" % get_constr_expr(constr_asserts, step)) else: print("%s Skipping step %d.." % (smt.timestamp(), step)) @@ -586,10 +586,10 @@ else: # not tempind last_check_step = step for i in range(1, step_size): if step+i < num_steps: - smt.write("(declare-fun s%d () %s_s)" % (step+i, topmod)) - smt.write("(assert (%s_u s%d))" % (topmod, step+i)) - smt.write("(assert (%s_h s%d))" % (topmod, step+i)) - smt.write("(assert (%s_t s%d s%d))" % (topmod, step+i-1, step+i)) + smt.write("(declare-fun s%d () |%s_s|)" % (step+i, topmod)) + smt.write("(assert (|%s_u| s%d))" % (topmod, step+i)) + smt.write("(assert (|%s_h| s%d))" % (topmod, step+i)) + smt.write("(assert (|%s_t| s%d s%d))" % (topmod, step+i-1, step+i)) smt.write("(assert %s)" % get_constr_expr(constr_assumes, step+i)) last_check_step = step+i @@ -601,7 +601,7 @@ else: # not tempind print("%s Checking asserts in steps %d to %d.." % (smt.timestamp(), step, last_check_step)) smt.write("(push 1)") - smt.write("(assert (not (and %s)))" % " ".join(["(%s_a s%d)" % (topmod, i) for i in range(step, last_check_step+1)] + + smt.write("(assert (not (and %s)))" % " ".join(["(|%s_a| s%d)" % (topmod, i) for i in range(step, last_check_step+1)] + [get_constr_expr(constr_asserts, i) for i in range(step, last_check_step+1)])) if smt.check_sat() == "sat": @@ -616,7 +616,7 @@ else: # not tempind smt.write("(pop 1)") for i in range(step, last_check_step+1): - smt.write("(assert (%s_a s%d))" % (topmod, i)) + smt.write("(assert (|%s_a| s%d))" % (topmod, i)) smt.write("(assert %s)" % get_constr_expr(constr_asserts, i)) if constr_final_start is not None: @@ -644,7 +644,7 @@ else: # not tempind else: # gentrace for i in range(step, last_check_step+1): - smt.write("(assert (%s_a s%d))" % (topmod, i)) + smt.write("(assert (|%s_a| s%d))" % (topmod, i)) smt.write("(assert %s)" % get_constr_expr(constr_asserts, i)) print("%s Solving for step %d.." % (smt.timestamp(), last_check_step)) diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index dad63e567..9c4a0225e 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -17,8 +17,7 @@ # OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. # -import sys -import subprocess +import sys, subprocess, re from select import select from time import time @@ -84,6 +83,10 @@ class SmtIo: if self.solver == "mathsat": popen_vargs = ['mathsat'] + if self.solver == "boolector": + self.declared_sorts = list() + popen_vargs = ['boolector', '--smt2', '-i'] + self.p = subprocess.Popen(popen_vargs, stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.STDOUT) self.start_time = time() @@ -104,11 +107,21 @@ class SmtIo: def write(self, stmt): stmt = stmt.strip() + + if self.solver == "boolector": + if stmt.startswith("(declare-sort"): + self.declared_sorts.append(stmt.split()[1]) + return + for n in self.declared_sorts: + stmt = stmt.replace(n, "(_ BitVec 16)") + if self.debug_print: print("> %s" % stmt) + if self.debug_file: print(stmt, file=self.debug_file) self.debug_file.flush() + self.p.stdin.write(bytes(stmt + "\n", "ascii")) self.p.stdin.flush() -- 2.30.2