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 | |
parent | 6f18015fdcb824f46b969882aa45187b46306e97 (diff) |
Tptp unsat cores (#1228)
* Support unsat cores for TPTP.
* Fix assertion
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/tptp/Tptp.g | 30 | ||||
-rw-r--r-- | src/parser/tptp/tptp.cpp | 36 | ||||
-rw-r--r-- | src/parser/tptp/tptp.h | 18 |
3 files changed, 68 insertions, 16 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] diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp index a01de9df4..e49315609 100644 --- a/src/parser/tptp/tptp.cpp +++ b/src/parser/tptp/tptp.cpp @@ -312,13 +312,8 @@ void Tptp::makeApplication(Expr& expr, std::string& name, } } -Command* Tptp::makeCommand(FormulaRole fr, Expr& expr, bool cnf) { - // For SZS ontology compliance. - // if we're in cnf() though, conjectures don't result in "Theorem" or - // "CounterSatisfiable". - if (!cnf && (fr == FR_NEGATED_CONJECTURE || fr == FR_CONJECTURE)) { - d_hasConjecture = true; - } + +Expr Tptp::getAssertionExpr(FormulaRole fr, Expr expr) { switch (fr) { case FR_AXIOM: case FR_HYPOTHESIS: @@ -329,19 +324,36 @@ Command* Tptp::makeCommand(FormulaRole fr, Expr& expr, bool cnf) { case FR_NEGATED_CONJECTURE: case FR_PLAIN: // it's a usual assert - return new AssertCommand(expr); + return expr; case FR_CONJECTURE: - // something to prove - return new AssertCommand(getExprManager()->mkExpr(kind::NOT, expr)); + // it should be negated when asserted + return getExprManager()->mkExpr(kind::NOT, expr); case FR_UNKNOWN: case FR_FI_DOMAIN: case FR_FI_FUNCTORS: case FR_FI_PREDICATES: case FR_TYPE: - return new EmptyCommand("Untreated role"); + // it does not correspond to an assertion + return d_nullExpr; + break; } assert(false); // unreachable - return nullptr; + return d_nullExpr; +} + +Command* Tptp::makeAssertCommand(FormulaRole fr, Expr expr, bool cnf, bool inUnsatCore) { + // For SZS ontology compliance. + // if we're in cnf() though, conjectures don't result in "Theorem" or + // "CounterSatisfiable". + if (!cnf && (fr == FR_NEGATED_CONJECTURE || fr == FR_CONJECTURE)) { + d_hasConjecture = true; + assert(!expr.isNull()); + } + if( expr.isNull() ){ + return new EmptyCommand("Untreated role for expression"); + }else{ + return new AssertCommand(expr, inUnsatCore); + } } }/* CVC4::parser namespace */ diff --git a/src/parser/tptp/tptp.h b/src/parser/tptp/tptp.h index e6d7bbb47..1cc9c2d7f 100644 --- a/src/parser/tptp/tptp.h +++ b/src/parser/tptp/tptp.h @@ -91,7 +91,20 @@ class Tptp : public Parser { void makeApplication(Expr& expr, std::string& name, std::vector<Expr>& args, bool term); - Command* makeCommand(FormulaRole fr, Expr& expr, bool cnf); + /** get assertion expression, based on the formula role. + * expr should have Boolean type. + * This returns the expression that should be asserted, given the formula role fr. + * For example, if the role is "conjecture", then the return value is the negation of expr. + */ + Expr getAssertionExpr(FormulaRole fr, Expr expr); + + /** returns the appropriate AssertCommand, given a role, expression expr to assert, + * and information about the assertion. + * The assertion expr is literally what should be asserted (it is already been processed + * with getAssertionExpr above). + * This may set a flag in the parser to mark that we have asserted a conjecture. + */ + Command* makeAssertCommand(FormulaRole fr, Expr expr, bool cnf, bool inUnsatCore); /** Ugly hack because I don't know how to return an expression from a token */ @@ -124,6 +137,9 @@ class Tptp : public Parser { // TPTP directory where to find includes; // empty if none could be determined std::string d_tptpDir; + + // the null expression + Expr d_nullExpr; // hack to make output SZS ontology-compliant bool d_hasConjecture; |