dlvhex  2.1.0
DLVHEX_NAMESPACE_BEGIN Namespace Reference

for one eval unit, we transform the rules (idb) independent of input interpretations as follows: * replace all external atoms with eatom replacements More...

Data Structures

struct  ExternalSolverHelper
struct  ExternalSolverHelper< GenuineSolver >
class  ASMOrdinaryASPSolver
struct  AuxiliaryKey
struct  AuxiliaryValue

Typedefs

typedef std::set< ComfortAtomIntBase
typedef boost::shared_ptr
< ASMOrdinaryASPSolver
ASMOrdinaryASPSolverPtr
typedef boost::bimaps::bimap
< AuxiliaryKey, AuxiliaryValue
AuxiliaryStorage
typedef
AuxiliaryStorage::value_type 
AuxiliaryStorageTranslation

Functions

std::size_t hash_value (const AuxiliaryKey &key)

Detailed Description

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 Documentation

Definition at line 121 of file Registry.cpp.

typedef AuxiliaryStorage::value_type DLVHEX_NAMESPACE_BEGIN::AuxiliaryStorageTranslation

Definition at line 122 of file Registry.cpp.

Definition at line 49 of file ComfortPluginInterface.cpp.


Function Documentation