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

diff --git a/contrib/run-script-casc24-fnt b/contrib/run-script-casc24-fnt
index 0230b8e137b1bb89e1fdddaa0cc88dfed7c56fd8..ef3cd4b6534f022a3fb349e5e746b0e477f589ce 100755 (executable)
--- 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 beae09823f8f2d9b87c5a5ef7fc4c4bb2b28c6b9..b3e69a9927a7640d19a192f603222578889e71bb 100644 (file)
--- 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 721337c9e154760cafd131be70c76592fd48afab..e1e4053ac4b316094c04135f11fd5144b2efb5ce 100644 (file)
--- 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 75e2b4fbe045e9f4c329c5ad5ed1ff5a09e0e222..607547bebbbfe4f3ba02e738afb5ff41783a6cde 100644 (file)
--- 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 ee7ee4c6170eee9fc061e4b6f887040dca96239e..ab4ea14c4a804da64a5b2eef404123650de93222 100644 (file)
--- 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 6b7adbbf7595daec7de89b336360d38bb0f53ec4..cea2462827ff602fb6710ba450d091d7e329381f 100644 (file)
--- 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: