* Support unsat cores for TPTP.
* Fix assertion
}
(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]
{ 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]
}
}
-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:
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 */
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 */
// 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;
#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;
// 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 */
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 */
projects / cvc5.git / commitdiff