Commit 40117469 authored by Mateusz Rychlicki's avatar Mateusz Rychlicki
Browse files

New Pipeline

parent b5807ce0
cmake_minimum_required(VERSION 3.3) # CMake version check
project(FairSyn VERSION 1.0)
set(CMAKE_CXX_STANDARD 11) # Enable c++11 standard
set(CMAKE_CXX_FLAGS "-O0 -Wall -Wextra -std=c++11 -Wfatal-errors -g -ldl --coverage -pthread") #-lgcov?
set(CMAKE_VERBOSE_MAKEFILE ON) # show everything
message("CMAKELIST: FaiSyn")
set(CMAKE_CXX_FLAGS_DEBUG "${CMAKE_CXX_FLAGS_DEBUG} -O0")
set(CMAKE_C_FLAGS_DEBUG "${CMAKE_C_FLAGS_DEBUG} -O0")
set(FAIRSYN_ROOT ${PROJECT_SOURCE_DIR})
set(CUDD_PATH "/home/mrychlicki/Desktop/cudd")
set(MASCOT_ROOT "/home/mrychlicki/Desktop/mascot-sds")
set(CUDD_LIBRARY_PATH "/home/mrychlicki/libraries/lib")
set(LD_LIBRARY_PATH "/home/mrychlicki/libraries/lib")
set(GOOGLE_TEST_PATH "/home/mrychlicki/Desktop/googletest")
set(SYLVAN_PATH "/home/mrychlicki/Desktop/sylvan")
set(CMAKE_BINARY_DIR ${FAIRSYN_ROOT}/build)
set(EXECUTABLE_OUTPUT_PATH ${CMAKE_BINARY_DIR}/bin)
set(LIBRARY_OUTPUT_PATH ${CMAKE_BINARY_DIR}/bin)
include_directories(${FAIRSYN_ROOT}/ubdd)
include_directories(
${SYLVAN_PATH}/*
${SYLVAN_PATH}/src
#
# CuddUBDD.hh
#
# created on: 10.09.2021 (In Progress)
# author: Mateusz Rychlicki
# Based on: https://github.com/pabloariasal/modern-cmake-sample/
#
cmake_minimum_required(VERSION 3.13...3.19 FATAL_ERROR)
project(libfairsyn VERSION 1.0.0 LANGUAGES CXX)
message(mascot/farisyn)
#Make sure that custom modules like FindRapidJSON are found
list(INSERT CMAKE_MODULE_PATH 0 ${CMAKE_CURRENT_SOURCE_DIR}/cmake)
##############################################
# Find system dependencies
set(MIN_Cudd_VERSION 3.0)
find_package(Cudd ${MIN_Cudd_VERSION} REQUIRED)
set(MIN_Sylvan_VERSION 1.6)
find_package(Sylvan REQUIRED)
##############################################
# Create target and set properties
add_library(fairsyn
src/ubdd/CuddUBDD.cpp
src/ubdd/CuddUBDDMintermIterator.cpp
src/ubdd/SylvanUBDD.cpp
src/ubdd/SylvanUBDDMintermIterator.cpp
)
#Add an alias so that library can be used inside the build tree, e.g. when testing
add_library(FairSyn::fairsyn ALIAS fairsyn)
#Set target properties
target_include_directories(fairsyn
PUBLIC
$<INSTALL_INTERFACE:include>
$<BUILD_INTERFACE:${CMAKE_CURRENT_SOURCE_DIR}/include>
PRIVATE
${CMAKE_CURRENT_SOURCE_DIR}/src
)
target_compile_features(fairsyn PRIVATE cxx_auto_type)
target_compile_options(fairsyn PRIVATE
$<$<OR:$<CXX_COMPILER_ID:Clang>,$<CXX_COMPILER_ID:AppleClang>,$<CXX_COMPILER_ID:GNU>>:
-Wall -Wextra -Wpedantic>)
target_link_libraries(fairsyn PRIVATE Cudd::Cudd Sylvan::Sylvan)
add_link_options(--coverage -pthread)
##############################################
# Installation instructions
include(GNUInstallDirs)
set(INSTALL_CONFIGDIR ${CMAKE_INSTALL_LIBDIR}/cmake/FairSyn)
install(TARGETS fairsyn
EXPORT fairsyn-targets
LIBRARY DESTINATION ${CMAKE_INSTALL_LIBDIR}
ARCHIVE DESTINATION ${CMAKE_INSTALL_LIBDIR}
)
#This is required so that the exported target has the name FairSyn and not fairsyn
set_target_properties(fairsyn PROPERTIES EXPORT_NAME FairSyn)
install(DIRECTORY include/ DESTINATION ${CMAKE_INSTALL_INCLUDEDIR})
#Export the targets to a script
install(EXPORT fairsyn-targets
FILE
FairSynTargets.cmake
NAMESPACE
FairSyn::
DESTINATION
${INSTALL_CONFIGDIR}
)
#Create a ConfigVersion.cmake file
include(CMakePackageConfigHelpers)
write_basic_package_version_file(
${CMAKE_CURRENT_BINARY_DIR}/FairSynConfigVersion.cmake
VERSION ${PROJECT_VERSION}
COMPATIBILITY AnyNewerVersion
)
include_directories(
${CUDD_PATH}
${CUDD_PATH}/include
${CUDD_PATH}/cudd
${CUDD_PATH}/lib
${CUDD_PATH}/util
${CUDD_PATH}/dddmph)
include_directories(${CUDD_LIBRARY_PATH})
configure_package_config_file(${CMAKE_CURRENT_LIST_DIR}/cmake/FairSynConfig.cmake.in
${CMAKE_CURRENT_BINARY_DIR}/FairSynConfig.cmake
INSTALL_DESTINATION ${INSTALL_CONFIGDIR}
)
#Install the config, configversion and custom find modules
install(FILES
${CMAKE_CURRENT_LIST_DIR}/cmake/FindCudd.cmake
${CMAKE_CURRENT_LIST_DIR}/cmake/FindSylvan.cmake
${CMAKE_CURRENT_BINARY_DIR}/FairSynConfig.cmake
${CMAKE_CURRENT_BINARY_DIR}/FairSynConfigVersion.cmake
DESTINATION ${INSTALL_CONFIGDIR}
)
##############################################
## Exporting from the build tree
configure_file(${CMAKE_CURRENT_LIST_DIR}/cmake/FindCudd.cmake
${CMAKE_CURRENT_BINARY_DIR}/FindCudd.cmake
COPYONLY)
configure_file(${CMAKE_CURRENT_LIST_DIR}/cmake/FindSylvan.cmake
${CMAKE_CURRENT_BINARY_DIR}/FindSylvan.cmake
COPYONLY)
export(EXPORT fairsyn-targets
FILE ${CMAKE_CURRENT_BINARY_DIR}/FairSynTargets.cmake
NAMESPACE FairSyn::)
add_subdirectory(${FAIRSYN_ROOT}/ubdd)
add_subdirectory(${FAIRSYN_ROOT}/tests)
#Register package in the User Package Registry
export(PACKAGE FairSyn)
##############################################
## Add test
enable_testing()
add_subdirectory(test)
message(mascot/fairsyn/cmake/FairSynConfig.cmake.in)
get_filename_component(FAIRSYN_CMAKE_DIR "${CMAKE_CURRENT_LIST_FILE}" PATH)
include(CMakeFindDependencyMacro)
list(APPEND CMAKE_MODULE_PATH ${FAIRSYN_CMAKE_DIR})
# NOTE: to find FindSylvan.cmake
find_dependency(Sylvan @MIN_Sylvan_VERSION@)
find_dependency(Cudd @MIN_Cudd_VERSION@)
list(REMOVE_AT CMAKE_MODULE_PATH -1)
if(NOT TARGET FairSyn::FairSyn)
include("${FAIRSYN_CMAKE_DIR}/FairSynTargets.cmake")
endif()
set(FAIRSYN_lIBRARIES FairSyn::FairSyn)
\ No newline at end of file
message(mascot/fairsyn/cmake/FindCudd.cmake)
find_package(PkgConfig)
pkg_check_modules(PC_Cudd QUIET Cudd)
find_path(Cudd_INCLUDE_DIR NAMES cudd.h uddObj.hh dddmp.h)
find_library(Cudd_STATIC_LIB_DIR NAMES libcudd.a)
find_library(Cudd_SHARED_LIB_DIR NAMES libcudd.so)
set(Cudd_VERSION ${PC_Cudd_VERSION})
mark_as_advanced(Cudd_FOUND Cudd_INCLUDE_DIR Cudd_VERSION)
include(FindPackageHandleStandardArgs)
find_package_handle_standard_args(Cudd
REQUIRED_VARS Cudd_INCLUDE_DIR
VERSION_VAR Cudd_VERSION
)
if(Cudd_FOUND)
#Set include dirs to parent, to enable includes like #include <rapidjson/document.h>
get_filename_component(Cudd_INCLUDE_DIRS ${Cudd_INCLUDE_DIR} DIRECTORY)
endif()
if(Cudd_FOUND AND NOT TARGET Cudd::Cudd)
add_library(Cudd::Cudd STATIC IMPORTED)
set_target_properties(
Cudd::Cudd
PROPERTIES
IMPORTED_LOCATION ${Cudd_STATIC_LIB_DIR}
INTERFACE_INCLUDE_DIRECTORIES "${Cudd_INCLUDE_DIRS}"
)
endif()
message(mascot/fairsyn/cmake/FindSylvan.cmake)
find_package(PkgConfig)
pkg_check_modules(PC_Sylvan QUIET Sylvan)
find_path(Sylvan_INCLUDE_DIR NAMES sylvan.h)
find_library(Sylvan_STATIC_LIB_DIR NAMES libSylvan.a)
find_library(Sylvan_SHARED_LIB_DIR NAMES libSylvan.so)
set(Sylvan_VERSION ${PC_Sylvan_VERSION})
mark_as_advanced(Sylvan_FOUND Sylvan_INCLUDE_DIR Sylvan_VERSION)
include(FindPackageHandleStandardArgs)
find_package_handle_standard_args(Sylvan
REQUIRED_VARS Sylvan_INCLUDE_DIR
VERSION_VAR Sylvan_VERSION
)
if(Sylvan_FOUND)
#Set include dirs to parent, to enable includes like #include <Sylvan/document.h>
get_filename_component(Sylvan_INCLUDE_DIRS ${Sylvan_INCLUDE_DIR} DIRECTORY)
endif()
if(Sylvan_FOUND AND NOT TARGET Sylvan::Sylvan)
add_library(Sylvan::Sylvan STATIC IMPORTED)
set_target_properties(
Sylvan::Sylvan
PROPERTIES
IMPORTED_LOCATION ${Sylvan_STATIC_LIB_DIR}
INTERFACE_INCLUDE_DIRECTORIES "${Sylvan_INCLUDE_DIRS}"
)
endif()
#add_link_options(--coverage)
cmake_minimum_required(VERSION 3.5.0)
project(googletest-download NONE)
include(ExternalProject)
ExternalProject_Add(googletest
GIT_REPOSITORY https://github.com/google/googletest.git
GIT_TAG master
SOURCE_DIR "${CMAKE_BINARY_DIR}/googletest-src"
BINARY_DIR "${CMAKE_BINARY_DIR}/googletest-build"
CONFIGURE_COMMAND ""
BUILD_COMMAND ""
INSTALL_COMMAND ""
TEST_COMMAND ""
)
......@@ -5,54 +5,54 @@
* author: Mateusz Rychlicki
*
*/
#pragma once
#ifndef BASEUBDD_HH_
#define BASEUBDD_HH_
#include "UBDDMintermIterator.hh"
#include <cstdio>
#include <string>
#include <vector>
// Base class
template <typename SubUBDD>// CRTP - Curiously recurring template pattern
class BaseUBDD {
public:
/**
namespace fairsyn {
// Base class
template <typename SubUBDD>// CRTP - Curiously recurring template pattern
class BaseUBDD {
public:
/**
* @brief Returns the Bdd representing "False"
*/
virtual SubUBDD zero() const = 0;
virtual SubUBDD zero() const = 0;
/**
/**
* @brief Returns the Bdd representing "True"
*/
virtual SubUBDD one() const = 0;
virtual SubUBDD one() const = 0;
/**
/**
* @brief Returns a new %UBDD variable.
* @details The new variable has an index equal to the largest previous
* index plus 1.
*/
virtual SubUBDD var() const = 0;
virtual SubUBDD var() const = 0;
/**
/**
* @brief Returns a %UBDD variable with this index. If doesn't exist then create it.
* @param index of variable.
* @details If nodeSize() < index then creates ubdds for all indexes between nodeSize() and index.
*/
virtual SubUBDD var(size_t index) const = 0;
virtual SubUBDD var(size_t index) const = 0;
/**
/**
* @brief Returns the number of %UBDD variables in existance.
*/
virtual size_t nodeSize() const = 0;
virtual size_t nodeSize() const = 0;
/**
/**
* @brief Gets the index of this node.
*/
virtual size_t nodeIndex() const = 0;
virtual size_t nodeIndex() const = 0;
/**
/**
* @brief Returns the Bdd representing a cube of variables, according to the given values.
* @param variables the variables that will be in the cube in their positive or negative form
* @param string a character array describing how the variables will appear in the result
......@@ -60,73 +60,73 @@ public:
* For every ith char in string, if it is 0, the corresponding variable will appear in its
* negative form, otherwise it will appear in its positive form.
*/
virtual SubUBDD cube(std::vector<SubUBDD> variables, std::vector<int> values) const = 0;
virtual SubUBDD cube(std::vector<SubUBDD> variables, std::vector<int> values) const = 0;
virtual SubUBDD cube(std::vector<SubUBDD> variables, std::vector<uint8_t> values) const = 0;
/**
virtual SubUBDD cube(std::vector<SubUBDD> variables, std::vector<uint8_t> values) const = 0;
/**
* @brief Returns the Bdd representing a cube of variables.
* @param variables the variables that will be in the cube in their positive form
* @details We assume that "values" contains only "1"
*/
virtual SubUBDD cube(std::vector<SubUBDD> variables) const = 0;
virtual SubUBDD cube(std::vector<SubUBDD> variables) const = 0;
/**
/**
* @brief Substitute all variables in the array from by the corresponding variables in to.
*/
virtual SubUBDD permute(const std::vector<size_t> &from, const std::vector<size_t> &to) const = 0;
virtual SubUBDD permute(const std::vector<size_t> &from, const std::vector<size_t> &to) const = 0;
/**
/**
* @brief Compute the number of satisfying variable assignments (minterms), using the given number of variables.
* @param number of variables
* @details Works like CountMinterm from cudd.
*/
virtual double countMinterm(size_t nvars) const = 0;
virtual double countMinterm(size_t nvars) const = 0;
virtual void printMinterm() const = 0;
virtual void printMinterm() const = 0;
/**
/**
* @brief Computes \exists cube: f
*/
virtual SubUBDD existAbstract(const SubUBDD &cube) const = 0;
virtual SubUBDD existAbstract(const SubUBDD &cube) const = 0;
/**
/**
* @brief Computes \exists cube: f \and g
*/
virtual SubUBDD andAbstract(const SubUBDD &g, const SubUBDD &cube) const = 0;
virtual SubUBDD andAbstract(const SubUBDD &g, const SubUBDD &cube) const = 0;
/**
/**
* @brief Generate minterm iterator
* @details Look at UBDDMintermIterator.hh and Polymorphism
*/
virtual UBDDMintermIterator *generateMintermIterator(std::vector<size_t> &ivars) const = 0; // todo const or no const?
virtual UBDDMintermIterator *generateMintermIterator(std::vector<size_t> &ivars) const = 0;// todo const or no const?
virtual SubUBDD complement(SubUBDD &symbolicSet,
std::vector<size_t> nofGridPoints,
std::vector<size_t> nofBddVars,
std::vector<std::vector<size_t>> indBddVars,
size_t dim) = 0;
virtual SubUBDD complement(SubUBDD &symbolicSet,
std::vector<size_t> nofGridPoints,
std::vector<size_t> nofBddVars,
std::vector<std::vector<size_t>> indBddVars,
size_t dim) = 0;
/**
/**
* @brief compute smallest radius of ball that contains L*cell
*/
virtual SubUBDD computePolytope(const size_t p,
const std::vector<double> &H,
const std::vector<double> &h,
int type,
size_t dim,
const std::vector<double> &eta,
const std::vector<double> &z,
const std::vector<double> &firstGridPoint,
const std::vector<size_t> &nofBddVars,
const std::vector<std::vector<size_t>> &indBddVars,
const std::vector<size_t> &nofGridPoints) = 0;
/**
virtual SubUBDD computePolytope(const size_t p,
const std::vector<double> &H,
const std::vector<double> &h,
int type,
size_t dim,
const std::vector<double> &eta,
const std::vector<double> &z,
const std::vector<double> &firstGridPoint,
const std::vector<size_t> &nofBddVars,
const std::vector<std::vector<size_t>> &indBddVars,
const std::vector<size_t> &nofGridPoints) = 0;
/**
* @brief Save %UBDD to file.
*/
virtual int save(FILE *file) = 0;
virtual int save(FILE *file) = 0;
/**
/**
* @brief Load %UBDD to file.
* If (newID) load(file,{},0).permute({1,2,3,4...n}, composeids});
*
......@@ -135,54 +135,52 @@ public:
*
* Cudd has bug when newID == 0.
* */
virtual SubUBDD load(FILE *file, std::vector<int> composeids, int newID) = 0;
virtual SubUBDD load(FILE *file, std::vector<int> composeids, int newID) = 0;
/**
/**
* @brief Convert a %BDD from a manager to another one.
* This is used for paralleling in cudd.
*/
virtual SubUBDD transfer(const SubUBDD &ubdd) const = 0;
virtual SubUBDD transfer(const SubUBDD &ubdd) const = 0;
virtual bool isCoverEqual(const SubUBDD &other) const = 0;
virtual bool isCoverEqual(const SubUBDD &other) const = 0;
virtual SubUBDD &operator=(const SubUBDD &right) = 0;
virtual bool operator==(const SubUBDD &other) const = 0;
virtual bool operator!=(const SubUBDD &other) const = 0;
virtual bool operator<=(const SubUBDD &other) const = 0;
virtual bool operator>=(const SubUBDD &other) const = 0;
virtual bool operator<(const SubUBDD &other) const = 0;
virtual bool operator>(const SubUBDD &other) const = 0;
virtual SubUBDD &operator=(const SubUBDD &right) = 0;
virtual bool operator==(const SubUBDD &other) const = 0;
virtual bool operator!=(const SubUBDD &other) const = 0;
virtual bool operator<=(const SubUBDD &other) const = 0;
virtual bool operator>=(const SubUBDD &other) const = 0;
virtual bool operator<(const SubUBDD &other) const = 0;
virtual bool operator>(const SubUBDD &other) const = 0;
/** @brief Not*/
virtual SubUBDD operator!() const = 0;
/** @brief Not*/
virtual SubUBDD operator!() const = 0;
/** @brief Not*/
virtual SubUBDD operator~() const = 0;
/** @brief Not*/
virtual SubUBDD operator~() const = 0;
/** @brief And*/
virtual SubUBDD operator*(const SubUBDD &other) const = 0;
virtual SubUBDD operator*=(const SubUBDD &other) = 0;
/** @brief And*/
virtual SubUBDD operator*(const SubUBDD &other) const = 0;
virtual SubUBDD operator*=(const SubUBDD &other) = 0;
/** @brief And*/
virtual SubUBDD operator&(const SubUBDD &other) const = 0;
virtual SubUBDD operator&=(const SubUBDD &other) = 0;
/** @brief And*/
virtual SubUBDD operator&(const SubUBDD &other) const = 0;
virtual SubUBDD operator&=(const SubUBDD &other) = 0;
/** @brief Or*/
virtual SubUBDD operator+(const SubUBDD &other) const = 0;
virtual SubUBDD operator+=(const SubUBDD &other) = 0;
/** @brief Or*/
virtual SubUBDD operator+(const SubUBDD &other) const = 0;
virtual SubUBDD operator+=(const SubUBDD &other) = 0;
/** @brief Or*/
virtual SubUBDD operator|(const SubUBDD &other) const = 0;
virtual SubUBDD operator|=(const SubUBDD &other) = 0;
/** @brief Or*/
virtual SubUBDD operator|(const SubUBDD &other) const = 0;
virtual SubUBDD operator|=(const SubUBDD &other) = 0;
/** @brief Xor*/
virtual SubUBDD operator^(const SubUBDD &other) const = 0;
virtual SubUBDD operator^=(const SubUBDD &other) = 0;
/** @brief Xor*/
virtual SubUBDD operator^(const SubUBDD &other) const = 0;
virtual SubUBDD operator^=(const SubUBDD &other) = 0;
/** @brief A and not B */
virtual SubUBDD operator-(const SubUBDD &other) const = 0;
virtual SubUBDD operator-=(const SubUBDD &other) = 0;
};
#endif /* BASEUBDD_HH_
*/
\ No newline at end of file
/** @brief A and not B */
virtual SubUBDD operator-(const SubUBDD &other) const = 0;
virtual SubUBDD operator-=(const SubUBDD &other) = 0;
};
}// namespace fairsyn
\ No newline at end of file
/*
* CuddUBDD.hh
*
* created on: 01.07.2021 (In Progress)
* author: Mateusz Rychlicki
*
*/
#pragma once
#include "BaseUBDD.hh"
#include "CuddUBDDMintermIterator.hh"
#include <complex>
#include <memory>
#include <utility>
#include "cudd.h"
#include "cuddObj.hh"
#include "dddmp.h"
namespace fairsyn {
class CuddUBDD : public BaseUBDD<CuddUBDD> {
public:
BDDcudd bdd_;
std::shared_ptr<Cudd> cudd_;
CuddUBDD(BDDcudd &bdd, std::shared_ptr<Cudd> cudd);
CuddUBDD(unsigned int numVars,
unsigned int numVarsZ,
unsigned int numSlots = CUDD_UNIQUE_SLOTS,
unsigned int cacheSize = CUDD_CACHE_SLOTS,
unsigned long maxMemory = 0,
PFC defaultHandler = defaultError);
CuddUBDD(const Cudd &x);
CuddUBDD(CuddUBDD &ubdd);
CuddUBDD(const CuddUBDD &ubdd);
CuddUBDD();
CuddUBDD zero() const override;
CuddUBDD one() const override;
CuddUBDD var() const override;
CuddUBDD var(size_t index) const override;
size_t nodeSize() const override;
size_t nodeIndex() const override;
size_t nodeCount() const;
CuddUBDD cube(std::vector<CuddUBDD> variables, std::vector<int> values) const override;
CuddUBDD cube(std::vector<CuddUBDD> variables, std::vector<uint8_t> values) const override;
CuddUBDD cube(std::vector<CuddUBDD> variables) const override;
CuddUBDD permute(const std::vector<size_t> &from, const std::vector<size_t> &to) const override;
double countMinterm(size_t nvars) const override;
void printMinterm() const override;
double readEpsilon() const;
CuddUBDD existAbstract(const CuddUBDD &cube) const override;
CuddUBDD andAbstract(const CuddUBDD &g, const CuddUBDD &cube) const override;
UBDDMintermIterator *generateMintermIterator(std::vector<size_t> &ivars) const override;
CuddUBDD complement(CuddUBDD &symbolicSet,
std::vector<size_t> nofGridPoints,
std::vector<size_t> nofBddVars,
std::vector<std::vector<size_t>> indBddVars,
size_t dim) override;
CuddUBDD computePolytope(const size_t p,
const std::vector<double> &H,
const std::vector<double> &h,
int type,
size_t dim,
const std::vector<double> &eta,
const std::vector<double> &z,
const std::vector<double> &firstGridPoint,
const std::vector<size_t> &nofBddVars,
const std::vector<std::vector<size_t>> &indBddVars,
const std::vector<size_t> &nofGridPoints) override;
int save(FILE *file) override;
CuddUBDD load(FILE *file, std::vector<int> composeids, int newID) override;
CuddUBDD transfer(const CuddUBDD &destination) const override;
bool isCoverEqual(const CuddUBDD &other) const override;
CuddUBDD &operator=(const CuddUBDD &right) override;
bool operator==(const CuddUBDD &other) const override;