diff --git a/CMakeLists.txt b/CMakeLists.txt index fea650dbac1..0c32e421f01 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -68,7 +68,6 @@ set_target_properties( json langapi linking - miniBDD pointer-analysis solvers test-bigint diff --git a/jbmc/regression/jbmc-generics/Makefile b/jbmc/regression/jbmc-generics/Makefile index 81024778e07..1639d08dea4 100644 --- a/jbmc/regression/jbmc-generics/Makefile +++ b/jbmc/regression/jbmc-generics/Makefile @@ -20,7 +20,7 @@ show: clean: find -name '*.out' -execdir $(RM) '{}' \; find -name '*.gb' -execdir $(RM) '{}' \; - $(RM) tests.log + $(RM) tests.log tests-symex-driven-loading.log %.class: %.java ../../src/org.cprover.jar javac -g -cp ../../src/org.cprover.jar:. $< diff --git a/jbmc/regression/strings-smoke-tests/Makefile b/jbmc/regression/strings-smoke-tests/Makefile index 4ff4e5ba834..6a87a176e59 100644 --- a/jbmc/regression/strings-smoke-tests/Makefile +++ b/jbmc/regression/strings-smoke-tests/Makefile @@ -28,4 +28,4 @@ show: clean: find -name '*.out' -execdir $(RM) '{}' \; find -name '*.gb' -execdir $(RM) '{}' \; - $(RM) tests.log + $(RM) tests.log tests-symex-driven-loading.log diff --git a/jbmc/unit/Makefile b/jbmc/unit/Makefile index 4f6b2ae29d4..5bf5f13742e 100644 --- a/jbmc/unit/Makefile +++ b/jbmc/unit/Makefile @@ -1,30 +1,53 @@ -.PHONY: all cprover.dir jprover.dir testing-utils.dir java-testing-utils.dir test +.PHONY: all jprover.dir test java-testing-utils-clean # Source files for test utilities SRC = $(CPROVER_DIR)/unit/unit_tests.cpp \ # Empty last line # Test source files -SRC += java_bytecode/goto-programs/class_hierarchy_output.cpp \ +SRC += java_bytecode/ci_lazy_methods/lazy_load_lambdas.cpp \ + java_bytecode/expr2java.cpp \ + java_bytecode/goto_program_generics/generic_bases_test.cpp \ + java_bytecode/goto_program_generics/generic_parameters_test.cpp \ + java_bytecode/goto_program_generics/mutually_recursive_generics.cpp \ java_bytecode/goto-programs/class_hierarchy_graph.cpp \ + java_bytecode/goto-programs/class_hierarchy_output.cpp \ java_bytecode/goto-programs/remove_virtual_functions_without_fallback.cpp \ + java_bytecode/inherited_static_fields/inherited_static_fields.cpp \ java_bytecode/java_bytecode_convert_class/convert_abstract_class.cpp \ java_bytecode/java_bytecode_convert_class/convert_java_annotations.cpp \ + java_bytecode/java_bytecode_convert_method/convert_initalizers.cpp \ java_bytecode/java_bytecode_convert_method/convert_invoke_dynamic.cpp \ + java_bytecode/java_bytecode_convert_method/convert_method.cpp \ + java_bytecode/java_bytecode_parse_generics/parse_bounded_generic_inner_classes.cpp \ + java_bytecode/java_bytecode_parse_generics/parse_derived_generic_class.cpp \ + java_bytecode/java_bytecode_parse_generics/parse_functions_with_generics.cpp \ + java_bytecode/java_bytecode_parse_generics/parse_generic_array_class.cpp \ java_bytecode/java_bytecode_parse_generics/parse_generic_class.cpp \ - java_bytecode/java_bytecode_parser/parse_java_class.cpp \ + java_bytecode/java_bytecode_parse_generics/parse_generic_class_with_generic_inner_classes.cpp \ + java_bytecode/java_bytecode_parse_generics/parse_generic_class_with_inner_classes.cpp \ + java_bytecode/java_bytecode_parse_generics/parse_generic_fields.cpp \ + java_bytecode/java_bytecode_parse_generics/parse_generic_functions.cpp \ + java_bytecode/java_bytecode_parse_generics/parse_generic_superclasses.cpp \ + java_bytecode/java_bytecode_parse_generics/parse_generic_wildcard_function.cpp \ + java_bytecode/java_bytecode_parse_generics/parse_nested_generics.cpp \ + java_bytecode/java_bytecode_parse_generics/parse_recursive_generic_class.cpp \ + java_bytecode/java_bytecode_parse_generics/parse_signature_descriptor_mismatch.cpp \ + java_bytecode/java_bytecode_parse_lambdas/java_bytecode_convert_class_lambda_method_handles.cpp \ + java_bytecode/java_bytecode_parse_lambdas/java_bytecode_parse_lambda_method_table.cpp \ + java_bytecode/java_bytecode_parser/parse_java_annotations.cpp \ java_bytecode/java_bytecode_parser/parse_java_attributes.cpp \ + java_bytecode/java_bytecode_parser/parse_java_class.cpp \ java_bytecode/java_object_factory/gen_nondet_string_init.cpp \ - java_bytecode/java_bytecode_parse_lambdas/java_bytecode_parse_lambda_method_table.cpp \ - java_bytecode/java_bytecode_parse_lambdas/java_bytecode_convert_class_lambda_method_handles.cpp \ + java_bytecode/java_replace_nondet/replace_nondet.cpp \ java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp \ java_bytecode/java_types/erase_type_arguments.cpp \ java_bytecode/java_types/generic_type_index.cpp \ java_bytecode/java_types/java_generic_symbol_type.cpp \ java_bytecode/java_types/java_type_from_string.cpp \ java_bytecode/java_utils_test.cpp \ + java_bytecode/java_virtual_functions/virtual_functions.cpp \ java_bytecode/load_method_by_regex.cpp \ - java_bytecode/inherited_static_fields/inherited_static_fields.cpp \ pointer-analysis/custom_value_set_analysis.cpp \ solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp \ solvers/refinement/string_refinement/dependency_graph.cpp \ @@ -33,9 +56,6 @@ SRC += java_bytecode/goto-programs/class_hierarchy_output.cpp \ util/has_subtype.cpp \ util/parameter_indices.cpp \ util/simplify_expr.cpp \ - java_bytecode/java_virtual_functions/virtual_functions.cpp \ - java_bytecode/java_bytecode_parse_generics/parse_generic_superclasses.cpp \ - java_bytecode/goto_program_generics/mutually_recursive_generics.cpp \ # Empty last line INCLUDES= -I ../src/ -I. -I $(CPROVER_DIR)/src -I $(CPROVER_DIR)/unit @@ -44,18 +64,18 @@ include ../src/config.inc include $(CPROVER_DIR)/src/config.inc include $(CPROVER_DIR)/src/common -cprover.dir: - $(MAKE) $(MAKEARGS) -C $(CPROVER_DIR)/src - jprover.dir: $(MAKE) $(MAKEARGS) -C ../src -cprover-testing-utils.dir: +$(CPROVER_DIR)/unit/testing-utils/testing-utils$(LIBEXT): jprover.dir $(MAKE) $(MAKEARGS) -C $(CPROVER_DIR)/unit/testing-utils -java-testing-utils.dir: +java-testing-utils/java-testing-utils$(LIBEXT): jprover.dir $(MAKE) $(MAKEARGS) -C java-testing-utils +java-testing-utils-clean: + $(MAKE) $(MAKEARGS) -C java-testing-utils clean + # We need to link bmc.o to the unit test, so here's everything it depends on... BMC_DEPS =$(CPROVER_DIR)/src/cbmc/all_properties$(OBJEXT) \ $(CPROVER_DIR)/src/cbmc/bmc$(OBJEXT) \ @@ -118,16 +138,25 @@ OBJ += $(CPROVER_LIBS) \ $(CPROVER_DIR)/unit/testing-utils/testing-utils$(LIBEXT) \ java-testing-utils/java-testing-utils$(LIBEXT) -TESTS = unit_tests$(EXEEXT) \ - # Empty last line +CATCH_TEST = unit_tests$(EXEEXT) +N_CATCH_TESTS = $(shell \ + cat $$(find . -name "*.cpp" ) | \ + grep -c -E "(SCENARIO|TEST_CASE)") + +CLEANFILES = $(CATCH_TEST) java-testing-utils/java-testing-utils$(LIBEXT) + +# only add a dependency for libraries to avoid triggering implicit rules, which +# would cause unnecessary rebuilds +$(filter %$(LIBEXT), CPROVER_LIBS): jprover.dir -CLEANFILES = $(TESTS) +all: $(CATCH_TEST) -all: cprover.dir cprover-testing-utils.dir jprover.dir java-testing-utils.dir - $(MAKE) $(MAKEARGS) $(TESTS) +clean: java-testing-utils-clean -test: all - $(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) ############################################################################### diff --git a/jbmc/unit/java_bytecode/expr2java.cpp b/jbmc/unit/java_bytecode/expr2java.cpp index c3f6bb10f18..124fd45622d 100644 --- a/jbmc/unit/java_bytecode/expr2java.cpp +++ b/jbmc/unit/java_bytecode/expr2java.cpp @@ -96,21 +96,37 @@ TEST_CASE( SECTION("Hex float to string (print a comment)") { const float value = std::strtod("0x1p+37f", nullptr); +#ifndef _MSC_VER REQUIRE( floating_point_to_java_string(value) == "0x1p+37f /* 1.37439e+11 */"); +#else + REQUIRE( + floating_point_to_java_string(value) == + "0x1.000000p+37f /* 1.37439e+11 */"); +#endif } SECTION("Hex double to string (print a comment)") { const double value = std::strtod("0x1p+37f", nullptr); +#ifndef _MSC_VER REQUIRE( floating_point_to_java_string(value) == "0x1p+37 /* 1.37439e+11 */"); +#else + REQUIRE( + floating_point_to_java_string(value) == + "0x1.000000p+37 /* 1.37439e+11 */"); +#endif } SECTION("Beyond numeric limits") { +#ifndef _MSC_VER REQUIRE( floating_point_to_java_string(-5.56268e-309) .find("/* -5.56268e-309 */") != std::string::npos); +#else + REQUIRE(floating_point_to_java_string(-5.56268e-309) == "-5.56268e-309"); +#endif } } diff --git a/src/ansi-c/Makefile b/src/ansi-c/Makefile index 4e741de9199..d0ccdf84a3a 100644 --- a/src/ansi-c/Makefile +++ b/src/ansi-c/Makefile @@ -115,8 +115,6 @@ cprover_library.inc: library/converter$(EXEEXT) library/*.c %.inc: %.h file_converter$(EXEEXT) ./file_converter$(EXEEXT) < $< > $@ -cprover_library.cpp: cprover_library.inc - ansi_c_internal_additions$(OBJEXT): $(BUILTIN_FILES) generated_files: \ diff --git a/src/cpp/Makefile b/src/cpp/Makefile index bad4f4030c1..3189c375ba7 100644 --- a/src/cpp/Makefile +++ b/src/cpp/Makefile @@ -59,6 +59,11 @@ all: cpp$(LIBEXT) ############################################################################### +# extra dependencies +cprover_library$(OBJEXT): cprover_library.inc + +############################################################################### + ../ansi-c/library/converter$(EXEEXT): ../ansi-c/library/converter.cpp $(MAKE) -C ../ansi-c library/converter$(EXEEXT) @@ -69,8 +74,6 @@ library_check: library/*.c cprover_library.inc: ../ansi-c/library/converter$(EXEEXT) library/*.c cat library/*.c | ../ansi-c/library/converter$(EXEEXT) > $@ -cprover_library.cpp: cprover_library.inc - generated_files: cprover_library.inc ############################################################################### diff --git a/src/util/format_expr.cpp b/src/util/format_expr.cpp index 7b087990324..40d895492be 100644 --- a/src/util/format_expr.cpp +++ b/src/util/format_expr.cpp @@ -88,7 +88,7 @@ static std::ostream &format_rec(std::ostream &os, const multi_ary_exprt &src) if(first) first = false; else - os << ' ' << src.id() << ' '; + os << ' ' << operator_str << ' '; const bool need_parentheses = bracket_subexpression(op, src); diff --git a/unit/.gitignore b/unit/.gitignore index d69e63165b4..326b381fbda 100644 --- a/unit/.gitignore +++ b/unit/.gitignore @@ -1,4 +1,3 @@ # Unit test binaries -miniBDD sharing_node unit_tests diff --git a/unit/CMakeLists.txt b/unit/CMakeLists.txt index 036cc3ce4c4..6c06a0fc205 100644 --- a/unit/CMakeLists.txt +++ b/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 $) -set_tests_properties(miniBDD PROPERTIES LABELS "CORE;CBMC") diff --git a/unit/Makefile b/unit/Makefile index fa9c96aac4b..bc9800d85a9 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -1,33 +1,36 @@ -.PHONY: all cprover.dir testing-utils.dir test +.PHONY: all cprover.dir test testing-utils-clean # Source files for test utilities SRC = unit_tests.cpp \ - catch_example.cpp \ # Empty last line # Test source files -SRC += unit_tests.cpp \ - analyses/ai/ai.cpp \ +SRC += analyses/ai/ai.cpp \ analyses/ai/ai_simplify_lhs.cpp \ analyses/call_graph.cpp \ analyses/constant_propagator.cpp \ + analyses/dependence_graph.cpp \ analyses/disconnect_unreachable_nodes_in_graph.cpp \ analyses/does_remove_const/does_expr_lose_const.cpp \ analyses/does_remove_const/does_type_preserve_const_correctness.cpp \ analyses/does_remove_const/is_type_at_least_as_const_as.cpp \ goto-programs/goto_trace_output.cpp \ + interpreter/interpreter.cpp \ + json/json_parser.cpp \ path_strategies.cpp \ + pointer-analysis/value_set.cpp \ solvers/floatbv/float_utils.cpp \ + solvers/miniBDD/miniBDD.cpp \ solvers/refinement/array_pool/array_pool.cpp \ solvers/refinement/string_constraint_generator_valueof/calculate_max_string_length.cpp \ solvers/refinement/string_constraint_generator_valueof/get_numeric_value_from_character.cpp \ solvers/refinement/string_constraint_generator_valueof/is_digit_with_radix.cpp \ solvers/refinement/string_refinement/concretize_array.cpp \ - solvers/refinement/string_refinement/substitute_array_list.cpp \ solvers/refinement/string_refinement/sparse_array.cpp \ + solvers/refinement/string_refinement/substitute_array_list.cpp \ solvers/refinement/string_refinement/union_find_replace.cpp \ - util/expr.cpp \ util/expr_cast/expr_cast.cpp \ + util/expr.cpp \ util/file_util.cpp \ util/get_base_name.cpp \ util/graph.cpp \ @@ -36,16 +39,14 @@ SRC += unit_tests.cpp \ util/message.cpp \ util/optional.cpp \ util/replace_symbol.cpp \ - util/sharing_node.cpp \ util/sharing_map.cpp \ + util/sharing_node.cpp \ util/small_map.cpp \ util/small_shared_two_way_ptr.cpp \ util/string_utils/split_string.cpp \ util/string_utils/strip_string.cpp \ util/symbol_table.cpp \ util/unicode.cpp \ - catch_example.cpp \ - interpreter/interpreter.cpp \ # Empty last line INCLUDES= -I ../src/ -I. @@ -56,9 +57,12 @@ include ../src/common cprover.dir: $(MAKE) $(MAKEARGS) -C ../src -testing-utils.dir: +testing-utils/testing-utils$(LIBEXT): cprover.dir $(MAKE) $(MAKEARGS) -C testing-utils +testing-utils-clean: + $(MAKE) $(MAKEARGS) -C testing-utils clean + # We need to link bmc.o to the unit test, so here's everything it depends on... BMC_DEPS =../src/cbmc/all_properties$(OBJEXT) \ ../src/cbmc/bmc$(OBJEXT) \ @@ -107,23 +111,29 @@ CPROVER_LIBS =../src/ansi-c/ansi-c$(LIBEXT) \ OBJ += $(CPROVER_LIBS) testing-utils/testing-utils$(LIBEXT) -TESTS = unit_tests$(EXEEXT) \ - miniBDD$(EXEEXT) \ - # Empty last line +CATCH_TEST = unit_tests$(EXEEXT) +N_CATCH_TESTS = $(shell \ + cat $$(find . -name "*.cpp" \ + -a -not -name "expr_undefined_casts.cpp") | \ + grep -c -E "(SCENARIO|TEST_CASE)") + +CLEANFILES = $(CATCH_TEST) testing-utils/testing-utils$(LIBEXT) -CLEANFILES = $(TESTS) +# only add a dependency for libraries to avoid triggering implicit rules, which +# would cause unnecessary rebuilds +$(filter %$(LIBEXT), CPROVER_LIBS): cprover.dir -all: cprover.dir testing-utils.dir - $(MAKE) $(MAKEARGS) $(TESTS) +all: $(CATCH_TEST) -test: all - $(foreach test,$(TESTS), (echo Running: $(test); ./$(test)) &&) true +clean: testing-utils-clean + +test: $(CATCH_TEST) + if ! ./$(CATCH_TEST) -l | grep -q "^$(N_CATCH_TESTS) test cases" ; then \ + ./$(CATCH_TEST) -l ; fi + ./$(CATCH_TEST) ############################################################################### unit_tests$(EXEEXT): $(OBJ) $(LINKBIN) - -miniBDD$(EXEEXT): miniBDD$(OBJEXT) $(CPROVER_LIBS) - $(LINKBIN) diff --git a/unit/catch_example.cpp b/unit/catch_example.cpp deleted file mode 100644 index f8cd903d7b7..00000000000 --- a/unit/catch_example.cpp +++ /dev/null @@ -1,25 +0,0 @@ -/*******************************************************************\ - - Module: Example Catch Tests - - Author: Diffblue Ltd. - -\*******************************************************************/ - -#include - -unsigned int Factorial(unsigned int number) -{ - return number>1?Factorial(number-1)*number:1; -} - -// This is an example unit test to demonstrate the build system and the -// catch unit test framework. The source code is taken from the documentation -// of catch. -TEST_CASE("Factorials are computed", "[core][factorial]") -{ - REQUIRE(Factorial(1)==1); - REQUIRE(Factorial(2)==2); - REQUIRE(Factorial(3)==6); - REQUIRE(Factorial(10)==3628800); -} diff --git a/unit/miniBDD.cpp b/unit/miniBDD.cpp deleted file mode 100644 index bd1eb77eec2..00000000000 --- a/unit/miniBDD.cpp +++ /dev/null @@ -1,95 +0,0 @@ -/*******************************************************************\ - -Module: A minimalistic BDD library, following Bryant's original paper - and Andersen's lecture notes - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -#include - -#include - -#include - -void test1() -{ - mini_bdd_mgrt mgr; - - mini_bddt x=mgr.Var("x"); - mini_bddt y=mgr.Var("y"); - mini_bddt z=mgr.Var("z"); - mini_bddt f=(x&y&z)|((!x)&(!y)&z); - y.clear(); - x.clear(); - z.clear(); - - // mgr.DumpDot(std::cout); - mgr.DumpTikZ(std::cout); -} - -void test2() -{ - mini_bdd_mgrt mgr; - - mini_bddt a=mgr.Var("a"); - mini_bddt b=mgr.Var("b"); - mini_bddt c=mgr.Var("c"); - mini_bddt d=mgr.Var("d"); - - mini_bddt final=(a==b)&(c==d); - - a.clear(); - b.clear(); - c.clear(); - d.clear(); - - mgr.DumpTikZ(std::cout, true); -} - -void test3() -{ - mini_bdd_mgrt mgr; - - mini_bddt final=mgr.Var("x")&mgr.Var("y"); - - mgr.DumpDot(std::cout); - #if 0 - mgr.DumpTikZ(std::cout); - mgr.DumpTable(std::cout); - #endif -} - -#include -#include -#include - -#include -#include -#include - -#include - -void test4() -{ - 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::cout << format(o) << std::endl; - - bdd_exprt t(ns); - t.from_expr(o); - - std::cout << format(t.as_expr()) << std::endl; -} - -int main() -{ - test3(); -} diff --git a/unit/miniBDD_new.cpp b/unit/solvers/miniBDD/miniBDD.cpp similarity index 76% rename from unit/miniBDD_new.cpp rename to unit/solvers/miniBDD/miniBDD.cpp index b38c1207e80..054bfdb8861 100644 --- a/unit/miniBDD_new.cpp +++ b/unit/solvers/miniBDD/miniBDD.cpp @@ -11,14 +11,14 @@ #include -#include #include +#include +#include -#include #include #include - -#include +#include +#include class bdd_propt:public propt { @@ -293,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"); + } + } } diff --git a/unit/solvers/miniBDD/module_dependencies.txt b/unit/solvers/miniBDD/module_dependencies.txt new file mode 100644 index 00000000000..05a5cc7502e --- /dev/null +++ b/unit/solvers/miniBDD/module_dependencies.txt @@ -0,0 +1,4 @@ +solvers/miniBDD +solvers/prop +testing-utils +util