souffle::Explain Class Reference

#include <Explain.h>

Collaboration diagram for souffle::Explain:

Public Member Functions
virtual void	explain ()=0
	Explain (ExplainProvenance &prov)
bool	processCommand (std::string &commandLine)
	~Explain ()=default

Data Fields
ExplainProvenance &	prov

Private Member Functions
virtual std::string	getInput ()=0
std::pair< std::string, std::vector< std::string > >	parseTuple (const std::string &str)
	Parse tuple, split into relation name and values. More...
virtual void	printError (const std::string &error)=0
virtual void	printInfo (const std::string &info)=0
virtual void	printPrompt (const std::string &prompt)=0
virtual void	printTree (Own< TreeNode > tree)=0

Detailed Description

Definition at line 68 of file Explain.h.

Constructor & Destructor Documentation

Explain()

souffle::Explain::Explain ( ExplainProvenance &  prov )

inline

Definition at line 72 of file Explain.h.

: prov(prov) {}

~Explain()

souffle::Explain::~Explain ( )

default

Member Function Documentation

explain()

virtual void souffle::Explain::explain ( )

pure virtual

getInput()

virtual std::string souffle::Explain::getInput ( )

privatepure virtual

Referenced by processCommand().

parseTuple()

std::pair<std::string, std::vector<std::string> > souffle::Explain::parseTuple ( const std::string &  str )

inlineprivate

Parse tuple, split into relation name and values.

Parameters

str	The string to parse, should be something like "R(x1, x2, x3, ...)"

Definition at line 298 of file Explain.h.

References str.

Referenced by processCommand().

printError()

virtual void souffle::Explain::printError ( const std::string &  error )

privatepure virtual

Referenced by processCommand().

printInfo()

virtual void souffle::Explain::printInfo ( const std::string &  info )

privatepure virtual

Referenced by processCommand().

printPrompt()

virtual void souffle::Explain::printPrompt ( const std::string &  prompt )

privatepure virtual

Referenced by processCommand().

printTree()

virtual void souffle::Explain::printTree ( Own< TreeNode >  tree )

privatepure virtual

Referenced by processCommand().

processCommand()

bool souffle::Explain::processCommand ( std::string &  commandLine )

inline

Definition at line 77 of file Explain.h.

                                                {
        std::vector<std::string> command = split(commandLine, ' ', 1);
 
        if (command.empty()) {
            return true;
        }
 
        if (command[0] == "setdepth") {
            if (command.size() != 2) {
                printError("Usage: setdepth <depth>\n");
                return true;
            }
            try {
                ExplainConfig::getExplainConfig().depthLimit = std::stoi(command[1]);
            } catch (std::exception& e) {
                printError("<" + command[1] + "> is not a valid depth\n");
                return true;
            }
            printInfo("Depth is now " + std::to_string(ExplainConfig::getExplainConfig().depthLimit) + "\n");
        } else if (command[0] == "explain") {
            std::pair<std::string, std::vector<std::string>> query;
            if (command.size() != 2) {
                printError("Usage: explain relation_name(\"<string element1>\", <number element2>, ...)\n");
                return true;
            }
            query = parseTuple(command[1]);
            printTree(prov.explain(query.first, query.second, ExplainConfig::getExplainConfig().depthLimit));
        } else if (command[0] == "subproof") {
            std::pair<std::string, std::vector<std::string>> query;
            int label = -1;
            if (command.size() <= 1) {
                printError("Usage: subproof relation_name(<label>)\n");
                return true;
            }
            query = parseTuple(command[1]);
            label = std::stoi(query.second[0]);
            printTree(prov.explainSubproof(query.first, label, ExplainConfig::getExplainConfig().depthLimit));
        } else if (command[0] == "explainnegation") {
            std::pair<std::string, std::vector<std::string>> query;
            if (command.size() != 2) {
                printError(
                        "Usage: explainnegation relation_name(\"<string element1>\", <number element2>, "
                        "...)\n");
                return true;
            }
            query = parseTuple(command[1]);
 
            // a counter for the rule numbers
            size_t i = 1;
            std::string rules;
 
            // if there are no rules, then this must be an EDB relation
            if (prov.getRules(query.first).size() == 0) {
                printInfo("The tuple would be an input fact!\n");
                return true;
            }
 
            for (auto rule : prov.getRules(query.first)) {
                rules += std::to_string(i) + ": ";
                rules += rule;
                rules += "\n\n";
                i++;
            }
            printInfo(rules);
 
            printPrompt("Pick a rule number: ");
 
            std::string ruleNum = getInput();
            auto variables = prov.explainNegationGetVariables(query.first, query.second, std::stoi(ruleNum));
 
            // @ and @non_matching are special sentinel values returned by ExplainProvenance
            if (variables.size() == 1 && variables[0] == "@") {
                printInfo("The tuple exists, cannot explain negation of it!\n");
                return true;
            } else if (variables.size() == 1 && variables[0] == "@non_matching") {
                printInfo("The variable bindings don't match, cannot explain!\n");
                return true;
            } else if (variables.size() == 1 && variables[0] == "@fact") {
                printInfo("The rule is a fact!\n");
                return true;
            }
 
            std::map<std::string, std::string> varValues;
            for (auto var : variables) {
                printPrompt("Pick a value for " + var + ": ");
                varValues[var] = getInput();
            }
 
            printTree(prov.explainNegation(query.first, std::stoi(ruleNum), query.second, varValues));
        } else if (command[0] == "rule" && command.size() == 2) {
            auto query = split(command[1], ' ');
            if (query.size() != 2) {
                printError("Usage: rule <relation name> <rule number>\n");
                return true;
            }
            try {
                printInfo(prov.getRule(query[0], std::stoi(query[1])) + "\n");
            } catch (std::exception& e) {
                printError("Usage: rule <relation name> <rule number>\n");
            }
        } else if (command[0] == "measure") {
            try {
                printInfo(prov.measureRelation(command[1]));
            } catch (std::exception& e) {
                printError("Usage: measure <relation name>\n");
            }
        } else if (command[0] == "output") {
            if (command.size() == 2) {
                // assign a new filestream, the old one is deleted by unique_ptr
                ExplainConfig::getExplainConfig().outputStream = mk<std::ofstream>(command[1]);
            } else if (command.size() == 1) {
                ExplainConfig::getExplainConfig().outputStream = nullptr;
            } else {
                printError("Usage: output  [<filename>]\n");
            }
        } else if (command[0] == "format") {
            if (command.size() == 2 && command[1] == "json") {
                ExplainConfig::getExplainConfig().json = true;
            } else if (command.size() == 2 && command[1] == "proof") {
                ExplainConfig::getExplainConfig().json = false;
            } else {
                printError("Usage: format <json|proof>\n");
            }
        } else if (command[0] == "exit" || command[0] == "q" || command[0] == "quit") {
            // close file stream so that output is actually written to file
            printPrompt("Exiting explain\n");
            return false;
        } else if (command[0] == "query") {
            // if there is no given relations, return directly
            if (command.size() != 2) {
                printError(
                        "Usage: query <relation1>(<element1>, <element2>, ...), "
                        "<relation2>(<element1>, <element2>, ...), ...\n");
                return true;
            }
            // vector relations stores relation name, args pair parsed by parseQueryTuple()
            std::vector<std::pair<std::string, std::vector<std::string>>> relations;
            // regex for relation string
            std::regex relationRegex(
                    "([a-zA-Z0-9_.-]*)[[:blank:]]*\\(([[:blank:]]*([0-9]+|\"[^\"]*\"|[a-zA-Z_][a-zA-Z_0-9]*)("
                    "[[:blank:]]*,[[:blank:]]*(["
                    "0-"
                    "9]+|\"[^\"]*\"|[a-zA-Z_][a-zA-Z_0-9]*))*)?\\)",
                    std::regex_constants::extended);
            std::smatch relationMatcher;
            std::string relationStr = command[1];
            // use relationRegex to match each relation string and call parseQueryTuple() to parse the
            // relation name and arguments
            while (std::regex_search(relationStr, relationMatcher, relationRegex)) {
                relations.push_back(parseQueryTuple(relationMatcher[0]));
 
                // check return value for parseQueryTuple, return if relation name is empty string or tuple
                // arguments is empty
                if (relations.back().first.size() == 0 || relations.back().second.size() == 0) {
                    printError(
                            "Usage: query <relation1>(<element1>, <element2>, ...), "
                            "<relation2>(<element1>, <element2>, ...), ...\n");
                    return true;
                }
                relationStr = relationMatcher.suffix().str();
            }
 
            // is no valid relation can be identified, return directly
            if (relations.size() == 0) {
                printError(
                        "Usage: query <relation1>(<element1>, <element2>, ...), "
                        "<relation2>(<element1>, <element2>, ...), ...\n");
                return true;
            }
 
            // call queryProcess function to process query
            prov.queryProcess(relations);
        } else {
            printError(
                    "\n----------\n"
                    "Commands:\n"
                    "----------\n"
                    "setdepth <depth>: Set a limit for printed derivation tree height\n"
                    "explain <relation>(<element1>, <element2>, ...): Prints derivation tree\n"
                    "explainnegation <relation>(<element1>, <element2>, ...): Enters an interactive\n"
                    "    interface where the non-existence of a tuple can be explained\n"
                    "subproof <relation>(<label>): Prints derivation tree for a subproof, label is\n"
                    "    generated if a derivation tree exceeds height limit\n"
                    "rule <relation name> <rule number>: Prints a rule\n"
                    "output <filename>: Write output into a file, or provide empty filename to\n"
                    "    disable output\n"
                    "format <json|proof>: switch format between json and proof-trees\n"
                    "query <relation1>(<element1>, <element2>, ...), <relation2>(<element1>, <element2>), "
                    "... :\n"
                    "check existence of constant tuples or find solutions for parameterised tuples\n"
                    "for parameterised query, use semicolon to find next solution and dot to break from "
                    "query\n"
                    "exit: Exits this interface\n\n");
        }
 
        return true;
    }

References souffle::ExplainConfig::depthLimit, e, souffle::ExplainProvenance::explain(), souffle::ExplainProvenance::explainNegation(), souffle::ExplainProvenance::explainNegationGetVariables(), souffle::ExplainProvenance::explainSubproof(), souffle::ExplainConfig::getExplainConfig(), getInput(), souffle::ExplainProvenance::getRule(), souffle::ExplainProvenance::getRules(), i, souffle::ExplainConfig::json, souffle::ExplainProvenance::measureRelation(), souffle::ExplainConfig::outputStream, parseTuple(), printError(), printInfo(), printPrompt(), printTree(), prov, souffle::ExplainProvenance::queryProcess(), relations, rule, and souffle::split().

Here is the call graph for this function:

Field Documentation

prov

ExplainProvenance& souffle::Explain::prov

Definition at line 70 of file Explain.h.

Referenced by processCommand().

---

The documentation for this class was generated from the following file:

• include/souffle/provenance/Explain.h