Update casc run script. Work on compliance for SZS output.

2 files changed, 14 insertions, 0 deletions

diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp
index ee7ee4c61..ab4ea14c4 100644
--- a/src/parser/tptp/tptp.cpp
+++ b/src/parser/tptp/tptp.cpp
@@ -52,6 +52,7 @@ Tptp::Tptp(ExprManager* exprManager, Input* input, bool strictMode, bool parseOn
         d_tptpDir.append("/");
       }
     }
+    d_hasConjecture = false;
 }
 
 void Tptp::addTheory(Theory theory) {
diff --git a/src/parser/tptp/tptp.h b/src/parser/tptp/tptp.h
index 6b7adbbf7..cea246282 100644
--- a/src/parser/tptp/tptp.h
+++ b/src/parser/tptp/tptp.h
@@ -24,6 +24,7 @@
 #include "util/hash.h"
 #include <ext/hash_set>
 #include <cassert>
+#include "parser/options.h"
 
 namespace CVC4 {
 
@@ -49,6 +50,11 @@ class Tptp : public Parser {
   // empty if none could be determined
   std::string d_tptpDir;
 
+  //hack to make output SZS ontology-compliant
+  bool d_hasConjecture;
+  // hack for szs compliance
+  bool d_szsCompliant;
+
 public:
   bool cnf; //in a cnf formula
 
@@ -181,6 +187,13 @@ inline void Tptp::makeApplication(Expr & expr, std::string & name,
 };
 
 inline Command* Tptp::makeCommand(FormulaRole fr, Expr & expr){
+  //hack for SZS ontology compliance
+  if(d_szsCompliant && (fr==FR_NEGATED_CONJECTURE || fr==FR_CONJECTURE)){
+    if( !d_hasConjecture ){
+      d_hasConjecture = true;
+      std::cout << "conjecture-";
+    }
+  }
   switch(fr){
   case FR_AXIOM:
   case FR_HYPOTHESIS: