Added $anyconst support to smt2 back-end

diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index af048859c99f51feb641638e66075f5a8c54ee24..43601cd248e4fec1955eec84f3c78d45d301f4b7 100644 (file)
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -403,6 +403,16 @@ struct Smt2Worker
                                return;
                        }
 
+                       if (cell->type == "$anyconst")
+                       {
+                               registers.insert(cell);
+                               decls.push_back(stringf("(declare-fun |%s#%d| (|%s_s|) (_ BitVec %d)) ; %s\n",
+                                               get_id(module), idcounter, get_id(module), GetSize(cell->getPort("\\Y")), log_signal(cell->getPort("\\Y"))));
+                               register_bv(cell->getPort("\\Y"), idcounter++);
+                               recursive_cells.erase(cell);
+                               return;
+                       }
+
                        if (cell->type == "$and") return export_bvop(cell, "(bvand A B)");
                        if (cell->type == "$or") return export_bvop(cell, "(bvor A B)");
                        if (cell->type == "$xor") return export_bvop(cell, "(bvxor A B)");
@@ -677,6 +687,13 @@ struct Smt2Worker
                                        trans.push_back(stringf("  (= %s %s) ; %s %s\n", expr_d.c_str(), expr_q.c_str(), get_id(cell), log_signal(cell->getPort("\\Q"))));
                                }
 
+                               if (cell->type == "$anyconst")
+                               {
+                                       std::string expr_d = get_bv(cell->getPort("\\Y"));
+                                       std::string expr_q = get_bv(cell->getPort("\\Y"), "next_state");
+                                       trans.push_back(stringf("  (= %s %s) ; %s %s\n", expr_d.c_str(), expr_q.c_str(), get_id(cell), log_signal(cell->getPort("\\Y"))));
+                               }
+
                                if (cell->type == "$mem")
                                {
                                        int arrayid = memarrays.at(cell);