Merge pull request #6 from olarozenfeld/fix-empath-mayor

Couple of bugfixes

Author: olarozenfeld

.bazelversion

@@ -0,0 +1 @@
+5.3.0

src/game_log.proto

@@ -296,6 +296,10 @@ message Event {
     StorytellerInteraction storyteller_interaction = 3;
     Nomination nomination = 4;
     Vote vote = 5;
+    // Use the empty string to indicate no execution in the rare case where you
+    // explicitly want to note that nobody was executed in final 3, and yet
+    // a Mayor win DID NOT occur, and you still want to solve at that point, and
+    // not after the game continued.
     string execution = 6;
     // Storyteller announces that the player is dead. This can be due to
     // execution, Slayer shot, Tinker, Witch, or any other day-time effect.

src/game_sat_solver.cc

@@ -127,7 +127,7 @@ void GameSatSolver::AddChefConstraints(int chef, int chef_number) {
       if (role_claims_[i][0] == RECLUSE) {
         evil_options_i.push_back(
             model_.NewEquivalentVarAnd(
-                {RoleVar(i, RECLUSE, night1), Not(PoisonerPickVar(i, night1))},
+                {RoleVar(i, RECLUSE, night1), Not(PoisonedVar(i, night1))},
                 absl::StrFormat("healthy_recluse_%s_%s", g_.PlayerName(i),
                                 night1)));
       }
@@ -151,7 +151,7 @@ void GameSatSolver::AddChefConstraints(int chef, int chef_number) {
       evil_pairs, chef_number, absl::StrFormat(
           "chef_%s_number_%d", g_.PlayerName(chef), chef_number));
   model_.AddOr(
-    {Not(RoleVar(chef, CHEF, night1)), PoisonerPickVar(chef, night1), correct});
+    {Not(RoleVar(chef, CHEF, night1)), PoisonedVar(chef, night1), correct});
 }
 
 void GameSatSolver::AddEmpathConstraints() {
@@ -167,17 +167,19 @@ void GameSatSolver::AddEmpathConstraints() {
 }
 
 void GameSatSolver::AddEmpathConstraints(
-    int player, int number, const Time& time) {
+    int player, int number, const Time& night_time) {
+  // Empath goes after Evils, so the time of all registration checks needs
+  // to be the daytime:
+  const Time time = night_time + 1;
   vector<int> alive_neighbors = g_.AliveNeighbors(player, time);  // Size 2.
   const int ping1 = alive_neighbors[0], ping2 = alive_neighbors[1];
-  // We assume a Spy will not be poisoned. But Empath goes after the Imp, so
-  // need to check day role.
+  // We assume a Spy will not be poisoned.
   BoolVar ping1_regs_good = model_.NewEquivalentVarOr(
-      {Not(StartingEvilVar(ping1)), RoleVar(ping1, SPY, time + 1)},
+      {Not(StartingEvilVar(ping1)), RoleVar(ping1, SPY, time)},
       absl::StrFormat("empath_%s_registers_%s_good_%s", g_.PlayerName(player),
                       g_.PlayerName(ping1), time));
   BoolVar ping2_regs_good = model_.NewEquivalentVarOr(
-      {Not(StartingEvilVar(ping2)), RoleVar(ping2, SPY, time + 1)},
+      {Not(StartingEvilVar(ping2)), RoleVar(ping2, SPY, time)},
       absl::StrFormat("empath_%s_registers_%s_good_%s", g_.PlayerName(player),
                       g_.PlayerName(ping2), time));
   vector<BoolVar> ping1_regs_evil_cases({StartingEvilVar(ping1)});
@@ -252,11 +254,13 @@ void GameSatSolver::AddFortuneTellerConstraints() {
 }
 
 void GameSatSolver::AddFortuneTellerConstraints(
-    int player, int pick1, int pick2, bool yes, const Time& time) {
+    int player, int pick1, int pick2, bool yes, const Time& night_time) {
+  // Fortune Teller goes after Evils, so time of all registration checks needs
+  // to be the daytime:
+  const Time time = night_time + 1;
   vector<BoolVar> yes_options({
-      // Fortune Teller goes after the Imp, so we need to check day roles.
-      RoleVar(pick1, IMP, time + 1), RedHerringVar(pick1),
-      RoleVar(pick2, IMP, time + 1), RedHerringVar(pick2)});
+      RoleVar(pick1, IMP, time), RedHerringVar(pick1),
+      RoleVar(pick2, IMP, time), RedHerringVar(pick2)});
   BoolVar poisoned_recluse;
   if (yes) {  // We can only infer Recluse possibilities from Yes answer.
     for (int pick : {pick1, pick2}) {
@@ -427,16 +431,20 @@ BoolVar GameSatSolver::AliveRoleVar(Role role, const Time& time) {
       absl::StrFormat("alive_%s_%s", Role_Name(role), time));
 }
 
+// This works for everyone except the Imp. The Imp is poisoned iff they were
+// picked by the Poisoner. Everyone else also need to account for the
+// Poisoner being alive on the *day after* the pick.
 BoolVar GameSatSolver::PoisonedVar(int player, const Time& time) {
   Time night = time.is_day ? time - 1 : time;
-  BoolVar picked = PoisonerPickVar(player, time);
+  BoolVar picked = PoisonerPickVar(player, night);
   const auto night_deaths = g_.Deaths(night);
   if (night_deaths.empty()) {
     return picked;
   }
-  // At most one night death in TB:
+  // This accounts for both a starpass to the Poisoner and Imp killing the
+  // Poisoner in the night.
   return model_.NewEquivalentVarAnd(
-      {Not(RoleVar(night_deaths[0], POISONER, night)), picked},
+      {AliveRoleVar(POISONER, night + 1), picked},
       absl::StrFormat("poisoned_%s_%s", g_.PlayerName(player), night));
 }
 
@@ -591,7 +599,8 @@ void GameSatSolver::AddNoVictoryConstraints(const Time& time) {
   vector<BoolVar> cases;
   // No Mayor win.
   if (num_alive - g_.Deaths(time).size() == 3 &&
-      g_.Execution(time) == kNoPlayer) {
+      g_.Execution(time) == kNoPlayer &&
+      (time < g_.CurrentTime() || g_.NoExecutionsDeclared())) {
     // Mayor was not alive or poisoned.
     for (int mayor : AliveRolePossibilities(MAYOR, time)) {
       cases.push_back(model_.NewEquivalentVarOr(
@@ -971,7 +980,7 @@ void GameSatSolver::AddImpStarpassConstraints(const Time& time) {
     const Role role_claim = role_claims_[i][time.count - 1];
     BoolVar healthy_recluse_i = role_claim == IMP ?
         model_.NewEquivalentVarAnd(
-            {RoleVar(i, RECLUSE, time), Not(PoisonerPickVar(i, time))},
+            {RoleVar(i, RECLUSE, time), Not(PoisonedVar(i, time))},
             absl::StrFormat("healthy_recluse_%s_%s", g_.PlayerName(i), time)) :
         model_.FalseVar();
     for (Role role : {POISONER, SPY, SCARLET_WOMAN, BARON, RECLUSE}) {
@@ -1017,12 +1026,12 @@ void GameSatSolver::AddImpActionConstraints(const internal::RoleAction& ra) {
     // Target was not a healthy Soldier
     if (IsRolePossible(imp_kill, SOLDIER, time)) {
       model_.AddOr({Not(RoleVar(imp_kill, SOLDIER, time)),
-                    PoisonerPickVar(imp_kill, time)});
+                    PoisonedVar(imp_kill, time)});
     }
     // Target was not healthy Monk protected
     for (int monk : PossibleMonkProtecting(imp_kill, time)) {
       model_.AddOr({Not(RoleVar(monk, MONK, time)),
-                    PoisonerPickVar(monk, time)});
+                    PoisonedVar(monk, time)});
     }
     return;
   }
@@ -1034,25 +1043,25 @@ void GameSatSolver::AddImpActionConstraints(const internal::RoleAction& ra) {
     if (IsRolePossible(target, SOLDIER, time)) {
       cases.push_back(model_.NewEquivalentVarAnd(
           {RoleVar(target, SOLDIER, time),
-           Not(PoisonerPickVar(target, time))},
+           Not(PoisonedVar(target, time))},
           absl::StrFormat("healthy_SOLDIER_%s_%s", g_.PlayerName(target),
                           time)));
     }
     // Target was healthy Monk protected
     for (int monk : PossibleMonkProtecting(target, time)) {
       cases.push_back(model_.NewEquivalentVarAnd(
           {RoleVar(monk, MONK, time),
-            Not(PoisonerPickVar(monk, time))},
+           Not(PoisonedVar(monk, time))},
           absl::StrFormat("healthy_MONK_%s_%s", g_.PlayerName(monk), time)));
     }
     // Target was a healthy Mayor, not healthy Monk protected, and bounced to no
     // kill.
     if (IsRolePossible(target, MAYOR, time)) {
       vector<BoolVar> mayor_bounce_no_kill(
-          {RoleVar(target, MAYOR, time), Not(PoisonerPickVar(target, time))});
+          {RoleVar(target, MAYOR, time), Not(PoisonedVar(target, time))});
       for (int monk : PossibleMonkProtecting(target, time)) {
         mayor_bounce_no_kill.push_back(model_.NewEquivalentVarOr(
-            {Not(RoleVar(monk, MONK, time)), PoisonerPickVar(monk, time)},
+            {Not(RoleVar(monk, MONK, time)), PoisonedVar(monk, time)},
             absl::StrFormat("not_healthy_MONK_%s_%s", g_.PlayerName(monk),
                             time)));
       }
@@ -1063,13 +1072,13 @@ void GameSatSolver::AddImpActionConstraints(const internal::RoleAction& ra) {
           // Healthy Soldier.
           if (IsRolePossible(i, SOLDIER, time)) {
             no_kill_cases.push_back(model_.NewEquivalentVarAnd(
-                {RoleVar(i, SOLDIER, time), Not(PoisonerPickVar(i, time))},
+                {RoleVar(i, SOLDIER, time), Not(PoisonedVar(i, time))},
                 absl::StrFormat("healthy_SOLDIER_%s_%s", g_.PlayerName(i),
                                 time)));
           }
           for (int monk : PossibleMonkProtecting(i, time)) {
             no_kill_cases.push_back(model_.NewEquivalentVarAnd(
-                {RoleVar(monk, MONK, time), Not(PoisonerPickVar(monk, time))},
+                {RoleVar(monk, MONK, time), Not(PoisonedVar(monk, time))},
                 absl::StrFormat("healthy_MONK_%s_%s", g_.PlayerName(monk),
                                 time)));
           }
@@ -1088,10 +1097,10 @@ void GameSatSolver::AddImpActionConstraints(const internal::RoleAction& ra) {
   // Kill bounces. Target is a healthy Mayor, not healthy Monk protected.
   if (IsRolePossible(target, MAYOR, time)) {
     model_.AddEquality(RoleVar(target, MAYOR, time), true);
-    model_.AddEquality(PoisonerPickVar(target, time), false);
+    model_.AddEquality(PoisonedVar(target, time), false);
     for (int monk : PossibleMonkProtecting(target, time)) {
       model_.AddOr({Not(RoleVar(monk, MONK, time)),
-                    PoisonerPickVar(monk, time)});
+                    PoisonedVar(monk, time)});
     }
     return;
   }
@@ -1125,12 +1134,12 @@ void GameSatSolver::AddImpConstraints(
     // Target was not a healthy Soldier
     if (IsRolePossible(imp_kill, SOLDIER, time)) {
       model_.AddOr({Not(RoleVar(imp_kill, SOLDIER, time)),
-                    PoisonerPickVar(imp_kill, time)});
+                    PoisonedVar(imp_kill, time)});
     }
     // Target was not healthy Monk protected
     for (int monk : PossibleMonkProtecting(imp_kill, time)) {
       model_.AddOr({Not(RoleVar(monk, MONK, time)),
-                    PoisonerPickVar(monk, time)});
+                    PoisonedVar(monk, time)});
     }
     return;
   }
@@ -1147,7 +1156,7 @@ void GameSatSolver::AddImpConstraints(
     for (int i : AliveRolePossibilities(role, time)) {
       cases.push_back(model_.NewEquivalentVarAnd(
           {RoleVar(i, role, time),
-            Not(PoisonerPickVar(i, time))},
+            Not(PoisonedVar(i, time))},
           absl::StrFormat("healthy_%s_%s_%s", Role_Name(role),
                           g_.PlayerName(i), time)));
     }

src/game_sat_solver_test.cc

@@ -13,6 +13,7 @@
 
 #include <filesystem>
 #include <map>
+#include <memory>
 
 #include "src/game_sat_solver.h"
 #include "src/game_state.h"
@@ -806,6 +807,32 @@ TEST(Starpass, PoisonerPerspectiveCatch) {
   EXPECT_WORLDS_EQ(Solve(g), expected_worlds);
 }
 
+TEST(Starpass, BaronPerspectiveCatch) {
+  GameState g(PLAYER, TROUBLE_BREWING, MakePlayers(7));
+  g.AddNight(1);
+  g.AddShownToken("P7", BARON);
+  g.AddDay(1);
+  g.AddRoleClaims(
+      {SOLDIER, EMPATH, MAYOR, RECLUSE, RAVENKEEPER, BUTLER, LIBRARIAN}, "P1");
+  g.AddClaimRoleAction("P2", g.NewEmpathInfo(0));
+  g.AddClaimRoleAction("P6", g.NewButlerAction("P2"));
+  g.AddClaimRoleAction("P7", g.NewLibrarianInfo("P2", "P3", DRUNK));
+  g.AddNominationVoteExecution("P2", "P4");
+  g.AddDeath("P4");
+  g.AddNight(2);
+  g.AddDay(2);
+  g.AddNightDeath("P2");
+  g.AddClaimRoleAction("P6", g.NewButlerAction("P2"));
+  g.AddNominationVoteExecution("P1", "P6");
+  g.AddDeath("P6");
+  g.AddNight(3);
+  g.AddShownToken("P7", IMP);
+  g.AddDay(3);
+  g.AddNightDeath("P5");
+  g.AddClaimRoleAction("P5", g.NewRavenkeeperAction("P3", IMP));
+  EXPECT_TRUE(IsValidWorld(g));
+}
+
 TEST(Starpass, InvalidPoisonerPerspectiveCatch) {
   GameState g(PLAYER, TROUBLE_BREWING, MakePlayers(5));
   g.AddNight(1);
@@ -1004,6 +1031,26 @@ TEST(FortuneTeller, LearnsTrueInfo) {
   EXPECT_TRUE(IsValidWorld(g));
 }
 
+TEST(FortuneTeller, UnpoisonedAfterStarpass) {
+  GameState g(PLAYER, TROUBLE_BREWING, MakePlayers(5));
+  g.AddNight(1);
+  g.AddShownToken("P1", POISONER);
+  g.AddRoleAction("P1", g.NewPoisonerAction("P4"));
+  g.AddDay(1);
+  g.AddRoleClaims({MAYOR, FORTUNE_TELLER, SLAYER, VIRGIN, SOLDIER}, "P1");
+  g.AddClaimRoleAction("P2", g.NewFortuneTellerAction("P3", "P4", true));
+  g.AddNominationVoteExecution("P1", "P4");
+  g.AddDeath("P4");
+  g.AddNight(2);
+  g.AddRoleAction("P1", g.NewPoisonerAction("P2"));
+  g.AddShownToken("P1", IMP);
+  g.AddDay(2);
+  g.AddNightDeath("P3");
+  g.AddClaimRoleAction("P2", g.NewFortuneTellerAction("P1", "P3", false));
+  // We know there is no way for the Fortune Teller to be wrong here.
+  EXPECT_FALSE(IsValidWorld(g));
+}
+
 TEST(Empath, LearnsTrueInfo) {
   GameState g(PLAYER, TROUBLE_BREWING, MakePlayers(10));
   g.AddNight(1);
@@ -1048,6 +1095,33 @@ TEST(Empath, LearnsTrueInfo) {
   EXPECT_WORLDS_EQ(Solve(g, r), {roles});
 }
 
+TEST(Empath, GainsInfoOnNewNeighbor) {
+  GameState g(PLAYER, TROUBLE_BREWING, MakePlayers(7));
+  g.AddNight(1);
+  g.AddShownToken("P1", EMPATH);
+  g.AddRoleAction("P1", g.NewEmpathInfo(0));
+  g.AddDay(1);
+  g.AddRoleClaims(
+      {EMPATH, SLAYER, SLAYER, RAVENKEEPER, SOLDIER, CHEF, MONK}, "P1");
+  g.AddClaimRoleAction("P1", g.NewEmpathInfo(0));
+  g.AddClaimRoleAction("P6", g.NewChefInfo(0));
+  // P3 double-claims the Slayer and gets Slayer-shot in the face:
+  g.AddRoleAction("P2", g.NewSlayerAction("P3"));
+  g.AddDeath("P3");  // Scarlet Woman confirmed!
+  g.AddNominationVoteExecution("P1", "P4");
+  g.AddDeath("P4");
+  g.AddNight(2);
+  g.AddRoleAction("P1", g.NewEmpathInfo(1));
+  g.AddDay(2);
+  g.AddNightDeath("P2");
+  g.AddClaimRoleAction("P1", g.NewEmpathInfo(1));
+  g.AddClaimRoleAction("P7", g.NewMonkAction("P1"));
+  vector<unordered_map<string, Role>> expected_worlds({
+      {{"P1", EMPATH}, {"P2", SLAYER}, {"P3", IMP}, {"P4", RAVENKEEPER},
+       {"P5", IMP}, {"P6", CHEF}, {"P7", MONK}}});
+  EXPECT_WORLDS_EQ(Solve(g), expected_worlds);
+}
+
 TEST(Slayer, ImpDeducesDrunkSlayer) {
   GameState g(PLAYER, TROUBLE_BREWING, MakePlayers(7));
   g.AddNight(1);
@@ -1255,6 +1329,27 @@ TEST(GameEndConditions, PoisonedMayorNoWin) {
   EXPECT_FALSE(IsValidWorld(g, r));
 }
 
+TEST(GameEndConditions, MayorMightBeDroisoned) {
+  GameState g(PLAYER, TROUBLE_BREWING, MakePlayers(5));
+  g.AddNight(1);
+  g.AddShownToken("P1", MAYOR);
+  g.AddDay(1);
+  g.AddRoleClaims({MAYOR, SLAYER, VIRGIN, RECLUSE, SAINT}, "P1");
+  g.AddNominationVoteExecution("P1", "P3");
+  g.AddDeath("P3");
+  g.AddNight(2);
+  g.AddDay(2);
+  g.AddNightDeath("P2");  // Final 3.
+  SolverRequest r = SolverRequestBuilder::FromCurrentRoles("P1", DRUNK);
+  EXPECT_TRUE(IsValidWorld(g, r));
+  r = SolverRequestBuilder()
+      .AddCurrentRoles("P1", MAYOR).AddHealthy("P1", 2).Build();
+  EXPECT_TRUE(IsValidWorld(g, r));
+  r = SolverRequestBuilder()
+      .AddCurrentRoles("P1", MAYOR).AddPoisoned("P1", 2).Build();
+  EXPECT_TRUE(IsValidWorld(g, r));
+}
+
 TEST(Spy, SpyPerspective) {
   GameState g(PLAYER, TROUBLE_BREWING, MakePlayers(13));
   g.AddNight(1);
@@ -1306,7 +1401,7 @@ TEST(Examples, ExamplesWork) {
   map<path, int> world_counts_by_game({
     {"tb/monk.pbtxt", 3},
     {"tb/teensy_observer.pbtxt", 3},
-    {"tb/virgin.pbtxt", 8},
+    {"tb/virgin.pbtxt", 9},
   });
   string dir = "src/examples/";
   for (const auto& it : world_counts_by_game) {

src/game_state.cc

@@ -364,6 +364,7 @@ GameState& GameState::AddDay(int count) {
   log_.add_events()->set_day(count);
   ++cur_time_;
   on_the_block_ = kNoPlayer;
+  declare_no_executions_ = false;
   executions_.push_back(kNoPlayer);
   execution_deaths_.push_back(kNoPlayer);
   night_deaths_.push_back(kNoPlayer);
@@ -516,7 +517,12 @@ GameState& GameState::AddVote(absl::Span<const string> votes,
 GameState& GameState::AddExecution(const string& name) {
   log_.add_events()->set_execution(name);
   CHECK(cur_time_.is_day) << "Executions can only occur during the day.";
-  const int executee = PlayerIndex(name);
+  CHECK(!declare_no_executions_) << "No executions was already declared.";
+  const int executee = PlayerIndex(name, true);
+  if (executee == kNoPlayer) {
+    declare_no_executions_ = true;
+    return *this;
+  }
   CHECK_EQ(executions_.back(), kNoPlayer)
       << "More than one execution attempted.";
   CHECK(!nominations_.empty()) << "Execution must have a preceding nomination.";
@@ -705,7 +711,7 @@ GameState& GameState::AddAllShownTokens(absl::Span<const Role> roles) {
   return *this;
 }
 
-// Returns the deaths chronilogically. Execution is always the last death.
+// Returns the deaths chronologically. Execution is always the last death.
 vector<int> GameState::Deaths(const Time& time) const {
   vector<int> result;
   if (time.is_day) {