324 lines
7.0 KiB
C++
324 lines
7.0 KiB
C++
/*
|
|
Copyright (c) 2012, 2013
|
|
Artur Meski <meski@ipipan.waw.pl>
|
|
|
|
Reuse of the code or its part for any purpose
|
|
without the author's permission is strictly prohibited.
|
|
*/
|
|
|
|
#include "formrsctl.hh"
|
|
|
|
|
|
std::string BoolContexts::toStr(void) const
|
|
{
|
|
if (oper == BCTX_PV)
|
|
{
|
|
return name;
|
|
}
|
|
else if (oper == BCTX_TF)
|
|
{
|
|
if (tf) return "true";
|
|
else return "false";
|
|
}
|
|
else if (oper == BCTX_AND)
|
|
{
|
|
return "(" + arg[0]->toStr() + " AND " + arg[1]->toStr() + ")";
|
|
}
|
|
else if (oper == BCTX_OR)
|
|
{
|
|
return "(" + arg[0]->toStr() + " OR " + arg[1]->toStr() + ")";
|
|
}
|
|
else if (oper == BCTX_XOR)
|
|
{
|
|
return "(" + arg[0]->toStr() + " XOR " + arg[1]->toStr() + ")";
|
|
}
|
|
else if (oper == BCTX_NOT)
|
|
{
|
|
return "~" + arg[0]->toStr();
|
|
}
|
|
|
|
else
|
|
{
|
|
return "??";
|
|
assert(0);
|
|
}
|
|
}
|
|
|
|
BDD BoolContexts::getBDD(const SymRS *srs) const
|
|
{
|
|
if (oper == BCTX_PV)
|
|
{
|
|
return srs->encActStrAtom(name);
|
|
}
|
|
else if (oper == BCTX_TF)
|
|
{
|
|
if (tf) return srs->getBDDtrue();
|
|
else return srs->getBDDfalse();
|
|
}
|
|
else if (oper == BCTX_AND)
|
|
{
|
|
return arg[0]->getBDD(srs) * arg[1]->getBDD(srs);
|
|
}
|
|
else if (oper == BCTX_OR)
|
|
{
|
|
return arg[0]->getBDD(srs) + arg[1]->getBDD(srs);
|
|
}
|
|
else if (oper == BCTX_XOR)
|
|
{
|
|
return arg[0]->getBDD(srs) ^ arg[1]->getBDD(srs);
|
|
}
|
|
else if (oper == BCTX_NOT)
|
|
{
|
|
return !arg[0]->getBDD(srs);
|
|
}
|
|
else
|
|
{
|
|
assert(0);
|
|
FERROR("Undefined operator used in Boolean context definition. This should not happen.");
|
|
return srs->getBDDfalse();
|
|
}
|
|
}
|
|
|
|
std::string FormRSCTL::toStr(void) const
|
|
{
|
|
if (oper == RSCTL_PV)
|
|
{
|
|
return name;
|
|
}
|
|
else if (oper == RSCTL_TF)
|
|
{
|
|
if (tf) return "true";
|
|
else return "false";
|
|
}
|
|
else if (oper == RSCTL_AND)
|
|
{
|
|
return "(" + arg[0]->toStr() + " AND " + arg[1]->toStr() + ")";
|
|
}
|
|
else if (oper == RSCTL_OR)
|
|
{
|
|
return "(" + arg[0]->toStr() + " OR " + arg[1]->toStr() + ")";
|
|
}
|
|
else if (oper == RSCTL_XOR)
|
|
{
|
|
return "(" + arg[0]->toStr() + " XOR " + arg[1]->toStr() + ")";
|
|
}
|
|
else if (oper == RSCTL_IMPL)
|
|
{
|
|
return "(" + arg[0]->toStr() + " IMPLIES " + arg[1]->toStr() + ")";
|
|
}
|
|
else if (oper == RSCTL_NOT)
|
|
{
|
|
return "~" + arg[0]->toStr();
|
|
}
|
|
else if (oper == RSCTL_EX)
|
|
{
|
|
return "EX(" + arg[0]->toStr() + ")";
|
|
}
|
|
else if (oper == RSCTL_EG)
|
|
{
|
|
return "EG(" + arg[0]->toStr() + ")";
|
|
}
|
|
else if (oper == RSCTL_EU)
|
|
{
|
|
return "EU(" + arg[0]->toStr() + "," + arg[1]->toStr() + ")";
|
|
}
|
|
else if (oper == RSCTL_EF)
|
|
{
|
|
return "EF(" + arg[0]->toStr() + ")";
|
|
}
|
|
else if (oper == RSCTL_AX)
|
|
{
|
|
return "AX(" + arg[0]->toStr() + ")";
|
|
}
|
|
else if (oper == RSCTL_AG)
|
|
{
|
|
return "AG(" + arg[0]->toStr() + ")";
|
|
}
|
|
else if (oper == RSCTL_AU)
|
|
{
|
|
return "AU(" + arg[0]->toStr() + "," + arg[1]->toStr() + ")";
|
|
}
|
|
else if (oper == RSCTL_AF)
|
|
{
|
|
return "AF(" + arg[0]->toStr() + ")";
|
|
}
|
|
else if (oper == RSCTL_EX_ACT)
|
|
{
|
|
return "E" + getActionsStr() + "X(" + arg[0]->toStr() + ")";
|
|
}
|
|
else if (oper == RSCTL_EG_ACT)
|
|
{
|
|
return "E" + getActionsStr() + "G(" + arg[0]->toStr() + ")";
|
|
}
|
|
else if (oper == RSCTL_EU_ACT)
|
|
{
|
|
return "E" + getActionsStr() + "U(" + arg[0]->toStr() + "," + arg[1]->toStr() + ")";
|
|
}
|
|
else if (oper == RSCTL_EF_ACT)
|
|
{
|
|
return "E" + getActionsStr() + "F(" + arg[0]->toStr() + ")";
|
|
}
|
|
else if (oper == RSCTL_AX_ACT)
|
|
{
|
|
return "A" + getActionsStr() + "X(" + arg[0]->toStr() + ")";
|
|
}
|
|
else if (oper == RSCTL_AG_ACT)
|
|
{
|
|
return "A" + getActionsStr() + "G(" + arg[0]->toStr() + ")";
|
|
}
|
|
else if (oper == RSCTL_AU_ACT)
|
|
{
|
|
return "A" + getActionsStr() + "U(" + arg[0]->toStr() + "," + arg[1]->toStr() + ")";
|
|
}
|
|
else if (oper == RSCTL_AF_ACT)
|
|
{
|
|
return "A" + getActionsStr() + "F(" + arg[0]->toStr() + ")";
|
|
}
|
|
|
|
else
|
|
{
|
|
return "??";
|
|
assert(0);
|
|
}
|
|
}
|
|
|
|
bool FormRSCTL::hasOper(Oper op) const
|
|
{
|
|
if (oper == op)
|
|
return true;
|
|
else
|
|
{
|
|
bool result = false;
|
|
if (arg[0] != NULL) result = arg[0]->hasOper(op);
|
|
if (!result && arg[1] != NULL) result = arg[1]->hasOper(op);
|
|
return result;
|
|
}
|
|
}
|
|
|
|
void FormRSCTL::encodeAtoms(const SymRS *srs)
|
|
{
|
|
if (RSCTL_COND_1ARG(oper))
|
|
{
|
|
arg[0]->encodeAtoms(srs);
|
|
}
|
|
else if (RSCTL_COND_2ARG(oper))
|
|
{
|
|
arg[0]->encodeAtoms(srs);
|
|
arg[1]->encodeAtoms(srs);
|
|
}
|
|
else if (oper == RSCTL_PV)
|
|
{
|
|
bdd = new BDD(srs->encAtom(name));
|
|
}
|
|
}
|
|
|
|
bool FormRSCTL::isERSCTL(void) const
|
|
{
|
|
if (oper == RSCTL_PV)
|
|
{
|
|
return true;
|
|
}
|
|
|
|
if (oper == RSCTL_NOT)
|
|
{
|
|
if (arg[0]->getOper() == RSCTL_PV || arg[0]->getOper() == RSCTL_TF)
|
|
return true;
|
|
else
|
|
return false;
|
|
}
|
|
|
|
if (RSCTL_COND_IS_UNIVERSAL(oper))
|
|
{
|
|
return false;
|
|
}
|
|
|
|
if (RSCTL_COND_1ARG(oper))
|
|
{
|
|
return arg[0]->isERSCTL();
|
|
}
|
|
|
|
if (RSCTL_COND_2ARG(oper))
|
|
{
|
|
return arg[0]->isERSCTL() && arg[1]->isERSCTL();
|
|
}
|
|
|
|
assert(0);
|
|
|
|
return false;
|
|
}
|
|
|
|
std::string FormRSCTL::getActionsStr(void) const
|
|
{
|
|
if (actions != NULL)
|
|
{
|
|
std::string r = "[ ";
|
|
bool firstact = true;
|
|
|
|
for (ActionsVec_f::iterator act = actions->begin(); act != actions->end(); ++act)
|
|
{
|
|
if (!firstact) r += ",";
|
|
else firstact = false;
|
|
r += "{";
|
|
bool firstent = true;
|
|
for (Action_f::iterator ent = act->begin(); ent != act->end(); ++ent)
|
|
{
|
|
if (!firstent) r += ",";
|
|
else firstent = false;
|
|
r += *ent;
|
|
}
|
|
r += "}";
|
|
}
|
|
r += " ]";
|
|
return r;
|
|
}
|
|
else if (boolCtx != NULL)
|
|
{
|
|
return "< " + boolCtx->toStr() + " >";
|
|
}
|
|
else
|
|
{
|
|
FERROR("Context not specified. This should not happen.");
|
|
}
|
|
}
|
|
|
|
void FormRSCTL::encodeActions(const SymRS *srs)
|
|
{
|
|
if (RSCTL_COND_ACT(oper))
|
|
{
|
|
if (actions_bdd != NULL) forgetActionsBDD();
|
|
actions_bdd = new BDD(srs->getBDDfalse());
|
|
assert(actions != NULL || boolCtx != NULL);
|
|
assert(!(actions != NULL && boolCtx != NULL));
|
|
if (actions != NULL)
|
|
{
|
|
for (ActionsVec_f::iterator act = actions->begin(); act != actions->end(); ++act)
|
|
{
|
|
BDD single_action = srs->getBDDtrue();
|
|
for (Action_f::iterator ent = act->begin(); ent != act->end(); ++ent)
|
|
{
|
|
single_action *= srs->encActStrAtom(*ent);
|
|
}
|
|
single_action = srs->compContext(single_action);
|
|
*actions_bdd += single_action;
|
|
}
|
|
}
|
|
else if (boolCtx != NULL)
|
|
{
|
|
*actions_bdd = boolCtx->getBDD(srs);
|
|
}
|
|
else
|
|
assert(0);
|
|
}
|
|
|
|
if (RSCTL_COND_1ARG(oper))
|
|
{
|
|
arg[0]->encodeActions(srs);
|
|
}
|
|
|
|
if (RSCTL_COND_2ARG(oper))
|
|
{
|
|
arg[0]->encodeActions(srs);
|
|
arg[1]->encodeActions(srs);
|
|
}
|
|
}
|