for one eval unit, we transform the rules (idb) independent of input interpretations as follows: * replace all external atoms with eatom replacements More...
|struct||ExternalSolverHelper< GenuineSolver >|
|typedef std::set< ComfortAtom >||IntBase|
< ASMOrdinaryASPSolver >
< AuxiliaryKey, AuxiliaryValue >
|std::size_t||hash_value (const AuxiliaryKey &key)|
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 auto strong safety 'g': aggregate input (internal AggregatePlugin) 'w': used for rewritten weak constraints (internal WeakConstraintPlugin) 'x': reserved for local use
|typedef AuxiliaryStorage::value_type DLVHEX_NAMESPACE_BEGIN::AuxiliaryStorageTranslation|