Merge branch 'divfloor-in-write_smt2' into smtlib2-expr-support

[yosys.git] / backends / smt2 / smt2.cc

diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index ed6f3aff980cf4d0308b42701cccf2aa491e8a51..4865db27761f8291c4bf375787cbedcf2502cb19 100644 (file)
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -436,6 +436,28 @@ struct Smt2Worker
                recursive_cells.erase(cell);
        }
 
+       void export_smtlib2_expr(RTLIL::Cell *cell)
+       {
+               RTLIL::SigSpec sig_a = cell->getPort(ID::A);
+               RTLIL::SigSpec sig_y = sigmap(cell->getPort(ID::Y));
+               string expr = cell->getParam(ID::EXPR).decode_string();
+
+               string a_bv = get_bv(sig_a);
+
+               if (verbose)
+                       log("%*s-> import cell: %s\n", 2 + 2 * GetSize(recursive_cells), "", log_id(cell));
+
+               int expr_idcounter = idcounter++;
+
+               decls.push_back(stringf("(define-fun |%s#%d| ((A (_ BitVec %d))) (_ BitVec %d) ; %s\n  %s\n)\n", get_id(module), expr_idcounter,
+                                       GetSize(sig_a), GetSize(sig_y), log_signal(sig_y), expr.c_str()));
+               decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) (_ BitVec %d) (|%s#%d| %s)) ; %s\n", get_id(module), idcounter,
+                                       get_id(module), GetSize(sig_y), get_id(module), expr_idcounter, a_bv.c_str(), log_signal(sig_y)));
+               register_bv(sig_y, idcounter++);
+
+               recursive_cells.erase(cell);
+       }
+
        void export_bvop(RTLIL::Cell *cell, std::string expr, char type = 0)
        {
                RTLIL::SigSpec sig_a, sig_b;
@@ -713,6 +735,10 @@ struct Smt2Worker
                                return;
                        }
 
+                       if (cell->type == ID($smtlib2_expr)) {
+                               return export_smtlib2_expr(cell);
+                       }
+
                        // FIXME: $slice $concat
                }