BoolDiffEnc¶
-
class BoolDiffEnc : public SubEnc¶
ブール微分を表すCNFを生成するクラス
StructEngine に部品として組み込んで用いる SubEnc の継承クラス
参考
起点となるノードにおける値の反転がいずれかの外部出力に伝搬する 条件を表す変数を生成する． 生成された変数は prop_var() で取得できる．
prop_var() が true になったときの十分条件は extract_sufficient_condition() で取得できる．
Public Functions
-
BoolDiffEnc(const TpgNode &root, const JsonValue &option = JsonValue{})¶
コンストラクタ
- パラメータ:
root -- [in] 起点のノード
option -- [in] オプション
-
BoolDiffEnc(const TpgNode &root, const TpgNodeList &output_list, const JsonValue &option = JsonValue{})¶
コンストラクタ
- パラメータ:
root -- [in] 起点のノード
output_list -- [in] 出力のリスト
option -- [in] オプション
-
~BoolDiffEnc()¶
デストラクタ
-
inline const TpgNodeList &tfo_list() const¶
root_node() の TFO を返す．
-
inline const TpgNodeList &output_list() const¶
root_node() から到達可能な外部出力のリストを返す．
-
inline SizeType output_num() const¶
root_node() から到達可能な外部出力の数を返す．
-
inline TpgNode output(SizeType pos) const¶
root_node() から到達可能な外部出力を返す．
- パラメータ:
pos -- [in] 出力番号 ( 0 <= pos < output_num() )
-
inline SatLiteral prop_var() const¶
微分結果を表す変数を返す．
-
inline SatLiteral prop_var(SizeType pos) const¶
微分結果を表す変数を返す．
- パラメータ:
pos -- [in] 出力番号 ( 0 <= pos < output_num() )
-
AssignList extract_sufficient_condition()¶
直前の check() が成功したときの十分条件を求める．
-
AssignList extract_sufficient_condition(SizeType pos)¶
直前の check() が成功したときの十分条件を求める．
- パラメータ:
pos -- [in] 出力番号 ( 0 <= pos < output_num() )
-
BoolDiffEnc(const TpgNode &root, const JsonValue &option = JsonValue{})¶