Tptp unsat cores (#1228)

* Support unsat cores for TPTP.

* Fix assertion

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;