Questions about provenance of souffle

[qunqunqun]

Hi, I have some questions about the provenance. As usually, I used the provenance function to debugging large datalog in doop -- context-insensitive.dl However, in provenance

isValue(?value) :- 
   MethodHandleCallGraphEdge(?callerCtx,?invo,?calleeCtx,?method,?mh,_),
   basic.ClassConstructor(?method,?type),
   ThisVar(?method,?thisVar),
   isImmutableHContext(?hctx),
   AssignReturnValue(?invo,?ret),
   Var_Type(?ret,?retType),
   basic.SubtypeOf(?type,?retType),
   ?value = cat(?type,cat(" value constructed by method handle ",?mh)).

When I output the rules in ExplainProvenanceImpl.h

        for (auto& rel : prog.getAllRelations()) {
            std::string name = rel->getName();
            // only process info relations
            if (name.find("@info") == std::string::npos) {
                continue;
            }
            // find all the info tuples
            for (auto& tuple : *rel) {
                std::vector<std::string> bodyLiterals;
                RamDomain ruleNum;
                tuple >> ruleNum;
                for (size_t i = 1; i + 1 < rel->getArity(); i++) {
                    std::string bodyLit;
                    tuple >> bodyLit;
                    bodyLiterals.push_back(bodyLit);
                }
                std::string rule;
                tuple >> rule; 
                std::cout << rule << std::endl;     

Then the output is

mainAnalysis.isValue(cat(?type,cat(" value constructed by method handle ",?mh))) :- 
   +disconnected63(),
   mainAnalysis.MethodHandleCallGraphEdge(_,?invo,_,?method,?mh,_),
   _ThisVar(?method,_),
   basic.ClassConstructor(?method,?type),
   AssignReturnValue(?invo,?ret),
   Var_Type(?ret,?retType),
   basic.SubtypeOf(?type,?retType).

1. What does the disconnected63 mean ? In which situation it may occur.

[b-scholz]

This is related to optimisation. The Datalog program is transformed to a new Datalog program that is optimised for speed.

In your situation, a fragment of the rule is an invariant and is evaluated outside of the rule. You can check the transformed Datalog program by typing:

souffle <program> --show=transformed-datalog 

and you will find the definition for

+disconnected63() :- ...