StructEngine¶
StructEngine は内部に SAT ソルバを持つ． 基本的にはコンストラクタで与えられた network 内のノードの入出力 関係を表すCNFをそのSATソルバに追加することになるが， 無駄なCNFを追加する必要はないのでどのノードを使用するかを指定する必要がある．
void
add_cur_node(
const TpgNode& node
);
void
add_cur_node_list(
const TpgNodeList& node_list
);
void
add_prev_node(
const TpgNode& node
);
void
add_prev_node_list(
const TpgNodeList& node_list
);
add_cur_node() と add_cur_node_list() では指定されたノードの推移的ファンアウトの推移的ファンインを 対象のノードに追加する． もちろん重複した追加は無視される．
add_prev_node() と add_prev_node_list() では指定されたノードの推移的ファンインを1時刻前のノードの 対象に追加する． もちろん重複した追加は無視される． こちらは遷移故障の1時刻前の条件に用いられる．
これらの関数は処理を行うべきノードのリストに追加しているだけで 実際の処理は行わない． 未処理のノードは SATソルバを起動する時には処理されるようになっているが， 明示的に処理済みにするためには以下の関数を呼び出す．
void
update();
-
class StructEngine¶
DTPG 用の基本的なエンコードを行うクラス
SATソルバとノード用の変数マップを持つ． 具体的な仕事は SubEnc の継承クラスを登録することで行う．
Subclassed by BdEngine
Public Functions
-
StructEngine(const TpgNetwork &network, const JsonValue &option = JsonValue{})¶
コンストラクタ
- パラメータ:
network -- [in] 対象のネットワーク
option -- [in] 初期化オプション "sat_param": JsonValue SATソルバの初期化パラメータ "justifier": string Justifier の初期化パラメータ
-
~StructEngine()¶
デストラクタ
保持している SubEnc はここで開放される．
-
void add_subenc(std::unique_ptr<SubEnc> &&enc)¶
SubEnc を追加する．
-
inline void add_cur_node_list(const TpgNodeList &node_list)¶
現時刻で考慮するノードのリストを追加する．
実際にはこのノードのTFOのTFIを対象にする．
-
inline void add_prev_node_list(const TpgNodeList &node_list)¶
1時刻前で考慮するノードのリストを追加する．
実際にはこのノードのTFIを対象にする．
-
inline void update()¶
未処理のノードを処理する．
-
AssignList justify(const AssignList &assign_list)¶
与えられた割り当てを満足する外部入力の割り当てを求める．
事前にSAT問題の充足解が求められている必要がある．
必要な値割り当てのみが記録される．
- パラメータ:
assign_list -- [in] 値割り当てのリスト
- 戻り値:
外部入力の割り当てリストを返す．
-
AssignList get_pi_assign()¶
現在の外部入力の割当を得る．
事前にSAT問題の充足解が求められている必要がある．
すべての外部入力になんらかの値が入る
- 戻り値:
外部入力の割り当てリストを返す．
-
std::vector<SatLiteral> conv_to_literal_list(const AssignList &assign_list)¶
値割り当てのリストを対応するリテラルのリストに変換する．
- パラメータ:
assign_list -- [in] 値割り当てのリスト
-
std::vector<SatLiteral> expr_to_cnf(const Expr &expr)¶
与えられた論理式を充足させるCNF式を作る．
論理式中の変数番号は TpgNode->id() * 2 + time に対応している．
- パラメータ:
expr -- [in] 論理式
- 戻り値:
条件を表すリテラルのリストを返す．
-
inline const TpgNetwork &network() const¶
対象のネットワークを得る．
-
inline const TpgNodeList &cur_node_list() const¶
関連するノードのリスト
-
inline const TpgNodeList &prev_node_list() const¶
1時刻前の値に関連するノードのリスト
-
SatLiteral new_variable(bool decision = false)¶
変数を作る．
- パラメータ:
decision -- [in] 決定変数のときに true とする．
-
SatBool3 solve(const std::vector<SatLiteral> &assumptions = {})¶
SAT問題を解く
- パラメータ:
assumptions -- [in] アサートするリテラルのリスト
-
SatStats get_stats() const¶
現在の内部状態を得る．
-
inline SatSolver &solver()¶
SATソルバを返す．
-
bool val(const TpgNode &node, int time)¶
値を返す．
直前に solver().solve() を呼んでいる必要がある．
- パラメータ:
node -- [in] 対象のノード
time -- [in] 時刻(0 or 1)
-
inline double cnf_time() const¶
CNF の生成時間を返す．
-
StructEngine(const TpgNetwork &network, const JsonValue &option = JsonValue{})¶