test for miniBDD
This commit is contained in:
parent
393256f5d2
commit
ff945b3e2b
|
@ -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
|
||||
|
||||
|
|
|
@ -0,0 +1,277 @@
|
|||
/*******************************************************************\
|
||||
|
||||
Module: Unit tests for miniBDD
|
||||
|
||||
Author: DiffBlue Limited. All rights reserved.
|
||||
|
||||
\*******************************************************************/
|
||||
|
||||
/// \file
|
||||
/// Unit tests for miniBDD
|
||||
|
||||
#include <catch.hpp>
|
||||
|
||||
#include <solvers/miniBDD/miniBDD.h>
|
||||
#include <solvers/flattening/boolbv.h>
|
||||
|
||||
#include <util/symbol_table.h>
|
||||
#include <util/arith_tools.h>
|
||||
#include <util/expanding_vector.h>
|
||||
|
||||
#include <iostream>
|
||||
|
||||
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.size(), "literal in map");
|
||||
mini_bddt bdd=bdd_map[a.var_no()];
|
||||
INVARIANT(bdd.is_initialized(), "initialized");
|
||||
if(a.sign())
|
||||
return !bdd;
|
||||
else
|
||||
return bdd;
|
||||
}
|
||||
|
||||
literalt to_literal(const mini_bddt &bdd)
|
||||
{
|
||||
if(bdd.is_constant())
|
||||
return const_literal(bdd.is_true());
|
||||
std::size_t index=bdd.node_number();
|
||||
bdd_map[index]=bdd;
|
||||
return literalt(index, false);
|
||||
}
|
||||
|
||||
literalt land(literalt a, literalt b) override
|
||||
{
|
||||
return to_literal(to_bdd(a) & to_bdd(b));
|
||||
}
|
||||
|
||||
literalt lor(literalt a, literalt b) override
|
||||
{
|
||||
UNREACHABLE;
|
||||
}
|
||||
|
||||
literalt land(const bvt &bv) override
|
||||
{
|
||||
mini_bddt result=mgr.True();
|
||||
|
||||
for(const auto &l : bv)
|
||||
result=result&to_bdd(l);
|
||||
|
||||
return to_literal(result);
|
||||
}
|
||||
|
||||
literalt lor(const bvt &bv) override
|
||||
{
|
||||
mini_bddt result=mgr.False();
|
||||
|
||||
for(const auto &l : bv)
|
||||
result=result|to_bdd(l);
|
||||
|
||||
return to_literal(result);
|
||||
}
|
||||
|
||||
literalt lxor(literalt a, literalt b) override
|
||||
{
|
||||
return to_literal(to_bdd(a) ^ to_bdd(b));
|
||||
}
|
||||
|
||||
literalt lxor(const bvt &bv) override
|
||||
{
|
||||
UNREACHABLE;
|
||||
}
|
||||
|
||||
literalt lnand(literalt a, literalt b) override
|
||||
{
|
||||
UNREACHABLE;
|
||||
}
|
||||
|
||||
literalt lnor(literalt a, literalt b) override
|
||||
{
|
||||
UNREACHABLE;
|
||||
}
|
||||
|
||||
literalt lequal(literalt a, literalt b) override
|
||||
{
|
||||
return to_literal(to_bdd(a)==to_bdd(b));
|
||||
}
|
||||
|
||||
literalt limplies(literalt a, literalt b) override
|
||||
{
|
||||
UNREACHABLE;
|
||||
}
|
||||
|
||||
literalt lselect(literalt a, literalt b, literalt c) override
|
||||
{
|
||||
UNREACHABLE;
|
||||
}
|
||||
|
||||
void lcnf(const bvt &bv) override
|
||||
{
|
||||
UNREACHABLE;
|
||||
}
|
||||
|
||||
literalt new_variable() override
|
||||
{
|
||||
return to_literal(mgr.Var(""));
|
||||
}
|
||||
|
||||
size_t no_variables() const override
|
||||
{
|
||||
return bdd_map.size();
|
||||
}
|
||||
|
||||
const std::string solver_text() override
|
||||
{
|
||||
return "BDDs";
|
||||
}
|
||||
|
||||
resultt prop_solve() override
|
||||
{
|
||||
UNREACHABLE;
|
||||
}
|
||||
|
||||
tvt l_get(literalt a) const override
|
||||
{
|
||||
UNREACHABLE;
|
||||
}
|
||||
|
||||
expanding_vectort<mini_bddt> 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());
|
||||
}
|
||||
}
|
Loading…
Reference in New Issue