This commit is contained in:
Eric Mertens 2023-04-07 09:07:32 -07:00
parent a1bd117b56
commit 930a02622d

View File

@ -50,21 +50,20 @@ public:
Grammar() : Grammar::base_type{input} { Grammar() : Grammar::base_type{input} {
using namespace qi::labels; using namespace qi::labels;
variable %= qi::as_string[+qi::alpha]; variable = qi::as_string[+qi::alpha];
op = qi::string("+") [ _val = Op::Add ] op =
| qi::string("-") [ _val = Op::Sub ] qi::string("+") [ _val = Op::Add ] |
| qi::string("*") [ _val = Op::Mul ] qi::string("-") [ _val = Op::Sub ] |
| qi::string("/") [ _val = Op::Div ]; qi::string("*") [ _val = Op::Mul ] |
expr = variable [phx::bind(&Expr::lhs, _val) = _1] qi::string("/") [ _val = Op::Div ];
>> " " expr =
>> op [phx::bind(&Expr::op, _val) = _1] variable [phx::bind(&Expr::lhs, _val) = _1] >> " " >>
>> " " op [phx::bind(&Expr::op, _val) = _1] >> " " >>
>> variable [phx::bind(&Expr::rhs, _val) = _1]; variable [phx::bind(&Expr::rhs, _val) = _1];
rhs = expr [ _val = _1 ] | qi::long_long [ _val = _1 ]; rhs = expr | qi::long_long;
line = variable [ phx::bind(&Entry::lvalue, _val) = _1] line =
>> ": " variable [ phx::bind(&Entry::lvalue, _val) = _1] >> ": " >>
>> rhs [ phx::bind(&Entry::rvalue, _val) = _1] rhs [ phx::bind(&Entry::rvalue, _val) = _1] >> "\n";
>> "\n";
input = *line; input = *line;
} }
}; };
@ -91,8 +90,7 @@ auto Eval(
std::string const& var) std::string const& var)
-> double -> double
{ {
auto it = values.find(var); if (auto const it = values.find(var); it != values.end()) {
if (it != values.end()) {
return it->second; return it->second;
} }
auto const& [lhs,rhs,op] = exprs.at(var); auto const& [lhs,rhs,op] = exprs.at(var);
@ -125,8 +123,8 @@ auto Part1(Input const& input) -> std::int64_t
auto Part2(Input const& input) -> std::int64_t auto Part2(Input const& input) -> std::int64_t
{ {
auto ctx = z3::context{}; auto ctx = z3::context{};
auto solve_eqs = z3::tactic{ctx, "solve-eqs"}; auto const solve_eqs = z3::tactic{ctx, "solve-eqs"};
auto smt = z3::tactic{ctx, "smt"}; auto const smt = z3::tactic{ctx, "smt"};
auto solver = (solve_eqs & smt).mk_solver(); auto solver = (solve_eqs & smt).mk_solver();
std::unordered_map<std::string, z3::expr> constants; std::unordered_map<std::string, z3::expr> constants;
@ -144,10 +142,10 @@ auto Part2(Input const& input) -> std::int64_t
} else if (entry.lvalue != "humn") { } else if (entry.lvalue != "humn") {
auto const rhs = auto const rhs =
std::visit(overloaded { std::visit(overloaded {
[&ctx](std::int64_t literal) { [&](std::int64_t literal) {
return ctx.int_val(literal); return ctx.int_val(literal);
}, },
[&ctx, &constants, &solver](Expr const& expr) { [&](Expr const& expr) {
auto const l = constants.at(expr.lhs); auto const l = constants.at(expr.lhs);
auto const r = constants.at(expr.rhs); auto const r = constants.at(expr.rhs);
switch (expr.op) { switch (expr.op) {