From 6406fdfc0ab951a4db6479cc3b782ae739d008f8 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Mon, 25 Feb 2019 15:59:30 +0000 Subject: [PATCH 1/2] Fix bdd.as_expr() There was a mistake in the way complement is computed when going to the then_branch. --- src/solvers/prop/bdd_expr.cpp | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/solvers/prop/bdd_expr.cpp b/src/solvers/prop/bdd_expr.cpp index 51718f3317a..1443a1b8b34 100644 --- a/src/solvers/prop/bdd_expr.cpp +++ b/src/solvers/prop/bdd_expr.cpp @@ -119,11 +119,14 @@ exprt bdd_exprt::as_expr(const bdd_nodet &r, bool complement) const if(r.else_branch().is_complement() != complement) { return and_exprt( - n_expr, as_expr(r.then_branch(), complement != r.is_complement())); + n_expr, + as_expr( + r.then_branch(), complement != r.then_branch().is_complement())); } return or_exprt( not_exprt(n_expr), - as_expr(r.then_branch(), complement != r.is_complement())); + as_expr( + r.then_branch(), complement != r.then_branch().is_complement())); } } else if(r.then_branch().is_constant()) From e1fb6b7fec3e8f123121eb7d4459b4c213782872 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Mon, 25 Feb 2019 16:13:41 +0000 Subject: [PATCH 2/2] Add unit test for BDD This adds a test case to check there are no mistakes in the BDD to expr conversions. This test can fail without the previous fix. --- unit/solvers/prop/bdd_expr.cpp | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) diff --git a/unit/solvers/prop/bdd_expr.cpp b/unit/solvers/prop/bdd_expr.cpp index 956410905d6..21eeda5ae97 100644 --- a/unit/solvers/prop/bdd_expr.cpp +++ b/unit/solvers/prop/bdd_expr.cpp @@ -44,4 +44,25 @@ SCENARIO("bdd_expr", "[core][solver][prop][bdd_expr]") REQUIRE(bdd.as_expr() == bdd2.as_expr()); } } + + GIVEN("A bdd for (a&!b)") + { + const symbol_exprt a("a", bool_typet()); + const symbol_exprt b("b", bool_typet()); + + bdd_exprt bdd{ns}; + bdd.from_expr(and_exprt(a, not_exprt(b))); + + WHEN("It is converted to an exprt") + { + const exprt result = bdd.as_expr(); + THEN("It is equal to the expression (a & !b) or (!b & a)") + { + REQUIRE(result.id() == ID_and); + REQUIRE(result.operands().size() == 2); + REQUIRE((result.op0() == a || result.op1() == a)); + REQUIRE((result.op0() == not_exprt(b) || result.op1() == not_exprt(b))); + } + } + } }