dlvhex  2.5.0
InternalGrounder Class Reference

Implements a grounder without using third-party software. More...

#include <include/dlvhex2/InternalGrounder.h>

Inheritance diagram for InternalGrounder:
Collaboration diagram for InternalGrounder:

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 OrdinaryASPProgramgetGroundProgram ()
 Extracts the ground program.
const OrdinaryASPProgramgetNongroundProgram ()
 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< IDgetFreeVars (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< IDgetOutputVariables (ID ruleID)
 Returns for a given rule the output variables.
std::vector< IDreorderRuleBody (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.
ProgramCtxctx
 ProgramCtx.
RegistryPtr reg
 Registry.
OptLevel optlevel
 Level of optimization used.
boost::unordered_map< ID, NodedepNodes
 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< IDgroundRules
 Generated ground rules in the current stratum.
std::vector< IDnonGroundRules
 Input nonground rules from the current stratum.
std::set< IDgroundedPredicates
 Predicates from a lower stratum (all derivable atoms are known).
std::set< IDsolvedPredicates
 Completely solved predicates (all ground instances are known to be true or false) (solvedPredicates is a subset of groundedPredicates).

Detailed Description

Implements a grounder without using third-party software.

Definition at line 54 of file InternalGrounder.h.


Member Typedef Documentation

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.


Member Enumeration Documentation

enum InternalGrounder::AppDir [protected]

Used in method InternalGrounder::applyIntFunction to specify the order of application of a builtin function.

Enumerator:
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.

Enumerator:
full 

Optimize any atoms when possible.

builtin 

Optimize only builtin atoms.

none 

No optimization.

Definition at line 58 of file InternalGrounder.h.


Constructor & Destructor Documentation


Member Function Documentation

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.

Parameters:
atomAtom to be marked.
groundRulesSet where new rule instances are to be added.
newDerivableAtomsAtoms 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.

Parameters:
adSee InternalGrounder:AppDir.
xInteger value 1.
yInteger value 2.
Returns:
Result according to InternalGrounder:AppDir.

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().

Applies a substitution to an atom.

Parameters:
sSubstitution of variables to terms.
atomIDAtom to apply s to.
Returns:
ID of atom 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().

Applies a substitution to a bulitin atom.

Parameters:
sSubstitution of variables to terms.
atomIDBuiltin atom to apply s to.
Returns:
ID of atom 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().

Applies a substitution to an ordinary atom.

Parameters:
sSubstitution of variables to terms.
atomIDOrdinary atom to apply s to.
Returns:
ID of atom 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.

Parameters:
atomIDAtom ID.
Returns:
String representation of 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.

Parameters:
ruleIDRule whos instances are currently enumerated.
bindersStores for each variable the body literal which currently binds it.
currentIndexIndex of the next body literal to be instantiated.
Returns:
Index of the body literal to backtrack to.

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.

Parameters:
bi1First builtin atom.
bi2Second builtin atom.
Returns:
True if 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.

Parameters:
ruleIDRule to ground (ground or nonground).
sComplete set or pairs of variables to be substituted and the values to be inserted.
groundedRulesContainer to receive the instance.
newDerivableAtomsSet 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().

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().

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.

Parameters:
bodyRule body.
Returns:
Binder, i.e., for each variable the index of a body literal which binds it.

Definition at line 1203 of file InternalGrounder.cpp.

References DBGLOG, and reg.

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.

Parameters:
bodyRule body.
litIndexIndex of a body literal up to which the binder is computed.
variablesVariables to search for.
Returns:
Index of the literal (before literal 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.

Parameters:
bodyRule body.
litIndexIndex of a literal in body.
Returns:
Set of all variables in literal litIndex in body which are not bounded by previous literals.

Definition at line 1246 of file InternalGrounder.cpp.

References reg.

Referenced by groundRule().

Extracts the ground program.

Returns:
Ground program.

Implements GenuineGrounder.

Definition at line 1521 of file InternalGrounder.cpp.

References groundProgram.

Referenced by InternalGrounder().

Extracts the ground program as string.

Returns:
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.

Returns:
Nonground program.

Definition at line 1528 of file InternalGrounder.cpp.

References inputprogram.

Extracts the nonground program as string.

Returns:
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.

Parameters:
ruleIDRule to check.
Returns:
Set of output variables in ruleID.

Definition at line 1263 of file InternalGrounder.cpp.

References ID::address, Rule::body, DBGLOG, getPredicateOfAtom(), Rule::head, isPredicateSolved(), and reg.

Referenced by groundRule().

int InternalGrounder::getStratumOfRule ( ID  ruleID) [protected]

Returns the stratum index of a rule.

Parameters:
ruleIDRule to check.
Returns:
Stratum of 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.

Parameters:
ruleIDRule to ground (ground or nonground).
sSet or pairs of variables to be substituted and the values to be inserted; can be incomplete.
groundedRulesContainer to receive the instance.
newDerivableAtomsSet 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().

bool InternalGrounder::isAtomDerivable ( ID  atom) [protected]

Checks if an atom is derivable (in principle, i.e., some rule derives it).

Parameters:
atomID of the atom to check.
Returns:
True if 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.

Parameters:
ruleIDRule to check.
Returns:
True if 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.

Parameters:
predPredicate ID.
Returns:
True if 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.

Parameters:
predPredicate to check.
Returns:
True if 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.

Parameters:
indexStratum 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.

Parameters:
literalIDLiteral to check.
patternLiteralLiteral to check against.
sSet or pairs of variables to be substituted and the values to be inserted; can be incomplete.
Returns:
True if 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.

Parameters:
literalIDBuiltin literal to check.
patternLiteralBuiltin literal to check against.
sSet or pairs of variables to be substituted and the values to be inserted; can be incomplete.
Returns:
True if 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.

Parameters:
literalIDLiteral to check.
sSet or pairs of variables to be substituted and the values to be inserted; can be incomplete.
startSearchIndexIndex to start search; start from 0 and pass the index previously returned by this method to iterate.
Returns:
Index of the next derivable atom which matches against 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.

Parameters:
literalIDBuiltin literal to check.
sSet or pairs of variables to be substituted and the values to be inserted; can be incomplete.
startSearchIndexIndex to start search; start from 0 and pass the index previously returned by this method to iterate.
Returns:
Index of the next derivable builtin atom which matches against 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.

Parameters:
literalIDBinary builtin literal to check.
sSet or pairs of variables to be substituted and the values to be inserted; can be incomplete.
startSearchIndexIndex to start search; start from 0 and pass the index previously returned by this method to iterate.
Returns:
Index of the next derivable binary builtin atom which matches against 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.

Parameters:
literalIDTernary builtin literal to check.
sSet or pairs of variables to be substituted and the values to be inserted; can be incomplete.
startSearchIndexIndex to start search; start from 0 and pass the index previously returned by this method to iterate.
Returns:
Index of the next derivable ternary builtin atom which matches against 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.

Parameters:
literalIDUnary builtin literal to check.
sSet or pairs of variables to be substituted and the values to be inserted; can be incomplete.
startSearchIndexIndex to start search; start from 0 and pass the index previously returned by this method to iterate.
Returns:
Index of the next derivable unary builtin atom which matches against 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.

Parameters:
literalIDOrdinary literal to check.
sSet or pairs of variables to be substituted and the values to be inserted; can be incomplete.
startSearchIndexIndex to start search; start from 0 and pass the index previously returned by this method to iterate.
Returns:
Index of the next derivable ordinary atom which matches against 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.

Parameters:
literalIDOrdinary literal to check.
patternLiteralOrdinary literal to check against.
sSet or pairs of variables to be substituted and the values to be inserted; can be incomplete.
Returns:
True if 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.

Parameters:
ruleIDRule 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.

Parameters:
ruleIDRule to reorder.
Returns:
Reordered rule body.

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.

Parameters:
ruleIDRule ID.
Returns:
String representation of 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).

Parameters:
atomAtom ID.

Definition at line 937 of file InternalGrounder.cpp.

References ID::address, DBGLOG, and trueAtoms.

Referenced by buildGroundInstance(), and groundStratum().


Field Documentation

Dependencies between program components (=program strata).

Definition at line 98 of file InternalGrounder.h.

Referenced by computeStrata().

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().

An atom which does not occur in the program.

Definition at line 107 of file InternalGrounder.h.

Referenced by buildGroundInstance(), and computeGloballyNewAtom().

Predicates from a lower stratum (all derivable atoms are known).

Definition at line 122 of file InternalGrounder.h.

Referenced by groundStratum(), and isPredicateGrounded().

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().

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().

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().

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().

Atoms which are definitely true (=EDB).

Definition at line 114 of file InternalGrounder.h.

Referenced by buildGroundInstance(), getGroundProgramString(), groundStratum(), InternalGrounder(), and setToTrue().


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