From 9078ed8afda029960c82934670db881c835d6f2b Mon Sep 17 00:00:00 2001 From: chriseth Date: Wed, 1 Jun 2022 13:23:43 +0200 Subject: [PATCH] Implement => for boolean equality. --- libsolutil/BooleanLP.cpp | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/libsolutil/BooleanLP.cpp b/libsolutil/BooleanLP.cpp index d570e8d6e..7c467eb16 100644 --- a/libsolutil/BooleanLP.cpp +++ b/libsolutil/BooleanLP.cpp @@ -779,6 +779,12 @@ void BooleanLPSolver::addBooleanEquality(Literal const& _left, smtutil::Expressi state().clauses.emplace_back(Clause{vector{_left, negate(a)}}); state().clauses.emplace_back(Clause{vector{_left, negate(b)}}); } + else if (_right.name == "=>") + { + solAssert(_right.arguments.size() == 2); + // a = (x => y) <=> a = or(-x, y) + addBooleanEquality(_left, !_right.arguments.at(0) || _right.arguments.at(1), move(_letBindings)); + } else if (_right.name == "=") { // l = eq(a, b) <=> (-l or -a or b) and (-l or a or -b) and (l or -a or -b) and (l or a or b)