CondGenMgr¶
-
class CondGenMgr¶
FFRの故障伝搬条件を表すCNFを作るクラス
実はただの関数
Public Static Functions
-
static std::vector<DetCond> make_cond(const TpgNetwork &network, const JsonValue &option)¶
FFRの故障伝搬条件を求める．
- パラメータ:
network -- [in] 対象のネットワーク
option -- [in] オプション
- 戻り値:
各 FFR の伝搬条件のリストを返す．
-
static std::vector<std::vector<SatLiteral>> make_cnf(StructEngine &engine, const std::vector<DetCond> &cond_list, const JsonValue &option, CondGenStats &stats)¶
FFRの故障伝搬条件を表すCNF式を作る．
- パラメータ:
engine -- [in] CNFの作成用のエンジン
cond_list -- [in] 条件のリスト
option -- [in] オプション
stats -- [out] 統計情報を入れるオブジェクト
-
static std::vector<std::vector<SatLiteral>> make_cnf_naive(StructEngine &engine, const JsonValue &option, CondGenStats &stats)¶
FFRの故障伝搬条件を表すCNF式を作る(ナイーブバージョン)
- パラメータ:
engine -- [in] CNFの作成用のエンジン
option -- [in] オプション
stats -- [out] 統計情報を入れるオブジェクト
-
static void make_base_cnf(StructEngine &engine)¶
正常回路用の CNF を作る．
- パラメータ:
engine -- [in] CNFの作成用のエンジン
-
static std::vector<Expr> make_expr(const std::vector<DetCond> &cond_list, const JsonValue &option)¶
DetCond から Expr を作る．
DetCond.type() が Detected/PartialDetected の場合のみ Expr を作る．
- パラメータ:
cond_list -- [in] 条件のリスト
option -- [in] オプション
-
static std::vector<std::vector<SatLiteral>> expr_to_cnf(StructEngine &engine, const std::vector<Expr> &expr_list, const JsonValue &option)¶
Expr を CNF に変換する．
- パラメータ:
engine -- [in] CNFの作成用のエンジン
expr_list -- [in] 式のリスト
option -- [in] オプション
-
static std::vector<SatLiteral> make_bd(StructEngine &engine, const std::vector<DetCond> &cond_list)¶
BoolDiffEnc を用いた条件を作る．
DetCond.type() が PartialDetected/Overflow の場合にのみ BoolDiffEnc を作る．
- パラメータ:
engine -- [in] CNFの作成用のエンジン
cond_list -- [in] 条件
-
static std::vector<DetCond> make_cond(const TpgNetwork &network, const JsonValue &option)¶