Added boolector support to yosys-smtbmc

diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index 30a6bb19cef0b7b1bc8f2888a46050d1f46e242a..b881f01545381996255d901c72b67c3f760f8dd2 100644 (file)
--- 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 1de0b2a308d8c0ccf0b3128f0e396392b69d51ef..22d48d886d7516da4c6370e87b46243524649e3f 100644 (file)
--- 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 dad63e567d4b23f6dbfaaf7dab25b23dff48b9a2..9c4a0225eea52b9edb90a7b866dcc7c0ac87668a 100644 (file)
--- 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()