Commit 17a0746c authored by Peter Navrátil's avatar Peter Navrátil
Browse files

fixed tests

parent 13eec212

bvec_cudd.cpp

+5 −10
Original line number Diff line number Diff line
@@ -18,7 +18,7 @@ namespace cudd { 
    	m_bitvec.resize(bitnum, value);

    }



    Bvec::Bvec(const Bvec& other) : m_manager(other.m_manager), /*m_bitvec(other.bitnum(), m_manager.bddZero())*/ m_bitvec(other.m_bitvec) {

    Bvec::Bvec(const Bvec& other) : m_manager(other.m_manager), m_bitvec(other.m_bitvec) {

    	/*if (other.bitnum() == 0)

    	{

    		//DEFAULT(dst);
@@ -60,10 +60,8 @@ namespace cudd { 
        return m_manager;

    }



    int

    bool

    Bvec::empty() const {

    //BDD empty() const;

    //bool empty() const {

    	return m_bitvec.empty();

    }
@@ -128,18 +126,15 @@ namespace cudd { 
    	return res;

    }



    int

    bool

    Bvec::bvec_isConst(const Bvec& src) {

    //bool Bvec::bvec_isConst(const Bvec& src) {

    	Cudd& manager = src.m_manager;

    	for (size_t i = 0; i < src.bitnum(); ++i) {

    		if (src[i].IsVar()) {

    			return 0;

    			//return false;

    			return false;

    		}

    	}

    	return 1;

    	//return true;

    	return true;

    }



    int

bvec_cudd.h

+7 −14
Original line number Diff line number Diff line
@@ -12,11 +12,6 @@ namespace cudd { 
    	std::vector<BDD> m_bitvec;

    	Cudd& m_manager;



    	/*Bvec*const Bvec& o) { ** NOTE: Must be a shallow copy! **

    		bitnum = o.bitnum;

    		bitvec = o.bitvec;

    	}*/



    public:



    	Bvec() = delete;
@@ -46,10 +41,8 @@ namespace cudd { 
        const Cudd&

        manager() const;



    	int

    	bool

    	empty() const;

        //BDD empty() const;

    	//bool empty() const;



    	static Bvec

    	bvec_build(Cudd& manager, size_t bitnum, bool isTrue);
@@ -69,14 +62,14 @@ namespace cudd { 
    	static Bvec

    	bvec_varvec(Cudd& manager, size_t bitnum, int *var);



    	static Bvec

    	bvec_coerce(size_t bitnum, const Bvec& vec);

    	Bvec

    	bvec_coerce(size_t bitnum);



    	static int

    	bvec_isConst(const Bvec& src);

    	bool

    	bvec_isConst();



    	static int

    	bvec_val(const Bvec& src);

    	int

    	bvec_val();



    	static Bvec

    	bvec_copy(const Bvec& other);

tests.cpp

+50 −70
Original line number Diff line number Diff line
@@ -8,6 +8,29 @@ 
#include <iostream>



namespace {

    void

    init()

    {

        int n_workers = 0; //auto-detect

        lace_init(n_workers, 0);

        lace_startup(0, NULL, NULL);

        sylvan::sylvan_set_limits(512*1024*1024, 1, 5);

        sylvan::sylvan_init_package();

        sylvan::sylvan_init_mtbdd();



        bdd_init(1000, 1000);

        bdd_setvarnum(20);

    }



    void

    finish()

    {

        sylvan::sylvan_stats_report(stdout);

        sylvan::sylvan_quit();

        lace_exit();



        bdd_done();

    }



    bool

    isEqual(const cudd::Bvec& cudd, const sylvan::Bvec& sylvan, const bvec& buddy, size_t val)
@@ -63,19 +86,10 @@ namespace { 
} // namespace



TEST_CASE("Construction tests") {

    int n_workers = 0; // auto-detect

    lace_init(n_workers, 0);

    lace_startup(0, NULL, NULL);

    sylvan::sylvan_set_limits(512*1024*1024, 1, 5);

    sylvan::sylvan_init_package();

    sylvan::sylvan_init_mtbdd();



    init();

    cudd::Cudd manager;

    size_t size = 0U;



    bdd_init(1000, 1000);

    bdd_setvarnum(20);



    SECTION("Test false bitvector") {

        size = 42U;

        cudd::Bvec bvec_cudd = cudd::Bvec::bvec_false(manager, size);
@@ -110,7 +124,7 @@ TEST_CASE("Construction tests") { 


    }



    SECTION("Test copy constructors") { //fix

    SECTION("Test copy constructors") {

        size_t val = 42U;

        size = 6U;

        cudd::Bvec bvec_cudd = cudd::Bvec::bvec_con(manager, size, val);
@@ -135,47 +149,32 @@ TEST_CASE("Construction tests") { 


    }



    SECTION("Test bvec_var") { //finish

    /*SECTION("Test bvec_var") {

        size = 8U;

        int offset = 1;

        int step = 2;

        cudd::Bvec bvec_cudd = cudd::Bvec::bvec_var(manager, size, offset, step);

        sylvan::Bvec bvec_sylvan = sylvan::Bvec::bvec_var(size, offset, step);

        bvec bvec_buddy = bvec_var_buddy(size, offset, step);

        //TODO

    }



    SECTION("Test bvec_varvec") { //finish

    SECTION("Test bvec_varvec") {

        std::vector<int> var {0, 1, 2, 3, 4, 5, 6, 7};

        size = var.size();

        cudd::Bvec bvec_cudd = cudd::Bvec::bvec_varvec(manager, size, var.data());

        sylvan::Bvec bvec_sylvan = sylvan::Bvec::bvec_varvec(size, var.data());

        bvec bvec_buddy = bvec_varvec_buddy(size, var.data());

    }



    }*/



    sylvan::sylvan_stats_report(stdout);

    sylvan::sylvan_quit();

    lace_exit();



    bdd_done();

    finish();

}





TEST_CASE("Manipulation tests") {

    int n_workers = 0; // auto-detect

    lace_init(n_workers, 0);

    lace_startup(0, NULL, NULL);

    sylvan::sylvan_set_limits(512*1024*1024, 1, 5);

    sylvan::sylvan_init_package();

    sylvan::sylvan_init_mtbdd();



    init();

    cudd::Cudd manager;

    size_t size = 0U;



    bdd_init(1000, 1000);

    bdd_setvarnum(20);



    SECTION("Test bitnum function") {

        size = 42U;

        cudd::Bvec cudd = cudd::Bvec::bvec_false(manager, size);
@@ -269,28 +268,15 @@ TEST_CASE("Manipulation tests") { 
        REQUIRE(cudd_val == buddy_val);

    }



    sylvan::sylvan_stats_report(stdout);

    sylvan::sylvan_quit();

    lace_exit();



    bdd_done();

    finish();

}



TEST_CASE("Map functions tests") {

    int n_workers = 0; // auto-detect

    lace_init(n_workers, 0);

    lace_startup(0, NULL, NULL);

    sylvan::sylvan_set_limits(512*1024*1024, 1, 5);

    sylvan::sylvan_init_package();

    sylvan::sylvan_init_mtbdd();



    init();

    cudd::Cudd manager;

    size_t size = 0U;



    bdd_init(1000, 1000);

    bdd_setvarnum(20);



    SECTION("Map1/negation test") {

    SECTION("Map1") {

        size = 8U;

        cudd::Bvec cudd = cudd::Bvec::bvec_false(manager, size);
@@ -314,7 +300,7 @@ TEST_CASE("Map functions tests") { 
        REQUIRE(isEqual(cudd, sylvan, buddy));

    }



    SECTION("Map2/* test") {

    SECTION("Map2 test") {

        size = 8U;

        cudd::Bvec cudd = cudd::Bvec::bvec_false(manager, size);
@@ -338,7 +324,7 @@ TEST_CASE("Map functions tests") { 
        REQUIRE(isEqual(cudd, sylvan, buddy));

    }



    SECTION("Map3 test") { //TODO

    SECTION("Map3 test") {

        size = 8U;

        cudd::Bvec cudd = cudd::Bvec::bvec_false(manager, size);
@@ -368,35 +354,29 @@ TEST_CASE("Map functions tests") { 
        REQUIRE(isEqual(cudd, sylvan, buddy));

    }



    sylvan::sylvan_stats_report(stdout);

    sylvan::sylvan_quit();

    lace_exit();

    finish();

}



TEST_CASE("Basic operations") {

    init();

    cudd::Cudd manager;

    size_t size = 0U;



    SECTION("") {



    bdd_done();

    }



/*TEST_CASE("") {

    int n_workers = 0; // auto-detect

    lace_init(n_workers, 0);

    lace_startup(0, NULL, NULL);

    sylvan::sylvan_set_limits(512*1024*1024, 1, 5);

    sylvan::sylvan_init_package();

    sylvan::sylvan_init_mtbdd();

    finish();

}



TEST_CASE("") {

    init();

    cudd::Cudd manager;

    size_t size = 0U;



    bdd_init(1000, 1000);

    bdd_setvarnum(20);



    SECTION("") {



    }



    sylvan::sylvan_stats_report(stdout);

    sylvan::sylvan_quit();

    lace_exit();



    bdd_done();

    finish();

}
 
*/