Simplify condition.

This commit is contained in:
chriseth 2022-03-20 21:52:26 +01:00
parent 6f7f60903e
commit 22aba74176

View File

@ -263,17 +263,15 @@ smtutil::Expression ReasoningBasedSimplifier::encodeEVMBuiltin(
return booleanValue(arguments.at(0) == constantValue(0)); return booleanValue(arguments.at(0) == constantValue(0));
case evmasm::Instruction::AND: case evmasm::Instruction::AND:
return smtutil::Expression::ite( return smtutil::Expression::ite(
(arguments.at(0) == 0 || arguments.at(0) == 1) && arguments.at(0) + arguments.at(1) <= 2,
(arguments.at(1) == 0 || arguments.at(1) == 1), booleanValue(arguments.at(0) + arguments.at(1) >= 2),
booleanValue(arguments.at(0) == 1 && arguments.at(1) == 1),
// TODO we could probably restrict it a bit more // TODO we could probably restrict it a bit more
newRestrictedVariable() newRestrictedVariable()
); );
case evmasm::Instruction::OR: case evmasm::Instruction::OR:
return smtutil::Expression::ite( return smtutil::Expression::ite(
(arguments.at(0) == 0 || arguments.at(0) == 1) && arguments.at(0) + arguments.at(1) <= 2,
(arguments.at(1) == 0 || arguments.at(1) == 1), booleanValue(arguments.at(0) + arguments.at(1) >= 1),
booleanValue(arguments.at(0) == 1 || arguments.at(1) == 1),
// TODO we could probably restrict it a bit more // TODO we could probably restrict it a bit more
newRestrictedVariable() newRestrictedVariable()
); );