Tptp unsat cores (#1228)

* Support unsat cores for TPTP.

* Fix assertion

1 files changed, 17 insertions, 1 deletions

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;