Add "write_smt2 -stdt" mode

diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index 9d07a1216e040dadefc291d903a2589c6e9e44af..372dbeb5725839db73c3b889ccc01a8f85a69e97 100644 (file)
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -32,11 +32,11 @@ struct Smt2Worker
        CellTypes ct;
        SigMap sigmap;
        RTLIL::Module *module;
-       bool bvmode, memmode, wiresmode, verbose, statebv;
+       bool bvmode, memmode, wiresmode, verbose, statebv, statedt;
        dict<IdString, int> &mod_stbv_width;
        int idcounter, statebv_width;
 
-       std::vector<std::string> decls, trans, hier;
+       std::vector<std::string> decls, trans, hier, dtmembers;
        std::map<RTLIL::SigBit, RTLIL::Cell*> bit_driver;
        std::set<RTLIL::Cell*> exported_cells, hiercells, hiercells_queue;
        pool<Cell*> recursive_cells, registers;
@@ -78,6 +78,14 @@ struct Smt2Worker
                                statebv_width += width;
                        }
                }
+               else if (statedt)
+               {
+                       if (width == 0) {
+                               decl_str = stringf("  (|%s| Bool)", name.c_str());
+                       } else {
+                               decl_str = stringf("  (|%s| (_ BitVec %d))", name.c_str(), width);
+                       }
+               }
                else
                {
                        if (width == 0) {
@@ -89,12 +97,16 @@ struct Smt2Worker
 
                if (!comment.empty())
                        decl_str += " ; " + comment;
-               decls.push_back(decl_str + "\n");
+
+               if (statedt)
+                       dtmembers.push_back(decl_str + "\n");
+               else
+                       decls.push_back(decl_str + "\n");
        }
 
-       Smt2Worker(RTLIL::Module *module, bool bvmode, bool memmode, bool wiresmode, bool verbose, bool statebv, dict<IdString, int> &mod_stbv_width) :
+       Smt2Worker(RTLIL::Module *module, bool bvmode, bool memmode, bool wiresmode, bool verbose, bool statebv, bool statedt, dict<IdString, int> &mod_stbv_width) :
                        ct(module->design), sigmap(module), module(module), bvmode(bvmode), memmode(memmode), wiresmode(wiresmode),
-                       verbose(verbose), statebv(statebv), mod_stbv_width(mod_stbv_width), idcounter(0), statebv_width(0)
+                       verbose(verbose), statebv(statebv), statedt(statedt), mod_stbv_width(mod_stbv_width), idcounter(0), statebv_width(0)
        {
                makebits(stringf("%s_is", get_id(module)));
 
@@ -583,8 +595,12 @@ struct Smt2Worker
                        }
                        else
                        {
-                               decls.push_back(stringf("(declare-fun |%s#%d#0| (|%s_s|) (Array (_ BitVec %d) (_ BitVec %d))) ; %s\n",
-                                               get_id(module), arrayid, get_id(module), abits, width, get_id(cell)));
+                               if (statedt)
+                                       dtmembers.push_back(stringf("  (|%s#%d#0| (Array (_ BitVec %d) (_ BitVec %d))) ; %s\n",
+                                                       get_id(module), arrayid, abits, width, get_id(cell)));
+                               else
+                                       decls.push_back(stringf("(declare-fun |%s#%d#0| (|%s_s|) (Array (_ BitVec %d) (_ BitVec %d))) ; %s\n",
+                                                       get_id(module), arrayid, get_id(module), abits, width, get_id(cell)));
 
                                decls.push_back(stringf("(define-fun |%s_m %s| ((state |%s_s|)) (Array (_ BitVec %d) (_ BitVec %d)) (|%s#%d#0| state))\n",
                                                get_id(module), get_id(cell), get_id(module), abits, width, get_id(module), arrayid));
@@ -649,6 +665,9 @@ struct Smt2Worker
 
                        if (statebv)
                                makebits(stringf("%s_h %s", get_id(module), get_id(cell->name)), mod_stbv_width.at(cell->type));
+                       if (statedt)
+                               dtmembers.push_back(stringf("  (|%s_h %s| |%s_s|)\n",
+                                               get_id(module), get_id(cell->name), get_id(cell->type)));
                        else
                                decls.push_back(stringf("(declare-fun |%s_h %s| (|%s_s|) |%s_s|)\n",
                                                get_id(module), get_id(cell->name), get_id(module), get_id(cell->type)));
@@ -1009,6 +1028,12 @@ struct Smt2Worker
                if (statebv) {
                        f << stringf("(define-sort |%s_s| () (_ BitVec %d))\n", get_id(module), statebv_width);
                        mod_stbv_width[module->name] = statebv_width;
+               } else
+               if (statedt) {
+                       f << stringf("(declare-datatype |%s_s| ((|%s_mk|\n", get_id(module), get_id(module));
+                       for (auto it : dtmembers)
+                               f << it;
+                       f << stringf(")))\n");
                } else
                        f << stringf("(declare-sort |%s_s| 0)\n", get_id(module));
 
@@ -1126,6 +1151,10 @@ struct Smt2Backend : public Backend {
                log("        sort. As a side-effect this will prevent use of arrays to model\n");
                log("        memories.\n");
                log("\n");
+               log("    -stdt\n");
+               log("        Use SMT-LIB 2.6 style datatypes to represent a state instead of an\n");
+               log("        uninterpreted sort.\n");
+               log("\n");
                log("    -nobv\n");
                log("        disable support for BitVec (FixedSizeBitVectors theory). without this\n");
                log("        option multi-bit wires are represented using the BitVec sort and\n");
@@ -1199,7 +1228,7 @@ struct Smt2Backend : public Backend {
        virtual void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design)
        {
                std::ifstream template_f;
-               bool bvmode = true, memmode = true, wiresmode = false, verbose = false, statebv = false;
+               bool bvmode = true, memmode = true, wiresmode = false, verbose = false, statebv = false, statedt = false;
 
                log_header(design, "Executing SMT2 backend.\n");
 
@@ -1218,6 +1247,12 @@ struct Smt2Backend : public Backend {
                        }
                        if (args[argidx] == "-stbv") {
                                statebv = true;
+                               statedt = false;
+                               continue;
+                       }
+                       if (args[argidx] == "-stdt") {
+                               statebv = false;
+                               statedt = true;
                                continue;
                        }
                        if (args[argidx] == "-nobv") {
@@ -1264,6 +1299,9 @@ struct Smt2Backend : public Backend {
                if (statebv)
                        *f << stringf("; yosys-smt2-stbv\n");
 
+               if (statedt)
+                       *f << stringf("; yosys-smt2-stdt\n");
+
                std::vector<RTLIL::Module*> sorted_modules;
 
                // extract module dependencies
@@ -1304,7 +1342,7 @@ struct Smt2Backend : public Backend {
 
                        log("Creating SMT-LIBv2 representation of module %s.\n", log_id(module));
 
-                       Smt2Worker worker(module, bvmode, memmode, wiresmode, verbose, statebv, mod_stbv_width);
+                       Smt2Worker worker(module, bvmode, memmode, wiresmode, verbose, statebv, statedt, mod_stbv_width);
                        worker.run();
                        worker.write(*f);
 

diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py
index 38e3f31197614e294f2e52fb62af097e116536b4..14ee787f606e08f9ea5dc0bcc97c8d7a44bdd93c 100644 (file)
--- a/backends/smt2/smtio.py
+++ b/backends/smt2/smtio.py
@@ -53,6 +53,7 @@ class SmtIo:
         self.logic_ax = True
         self.logic_uf = True
         self.logic_bv = True
+        self.logic_dt = False
         self.produce_models = True
         self.smt2cache = [list()]
         self.p = None
@@ -82,6 +83,34 @@ class SmtIo:
             self.info_stmts = list()
             self.nocomments = False
 
+        if self.unroll:
+            self.logic_uf = False
+            self.unroll_idcnt = 0
+            self.unroll_buffer = ""
+            self.unroll_sorts = set()
+            self.unroll_objs = set()
+            self.unroll_decls = dict()
+            self.unroll_cache = dict()
+            self.unroll_stack = list()
+
+        self.start_time = time()
+
+        self.modinfo = dict()
+        self.curmod = None
+        self.topmod = None
+        self.setup_done = False
+
+    def setup(self):
+        assert not self.setup_done
+
+        if self.logic is None:
+            self.logic = ""
+            if self.logic_qf: self.logic += "QF_"
+            if self.logic_ax: self.logic += "A"
+            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":
             self.popen_vargs = ['yices-smt2', '--incremental'] + self.solver_opts
 
@@ -89,7 +118,7 @@ class SmtIo:
             self.popen_vargs = ['z3', '-smt2', '-in'] + self.solver_opts
 
         if self.solver == "cvc4":
-            self.popen_vargs = ['cvc4', '--incremental', '--lang', 'smt2'] + self.solver_opts
+            self.popen_vargs = ['cvc4', '--incremental', '--lang', 'smt2.6' if self.logic_dt else 'smt2'] + self.solver_opts
 
         if self.solver == "mathsat":
             self.popen_vargs = ['mathsat'] + self.solver_opts
@@ -116,33 +145,6 @@ class SmtIo:
             if not self.noincr:
                 self.p = subprocess.Popen(self.popen_vargs, stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.STDOUT)
 
-        if self.unroll:
-            self.logic_uf = False
-            self.unroll_idcnt = 0
-            self.unroll_buffer = ""
-            self.unroll_sorts = set()
-            self.unroll_objs = set()
-            self.unroll_decls = dict()
-            self.unroll_cache = dict()
-            self.unroll_stack = list()
-
-        self.start_time = time()
-
-        self.modinfo = dict()
-        self.curmod = None
-        self.topmod = None
-        self.setup_done = False
-
-    def setup(self):
-        assert not self.setup_done
-
-        if self.logic is None:
-            self.logic = ""
-            if self.logic_qf: self.logic += "QF_"
-            if self.logic_ax: self.logic += "A"
-            if self.logic_uf: self.logic += "UF"
-            if self.logic_bv: self.logic += "BV"
-
         self.setup_done = True
 
         if self.produce_models:
@@ -209,6 +211,9 @@ class SmtIo:
     def write(self, stmt, unroll=True):
         if stmt.startswith(";"):
             self.info(stmt)
+            if not self.setup_done:
+                self.info_stmts.append(stmt)
+                return
         elif not self.setup_done:
             self.setup()
 
@@ -304,6 +309,10 @@ class SmtIo:
             if self.logic is None:
                 self.logic_bv = False
 
+        if fields[1] == "yosys-smt2-stdt":
+            if self.logic is None:
+                self.logic_dt = True
+
         if fields[1] == "yosys-smt2-module":
             self.curmod = fields[2]
             self.modinfo[self.curmod] = SmtModInfo()