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: [PATCH] Update casc run script.  Work on compliance for SZS output.

---
 contrib/run-script-casc24-fnt | 24 ++++++++++++++++--------
 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 +++++++++++++
 6 files changed, 42 insertions(+), 9 deletions(-)

diff --git a/contrib/run-script-casc24-fnt b/contrib/run-script-casc24-fnt
index 0230b8e13..ef3cd4b65 100755
--- a/contrib/run-script-casc24-fnt
+++ b/contrib/run-script-casc24-fnt
@@ -11,17 +11,25 @@ filename=${file%.*}
 # which case this run script terminates immediately.  Otherwise, this
 # function returns normally.
 function trywith {
-  result="$($cvc4 -L tptp --no-checking --no-interactive "$@" $bench)"
+  result="$( ulimit -t "$1";shift;$cvc4 -L tptp --szs-compliant --no-checking --no-interactive "$@" $bench)"
   case "$result" in
     sat) echo "SZS Satisfiable for $filename"; exit 0;;
     unsat) echo "SZS Unsatisfiable for $filename"; exit 0;;
+    conjecture-sat) echo "SZS CounterSatisfiable for $filename"; exit 0;;
+    conjecture-unsat) echo "SZS Theorem for $filename"; exit 0;;
+  esac
+}
+function finishwith {
+  result="$( $cvc4 -L tptp --szs-compliant --no-checking --no-interactive "$@" $bench)"
+  case "$result" in
+    sat) echo "SZS Satisfiable for $filename"; exit 0;;
+    unsat) echo "SZS Unsatisfiable for $filename"; exit 0;;
+    conjecture-sat) echo "SZS CounterSatisfiable for $filename"; exit 0;;
+    conjecture-unsat) echo "SZS Theorem for $filename"; exit 0;;
   esac
 }
 
-
-trywith --finite-model-find --uf-ss-totality --tlimit-per=10000
-trywith --finite-model-find --decision=justification --tlimit-per=10000
-trywith --finite-model-find --decision=justification --fmf-fmc
-;;
-
-
+trywith 15 --finite-model-find --uf-ss-totality
+trywith 15 --finite-model-find --decision=justification --fmf-fmc
+finishwith --finite-model-find --decision=justification
+echo "SZS GaveUp for $filename"
\ No newline at end of file
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:
-- 
2.30.2