SemOpt
$Revision:72+[d9d7a33b5c20+]$
|
Functions computing the preferred extensions of an AF
according to the algorithm described in TAFA-13.
More...
#include "semopt.h"
Go to the source code of this file.
Functions | |
int | PiGreek (SATFormulae *sat, AF *af, int encoding) |
Function computing the labelling constraints encoding in a SATFormulae given an AF and the type of encoding desired. | |
void | aSolution (vector< int > *res, dArray *vals, AF *af) |
Given a solution returned by a SAT Solver, and given a dArray of the same size of the number of arguments af , if the argument whose number is num is labelled IN , then it writes 1 in the position num of the given dArray , 0 otherwise. | |
void | INARGS (vector< int > *assign, vector< Argument * > *toarg, vector< Argument * > *closeworld, AF *af) |
Given a solution returned by a SAT Solver, it fills in two vector of Argument where the first contains the pointers to the Argument that are labelled IN in the solution, and the second containing all the other Argument . | |
int | PrefSat (dMatrix *preferred_extensions, AF *af, int encoding, int(*SatSolver)(stringstream *, int, int, vector< int > *)) |
This is the function that in TAFA-13 is described by Algorithm 1. |
Functions computing the preferred extensions of an AF
according to the algorithm described in TAFA-13.
Definition in file prefSAT.cpp.
Given a solution returned by a SAT Solver, and given a dArray
of the same size of the number of arguments af
, if the argument whose number is num
is labelled IN
, then it writes 1
in the position num
of the given dArray
, 0
otherwise.
[in] | res | A pointer to a vector<int> which represents the results of the SAT Solver |
[out] | vals | A pointer to a dArray whose size is equals to the number of Argument |
[in] | af | A pointer to the AF considered in this case |
void |
res
Definition at line 204 of file prefSAT.cpp.
References AF::getArgumentByNumber(), and Argument::InVar().
Referenced by PrefSat().
void INARGS | ( | vector< int > * | assign, |
vector< Argument * > * | toarg, | ||
vector< Argument * > * | closeworld, | ||
AF * | af | ||
) |
Given a solution returned by a SAT Solver, it fills in two vector
of Argument
where the first contains the pointers to the Argument
that are labelled IN
in the solution, and the second containing all the other Argument
.
[in] | assign | A pointer to a vector<int> which represents the results of the SAT Solver |
[out] | toarg | A pointer to a vector<Argument *> which represents (in the TAFA-13 terminology) the set of arguments ![]() |
[out] | closeworld | A pointer to a vector<Argument *> which represents (in the TAFA-13 terminology) the set of arguments ![]() |
[in] | af | A pointer to the AF considered in this case |
void |
assign
Definition at line 230 of file prefSAT.cpp.
References AF::getArgumentByNumber(), and AF::numArgs().
Referenced by PrefSat().
int PiGreek | ( | SATFormulae * | sat, |
AF * | af, | ||
int | encoding | ||
) |
Function computing the labelling constraints encoding in a SATFormulae
given an AF
and the type of encoding desired.
[out] | sat | A pointer to an initialised SATFormulae object which will contains the SAT formuale of the given AF | ||||||||||||||
[in] | af | The pointer to the object instance of AF which represents the argumentation framework from which we want to derive the labellings contraints | ||||||||||||||
[in] | encoding | An int representing the type of encoding desired according to the given table
|
int | The number of OrClause added to the parameter sat |
Definition at line 35 of file prefSAT.cpp.
References OrClause::addHeadVariable(), OrClause::appendVariable(), SetArguments::begin(), OrClause::clone(), debug, SetArguments::empty(), SetArguments::end(), AF::getArgumentByNumber(), Argument::getName(), AF::getPredecessors(), Argument::InVar(), Argument::NotInVar(), Argument::NotOutVar(), Argument::NotUndecVar(), AF::numArgs(), Argument::OutVar(), and Argument::UndecVar().
Referenced by PrefSat().
int PrefSat | ( | dMatrix * | preferred_extensions, |
AF * | af, | ||
int | encoding, | ||
int(*)(stringstream *, int, int, vector< int > *) | SatSolver | ||
) |
This is the function that in TAFA-13 is described by Algorithm 1.
This function has been rewritten for adhering to Algorithm 1 of TAFA-13, but the one used for the empirical evaluation in TAFA-13 was slightly different as it adopts some straightforward optimisations
[out] | preferred_extensions | Pointer to a dMatrix which will contain the computed preferred extensions. E.g., if the set of arguments is ![]() preferred_extensions will result:
AF are: | ||||||||||||||||||||
[in] | af | A pointer to the AF considered in this case | ||||||||||||||||||||
[in] | encoding | An integer representing the desired encoding, see PiGreek for an explanation | ||||||||||||||||||||
[in] | SatSolver | A pointer to a function which acts as a SAT Solver, whose signature must be: int name-function(stringstream *, int, int, vector<int> *);returning an int which will be equal to 20 if no solution has been found, and accepting as input:
|
int | 0 if the preferred extensions are correctely computed, 1 if the SatSolver is not specified, |
encoding
Definition at line 288 of file prefSAT.cpp.
References OrClause::appendVariable(), aSolution(), debug, INARGS(), AF::numArgs(), and PiGreek().