From 38216791c43f9be4afecbc700548d1dbba63acb0 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 10 May 2013 15:18:20 -0500
Subject: Update casc run script.  Work on compliance for SZS output.

---
 src/parser/options            |  3 +++
 src/parser/parser_builder.cpp |  7 ++++++-
 src/parser/parser_builder.h   |  3 +++
 src/parser/tptp/tptp.cpp      |  1 +
 src/parser/tptp/tptp.h        | 13 +++++++++++++
 5 files changed, 26 insertions(+), 1 deletion(-)

(limited to 'src')

diff --git a/src/parser/options b/src/parser/options
index beae09823..b3e69a992 100644
--- a/src/parser/options
+++ b/src/parser/options
@@ -14,4 +14,7 @@ option memoryMap --mmap bool
 option semanticChecks /--no-checking bool :default DO_SEMANTIC_CHECKS_BY_DEFAULT :link /--no-type-checking
  disable ALL semantic checks, including type checks
 
+option szsCompliant --szs-compliant bool :default false
+ temporary support for szs ontolotogy, print if conjecture is found
+
 endmodule
diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp
index 721337c9e..e1e4053ac 100644
--- a/src/parser/parser_builder.cpp
+++ b/src/parser/parser_builder.cpp
@@ -89,7 +89,11 @@ Parser* ParserBuilder::build()
     parser = new Smt2(d_exprManager, input, d_strictMode, d_parseOnly);
     break;
   case language::input::LANG_TPTP:
-    parser = new Tptp(d_exprManager, input, d_strictMode, d_parseOnly);
+  {
+    Tptp * tparser = new Tptp(d_exprManager, input, d_strictMode, d_parseOnly);
+    tparser->d_szsCompliant = d_szsCompliant;
+    parser = tparser;
+  }
     break;
   default:
     parser = new Parser(d_exprManager, input, d_strictMode, d_parseOnly);
@@ -141,6 +145,7 @@ ParserBuilder& ParserBuilder::withParseOnly(bool flag) {
 }
 
 ParserBuilder& ParserBuilder::withOptions(const Options& options) {
+  d_szsCompliant = options[options::szsCompliant];
   return
     withInputLanguage(options[options::inputLanguage])
       .withMmap(options[options::memoryMap])
diff --git a/src/parser/parser_builder.h b/src/parser/parser_builder.h
index 75e2b4fbe..607547beb 100644
--- a/src/parser/parser_builder.h
+++ b/src/parser/parser_builder.h
@@ -77,6 +77,9 @@ class CVC4_PUBLIC ParserBuilder {
   /** Are we parsing only? */
   bool d_parseOnly;
 
+  /** hack for szs compliance */
+  bool d_szsCompliant;
+
   /** Initialize this parser builder */
   void init(ExprManager* exprManager, const std::string& filename);
 
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:
-- 
cgit v1.2.3