feat(library/tactic): add support for migratic tactic framework object between Lua states

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/library/tactic/cex_builder.cpp

@@ -63,8 +63,13 @@ static const struct luaL_Reg cex_builder_m[] = {
     {0, 0}
 };
 
+static void cex_builder_migrate(lua_State * src, int i, lua_State * tgt) {
+    push_cex_builder(tgt, to_cex_builder(src, i));
+}
+
 void open_cex_builder(lua_State * L) {
     luaL_newmetatable(L, cex_builder_mt);
+    set_migrate_fn_field(L, -1, cex_builder_migrate);
     lua_pushvalue(L, -1);
     lua_setfield(L, -2, "__index");
     setfuncs(L, cex_builder_m, 0);

src/library/tactic/goal.cpp

@@ -294,8 +294,17 @@ static const struct luaL_Reg goal_m[] = {
     {0, 0}
 };
 
+static void hypotheses_migrate(lua_State * src, int i, lua_State * tgt) {
+    push_hypotheses(tgt, to_hypotheses(src, i));
+}
+
+static void goal_migrate(lua_State * src, int i, lua_State * tgt) {
+    push_goal(tgt, to_goal(src, i));
+}
+
 void open_goal(lua_State * L) {
     luaL_newmetatable(L, hypotheses_mt);
+    set_migrate_fn_field(L, -1, hypotheses_migrate);
     lua_pushvalue(L, -1);
     lua_setfield(L, -2, "__index");
     setfuncs(L, hypotheses_m, 0);
@@ -304,6 +313,7 @@ void open_goal(lua_State * L) {
     SET_GLOBAL_FUN(mk_hypotheses, "hypotheses");
 
     luaL_newmetatable(L, goal_mt);
+    set_migrate_fn_field(L, -1, goal_migrate);
     lua_pushvalue(L, -1);
     lua_setfield(L, -2, "__index");
     setfuncs(L, goal_m, 0);

src/library/tactic/proof_builder.cpp

@@ -114,8 +114,21 @@ static const struct luaL_Reg proof_builder_m[] = {
     {0, 0}
 };
 
+static void proof_map_migrate(lua_State * src, int i, lua_State * tgt) {
+    push_proof_map(tgt, to_proof_map(src, i));
+}
+
+static void assignment_migrate(lua_State * src, int i, lua_State * tgt) {
+    push_assignment(tgt, to_assignment(src, i));
+}
+
+static void proof_builder_migrate(lua_State * src, int i, lua_State * tgt) {
+    push_proof_builder(tgt, to_proof_builder(src, i));
+}
+
 void open_proof_builder(lua_State * L) {
     luaL_newmetatable(L, proof_map_mt);
+    set_migrate_fn_field(L, -1, proof_map_migrate);
     lua_pushvalue(L, -1);
     lua_setfield(L, -2, "__index");
     setfuncs(L, proof_map_m, 0);
@@ -124,6 +137,7 @@ void open_proof_builder(lua_State * L) {
     SET_GLOBAL_FUN(mk_proof_map, "proof_map");
 
     luaL_newmetatable(L, assignment_mt);
+    set_migrate_fn_field(L, -1, assignment_migrate);
     lua_pushvalue(L, -1);
     lua_setfield(L, -2, "__index");
     setfuncs(L, assignment_m, 0);
@@ -132,6 +146,7 @@ void open_proof_builder(lua_State * L) {
     SET_GLOBAL_FUN(mk_assignment, "assignment");
 
     luaL_newmetatable(L, proof_builder_mt);
+    set_migrate_fn_field(L, -1, proof_builder_migrate);
     lua_pushvalue(L, -1);
     lua_setfield(L, -2, "__index");
     setfuncs(L, proof_builder_m, 0);

src/library/tactic/proof_state.cpp

@@ -239,8 +239,17 @@ static const struct luaL_Reg proof_state_m[] = {
     {0, 0}
 };
 
+static void goals_migrate(lua_State * src, int i, lua_State * tgt) {
+    push_goals(tgt, to_goals(src, i));
+}
+
+static void proof_state_migrate(lua_State * src, int i, lua_State * tgt) {
+    push_proof_state(tgt, to_proof_state(src, i));
+}
+
 void open_proof_state(lua_State * L) {
     luaL_newmetatable(L, goals_mt);
+    set_migrate_fn_field(L, -1, goals_migrate);
     lua_pushvalue(L, -1);
     lua_setfield(L, -2, "__index");
     setfuncs(L, goals_m, 0);
@@ -249,6 +258,7 @@ void open_proof_state(lua_State * L) {
     SET_GLOBAL_FUN(mk_goals, "goals");
 
     luaL_newmetatable(L, proof_state_mt);
+    set_migrate_fn_field(L, -1, proof_state_migrate);
     lua_pushvalue(L, -1);
     lua_setfield(L, -2, "__index");
     setfuncs(L, proof_state_m, 0);

src/library/tactic/tactic.cpp

@@ -430,6 +430,10 @@ static const struct luaL_Reg tactic_m[] = {
     {0, 0}
 };
 
+static void tactic_migrate(lua_State * src, int i, lua_State * tgt) {
+    push_tactic(tgt, to_tactic(src, i));
+}
+
 void open_tactic(lua_State * L) {
     luaL_newmetatable(L, proof_state_seq_mt);
     lua_pushvalue(L, -1);
@@ -438,6 +442,7 @@ void open_tactic(lua_State * L) {
     SET_GLOBAL_FUN(proof_state_seq_pred, "is_proof_state_seq");
 
     luaL_newmetatable(L, tactic_mt);
+    set_migrate_fn_field(L, -1, tactic_migrate);
     lua_pushvalue(L, -1);
     lua_setfield(L, -2, "__index");
     setfuncs(L, tactic_m, 0);

src/util/interrupt.cpp

@@ -40,6 +40,7 @@ void sleep_for(unsigned ms, unsigned step_ms) {
         check_interrupted();
     }
     std::this_thread::sleep_for(r);
+    check_interrupted();
 }
 
 std::atomic_bool * interruptible_thread::get_flag_addr() {

tests/lua/threads/tactict1.lua

@@ -0,0 +1,36 @@
+local env  = environment()
+local ios  = io_state()
+local Bool = Const("Bool")
+env:add_var("p", Bool)
+env:add_var("q", Bool)
+local p, q = Consts("p, q")
+local ctx  = context()
+
+S = State()
+-- Create tactic t1 in a different Lua State.
+-- So, t1 can be executed by a different execution
+-- thread
+local t1 = S:eval([[
+     counter1 = 0
+     return tactic(function(env, ios, s)
+                     while true do
+                        print("tactic 1")
+                        counter1 = counter1 + 1
+                        sleep(10)
+                     end
+                  end)
+]])
+
+counter2 = 0
+local t2 = tactic(function(env, ios, s)
+                     while true do
+                        print("tactic 2")
+                        counter2 = counter2 + 1
+                        sleep(10)
+                     end
+                  end)
+
+local T = (t1:par(t2)):try_for(150)
+T:solve(env, ios, ctx, p)
+assert(counter2 > 2)
+S:eval([[ assert(counter1 > 2) ]])