glguy/aocpp
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

z3 compat

Browse Source
This commit is contained in:
Eric Mertens 2023-04-06 21:07:44 -07:00
parent 509672bc9e
commit a1bd117b56
1 changed files with 3 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
2022/21.cpp
View File

@ -163,10 +163,12 @@ auto Part2(Input const& input) -> std::int64_t
solver.add(constants.at(entry.lvalue) == rhs); solver.add(constants.at(entry.lvalue) == rhs);
} }
} }
if (solver.check() != z3::sat) { if (solver.check() != z3::sat) {
throw std::runtime_error{"no solution to part 2"}; throw std::runtime_error{"no solution to part 2"};
} }
return solver.get_model().eval(constants.at("humn")).as_int64();
return solver.get_model().eval(constants.at("humn")).get_numeral_int64();
} }
} // namespace } // namespace