diff options
Diffstat (limited to 'src/parser/tptp/Tptp.g')
| -rw-r--r-- | src/parser/tptp/Tptp.g | 18 |
1 files changed, 6 insertions, 12 deletions
diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g index 8e29c25f1..71c1de2fa 100644 --- a/src/parser/tptp/Tptp.g +++ b/src/parser/tptp/Tptp.g @@ -121,6 +121,8 @@ using namespace CVC4::parser; #define PARSER_STATE ((Tptp*)PARSER->super) #undef SOLVER #define SOLVER PARSER_STATE->getSolver() +#undef SYM_MAN +#define SYM_MAN PARSER_STATE->getSymbolManager() #undef MK_TERM #define MK_TERM SOLVER->mkTerm #define UNSUPPORTED PARSER_STATE->unimplementedFeature @@ -164,9 +166,7 @@ parseCommand returns [CVC4::Command* cmd = NULL] CVC4::api::Term aexpr = PARSER_STATE->getAssertionExpr(fr, expr); if( !aexpr.isNull() ){ // set the expression name (e.g. used with unsat core printing) - Command* csen = new SetExpressionNameCommand(aexpr, name); - csen->setMuted(true); - PARSER_STATE->preemptCommand(csen); + SYM_MAN->setExpressionName(aexpr, name, true); } // make the command to assert the formula cmd = PARSER_STATE->makeAssertCommand(fr, aexpr, /* cnf == */ true, true); @@ -178,9 +178,7 @@ parseCommand returns [CVC4::Command* cmd = NULL] CVC4::api::Term aexpr = PARSER_STATE->getAssertionExpr(fr,expr); if( !aexpr.isNull() ){ // set the expression name (e.g. used with unsat core printing) - Command* csen = new SetExpressionNameCommand(aexpr, name); - csen->setMuted(true); - PARSER_STATE->preemptCommand(csen); + SYM_MAN->setExpressionName(aexpr, name, true); } // make the command to assert the formula cmd = PARSER_STATE->makeAssertCommand(fr, aexpr, /* cnf == */ false, true); @@ -194,9 +192,7 @@ parseCommand returns [CVC4::Command* cmd = NULL] CVC4::api::Term aexpr = PARSER_STATE->getAssertionExpr(fr,expr); if( !aexpr.isNull() ){ // set the expression name (e.g. used with unsat core printing) - Command* csen = new SetExpressionNameCommand(aexpr, name); - csen->setMuted(true); - PARSER_STATE->preemptCommand(csen); + SYM_MAN->setExpressionName(aexpr, name, true); } // make the command to assert the formula cmd = PARSER_STATE->makeAssertCommand(fr, aexpr, /* cnf == */ false, true); @@ -219,9 +215,7 @@ parseCommand returns [CVC4::Command* cmd = NULL] if (!aexpr.isNull()) { // set the expression name (e.g. used with unsat core printing) - Command* csen = new SetExpressionNameCommand(aexpr, name); - csen->setMuted(true); - PARSER_STATE->preemptCommand(csen); + SYM_MAN->setExpressionName(aexpr, name, true); } // make the command to assert the formula cmd = PARSER_STATE->makeAssertCommand( |