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

Author: tautschnig

unit/CMakeLists.txt

@@ -3,9 +3,6 @@ file(GLOB_RECURSE sources "*.cpp" "*.h")
 file(GLOB_RECURSE testing_utils "testing-utils/*.cpp" "testing-utils/*.h")
 
 list(REMOVE_ITEM sources
-    # Used in executables
-    ${CMAKE_CURRENT_SOURCE_DIR}/miniBDD.cpp
-
     # Don't build
     ${CMAKE_CURRENT_SOURCE_DIR}/elf_reader.cpp
     ${CMAKE_CURRENT_SOURCE_DIR}/smt2_parser.cpp
@@ -48,14 +45,3 @@ add_test(
     WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR}
 )
 set_tests_properties(unit PROPERTIES LABELS "CORE;CBMC")
-
-add_executable(miniBDD miniBDD.cpp)
-target_include_directories(miniBDD
-    PUBLIC
-    ${CBMC_BINARY_DIR}
-    ${CBMC_SOURCE_DIR}
-    ${CMAKE_CURRENT_SOURCE_DIR}
-)
-target_link_libraries(miniBDD solvers ansi-c)
-add_test(NAME miniBDD COMMAND $<TARGET_FILE:miniBDD>)
-set_tests_properties(miniBDD PROPERTIES LABELS "CORE;CBMC")

unit/Makefile

@@ -116,21 +116,17 @@ 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)
 
 clean: testing-utils-clean
 
-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)
@@ -140,6 +136,3 @@ test: $(CATCH_TEST) $(TESTS)
 
 unit_tests$(EXEEXT): $(OBJ)
 	$(LINKBIN)
-
-miniBDD$(EXEEXT): miniBDD$(OBJEXT) $(CPROVER_LIBS)
-	$(LINKBIN)

unit/miniBDD.cpp

@@ -11,12 +11,14 @@
 
 #include <testing-utils/catch.hpp>
 
-#include <solvers/miniBDD/miniBDD.h>
 #include <solvers/flattening/boolbv.h>
+#include <solvers/miniBDD/miniBDD.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,70 @@ SCENARIO("miniBDD", "[core][solver][miniBDD]")
 
     REQUIRE(!result.is_constant());
   }
+
+  GIVEN("A bdd for x&y")
+  {
+    mini_bdd_mgrt mgr;
+
+    mini_bddt x_bdd = mgr.Var("x");
+    mini_bddt y_bdd = mgr.Var("y");
+    mini_bddt final_bdd = x_bdd & y_bdd;
+
+    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] \" x \" }; \"2\"; \"4\"; }\n"
+      "{ rank=same; { node [shape=plaintext,fontname="
+      "\"Times Italic\",fontsize=24] \" y \" }; \"3\"; }\n"
+      "\n"
+      "{ edge [style = invis]; \" x \" -> \" y \" -> \"T\"; }\n"
+      "\n"
+      "\"2\" -> \"1\" [style=solid,arrowsize=\".75\"];\n"
+      "\"2\" -> \"0\" [style=dashed,arrowsize=\".75\"];\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");
+    }
+  }
 }