Make the remaining (relevant) miniBDD catch-style unit tests

Author: tautschnig

unit/Makefile

@@ -116,19 +116,15 @@ N_CATCH_TESTS = $(shell \
                     -a -not -name "expr_undefined_casts.cpp") | \
                   grep -c -E "(SCENARIO|TEST_CASE)")
 
-TESTS = miniBDD$(EXEEXT) \
-        # Empty last line
-
-CLEANFILES = $(CATCH_TEST) $(TESTS) testing-utils/testing-utils$(LIBEXT)
+CLEANFILES = $(CATCH_TEST) testing-utils/testing-utils$(LIBEXT)
 
 # only add a dependency for libraries to avoid triggering implicit rules, which
 # would cause unnecessary rebuilds
 $(filter %$(LIBEXT), CPROVER_LIBS): cprover.dir
 
-all: $(CATCH_TEST) $(TESTS)
+all: $(CATCH_TEST)
 
-test: $(CATCH_TEST) $(TESTS)
-	$(foreach test,$(TESTS), (echo Running: $(test); ./$(test)) &&) true
+test: $(CATCH_TEST)
 	if ! ./$(CATCH_TEST) -l | grep -q "^$(N_CATCH_TESTS) test cases" ; then \
 		./$(CATCH_TEST) -l ; fi
 	./$(CATCH_TEST)
@@ -138,6 +134,3 @@ test: $(CATCH_TEST) $(TESTS)
 
 unit_tests$(EXEEXT): $(OBJ)
 	$(LINKBIN)
-
-miniBDD$(EXEEXT): miniBDD$(OBJEXT) $(CPROVER_LIBS)
-	$(LINKBIN)

unit/miniBDD.cpp

@@ -13,10 +13,12 @@
 
 #include <solvers/miniBDD/miniBDD.h>
 #include <solvers/flattening/boolbv.h>
+#include <solvers/prop/bdd_expr.h>
 
-#include <util/symbol_table.h>
 #include <util/arith_tools.h>
 #include <util/expanding_vector.h>
+#include <util/format_expr.h>
+#include <util/symbol_table.h>
 
 class bdd_propt:public propt
 {
@@ -291,4 +293,65 @@ SCENARIO("miniBDD", "[core][solver][miniBDD]")
 
     REQUIRE(!result.is_constant());
   }
+
+  GIVEN("A bdd for x&y")
+  {
+    mini_bdd_mgrt mgr;
+
+    mini_bddt final_bdd = mgr.Var("x") & mgr.Var("y");
+
+    std::ostringstream oss;
+    mgr.DumpDot(oss);
+
+    const std::string dot_string =
+      "digraph BDD {\n"
+      "center = true;\n"
+      "{ rank = same; { node [style=invis]; \"T\" };\n"
+      "  { node [shape=box,fontsize=24]; \"0\"; }\n"
+      "  { node [shape=box,fontsize=24]; \"1\"; }\n"
+      "}\n"
+      "\n"
+      "{ rank=same; { node [shape=plaintext,fontname="
+      "\"Times Italic\",fontsize=24] \" y \" }; \"4\"; }\n"
+      "{ rank=same; { node [shape=plaintext,fontname="
+      "\"Times Italic\",fontsize=24] \" x \" }; \"3\"; }\n"
+      "\n"
+      "{ edge [style = invis]; \" y \" -> \" x \" -> \"T\"; }\n"
+      "\n"
+      "\"3\" -> \"1\" [style=solid,arrowsize=\".75\"];\n"
+      "\"3\" -> \"0\" [style=dashed,arrowsize=\".75\"];\n"
+      "\n"
+      "\"4\" -> \"3\" [style=solid,arrowsize=\".75\"];\n"
+      "\"4\" -> \"0\" [style=dashed,arrowsize=\".75\"];\n"
+      "\n"
+      "}\n";
+
+    REQUIRE(oss.str() == dot_string);
+  }
+
+  GIVEN("A bdd for (a&b)|!a")
+  {
+    symbol_exprt a("a", bool_typet());
+    symbol_exprt b("b", bool_typet());
+
+    or_exprt o(and_exprt(a, b), not_exprt(a));
+
+    symbol_tablet symbol_table;
+    namespacet ns(symbol_table);
+
+    {
+      std::ostringstream oss;
+      oss << format(o);
+      REQUIRE(oss.str() == "(a ∧ b) ∨ (¬a)");
+    }
+
+    bdd_exprt t(ns);
+    t.from_expr(o);
+
+    {
+      std::ostringstream oss;
+      oss << format(t.as_expr());
+      REQUIRE(oss.str() == "(¬a) ∨ b");
+    }
+  }
 }