From c4c3af0300232981ddd5a75a1f6f7c8d13d8349a Mon Sep 17 00:00:00 2001 From: Artur Meski Date: Sun, 15 Apr 2018 12:25:57 +0100 Subject: [PATCH] Removed action sets in formulae --- formrsctl.cc | 101 +++++++++++++++++++-------------------- formrsctl.hh | 74 ++++++++++++++--------------- rsin_parser.yy | 126 +++++++++++++++++++++++++------------------------ 3 files changed, 152 insertions(+), 149 deletions(-) diff --git a/formrsctl.cc b/formrsctl.cc index 2b97e25..570544b 100644 --- a/formrsctl.cc +++ b/formrsctl.cc @@ -226,40 +226,40 @@ bool FormRSCTL::isERSCTL(void) const std::string FormRSCTL::getActionsStr(void) const { - if (actions != nullptr) { - 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 != nullptr) { + // if (actions != nullptr) { + // 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; + // } + if (boolCtx != nullptr) { return "< " + boolCtx->toStr() + " >"; } else { @@ -275,23 +275,24 @@ void FormRSCTL::encodeActions(const SymRS *srs) } actions_bdd = new BDD(srs->getBDDfalse()); - assert(actions != nullptr || boolCtx != nullptr); - assert(!(actions != nullptr && boolCtx != nullptr)); + assert(boolCtx != nullptr); + // assert(actions != nullptr || boolCtx != nullptr); + // assert(!(actions != nullptr && boolCtx != nullptr)); - if (actions != nullptr) { - 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->encActStrEntity(*ent); - } - - single_action = srs->compContext(single_action); - *actions_bdd += single_action; - } - } - else if (boolCtx != nullptr) { + // if (actions != nullptr) { + // 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->encActStrEntity(*ent); + // } + // + // single_action = srs->compContext(single_action); + // *actions_bdd += single_action; + // } + // } + if (boolCtx != nullptr) { *actions_bdd = boolCtx->getBDD(srs); } else { diff --git a/formrsctl.hh b/formrsctl.hh index f83a709..60a9db8 100644 --- a/formrsctl.hh +++ b/formrsctl.hh @@ -65,9 +65,9 @@ using std::endl; typedef unsigned char Oper; -typedef std::string Entity_f; -typedef std::set Action_f; -typedef vector ActionsVec_f; +// typedef std::string Entity_f; +// typedef std::set Action_f; +// typedef vector ActionsVec_f; class BoolContexts { @@ -159,7 +159,7 @@ class FormRSCTL std::string proc_name; bool tf; BDD *bdd; - ActionsVec_f *actions; + // ActionsVec_f *actions; BDD *actions_bdd; BoolContexts *boolCtx; public: @@ -177,7 +177,7 @@ class FormRSCTL arg[0] = nullptr; arg[1] = nullptr; bdd = nullptr; - actions = nullptr; + // actions = nullptr; actions_bdd = nullptr; boolCtx = nullptr; } @@ -194,7 +194,7 @@ class FormRSCTL arg[0] = nullptr; arg[1] = nullptr; bdd = nullptr; - actions = nullptr; + // actions = nullptr; actions_bdd = nullptr; boolCtx = nullptr; } @@ -210,7 +210,7 @@ class FormRSCTL arg[0] = form1; arg[1] = form2; bdd = nullptr; - actions = nullptr; + // actions = nullptr; actions_bdd = nullptr; boolCtx = nullptr; } @@ -218,19 +218,19 @@ class FormRSCTL /** * @brief Constructor for two-argument formula with action restrictions. */ - FormRSCTL(Oper op, ActionsVec_f *acts, FormRSCTL *form1, FormRSCTL *form2) - { - assert(acts != nullptr); - assert(RSCTL_COND_2ARG(op)); - assert(RSCTL_COND_ACT(op)); - oper = op; - arg[0] = form1; - arg[1] = form2; - bdd = nullptr; - actions = acts; - actions_bdd = nullptr; - boolCtx = nullptr; - } + // FormRSCTL(Oper op, ActionsVec_f *acts, FormRSCTL *form1, FormRSCTL *form2) + // { + // assert(acts != nullptr); + // assert(RSCTL_COND_2ARG(op)); + // assert(RSCTL_COND_ACT(op)); + // oper = op; + // arg[0] = form1; + // arg[1] = form2; + // bdd = nullptr; + // actions = acts; + // actions_bdd = nullptr; + // boolCtx = nullptr; + // } /** * @brief Constructor for two-argument formula with Boolean context restrictions. @@ -244,7 +244,7 @@ class FormRSCTL arg[0] = form1; arg[1] = form2; bdd = nullptr; - actions = nullptr; + // actions = nullptr; actions_bdd = nullptr; boolCtx = bctx; } @@ -260,7 +260,7 @@ class FormRSCTL arg[0] = form1; arg[1] = nullptr; bdd = nullptr; - actions = nullptr; + // actions = nullptr; actions_bdd = nullptr; boolCtx = nullptr; } @@ -268,19 +268,19 @@ class FormRSCTL /** * @brief Constructor for one-argument formula with action restrictions. */ - FormRSCTL(Oper op, ActionsVec_f *acts, FormRSCTL *form1) - { - assert(acts != nullptr); - assert(RSCTL_COND_1ARG(op)); - assert(RSCTL_COND_ACT(op)); - oper = op; - arg[0] = form1; - arg[1] = nullptr; - bdd = nullptr; - actions = acts; - actions_bdd = nullptr; - boolCtx = nullptr; - } + // FormRSCTL(Oper op, ActionsVec_f *acts, FormRSCTL *form1) + // { + // assert(acts != nullptr); + // assert(RSCTL_COND_1ARG(op)); + // assert(RSCTL_COND_ACT(op)); + // oper = op; + // arg[0] = form1; + // arg[1] = nullptr; + // bdd = nullptr; + // // actions = acts; + // actions_bdd = nullptr; + // boolCtx = nullptr; + // } /** * @brief Constructor for one-argument formula with Boolean context restrictions. @@ -294,7 +294,7 @@ class FormRSCTL arg[0] = form1; arg[1] = nullptr; bdd = nullptr; - actions = nullptr; + // actions = nullptr; actions_bdd = nullptr; boolCtx = bctx; } @@ -307,7 +307,7 @@ class FormRSCTL delete arg[0]; delete arg[1]; delete bdd; - delete actions; + // delete actions; delete actions_bdd; delete boolCtx; } diff --git a/rsin_parser.yy b/rsin_parser.yy index fdf79b2..6910086 100644 --- a/rsin_parser.yy +++ b/rsin_parser.yy @@ -34,9 +34,9 @@ class rsin_driver; int ival; std::string *sval; FormRSCTL *frsctl; - Entity_f *ent; - Action_f *act; - ActionsVec_f *actionsVec; + // Entity_f *ent; + // Action_f *act; + // ActionsVec_f *actionsVec; BoolContexts *fboolctx; }; @@ -61,9 +61,9 @@ class rsin_driver; //%right SRB %type rsctl_form -%type f_entity -%type action -%type actions +// %type f_entity +// %type action +// %type actions %type bool_contexts //%printer { yyoutput << *$$; } "identifier" @@ -281,40 +281,40 @@ bool_contexts: IDENTIFIER DOT IDENTIFIER { } ; -actions: - LCB action RCB { - $$ = new ActionsVec_f; - $$->push_back(*$2); - free($2); - } - | actions COMMA LCB action RCB { - $$ = $1; - $$->push_back(*$4); - free($4); - } - ; +// actions: +// LCB action RCB { +// $$ = new ActionsVec_f; +// $$->push_back(*$2); +// free($2); +// } +// | actions COMMA LCB action RCB { +// $$ = $1; +// $$->push_back(*$4); +// free($4); +// } +// ; -action: - { - $$ = new Action_f; - } - | f_entity { - $$ = new Action_f; - $$->insert(*$1); - free($1); - } - | action COMMA f_entity { - $$ = $1; - $$->insert(*$3); - free($3); - } - ; +// action: +// { +// $$ = new Action_f; +// } +// | f_entity { +// $$ = new Action_f; +// $$->insert(*$1); +// free($1); +// } +// | action COMMA f_entity { +// $$ = $1; +// $$->insert(*$3); +// free($3); +// } +// ; -f_entity: IDENTIFIER { - $$ = new Entity_f(*$1); - free($1); - } - ; +// f_entity: IDENTIFIER { +// $$ = new Entity_f(*$1); +// free($1); +// } +// ; rsctl_form: IDENTIFIER DOT IDENTIFIER { $$ = new FormRSCTL(*$1, *$3); @@ -363,30 +363,32 @@ rsctl_form: IDENTIFIER DOT IDENTIFIER { | AG rsctl_form { $$ = new FormRSCTL(RSCTL_AG, $2); } - | E LSB actions RSB X rsctl_form { - $$ = new FormRSCTL(RSCTL_EX_ACT, $3, $6); - } - | E LSB actions RSB U LRB rsctl_form COMMA rsctl_form RRB { - $$ = new FormRSCTL(RSCTL_EU_ACT, $3, $7, $9); - } - | E LSB actions RSB F rsctl_form { - $$ = new FormRSCTL(RSCTL_EF_ACT, $3, $6); - } - | E LSB actions RSB G rsctl_form { - $$ = new FormRSCTL(RSCTL_EG_ACT, $3, $6); - } - | A LSB actions RSB X rsctl_form { - $$ = new FormRSCTL(RSCTL_AX_ACT, $3, $6); - } - | A LSB actions RSB U LRB rsctl_form COMMA rsctl_form RRB { - $$ = new FormRSCTL(RSCTL_AU_ACT, $3, $7, $9); - } - | A LSB actions RSB F rsctl_form { - $$ = new FormRSCTL(RSCTL_AF_ACT, $3, $6); - } - | A LSB actions RSB G rsctl_form { - $$ = new FormRSCTL(RSCTL_AG_ACT, $3, $6); - } + + // | E LSB actions RSB X rsctl_form { + // $$ = new FormRSCTL(RSCTL_EX_ACT, $3, $6); + // } + // | E LSB actions RSB U LRB rsctl_form COMMA rsctl_form RRB { + // $$ = new FormRSCTL(RSCTL_EU_ACT, $3, $7, $9); + // } + // | E LSB actions RSB F rsctl_form { + // $$ = new FormRSCTL(RSCTL_EF_ACT, $3, $6); + // } + // | E LSB actions RSB G rsctl_form { + // $$ = new FormRSCTL(RSCTL_EG_ACT, $3, $6); + // } + // | A LSB actions RSB X rsctl_form { + // $$ = new FormRSCTL(RSCTL_AX_ACT, $3, $6); + // } + // | A LSB actions RSB U LRB rsctl_form COMMA rsctl_form RRB { + // $$ = new FormRSCTL(RSCTL_AU_ACT, $3, $7, $9); + // } + // | A LSB actions RSB F rsctl_form { + // $$ = new FormRSCTL(RSCTL_AF_ACT, $3, $6); + // } + // | A LSB actions RSB G rsctl_form { + // $$ = new FormRSCTL(RSCTL_AG_ACT, $3, $6); + // } + /* contexts as boolean formulae */ | E LAB bool_contexts RAB X rsctl_form { $$ = new FormRSCTL(RSCTL_EX_ACT, $3, $6);