Skip to content

Couple of bugfixes #6

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
olarozenfeld merged 1 commit into from
Apr 6, 2025
Merged

Couple of bugfixes #6

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions .bazelversion
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
5.3.0
4 changes: 4 additions & 0 deletions src/game_log.proto
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
67 changes: 38 additions & 29 deletions src/game_sat_solver.cc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)));
}
Expand All @@ -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() {
Expand All @@ -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)});
Expand Down Expand Up @@ -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}) {
Expand Down Expand Up @@ -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));
}

Expand Down Expand Up @@ -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(
Expand Down Expand Up @@ -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}) {
Expand Down Expand Up @@ -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;
}
Expand All @@ -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)));
}
Expand All @@ -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)));
}
Expand All @@ -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;
}
Expand Down Expand Up @@ -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;
}
Expand All @@ -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)));
}
Expand Down
97 changes: 96 additions & 1 deletion src/game_sat_solver_test.cc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,7 @@

#include <filesystem>
#include <map>
#include <memory>

#include "src/game_sat_solver.h"
#include "src/game_state.h"
Expand Down Expand Up @@ -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);
Expand Down Expand Up @@ -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);
Expand Down Expand Up @@ -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);
Expand Down Expand Up @@ -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);
Expand Down Expand Up @@ -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) {
Expand Down
10 changes: 8 additions & 2 deletions src/game_state.cc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand Down Expand Up @@ -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.";
Expand Down Expand Up @@ -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) {
Expand Down
Loading