up_scc_binary.cpp 979 Bytes
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
/*
 * Project SUBool
 * Petr Kucera, 2021
 */
/**@file up_scc_binary.cpp
 * Encoding based on SCCs of the graph of the implication system with levels
 * encoded in binary.
 */

#include "up_scc_binary.h"

void
SUBool::UPSCCBinary::Encode(unsigned max_level, std::vector<unsigned> *inputs,
    std::vector<unsigned> *outputs, std::vector<Clause> *clauses) const
{
   throw NotImplementedException("UPSCCBinary::Encode", "Not yet implemented");
}

auto
SUBool::UPSCCBinary::EstimateSize(unsigned max_level) const -> NFSize
{
   throw NotImplementedException(
       "UPSCCBinary::EstimateSize", "Not yet implemented");
}

unsigned
SUBool::UPSCCBinary::MaxLevelBound() const
{
   return mSCCGraph.MaxEffSCCVarSize();
   throw NotImplementedException(
       "UPSCCBinary::MaxLevelBound", "Not yet implemented");
}

unsigned
SUBool::UPSCCBinary::NextLevelBound(unsigned level) const
{
   throw NotImplementedException(
       "UPSCCBinary::NextLevelBound", "Not yet implemented");
}