dlvhex
2.5.0
|
for one eval unit, we transform the rules (idb) independent of input interpretations as follows: * replace all external atoms with eatom replacements More...
for one eval unit, we transform the rules (idb) independent of input interpretations as follows: * replace all external atoms with eatom replacements
auxiliary constant symbol type usage: 'i': auxiliary input grounding predicates for external atoms in rules (source ID is an eatom) 'r': replacement predicates for external atoms (source ID is a constant term) 'n': negated replacement predicates for external atoms (for guessing rules) (source ID is a constant term) 'f': FLP-calculation auxiliary predicate (source ID is a rule) 'q': Query evaluation auxiliary (QueryPlugin) (source ID is ID(0,0) or ID(0,1) ...
-> "xidb" (like in other model generators) * create for each inner eatom a guessing rule for grounding and guessing eatoms -> "gidb" * create for each rule in xidb a rule with same body and individual flp auxiliary head containing all variables in the rule (constraints can stay untouched) -> "xidbflphead" * create for each rule in xidb a rule with body extended by respective flp auxiliary predicate containing all variables -> "xidbflpbody"
evaluation works as follows: * evaluate outer eatoms -> yields eedb replacements in interpretation * evaluate edb + eedb + xidb + gidb -> yields guesses M_1,...,M_n * check for each guess M * whether eatoms have been guessed correctly (remove others) * whether M is model of FLP reduct of xidb wrt edb, eedb and M this check is achieved by doing the following * evaluate edb + eedb + xidbflphead + M -> yields singleton answer set containing flp heads F for non-blocked rules (if there is no result answer set, some constraint fired and M can be discarded) * evaluate edb + eedb + xidbflpbody + (M guess_auxiliaries) + F -> yields singleton answer set M' (there must be an answer set, or something went wrong) * if (M' F) == M then M is a model of the FLP reduct -> store as candidate * drop non-subset-minimal candidates * return remaining candidates as minimal models (this means, that for one input, all models have to be calculated before the first one can be returned due to the minimality check)
see QueryPlugin.cpp) 's': Strong negation auxiliary (StrongNegationPlugin) (source ID is a constant term) 'h': Higher order auxiliary (HigherOrderPlugin) (source ID is an integer (arity)) 'a': Action auxiliary (ActionPlugin) (source ID is the ID of the name of the action) 'd': domain predicates for liberal safety 'g': aggregate input (internal AggregatePlugin) 'c': choice rules (internal ChoicePlugin) 'w': used for rewritten weak constraints (internal WeakConstraintPlugin) '0': null terms (used for existential quantification, see ExistsPlugin.cpp) 'F': explicit representation of false atoms (used for external source inlining) 'o': special atoms introduced by gringo (IDs of kind integer) and predicate for guard atoms (ID(0, 0)) 'x': reserved for local use
typedef boost::shared_ptr<ASMOrdinaryASPSolver> DLVHEX_NAMESPACE_BEGIN::ASMOrdinaryASPSolverPtr |
Definition at line 98 of file GuessAndCheckModelGenerator.cpp.
typedef boost::bimaps::bimap<AuxiliaryKey, AuxiliaryValue> DLVHEX_NAMESPACE_BEGIN::AuxiliaryStorage |
Definition at line 128 of file Registry.cpp.
typedef AuxiliaryStorage::value_type DLVHEX_NAMESPACE_BEGIN::AuxiliaryStorageTranslation |
Definition at line 129 of file Registry.cpp.
Definition at line 63 of file ManualEvalHeuristicsPlugin.cpp.
Definition at line 67 of file ManualEvalHeuristicsPlugin.cpp.
Definition at line 66 of file ComponentGraph.cpp.
Definition at line 66 of file ManualEvalHeuristicsPlugin.cpp.
Definition at line 65 of file ComponentGraph.cpp.
Definition at line 67 of file ComponentGraph.cpp.
Definition at line 68 of file ComponentGraph.cpp.
typedef ManualEvalHeuristicsPlugin::CtxData::InstructionList DLVHEX_NAMESPACE_BEGIN::InstructionList |
Definition at line 68 of file ManualEvalHeuristicsPlugin.cpp.
typedef std::set<ComfortAtom> DLVHEX_NAMESPACE_BEGIN::IntBase |
Definition at line 52 of file ComfortPluginInterface.cpp.
Definition at line 61 of file ComponentGraph.cpp.
typedef std::set<Node> DLVHEX_NAMESPACE_BEGIN::NodeSet |
Definition at line 62 of file ComponentGraph.cpp.
typedef std::vector<Node> DLVHEX_NAMESPACE_BEGIN::NodeVector |
Definition at line 63 of file ComponentGraph.cpp.
typedef std::map<Component, unsigned > DLVHEX_NAMESPACE_BEGIN::UnitBackMap |
Definition at line 70 of file ManualEvalHeuristicsPlugin.cpp.
typedef std::map<unsigned, std::list<Component> > DLVHEX_NAMESPACE_BEGIN::UnitMap |
Definition at line 69 of file ManualEvalHeuristicsPlugin.cpp.
std::size_t DLVHEX_NAMESPACE_BEGIN::hash_value | ( | const AuxiliaryKey & | key | ) |
Definition at line 104 of file Registry.cpp.
References ID::address, DLVHEX_NAMESPACE_BEGIN::AuxiliaryKey::id, ID::kind, and DLVHEX_NAMESPACE_BEGIN::AuxiliaryKey::type.