From 9af7e38d6f0b3d01dea795a4847153047ac87f6e Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 18 Oct 2017 15:19:10 -0500 Subject: [PATCH] Tptp unsat cores (#1228) * Support unsat cores for TPTP. * Fix assertion --- src/parser/tptp/Tptp.g | 30 +++++++++++++++++++++++--- src/parser/tptp/tptp.cpp | 36 ++++++++++++++++++++----------- src/parser/tptp/tptp.h | 18 +++++++++++++++- src/printer/tptp/tptp_printer.cpp | 19 +++++++++++++++- src/printer/tptp/tptp_printer.h | 5 +++++ 5 files changed, 91 insertions(+), 17 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& 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; diff --git a/src/printer/tptp/tptp_printer.cpp b/src/printer/tptp/tptp_printer.cpp index 5fc9b7ed8..102419ec4 100644 --- a/src/printer/tptp/tptp_printer.cpp +++ b/src/printer/tptp/tptp_printer.cpp @@ -23,6 +23,8 @@ #include "expr/expr.h" // for ExprSetDepth etc.. #include "expr/node_manager.h" // for VarNameAttr #include "options/language.h" // for LANG_AST +#include "options/smt_options.h" // for unsat cores +#include "smt/smt_engine.h" #include "smt/command.h" using namespace std; @@ -58,7 +60,22 @@ void TptpPrinter::toStream(std::ostream& out, const Model& m, const Command* c) // shouldn't be called; only the non-Command* version above should be Unreachable(); } - +void TptpPrinter::toStream(std::ostream& out, const UnsatCore& core) const throw() { + out << "% SZS output start UnsatCore " << std::endl; + SmtEngine * smt = core.getSmtEngine(); + Assert( smt!=NULL ); + for(UnsatCore::const_iterator i = core.begin(); i != core.end(); ++i) { + std::string name; + if (smt->getExpressionName(*i, name)) { + // Named assertions always get printed + out << name << endl; + } else if (options::dumpUnsatCoresFull()) { + // Unnamed assertions only get printed if the option is set + out << *i << endl; + } + } + out << "% SZS output end UnsatCore " << std::endl; +} }/* CVC4::printer::tptp namespace */ }/* CVC4::printer namespace */ diff --git a/src/printer/tptp/tptp_printer.h b/src/printer/tptp/tptp_printer.h index 7c8ddbd20..731885068 100644 --- a/src/printer/tptp/tptp_printer.h +++ b/src/printer/tptp/tptp_printer.h @@ -35,6 +35,11 @@ public: void toStream(std::ostream& out, const Command* c, int toDepth, bool types, size_t dag) const throw(); void toStream(std::ostream& out, const CommandStatus* s) const throw(); void toStream(std::ostream& out, const Model& m) const throw(); + /** print unsat core to stream + * We use the expression names stored in the SMT engine associated with the unsat core + * with UnsatCore::getSmtEngine. + */ + void toStream(std::ostream& out, const UnsatCore& core) const throw(); };/* class TptpPrinter */ }/* CVC4::printer::tptp namespace */ -- 2.30.2