dlvhex
2.5.0
|
Implements a grounder without using third-party software. More...
#include <include/dlvhex2/InternalGrounder.h>
Public Types | |
enum | OptLevel { full, builtin, none } |
Defines how much the grounder optimizes. More... | |
typedef boost::shared_ptr < InternalGrounder > | Ptr |
typedef boost::shared_ptr < const InternalGrounder > | ConstPtr |
Public Member Functions | |
InternalGrounder (ProgramCtx &ctx, const OrdinaryASPProgram &p, OptLevel=full) | |
Constructor; will immediately run the grounder! | |
const OrdinaryASPProgram & | getGroundProgram () |
Extracts the ground program. | |
const OrdinaryASPProgram & | getNongroundProgram () |
Extracts the nonground program. | |
std::string | getGroundProgramString () |
Extracts the ground program as string. | |
std::string | getNongroundProgramString () |
Extracts the nonground program as string. | |
Protected Types | |
enum | AppDir { x_op_y_eq_ret, x_op_ret_eq_y, ret_op_y_eq_x } |
Used in method InternalGrounder::applyIntFunction to specify the order of application of a builtin function. More... | |
typedef boost::unordered_map < ID, ID > | Substitution |
typedef boost::unordered_map < ID, int > | Binder |
typedef boost::adjacency_list < boost::vecS, boost::vecS, boost::bidirectionalS, ID > | DepGraph |
typedef DepGraph::vertex_descriptor | Node |
typedef boost::adjacency_list < boost::vecS, boost::vecS, boost::bidirectionalS, int > | SCCDepGraph |
Protected Member Functions | |
void | computeDepGraph () |
Construct atom dependency graph. | |
ID | preprocessRule (ID ruleID) |
Check if rule can be handled and insert variable names for anonymous variables. | |
void | computeStrata () |
Partitions the program into strata using the atom dependency graph. | |
void | buildPredicateIndex () |
Extract for all predicates the rules and atoms where it occurs. | |
void | loadStratum (int index) |
Load stratum into groundRules and nonGroundRules. | |
void | groundStratum (int index) |
Grounds a specific stratum. | |
void | groundRule (ID ruleID, Substitution &s, std::vector< ID > &groundedRules, Set< ID > &newDerivableAtoms) |
Generates all ground instances of a rule. | |
void | buildGroundInstance (ID ruleID, Substitution s, std::vector< ID > &groundedRules, Set< ID > &newDerivableAtoms) |
Generates a single ground instance of a rule. | |
bool | match (ID literalID, ID patternLiteral, Substitution &s) |
Checks if a literal matches a given pattern using a substitution. | |
bool | matchOrdinary (ID literalID, ID patternAtom, Substitution &s) |
Checks if an ordinary literal matches a given pattern using a substitution. | |
bool | matchBuiltin (ID literalID, ID patternAtom, Substitution &s) |
Checks if a builtin literal matches a given pattern using a substitution. | |
int | matchNextFromExtension (ID literalID, Substitution &s, int startSearchIndex) |
Computes the index of the next derivable atom which matches against the given literal using a given substitution. | |
int | matchNextFromExtensionOrdinary (ID literalID, Substitution &s, int startSearchIndex) |
Computes the index of the next derivable ordinary atom which matches against the given literal using a given substitution. | |
int | matchNextFromExtensionBuiltin (ID literalID, Substitution &s, int startSearchIndex) |
Computes the index of the next derivable builtin atom which matches against the given literal using a given substitution. | |
int | matchNextFromExtensionBuiltinUnary (ID literalID, Substitution &s, int startSearchIndex) |
Computes the index of the next derivable unary builtin atom which matches against the given literal using a given substitution. | |
int | matchNextFromExtensionBuiltinBinary (ID literalID, Substitution &s, int startSearchIndex) |
Computes the index of the next derivable binary builtin atom which matches against the given literal using a given substitution. | |
int | matchNextFromExtensionBuiltinTernary (ID literalID, Substitution &s, int startSearchIndex) |
Computes the index of the next derivable ternary builtin atom which matches against the given literal using a given substitution. | |
int | backtrack (ID ruleID, Binder &binders, int currentIndex) |
Backtracks to the previous substitution where search is to be continued. | |
void | setToTrue (ID atom) |
Makes atom permanently true (EDB fact). | |
void | addDerivableAtom (ID atom, std::vector< ID > &groundRules, Set< ID > &newDerivableAtoms) |
Is called after one or more atoms became derivable. | |
ID | applySubstitutionToAtom (Substitution s, ID atomID) |
Applies a substitution to an atom. | |
ID | applySubstitutionToOrdinaryAtom (Substitution s, ID atomID) |
Applies a substitution to an ordinary atom. | |
ID | applySubstitutionToBuiltinAtom (Substitution s, ID atomID) |
Applies a substitution to a bulitin atom. | |
std::string | atomToString (ID atomID) |
Returns a string representation of an atom. | |
std::string | ruleToString (ID ruleID) |
Returns a string representation of a rule. | |
ID | getPredicateOfAtom (ID atomID) |
Extracts the predicate from an atom. | |
bool | isGroundRule (ID ruleID) |
Checks if a rule id ground. | |
bool | isPredicateGrounded (ID pred) |
Checks if a predicate is fully grounded, i.e., it comes from a lower stratum. | |
bool | isPredicateSolved (ID pred) |
Checks if a predicate is fully solved. | |
bool | isAtomDerivable (ID atom) |
Checks if an atom is derivable (in principle, i.e., some rule derives it). | |
int | getStratumOfRule (ID ruleID) |
Returns the stratum index of a rule. | |
void | computeGloballyNewAtom () |
Constructs a new atom which does not yet occur in the ground program and stored it in globallyNewAtom. | |
Binder | getBinderOfRule (std::vector< ID > &body) |
Retrieves for a given rule body its binder. | |
int | getClosestBinder (std::vector< ID > &body, int litIndex, std::set< ID > variables) |
Retrieves for a given rule body the literal up to litIndex which first binds a variable from variables . | |
std::set< ID > | getFreeVars (std::vector< ID > &body, int litIndex) |
Returns for a given literal in a rule all variables which are not bounded before that literal. | |
std::set< ID > | getOutputVariables (ID ruleID) |
Returns for a given rule the output variables. | |
std::vector< ID > | reorderRuleBody (ID ruleID) |
Reorders a rule (mainly for optimization purposes). | |
bool | biDependency (ID bi1, ID bi2) |
Checks if two builtin atoms depend on each other. | |
int | applyIntFunction (AppDir ad, ID op, int x, int y) |
Applies a builtin function to two values. | |
Protected Attributes | |
OrdinaryASPProgram | inputprogram |
Nonground input program. | |
OrdinaryASPProgram | groundProgram |
Ground output program after the grounder has finished. | |
ProgramCtx & | ctx |
ProgramCtx. | |
RegistryPtr | reg |
Registry. | |
OptLevel | optlevel |
Level of optimization used. | |
boost::unordered_map< ID, Node > | depNodes |
Nodes of depSCC. | |
DepGraph | depGraph |
Atom dependency graph. | |
std::vector< Set< ID > > | depSCC |
Strongly connected components of depSCC. | |
SCCDepGraph | compDependencies |
Dependencies between program components (=program strata). | |
std::vector< std::set< ID > > | predicatesOfStratum |
Stores for each stratum the contained predicates. | |
std::vector< std::set< ID > > | rulesOfStratum |
Stores for each stratum the contained rules. | |
boost::unordered_map< ID, int > | stratumOfPredicate |
Stores for each predicate its stratum index. | |
ID | globallyNewAtom |
An atom which does not occur in the program. | |
boost::unordered_map< ID, std::vector< ID > > | derivableAtomsOfPredicate |
Stores for each predicate (=term) the set of ground atoms over this predicate which are currently derivable. | |
boost::unordered_map< ID, std::set< std::pair< int, int > > > | positionsOfPredicate |
Stores for each predicate the set of non-ground rules and body positions where the predicate occurs. | |
InterpretationPtr | trueAtoms |
Atoms which are definitely true (=EDB). | |
std::vector< ID > | groundRules |
Generated ground rules in the current stratum. | |
std::vector< ID > | nonGroundRules |
Input nonground rules from the current stratum. | |
std::set< ID > | groundedPredicates |
Predicates from a lower stratum (all derivable atoms are known). | |
std::set< ID > | solvedPredicates |
Completely solved predicates (all ground instances are known to be true or false) (solvedPredicates is a subset of groundedPredicates). |
Implements a grounder without using third-party software.
Definition at line 54 of file InternalGrounder.h.
typedef boost::unordered_map<ID, int> InternalGrounder::Binder [protected] |
Definition at line 70 of file InternalGrounder.h.
typedef boost::shared_ptr<const InternalGrounder> InternalGrounder::ConstPtr |
Reimplemented from GenuineGrounder.
Definition at line 358 of file InternalGrounder.h.
typedef boost::adjacency_list<boost::vecS, boost::vecS, boost::bidirectionalS, ID> InternalGrounder::DepGraph [protected] |
Definition at line 84 of file InternalGrounder.h.
typedef DepGraph::vertex_descriptor InternalGrounder::Node [protected] |
Definition at line 85 of file InternalGrounder.h.
typedef boost::shared_ptr<InternalGrounder> InternalGrounder::Ptr |
Reimplemented from GenuineGrounder.
Definition at line 357 of file InternalGrounder.h.
typedef boost::adjacency_list<boost::vecS, boost::vecS, boost::bidirectionalS, int> InternalGrounder::SCCDepGraph [protected] |
Definition at line 96 of file InternalGrounder.h.
typedef boost::unordered_map<ID, ID> InternalGrounder::Substitution [protected] |
Definition at line 69 of file InternalGrounder.h.
enum InternalGrounder::AppDir [protected] |
Used in method InternalGrounder::applyIntFunction to specify the order of application of a builtin function.
x_op_y_eq_ret |
X*Y=Z means to assign Z to the value of X*Y. |
x_op_ret_eq_y |
X*Z=Y means to assign Z to the value of Y/X. |
ret_op_y_eq_x |
Z*X=Y means to assign Z to the value of X/Y. |
Definition at line 322 of file InternalGrounder.h.
Defines how much the grounder optimizes.
full |
Optimize any atoms when possible. |
builtin |
Optimize only builtin atoms. |
none |
No optimization. |
Definition at line 58 of file InternalGrounder.h.
InternalGrounder::InternalGrounder | ( | ProgramCtx & | ctx, |
const OrdinaryASPProgram & | p, | ||
OptLevel | ol = full |
||
) |
Constructor; will immediately run the grounder!
ctx | ProgramCtx. p Program to ground. |
OptLevel | Specifies how much to optimize. |
Definition at line 1439 of file InternalGrounder.cpp.
References computeDepGraph(), computeGloballyNewAtom(), computeStrata(), ctx, DBGLOG, DLVHEX_BENCHMARK_REGISTER_AND_SCOPE, getGroundProgram(), groundProgram, groundRules, groundStratum(), inputprogram, OrdinaryASPProgram::mask, OrdinaryASPProgram::maxint, predicatesOfStratum, reg, ProgramCtx::registry(), ruleToString(), and trueAtoms.
void InternalGrounder::addDerivableAtom | ( | ID | atom, |
std::vector< ID > & | groundRules, | ||
Set< ID > & | newDerivableAtoms | ||
) | [protected] |
Is called after one or more atoms became derivable.
Triggers the instantiation of depending rules.
atom | Atom to be marked. |
groundRules | Set where new rule instances are to be added. |
newDerivableAtoms | Atoms which recently became derivable. |
Definition at line 945 of file InternalGrounder.cpp.
References Rule::body, DBGLOG, derivableAtomsOfPredicate, Atom::front(), groundRule(), isAtomDerivable(), match(), nonGroundRules, positionsOfPredicate, and reg.
Referenced by groundStratum().
int InternalGrounder::applyIntFunction | ( | AppDir | ad, |
ID | op, | ||
int | x, | ||
int | y | ||
) | [protected] |
Applies a builtin function to two values.
ad | See InternalGrounder:AppDir. |
x | Integer value 1. |
y | Integer value 2. |
Definition at line 1395 of file InternalGrounder.cpp.
References ID::address, ret_op_y_eq_x, ID::TERM_BUILTIN_ADD, ID::TERM_BUILTIN_DIV, ID::TERM_BUILTIN_MOD, ID::TERM_BUILTIN_MUL, ID::TERM_BUILTIN_SUB, x_op_ret_eq_y, and x_op_y_eq_ret.
Referenced by matchNextFromExtensionBuiltinTernary().
ID InternalGrounder::applySubstitutionToAtom | ( | Substitution | s, |
ID | atomID | ||
) | [protected] |
Applies a substitution to an atom.
s | Substitution of variables to terms. |
atomID | Atom to apply s to. |
atomID
after s
was applied. Definition at line 976 of file InternalGrounder.cpp.
References applySubstitutionToBuiltinAtom(), applySubstitutionToOrdinaryAtom(), ID_FAIL(), ID::isBuiltinAtom(), and ID::isOrdinaryAtom().
Referenced by buildGroundInstance(), and groundRule().
ID InternalGrounder::applySubstitutionToBuiltinAtom | ( | Substitution | s, |
ID | atomID | ||
) | [protected] |
Applies a substitution to a bulitin atom.
s | Substitution of variables to terms. |
atomID | Builtin atom to apply s to. |
atomID
after s
was applied. Definition at line 1036 of file InternalGrounder.cpp.
References ID::MAINKIND_ATOM, reg, ID::SUBKIND_ATOM_BUILTIN, and Atom::tuple.
Referenced by applySubstitutionToAtom().
ID InternalGrounder::applySubstitutionToOrdinaryAtom | ( | Substitution | s, |
ID | atomID | ||
) | [protected] |
Applies a substitution to an ordinary atom.
s | Substitution of variables to terms. |
atomID | Ordinary atom to apply s to. |
atomID
after s
was applied. Definition at line 992 of file InternalGrounder.cpp.
References ID::ALL_ONES, IDKind, ID::isOrdinaryGroundAtom(), ID::kind, ID::MAINKIND_ATOM, ID::MAINKIND_MASK, reg, ID::SUBKIND_ATOM_ORDINARYG, ID::SUBKIND_ATOM_ORDINARYN, ID::SUBKIND_MASK, and Atom::tuple.
Referenced by applySubstitutionToAtom().
std::string InternalGrounder::atomToString | ( | ID | atomID | ) | [protected] |
Returns a string representation of an atom.
atomID
. Definition at line 1055 of file InternalGrounder.cpp.
References RawPrinter::print(), and reg.
int InternalGrounder::backtrack | ( | ID | ruleID, |
Binder & | binders, | ||
int | currentIndex | ||
) | [protected] |
Backtracks to the previous substitution where search is to be continued.
Uses the DLV algorithm.
ruleID | Rule whos instances are currently enumerated. |
binders | Stores for each variable the body literal which currently binds it. |
currentIndex | Index of the next body literal to be instantiated. |
Definition at line 925 of file InternalGrounder.cpp.
References Rule::body, and reg.
Referenced by groundRule().
bool InternalGrounder::biDependency | ( | ID | bi1, |
ID | bi2 | ||
) | [protected] |
Checks if two builtin atoms depend on each other.
bi1 | First builtin atom. |
bi2 | Second builtin atom. |
bi1
and bi2
depend on each other. Definition at line 1353 of file InternalGrounder.cpp.
References reg, and Atom::tuple.
Referenced by reorderRuleBody().
void InternalGrounder::buildGroundInstance | ( | ID | ruleID, |
Substitution | s, | ||
std::vector< ID > & | groundedRules, | ||
Set< ID > & | newDerivableAtoms | ||
) | [protected] |
Generates a single ground instance of a rule.
ruleID | Rule to ground (ground or nonground). |
s | Complete set or pairs of variables to be substituted and the values to be inserted. |
groundedRules | Container to receive the instance. |
newDerivableAtoms | Set of atoms to be extended by those which become newly derivable by the new rule instance. |
Definition at line 555 of file InternalGrounder.cpp.
References ID::address, applySubstitutionToAtom(), Rule::body, DBGLOG, Atom::front(), full, globallyNewAtom, Rule::head, ID_FAIL(), IDKind, Set< T >::insert(), isAtomDerivable(), ID::isBuiltinAtom(), ID::isNaf(), ID::isOrdinaryAtom(), isPredicateGrounded(), Rule::level, ID::MAINKIND_LITERAL, ID::MAINKIND_RULE, ID::NAF_MASK, none, optlevel, ID::PROPERTY_RULE_DISJ, reg, ruleToString(), setToTrue(), ID::SUBKIND_ATOM_ORDINARYG, ID::SUBKIND_RULE_CONSTRAINT, ID::SUBKIND_RULE_REGULAR, trueAtoms, and Rule::weight.
Referenced by groundRule().
void InternalGrounder::buildPredicateIndex | ( | ) | [protected] |
Extract for all predicates the rules and atoms where it occurs.
Definition at line 308 of file InternalGrounder.cpp.
References Rule::body, DBGLOG, getPredicateOfAtom(), nonGroundRules, positionsOfPredicate, and reg.
Referenced by loadStratum().
DLVHEX_NAMESPACE_BEGIN void InternalGrounder::computeDepGraph | ( | ) | [protected] |
Construct atom dependency graph.
Definition at line 54 of file InternalGrounder.cpp.
References Rule::body, DBGLOG, depGraph, depNodes, OrdinaryASPProgram::edb, getPredicateOfAtom(), Rule::head, OrdinaryASPProgram::idb, inputprogram, ID::MAINKIND_ATOM, reg, ruleToString(), and ID::SUBKIND_ATOM_ORDINARYG.
Referenced by InternalGrounder().
void InternalGrounder::computeGloballyNewAtom | ( | ) | [protected] |
Constructs a new atom which does not yet occur in the ground program and stored it in globallyNewAtom.
Definition at line 1155 of file InternalGrounder.cpp.
References Rule::body, OrdinaryASPProgram::edb, getPredicateOfAtom(), globallyNewAtom, Rule::head, OrdinaryASPProgram::idb, inputprogram, ID::isConstantTerm(), ID::isPredicateTerm(), ID::MAINKIND_ATOM, ID::MAINKIND_TERM, reg, ID::SUBKIND_ATOM_ORDINARYG, ID::SUBKIND_TERM_CONSTANT, and Atom::tuple.
Referenced by InternalGrounder().
void InternalGrounder::computeStrata | ( | ) | [protected] |
Partitions the program into strata using the atom dependency graph.
Definition at line 231 of file InternalGrounder.cpp.
References compDependencies, DBGLOG, depGraph, depNodes, depSCC, getStratumOfRule(), OrdinaryASPProgram::idb, inputprogram, predicatesOfStratum, preprocessRule(), rulesOfStratum, and stratumOfPredicate.
Referenced by InternalGrounder().
InternalGrounder::Binder InternalGrounder::getBinderOfRule | ( | std::vector< ID > & | body | ) | [protected] |
Retrieves for a given rule body its binder.
body | Rule body. |
Definition at line 1203 of file InternalGrounder.cpp.
Referenced by groundRule().
int InternalGrounder::getClosestBinder | ( | std::vector< ID > & | body, |
int | litIndex, | ||
std::set< ID > | variables | ||
) | [protected] |
Retrieves for a given rule body the literal up to litIndex
which first binds a variable from variables
.
body | Rule body. |
litIndex | Index of a body literal up to which the binder is computed. |
variables | Variables to search for. |
litIndex
) which first binds a variable from variables
, or -1 if no such literal exists. Definition at line 1223 of file InternalGrounder.cpp.
References reg.
Referenced by groundRule().
std::set< ID > InternalGrounder::getFreeVars | ( | std::vector< ID > & | body, |
int | litIndex | ||
) | [protected] |
Returns for a given literal in a rule all variables which are not bounded before that literal.
body | Rule body. |
litIndex | Index of a literal in body . |
litIndex
in body
which are not bounded by previous literals. Definition at line 1246 of file InternalGrounder.cpp.
References reg.
Referenced by groundRule().
const OrdinaryASPProgram & InternalGrounder::getGroundProgram | ( | ) | [virtual] |
Extracts the ground program.
Implements GenuineGrounder.
Definition at line 1521 of file InternalGrounder.cpp.
References groundProgram.
Referenced by InternalGrounder().
std::string InternalGrounder::getGroundProgramString | ( | ) |
Extracts the ground program as string.
Definition at line 1474 of file InternalGrounder.cpp.
References groundRules, ID::MAINKIND_ATOM, ruleToString(), ID::SUBKIND_ATOM_ORDINARYG, and trueAtoms.
Extracts the nonground program.
Definition at line 1528 of file InternalGrounder.cpp.
References inputprogram.
std::string InternalGrounder::getNongroundProgramString | ( | ) |
Extracts the nonground program as string.
Definition at line 1498 of file InternalGrounder.cpp.
References OrdinaryASPProgram::edb, OrdinaryASPProgram::idb, inputprogram, ID::MAINKIND_ATOM, ruleToString(), and ID::SUBKIND_ATOM_ORDINARYG.
std::set< ID > InternalGrounder::getOutputVariables | ( | ID | ruleID | ) | [protected] |
Returns for a given rule the output variables.
This is the set of all variables which occur in literals over unsolved predicates.
ruleID | Rule to check. |
ruleID
. Definition at line 1263 of file InternalGrounder.cpp.
References ID::address, Rule::body, DBGLOG, getPredicateOfAtom(), Rule::head, isPredicateSolved(), and reg.
Referenced by groundRule().
ID InternalGrounder::getPredicateOfAtom | ( | ID | atomID | ) | [protected] |
Extracts the predicate from an atom.
atomID
. Definition at line 1073 of file InternalGrounder.cpp.
References Atom::front(), ID_FAIL(), ID::isAggregateAtom(), ID::isBuiltinAtom(), ID::isOrdinaryAtom(), ID::isOrdinaryGroundAtom(), and reg.
Referenced by buildPredicateIndex(), computeDepGraph(), computeGloballyNewAtom(), getOutputVariables(), isAtomDerivable(), and matchNextFromExtensionOrdinary().
int InternalGrounder::getStratumOfRule | ( | ID | ruleID | ) | [protected] |
Returns the stratum index of a rule.
ruleID | Rule to check. |
ruleID
(0-based). Definition at line 1126 of file InternalGrounder.cpp.
References Rule::body, DBGLOG, Atom::front(), Rule::head, ID::isOrdinaryAtom(), ID::isOrdinaryGroundAtom(), reg, ruleToString(), and stratumOfPredicate.
Referenced by computeStrata().
void InternalGrounder::groundRule | ( | ID | ruleID, |
Substitution & | s, | ||
std::vector< ID > & | groundedRules, | ||
Set< ID > & | newDerivableAtoms | ||
) | [protected] |
Generates all ground instances of a rule.
ruleID | Rule to ground (ground or nonground). |
s | Set or pairs of variables to be substituted and the values to be inserted; can be incomplete. |
groundedRules | Container to receive the instance. |
newDerivableAtoms | Set of atoms to be extended by those which become newly derivable by the new rule instance. |
Definition at line 409 of file InternalGrounder.cpp.
References applySubstitutionToAtom(), backtrack(), buildGroundInstance(), DBGLOG, getBinderOfRule(), getClosestBinder(), getFreeVars(), getOutputVariables(), ID::isNaf(), matchNextFromExtension(), reg, reorderRuleBody(), and ruleToString().
Referenced by addDerivableAtom(), and groundStratum().
void InternalGrounder::groundStratum | ( | int | index | ) | [protected] |
Grounds a specific stratum.
index | Stratum to ground. |
Definition at line 338 of file InternalGrounder.cpp.
References addDerivableAtom(), ID::address, DBGLOG, derivableAtomsOfPredicate, OrdinaryASPProgram::edb, groundedPredicates, groundRule(), groundRules, inputprogram, loadStratum(), ID::MAINKIND_ATOM, nonGroundRules, predicatesOfStratum, setToTrue(), Set< T >::size(), solvedPredicates, ID::SUBKIND_ATOM_ORDINARYG, and trueAtoms.
Referenced by InternalGrounder().
bool InternalGrounder::isAtomDerivable | ( | ID | atom | ) | [protected] |
Checks if an atom is derivable (in principle, i.e., some rule derives it).
atom | ID of the atom to check. |
atom
is derivable and false otherwise. Definition at line 1115 of file InternalGrounder.cpp.
References ID::address, derivableAtomsOfPredicate, and getPredicateOfAtom().
Referenced by addDerivableAtom(), buildGroundInstance(), and matchNextFromExtensionOrdinary().
bool InternalGrounder::isGroundRule | ( | ID | ruleID | ) | [protected] |
Checks if a rule id ground.
ruleID | Rule to check. |
ruleID
is ground and false otherwise. Definition at line 1090 of file InternalGrounder.cpp.
References Rule::body, ID::isOrdinaryGroundAtom(), and reg.
bool InternalGrounder::isPredicateGrounded | ( | ID | pred | ) | [protected] |
Checks if a predicate is fully grounded, i.e., it comes from a lower stratum.
pred
is fully grounded. Definition at line 1101 of file InternalGrounder.cpp.
References groundedPredicates.
Referenced by buildGroundInstance().
bool InternalGrounder::isPredicateSolved | ( | ID | pred | ) | [protected] |
Checks if a predicate is fully solved.
Completely solved predicates are those such that all ground instances are known to be true or false. SolvedPredicates is a subset of groundedPredicates.
pred | Predicate to check. |
pred
is fully solved. Definition at line 1108 of file InternalGrounder.cpp.
References solvedPredicates.
Referenced by getOutputVariables(), and matchNextFromExtensionOrdinary().
void InternalGrounder::loadStratum | ( | int | index | ) | [protected] |
Load stratum into groundRules and nonGroundRules.
index | Stratum to load. |
Definition at line 328 of file InternalGrounder.cpp.
References buildPredicateIndex(), DBGLOG, nonGroundRules, and rulesOfStratum.
Referenced by groundStratum().
bool InternalGrounder::match | ( | ID | literalID, |
ID | patternLiteral, | ||
Substitution & | s | ||
) | [protected] |
Checks if a literal matches a given pattern using a substitution.
literalID | Literal to check. |
patternLiteral | Literal to check against. |
s | Set or pairs of variables to be substituted and the values to be inserted; can be incomplete. |
literalID
after application of s
unifies with patternLiteral
, and false otherwise. Definition at line 651 of file InternalGrounder.cpp.
References ID::isBuiltinAtom(), ID::isNaf(), ID::isOrdinaryAtom(), matchBuiltin(), and matchOrdinary().
Referenced by addDerivableAtom(), and matchNextFromExtensionOrdinary().
bool InternalGrounder::matchBuiltin | ( | ID | literalID, |
ID | patternAtom, | ||
Substitution & | s | ||
) | [protected] |
Checks if a builtin literal matches a given pattern using a substitution.
literalID | Builtin literal to check. |
patternLiteral | Builtin literal to check against. |
s | Set or pairs of variables to be substituted and the values to be inserted; can be incomplete. |
literalID
after application of s
unifies with patternLiteral
, and false otherwise. Definition at line 689 of file InternalGrounder.cpp.
References ID::isNaf(), reg, and Atom::tuple.
Referenced by match().
int InternalGrounder::matchNextFromExtension | ( | ID | literalID, |
Substitution & | s, | ||
int | startSearchIndex | ||
) | [protected] |
Computes the index of the next derivable atom which matches against the given literal using a given substitution.
literalID | Literal to check. |
s | Set or pairs of variables to be substituted and the values to be inserted; can be incomplete. |
startSearchIndex | Index to start search; start from 0 and pass the index previously returned by this method to iterate. |
literalID
using substitution s
. Definition at line 715 of file InternalGrounder.cpp.
References ID::isBuiltinAtom(), ID::isOrdinaryAtom(), matchNextFromExtensionBuiltin(), and matchNextFromExtensionOrdinary().
Referenced by groundRule().
int InternalGrounder::matchNextFromExtensionBuiltin | ( | ID | literalID, |
Substitution & | s, | ||
int | startSearchIndex | ||
) | [protected] |
Computes the index of the next derivable builtin atom which matches against the given literal using a given substitution.
literalID | Builtin literal to check. |
s | Set or pairs of variables to be substituted and the values to be inserted; can be incomplete. |
startSearchIndex | Index to start search; start from 0 and pass the index previously returned by this method to iterate. |
literalID
using substitution s
. Definition at line 778 of file InternalGrounder.cpp.
References DBGLOG, ID::isNaf(), matchNextFromExtensionBuiltinBinary(), matchNextFromExtensionBuiltinTernary(), matchNextFromExtensionBuiltinUnary(), reg, ID::TERM_BUILTIN_ADD, ID::TERM_BUILTIN_DIV, ID::TERM_BUILTIN_EQ, ID::TERM_BUILTIN_GE, ID::TERM_BUILTIN_GT, ID::TERM_BUILTIN_INT, ID::TERM_BUILTIN_LE, ID::TERM_BUILTIN_LT, ID::TERM_BUILTIN_MOD, ID::TERM_BUILTIN_MUL, ID::TERM_BUILTIN_NE, ID::TERM_BUILTIN_SUB, ID::TERM_BUILTIN_SUCC, and Atom::tuple.
Referenced by matchNextFromExtension().
int InternalGrounder::matchNextFromExtensionBuiltinBinary | ( | ID | literalID, |
Substitution & | s, | ||
int | startSearchIndex | ||
) | [protected] |
Computes the index of the next derivable binary builtin atom which matches against the given literal using a given substitution.
literalID | Binary builtin literal to check. |
s | Set or pairs of variables to be substituted and the values to be inserted; can be incomplete. |
startSearchIndex | Index to start search; start from 0 and pass the index previously returned by this method to iterate. |
literalID
using substitution s
. Definition at line 843 of file InternalGrounder.cpp.
References reg, ID::TERM_BUILTIN_EQ, ID::TERM_BUILTIN_GE, ID::TERM_BUILTIN_GT, ID::TERM_BUILTIN_LE, ID::TERM_BUILTIN_LT, ID::TERM_BUILTIN_NE, ID::TERM_BUILTIN_SUCC, ID::termFromInteger(), and Atom::tuple.
Referenced by matchNextFromExtensionBuiltin().
int InternalGrounder::matchNextFromExtensionBuiltinTernary | ( | ID | literalID, |
Substitution & | s, | ||
int | startSearchIndex | ||
) | [protected] |
Computes the index of the next derivable ternary builtin atom which matches against the given literal using a given substitution.
literalID | Ternary builtin literal to check. |
s | Set or pairs of variables to be substituted and the values to be inserted; can be incomplete. |
startSearchIndex | Index to start search; start from 0 and pass the index previously returned by this method to iterate. |
literalID
using substitution s
. Definition at line 887 of file InternalGrounder.cpp.
References applyIntFunction(), ctx, ProgramCtx::maxint, reg, ID::termFromInteger(), Atom::tuple, and x_op_y_eq_ret.
Referenced by matchNextFromExtensionBuiltin().
int InternalGrounder::matchNextFromExtensionBuiltinUnary | ( | ID | literalID, |
Substitution & | s, | ||
int | startSearchIndex | ||
) | [protected] |
Computes the index of the next derivable unary builtin atom which matches against the given literal using a given substitution.
literalID | Unary builtin literal to check. |
s | Set or pairs of variables to be substituted and the values to be inserted; can be incomplete. |
startSearchIndex | Index to start search; start from 0 and pass the index previously returned by this method to iterate. |
literalID
using substitution s
. Definition at line 812 of file InternalGrounder.cpp.
References ctx, ProgramCtx::maxint, reg, ID::TERM_BUILTIN_INT, ID::termFromInteger(), and Atom::tuple.
Referenced by matchNextFromExtensionBuiltin().
int InternalGrounder::matchNextFromExtensionOrdinary | ( | ID | literalID, |
Substitution & | s, | ||
int | startSearchIndex | ||
) | [protected] |
Computes the index of the next derivable ordinary atom which matches against the given literal using a given substitution.
literalID | Ordinary literal to check. |
s | Set or pairs of variables to be substituted and the values to be inserted; can be incomplete. |
startSearchIndex | Index to start search; start from 0 and pass the index previously returned by this method to iterate. |
literalID
using substitution s
. Definition at line 732 of file InternalGrounder.cpp.
References ID::address, ID::ALL_ONES, DBGLOG, derivableAtomsOfPredicate, Atom::front(), getPredicateOfAtom(), isAtomDerivable(), ID::isNaf(), ID::isOrdinaryGroundAtom(), ID::isOrdinaryNongroundAtom(), isPredicateSolved(), ID::kind, ID::MAINKIND_ATOM, ID::MAINKIND_MASK, match(), ID::NAF_MASK, and reg.
Referenced by matchNextFromExtension().
bool InternalGrounder::matchOrdinary | ( | ID | literalID, |
ID | patternAtom, | ||
Substitution & | s | ||
) | [protected] |
Checks if an ordinary literal matches a given pattern using a substitution.
literalID | Ordinary literal to check. |
patternLiteral | Ordinary literal to check against. |
s | Set or pairs of variables to be substituted and the values to be inserted; can be incomplete. |
literalID
after application of s
unifies with patternLiteral
, and false otherwise. Definition at line 671 of file InternalGrounder.cpp.
References ID::isOrdinaryGroundAtom(), reg, Atom::tuple, and OrdinaryAtom::unifiesWith().
Referenced by match().
ID InternalGrounder::preprocessRule | ( | ID | ruleID | ) | [protected] |
Check if rule can be handled and insert variable names for anonymous variables.
ruleID | Rule to preprocess. |
Definition at line 110 of file InternalGrounder.cpp.
References Rule::body, DBGLOG, ID::hasRuleHeadGuard(), Rule::head, ExternalAtom::inputs, ID::isAnonymousVariable(), ID::isBuiltinAtom(), ID::isExternalAtom(), ID::isNaf(), ID::isOrdinaryAtom(), ID::literalFromAtom(), reg, and Atom::tuple.
Referenced by computeStrata().
std::vector< ID > InternalGrounder::reorderRuleBody | ( | ID | ruleID | ) | [protected] |
Reorders a rule (mainly for optimization purposes).
Will place positive atoms first and ordinary atoms before builtin atoms.
ruleID | Rule to reorder. |
Definition at line 1293 of file InternalGrounder.cpp.
References ID::address, biDependency(), Rule::body, DBGLOG, ID::isBuiltinAtom(), ID::isNaf(), and reg.
Referenced by groundRule().
std::string InternalGrounder::ruleToString | ( | ID | ruleID | ) | [protected] |
Returns a string representation of a rule.
ruleID
. Definition at line 1064 of file InternalGrounder.cpp.
References RawPrinter::print(), and reg.
Referenced by buildGroundInstance(), computeDepGraph(), getGroundProgramString(), getNongroundProgramString(), getStratumOfRule(), groundRule(), and InternalGrounder().
void InternalGrounder::setToTrue | ( | ID | atom | ) | [protected] |
Makes atom
permanently true (EDB fact).
Definition at line 937 of file InternalGrounder.cpp.
References ID::address, DBGLOG, and trueAtoms.
Referenced by buildGroundInstance(), and groundStratum().
SCCDepGraph InternalGrounder::compDependencies [protected] |
Dependencies between program components (=program strata).
Definition at line 98 of file InternalGrounder.h.
Referenced by computeStrata().
ProgramCtx& InternalGrounder::ctx [protected] |
Definition at line 77 of file InternalGrounder.h.
Referenced by InternalGrounder(), matchNextFromExtensionBuiltinTernary(), and matchNextFromExtensionBuiltinUnary().
DepGraph InternalGrounder::depGraph [protected] |
Atom dependency graph.
Definition at line 89 of file InternalGrounder.h.
Referenced by computeDepGraph(), and computeStrata().
boost::unordered_map<ID, Node> InternalGrounder::depNodes [protected] |
Nodes of depSCC.
Definition at line 87 of file InternalGrounder.h.
Referenced by computeDepGraph(), and computeStrata().
std::vector<Set<ID> > InternalGrounder::depSCC [protected] |
Strongly connected components of depSCC.
Store for each component the contained predicates.
Definition at line 93 of file InternalGrounder.h.
Referenced by computeStrata().
boost::unordered_map<ID, std::vector<ID> > InternalGrounder::derivableAtomsOfPredicate [protected] |
Stores for each predicate (=term) the set of ground atoms over this predicate which are currently derivable.
Definition at line 109 of file InternalGrounder.h.
Referenced by addDerivableAtom(), groundStratum(), isAtomDerivable(), and matchNextFromExtensionOrdinary().
ID InternalGrounder::globallyNewAtom [protected] |
An atom which does not occur in the program.
Definition at line 107 of file InternalGrounder.h.
Referenced by buildGroundInstance(), and computeGloballyNewAtom().
std::set<ID> InternalGrounder::groundedPredicates [protected] |
Predicates from a lower stratum (all derivable atoms are known).
Definition at line 122 of file InternalGrounder.h.
Referenced by groundStratum(), and isPredicateGrounded().
OrdinaryASPProgram InternalGrounder::groundProgram [protected] |
Ground output program after the grounder has finished.
Definition at line 75 of file InternalGrounder.h.
Referenced by getGroundProgram(), and InternalGrounder().
std::vector<ID> InternalGrounder::groundRules [protected] |
Generated ground rules in the current stratum.
Definition at line 117 of file InternalGrounder.h.
Referenced by getGroundProgramString(), groundStratum(), and InternalGrounder().
OrdinaryASPProgram InternalGrounder::inputprogram [protected] |
Nonground input program.
Definition at line 73 of file InternalGrounder.h.
Referenced by computeDepGraph(), computeGloballyNewAtom(), computeStrata(), getNongroundProgram(), getNongroundProgramString(), groundStratum(), and InternalGrounder().
std::vector<ID> InternalGrounder::nonGroundRules [protected] |
Input nonground rules from the current stratum.
Definition at line 119 of file InternalGrounder.h.
Referenced by addDerivableAtom(), buildPredicateIndex(), groundStratum(), and loadStratum().
OptLevel InternalGrounder::optlevel [protected] |
Level of optimization used.
Definition at line 81 of file InternalGrounder.h.
Referenced by buildGroundInstance().
boost::unordered_map<ID, std::set<std::pair<int, int> > > InternalGrounder::positionsOfPredicate [protected] |
Stores for each predicate the set of non-ground rules and body positions where the predicate occurs.
Definition at line 111 of file InternalGrounder.h.
Referenced by addDerivableAtom(), and buildPredicateIndex().
std::vector<std::set<ID> > InternalGrounder::predicatesOfStratum [protected] |
Stores for each stratum the contained predicates.
Definition at line 100 of file InternalGrounder.h.
Referenced by computeStrata(), groundStratum(), and InternalGrounder().
RegistryPtr InternalGrounder::reg [protected] |
Definition at line 79 of file InternalGrounder.h.
Referenced by addDerivableAtom(), applySubstitutionToBuiltinAtom(), applySubstitutionToOrdinaryAtom(), atomToString(), backtrack(), biDependency(), buildGroundInstance(), buildPredicateIndex(), computeDepGraph(), computeGloballyNewAtom(), getBinderOfRule(), getClosestBinder(), getFreeVars(), getOutputVariables(), getPredicateOfAtom(), getStratumOfRule(), groundRule(), InternalGrounder(), isGroundRule(), matchBuiltin(), matchNextFromExtensionBuiltin(), matchNextFromExtensionBuiltinBinary(), matchNextFromExtensionBuiltinTernary(), matchNextFromExtensionBuiltinUnary(), matchNextFromExtensionOrdinary(), matchOrdinary(), preprocessRule(), reorderRuleBody(), and ruleToString().
std::vector<std::set<ID> > InternalGrounder::rulesOfStratum [protected] |
Stores for each stratum the contained rules.
Definition at line 102 of file InternalGrounder.h.
Referenced by computeStrata(), and loadStratum().
std::set<ID> InternalGrounder::solvedPredicates [protected] |
Completely solved predicates (all ground instances are known to be true or false) (solvedPredicates is a subset of groundedPredicates).
Definition at line 125 of file InternalGrounder.h.
Referenced by groundStratum(), and isPredicateSolved().
boost::unordered_map<ID, int> InternalGrounder::stratumOfPredicate [protected] |
Stores for each predicate its stratum index.
Definition at line 104 of file InternalGrounder.h.
Referenced by computeStrata(), and getStratumOfRule().
InterpretationPtr InternalGrounder::trueAtoms [protected] |
Atoms which are definitely true (=EDB).
Definition at line 114 of file InternalGrounder.h.
Referenced by buildGroundInstance(), getGroundProgramString(), groundStratum(), InternalGrounder(), and setToTrue().