diff --git a/src/solvers/miniBDD/miniBDD.cpp b/src/solvers/miniBDD/miniBDD.cpp index aebe4e0a3a4..4c00b1de85b 100644 --- a/src/solvers/miniBDD/miniBDD.cpp +++ b/src/solvers/miniBDD/miniBDD.cpp @@ -463,14 +463,20 @@ mini_bddt mini_bdd_mgrt::mk( } bool mini_bdd_mgrt::reverse_keyt::operator<( - const mini_bdd_mgrt::reverse_keyt &other) const + const mini_bdd_mgrt::reverse_keyt &y) const { - if(varother.var || low>other.low) + else if(x.var>y.var) return false; - - return highy.low) + return false; + else + return x.high reverse_mapt; diff --git a/src/util/invariant.h b/src/util/invariant.h index 325020a0d6e..a7df274e81d 100644 --- a/src/util/invariant.h +++ b/src/util/invariant.h @@ -149,6 +149,9 @@ void report_exception_to_stderr(const invariant_failedt &); /// \param params : (variadic) parameters to forward to ET's constructor /// its backtrace member will be set before it is used. template +#ifdef __GNUC__ +__attribute__((noreturn)) +#endif typename std::enable_if::value>::type invariant_violated_structured( const std::string &file, @@ -171,6 +174,9 @@ invariant_violated_structured( /// \param function : C string giving the name of the function. /// \param line : The line number of the invariant /// \param reason : brief description of the invariant violation. +#ifdef __GNUC__ +__attribute__((noreturn)) +#endif inline void invariant_violated_string( const std::string &file, const std::string &function, diff --git a/unit/Makefile b/unit/Makefile index 3e5bb48afbe..409402af1f1 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -11,6 +11,7 @@ SRC += unit_tests.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 \ + miniBDD_new.cpp \ catch_example.cpp \ # Empty last line diff --git a/unit/miniBDD_new.cpp b/unit/miniBDD_new.cpp new file mode 100644 index 00000000000..0c176c7f82e --- /dev/null +++ b/unit/miniBDD_new.cpp @@ -0,0 +1,277 @@ +/*******************************************************************\ + + Module: Unit tests for miniBDD + + Author: DiffBlue Limited. All rights reserved. + +\*******************************************************************/ + +/// \file +/// Unit tests for miniBDD + +#include + +#include +#include + +#include +#include +#include + +#include + +class bdd_propt:public propt +{ +public: + mini_bdd_mgrt &mgr; + + explicit bdd_propt(mini_bdd_mgrt &_mgr):mgr(_mgr) + { + // True and False + bdd_map.push_back(mgr.False()); + bdd_map.push_back(mgr.True()); + } + + mini_bddt to_bdd(literalt a) + { + if(a.is_true()) + return mgr.True(); + if(a.is_false()) + return mgr.False(); + INVARIANT(a.var_no() bdd_map; + + bool has_set_to() const override { return false; } + bool cnf_handled_well() const override { return false; } +}; + +SCENARIO("miniBDD", "[core][solver][miniBDD]") +{ + GIVEN("A bdd for x&!x") + { + symbol_tablet symbol_table; + namespacet ns(symbol_table); + mini_bdd_mgrt bdd_mgr; + bdd_propt bdd_prop(bdd_mgr); + prop_conv_solvert solver(ns, bdd_prop); + + symbol_exprt var("x", bool_typet()); + literalt result= + solver.convert(and_exprt(var, not_exprt(var))); + + REQUIRE(result.is_false()); + } + + GIVEN("A bdd for x&!x==0") + { + symbol_tablet symbol_table; + namespacet ns(symbol_table); + mini_bdd_mgrt bdd_mgr; + bdd_propt bdd_prop(bdd_mgr); + boolbvt boolbv(ns, bdd_prop); + + unsignedbv_typet type(2); + symbol_exprt var("x", type); + equal_exprt equality( + bitand_exprt(var, bitnot_exprt(var)), + from_integer(0, type)); + + literalt result= + boolbv.convert(equality); + + REQUIRE(result.is_true()); + } + + GIVEN("A bdd for x+x==1") + { + symbol_tablet symbol_table; + namespacet ns(symbol_table); + mini_bdd_mgrt bdd_mgr; + bdd_propt bdd_prop(bdd_mgr); + boolbvt boolbv(ns, bdd_prop); + + unsignedbv_typet type(32); + symbol_exprt var("x", type); + equal_exprt equality( + plus_exprt(var, var), + from_integer(1, type)); + + literalt result= + boolbv.convert(equality); + + REQUIRE(result.is_false()); + } + + GIVEN("A bdd for x*y==y*x") + { + symbol_tablet symbol_table; + namespacet ns(symbol_table); + mini_bdd_mgrt bdd_mgr; + bdd_propt bdd_prop(bdd_mgr); + boolbvt boolbv(ns, bdd_prop); + + unsignedbv_typet type(4); + symbol_exprt var_x("x", type); + symbol_exprt var_y("y", type); + equal_exprt equality( + mult_exprt(var_x, var_y), + mult_exprt(var_y, var_x)); + + literalt result= + boolbv.convert(equality); + + REQUIRE(result.is_true()); + } + + GIVEN("A bdd for x*x==2") + { + symbol_tablet symbol_table; + namespacet ns(symbol_table); + mini_bdd_mgrt bdd_mgr; + bdd_propt bdd_prop(bdd_mgr); + boolbvt boolbv(ns, bdd_prop); + + unsignedbv_typet type(8); + symbol_exprt var_x("x", type); + equal_exprt equality( + mult_exprt(var_x, var_x), + from_integer(2, type)); + + literalt result= + boolbv.convert(equality); + + REQUIRE(result.is_false()); + } + + GIVEN("A bdd for x*x==4") + { + symbol_tablet symbol_table; + namespacet ns(symbol_table); + mini_bdd_mgrt bdd_mgr; + bdd_propt bdd_prop(bdd_mgr); + boolbvt boolbv(ns, bdd_prop); + + unsignedbv_typet type(8); + symbol_exprt var_x("x", type); + equal_exprt equality( + mult_exprt(var_x, var_x), + from_integer(4, type)); + + literalt result= + boolbv.convert(equality); + + REQUIRE(!result.is_constant()); + } +}