两种基于Tableaux算法的reasoner的源码分析（2）

CGLabel Label;                     // 概念标签集合（所有断言的集合）

#ifdef RKG_IR_IN_NODE_LABEL
IRInfo IR;                         // 不等式关系信息（用于处理"不同个体"）
#endif

ArcCollection Neighbour;           // 角色边列表（指向其他节点）
TSaveList<SaveState> saves;        // 历史状态栈（用于回溯）

unsigned int id;                   // 节点唯一 ID
BipolarPointer Init;               // 创建该节点时的初始概念

const DlCompletionTree* Blocker;   // 当前阻塞该节点的节点（若有）
DepSet pDep;                       // 用于 purge 操作的依赖集

unsigned int curLevel;             // 当前级别（用于回溯）
CTNominalLevel nominalLevel;       // 名义级别（0=名义，-1=块状）

// 布尔标志（位域）
bool flagDataNode : 1;             // 是否数据节点（字面量）
bool cached : 1;                   // 是否已缓存（用于优化）
bool pBlocked : 1;                 // 是否被永久阻塞（purge）
bool dBlocked : 1;                 // 是否被直接阻塞（directly）
bool affected : 1;                 // 是否因阻塞变化而受影响

protected:
    DlCompletionTree* Node = nullptr;  // 1. 箭头指向谁？（指向的目标节点）
    const TRole* Role = nullptr;       // 2. 这条线上标着什么标签？（比如角色 R）
    DepSet depSet;                     // 3. 这条边依赖哪些"决策"产生的？（用于回溯）
    DlCompletionTreeArc* Reverse = nullptr; // 4. 反向的边在哪里？（用于双向查找）
    bool SuccEdge = true;              // 5. 这条边是"向下"（Succ）还是"向上"（Pred）？

bool isIBlocked ( void ) const { return (Role == nullptr); }

bool DlSatTester :: checkSatisfiability ( void )
{
    unsigned int loop = 0;
    for (;;)
    {
        if ( curNode == nullptr )
        {
            if ( TODO.empty() )
            {
                if ( performAfterReasoning() )     // 处理公平性等
                    if ( tunedRestore() )
                        return false;
                if ( TODO.empty() )
                    return true;
            }

            const ToDoEntry* curTDE = TODO.getNextEntry ();  // 取出最高优先级任务
            curNode = curTDE->Node;
            curConcept = curNode->label().getConcept(curTDE->offset);
        }

        if ( ++loop == 5000 ) { /* 超时检查 */ }

        if ( commonTactic() )     // 执行规则，若返回 true 表示发生冲突
        {
            if ( tunedRestore() ) // 尝试回溯，若失败则不可满足
                return false;
        }
        else
            curNode = nullptr;
    }
}