Commit 13eec212 authored by Peter Navrátil's avatar Peter Navrátil
Browse files

fixed tests

parent a30ace47

bvec_cudd.h

+0 −1
Original line number Diff line number Diff line
@@ -5,7 +5,6 @@ 
#include <iostream>

#include <vector>

#include <cuddObj.hh>

#include "cudd.h"



namespace cudd {

tests.cpp

+43 −44
Original line number Diff line number Diff line
@@ -66,12 +66,16 @@ TEST_CASE("Construction tests") { 
    int n_workers = 0; // auto-detect

    lace_init(n_workers, 0);

    lace_startup(0, NULL, NULL);

    cudd::Cudd manager;

    size_t size = 0U;

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

    sylvan::sylvan_init_package();

    sylvan::sylvan_init_mtbdd();



    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);
@@ -103,6 +107,7 @@ TEST_CASE("Construction tests") { 
        bvec bvec_buddy = bvec_con_buddy(size, val);



        REQUIRE(isEqual(bvec_cudd, bvec_sylvan, bvec_buddy, val));



    }



    SECTION("Test copy constructors") { //fix
@@ -127,6 +132,7 @@ TEST_CASE("Construction tests") { 
        REQUIRE((bvec_buddy == buddy_operator) == bddtrue);



        REQUIRE(isEqual(bvec_cudd, bvec_sylvan, bvec_buddy, val));



    }



    SECTION("Test bvec_var") { //finish
@@ -136,7 +142,6 @@ TEST_CASE("Construction tests") { 
        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

    }
@@ -146,7 +151,6 @@ TEST_CASE("Construction tests") { 
        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());



    }
@@ -154,7 +158,7 @@ TEST_CASE("Construction tests") { 
    sylvan::sylvan_quit();

    lace_exit();





    bdd_done();

}
@@ -162,12 +166,16 @@ TEST_CASE("Manipulation tests") { 
    int n_workers = 0; // auto-detect

    lace_init(n_workers, 0);

    lace_startup(0, NULL, NULL);

    cudd::Cudd manager;

    size_t size = 0U;

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

    sylvan::sylvan_init_package();

    sylvan::sylvan_init_mtbdd();



    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);
@@ -242,7 +250,7 @@ TEST_CASE("Manipulation tests") { 
        //TODO isequalvar

        REQUIRE(cudd::Bvec::bvec_isConst(cudd_var) == 0);

        REQUIRE(sylvan::Bvec::bvec_isConst(sylvan_var) == 0);

        //REQUIRE(bvec_isconst(buddy_var) == 0); find bug

        REQUIRE(bvec_isconst(buddy_var) == 0);

    }



    SECTION("Test bvec_val") {
@@ -265,18 +273,23 @@ TEST_CASE("Manipulation tests") { 
    sylvan::sylvan_quit();

    lace_exit();



    bdd_done();

}



TEST_CASE("Map functions tests") {

    int n_workers = 0; // auto-detect

    lace_init(n_workers, 0);

    lace_startup(0, NULL, NULL);

    cudd::Cudd manager;

    size_t size = 0U;

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

    sylvan::sylvan_init_package();

    sylvan::sylvan_init_mtbdd();



    cudd::Cudd manager;

    size_t size = 0U;



    bdd_init(1000, 1000);

    bdd_setvarnum(20);



    SECTION("Map1/negation test") {

        size = 8U;

        cudd::Bvec cudd = cudd::Bvec::bvec_false(manager, size);
@@ -295,11 +308,10 @@ TEST_CASE("Map functions tests") { 
        sylvan = !sylvan;

        REQUIRE((sylvan == sylvan::Bvec::bvec_true(size)).isOne());

        REQUIRE(!isEqual(cudd, sylvan, buddy));

        /*std::cout << "pred" << std::endl;

        buddy = !buddy; //wtf?

        std::cout << "za" << std::endl;

        REQUIRE((buddy == bvec_true_buddy(size)) == bddtrue); //fix

        REQUIRE(isEqual(cudd, sylvan, buddy));*/



        buddy = !buddy;

        REQUIRE((buddy == bvec_true_buddy(size)) == bddtrue);

        REQUIRE(isEqual(cudd, sylvan, buddy));

    }



    SECTION("Map2/* test") {
@@ -341,56 +353,41 @@ TEST_CASE("Map functions tests") { 
                return (f & s) & t;

            });



        //REQUIRE(cudd.bitnum() == (size + size));

        //REQUIRE(!isEqual(cudd, sylvan, buddy));

        REQUIRE(isEqual(cudd, sylvan, buddy));



        sylvan = sylvan::Bvec::bvec_map3(sylvan, sylvan, sylvan,

            [] (const sylvan::Bdd& f, const sylvan::Bdd& s, const sylvan::Bdd& t) {

                return (f & s) & t;

            });

        //REQUIRE(sylvan.bitnum() == (size + size));

        //REQUIRE(!isEqual(cudd, sylvan, buddy));

        REQUIRE(isEqual(cudd, sylvan, buddy));



        //buddy = map3(buddy, ;

        // REQUIRE(buddy.bitnum() == (size + size)); //fix

        // REQUIRE(isEqual(cudd, sylvan, buddy));

        buddy = bvec_map3(buddy, buddy, buddy,

            [] (const bdd& f, const bdd& s, const bdd& t) {

                return (f & s) & t;

            });

        REQUIRE(isEqual(cudd, sylvan, buddy));

    }



    sylvan::sylvan_stats_report(stdout);

    sylvan::sylvan_quit();

    lace_exit();



    bdd_done();

}



TEST_CASE("") {

/*TEST_CASE("") {

    int n_workers = 0; // auto-detect

    lace_init(n_workers, 0);

    lace_startup(0, NULL, NULL);

    cudd::Cudd manager;

    size_t size = 0U;

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

    sylvan::sylvan_init_package();

    sylvan::sylvan_init_mtbdd();



    SECTION("") {



    }



    sylvan::sylvan_stats_report(stdout);

    sylvan::sylvan_quit();

    lace_exit();



}



TEST_CASE("") {

    int n_workers = 0; // auto-detect

    lace_init(n_workers, 0);

    lace_startup(0, NULL, NULL);

    cudd::Cudd manager;

    size_t size = 0U;

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

    sylvan::sylvan_init_package();

    sylvan::sylvan_init_mtbdd();



    bdd_init(1000, 1000);

    bdd_setvarnum(20);



    SECTION("") {
@@ -400,4 +397,6 @@ TEST_CASE("") { 
    sylvan::sylvan_quit();

    lace_exit();



    bdd_done();

}

*/