Further refactoring

Author: trolando

CMakeLists.txt

@@ -22,25 +22,25 @@ find_package(Boost REQUIRED random)
 # Knor itself
 add_executable(knor)
 target_sources(knor
-  PRIVATE
-    src/aigcircuit.cpp
-    src/aiger.c
-    src/abcminimization.cpp
-    src/aigencoder.cpp
-    src/bddtools.cpp
-    src/bisim.cpp
-    src/explicitgame.cpp
-    src/knor.cpp
-    src/simplehoa.c
-    src/symgame.cpp
-    ${BISON_hoaparser_OUTPUTS}
-    ${FLEX_hoalexer_OUTPUTS}
+    PRIVATE
+        src/aigcircuit.cpp
+        src/aiger.c
+        src/abcminimization.cpp
+        src/aigencoder.cpp
+        src/bddtools.cpp
+        src/bisim.cpp
+        src/gameconstructor.cpp
+        src/knor.cpp
+        src/simplehoa.c
+        src/symgame.cpp
+        ${BISON_hoaparser_OUTPUTS}
+        ${FLEX_hoalexer_OUTPUTS}
 )
 target_compile_features(knor PUBLIC c_std_11 cxx_std_17)
 target_compile_options(knor PRIVATE -Wall -Wextra -fno-strict-aliasing -Wno-deprecated -Wno-unused-parameter)
 target_link_libraries(knor PRIVATE oink::oink sylvan::sylvan libabc)
 target_link_libraries(knor PRIVATE Boost::boost)
 if(CMAKE_HOST_SYSTEM MATCHES Linux)
-  target_link_libraries(knor PRIVATE "-static")
+    target_link_libraries(knor PRIVATE "-static")
 endif()
 target_include_directories(knor PRIVATE src)

src/aigencoder.cpp

@@ -374,7 +374,7 @@ AIGEncoder::processSOP()
         states_vec.push_back(state);
 
         // encode state using NS vars
-        cap_bdd = SymGame::encode_state(state, game.ns_vars);
+        cap_bdd = BDDTools::encode_state(state, game.ns_vars);
         // keep s > u of this state
         cap_bdd = sylvan_and_exists(full, cap_bdd, game.ns_vars);
 
@@ -599,7 +599,7 @@ void AIGEncoder::processOnehot()
         }
 
         // encode state using NS vars
-        cap_bdd = SymGame::encode_state(state, game.ns_vars);
+        cap_bdd = BDDTools::encode_state(state, game.ns_vars);
         // keep s > u of this state
         cap_bdd = sylvan_and_exists(full, cap_bdd, game.ns_vars);
 

src/bddtools.cpp

@@ -56,3 +56,79 @@ MTBDD BDDTools::pathsToSubroot(MTBDD root, uint32_t firstVar, MTBDD subroot)
 {
     return RUN(paths_to_subroot, root, firstVar, subroot);
 }
+
+/**
+ * Encode a state as a BDD, using statebits 0..<statebits>, offsetted by <offset>+<priobits>
+ * High-significant bits come before low-significant bits in the BDD
+ */
+MTBDD BDDTools::encode_state(uint32_t state, MTBDD statevars)
+{
+    // convert statevars to stack
+    std::vector<unsigned int> vars;
+    while (statevars != mtbdd_set_empty()) {
+        vars.push_back(mtbdd_set_first(statevars));
+        statevars = mtbdd_set_next(statevars);
+    }
+    // create a cube
+    auto cube = mtbdd_true;
+    while (!vars.empty()) {
+        auto var = vars.back();
+        vars.pop_back();
+        if (state & 1) cube = mtbdd_makenode(var, mtbdd_false, cube);
+        else cube = mtbdd_makenode(var, cube, mtbdd_false);
+        state >>= 1;
+    }
+    return cube;
+}
+
+/**
+ * Encode priority i.e. all states via priority <priority>
+ */
+MTBDD BDDTools::encode_prio(int priority, int priobits)
+{
+    MTBDD cube = mtbdd_true;
+    for (int i=0; i<priobits; i++) {
+        if (priority & 1) cube = mtbdd_makenode(priobits-i-1, mtbdd_false, cube);
+        else cube = mtbdd_makenode(priobits-i-1, cube, mtbdd_false);
+        priority >>= 1;
+    }
+    return cube;
+}
+
+
+/**
+* Encode a priostate as a BDD, with priobits before statebits
+* High-significant bits come before low-significant bits in the BDD
+*/
+MTBDD BDDTools::encode_priostate(uint32_t state, uint32_t priority, MTBDD statevars, MTBDD priovars)
+{
+    // convert statevars to stack
+    std::vector<unsigned int> vars;
+    while (statevars != mtbdd_set_empty()) {
+        vars.push_back(mtbdd_set_first(statevars));
+        statevars = mtbdd_set_next(statevars);
+    }
+    // create the cube
+    auto cube = mtbdd_true;
+    while (!vars.empty()) {
+        auto var = vars.back();
+        vars.pop_back();
+        if (state & 1) cube = mtbdd_makenode(var, mtbdd_false, cube);
+        else cube = mtbdd_makenode(var, cube, mtbdd_false);
+        state >>= 1;
+    }
+    // convert priovars to stack
+    while (priovars != mtbdd_set_empty()) {
+        vars.push_back(mtbdd_set_first(priovars));
+        priovars = mtbdd_set_next(priovars);
+    }
+    // create the rest of the cube
+    while (!vars.empty()) {
+        auto var = vars.back();
+        vars.pop_back();
+        if (priority & 1) cube = mtbdd_makenode(var, mtbdd_false, cube);
+        else cube = mtbdd_makenode(var, cube, mtbdd_false);
+        priority >>= 1;
+    }
+    return cube;
+}

src/bddtools.hpp

@@ -32,6 +32,24 @@ class BDDTools {
      * @return a BDD with all paths to the given subroot.
      */
     static sylvan::MTBDD pathsToSubroot(sylvan::MTBDD root, uint32_t firstVar, sylvan::MTBDD subroot);
+
+    /**
+     * Encode a priostate as a BDD, using priobits before statebits
+     * High-significant bits come before low-significant bits in the BDD
+     */
+    static sylvan::MTBDD encode_priostate(uint32_t state, uint32_t priority, sylvan::MTBDD statevars, sylvan::MTBDD priovars);
+
+    /**
+     * Encode a state as a BDD, using statebits 0..<statebits>, offsetted by <offset>+<priobits>
+     * High-significant bits come before low-significant bits in the BDD
+     */
+    static sylvan::MTBDD encode_state(uint32_t state, sylvan::MTBDD state_vars);
+
+    /**
+     * Encode priority i.e. all states via priority <priority>
+     */
+    static sylvan::MTBDD encode_prio(int priority, int priobits);
+
 };
 
 #endif //KNOR_BDDTOOLS_HPP