diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-10-18 15:19:10 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-10-18 15:19:10 -0500 |
| commit | 9af7e38d6f0b3d01dea795a4847153047ac87f6e (patch) | |
| tree | f16aed9383cead45ea321229560533f3c94b9566 /src/parser/tptp/Tptp.g | |
| parent | 6f18015fdcb824f46b969882aa45187b46306e97 (diff) | |
Tptp unsat cores (#1228)
* Support unsat cores for TPTP.
* Fix assertion
Diffstat (limited to 'src/parser/tptp/Tptp.g')
| -rw-r--r-- | src/parser/tptp/Tptp.g | 30 |
1 files changed, 27 insertions, 3 deletions
diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g index 8163eb239..1bed63496 100644 --- a/src/parser/tptp/Tptp.g +++ b/src/parser/tptp/Tptp.g @@ -170,13 +170,29 @@ parseCommand returns [CVC4::Command* cmd = NULL] } (COMMA_TOK anything*)? RPAREN_TOK DOT_TOK { - cmd = PARSER_STATE->makeCommand(fr, expr, /* cnf == */ true); + Expr 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); + } + // make the command to assert the formula + cmd = PARSER_STATE->makeAssertCommand(fr, aexpr, /* cnf == */ true, true); } | FOF_TOK LPAREN_TOK nameN[name] COMMA_TOK formulaRole[fr] COMMA_TOK { PARSER_STATE->setCnf(false); PARSER_STATE->setFof(true); } fofFormula[expr] (COMMA_TOK anything*)? RPAREN_TOK DOT_TOK { - cmd = PARSER_STATE->makeCommand(fr, expr, /* cnf == */ false); + Expr 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); + } + // make the command to assert the formula + cmd = PARSER_STATE->makeAssertCommand(fr, aexpr, /* cnf == */ false, true); } | TFF_TOK LPAREN_TOK nameN[name] COMMA_TOK ( TYPE_TOK COMMA_TOK tffTypedAtom[cmd] @@ -184,7 +200,15 @@ parseCommand returns [CVC4::Command* cmd = NULL] { PARSER_STATE->setCnf(false); PARSER_STATE->setFof(false); } tffFormula[expr] (COMMA_TOK anything*)? { - cmd = PARSER_STATE->makeCommand(fr, expr, /* cnf == */ false); + Expr 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); + } + // make the command to assert the formula + cmd = PARSER_STATE->makeAssertCommand(fr, aexpr, /* cnf == */ false, true); } ) RPAREN_TOK DOT_TOK | INCLUDE_TOK LPAREN_TOK unquotedFileName[name] |