From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Mon, 31 Mar 2014 20:07:58 +0000 (-0400)
Subject: Travis-CI test for new-theory script, also related bugfixes.
X-Git-Tag: cvc5-1.0.0~6990
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9af3f271937cb9389f8e5b8f1b302f48bc6cdd9a;p=cvc5.git

Travis-CI test for new-theory script, also related bugfixes.
---

diff --git a/.travis.yml b/.travis.yml
index 9b8482c00..10eea921b 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -22,10 +22,16 @@ before_script:
 script:
  - normal="$(echo -e '\033[0m')" red="$normal$(echo -e '\033[01;31m')" green="$normal$(echo -e '\033[01;32m')"
  - if [ -n "$TRAVIS_CVC4" ]; then
+     if [ -n "$TRAVIS_CVC4_DISTCHECK" ]; then
+       (contrib/new-theory test_newtheory || (echo; echo "${red}NEWTHEORY FAILED${normal}"; echo; exit 1)) &&
+       (grep -q '^THEORIES *=.* test_newtheory' src/Makefile.am || (echo; echo "${red}NEWTHEORY FAILED${normal}"; echo; exit 1)) &&
+       (contrib/new-theory --alternate test_newtheory test_newalttheory || (echo; echo "${red}NEWTHEORY-ALTERNATE FAILED${normal}"; echo; exit 1)) &&
+       (grep -q '^THEORIES *=.* test_newalttheory' src/Makefile.am || (echo; echo "${red}NEWTHEORY-ALTERNATE FAILED${normal}"; echo; exit 1));
+     fi;
      echo "CVC4 config - $TRAVIS_CVC4_CONFIG" &&
      (./configure --enable-unit-testing --enable-proof --with-portfolio $TRAVIS_CVC4_CONFIG || (echo; cat builds/config.log; echo; echo "${red}CONFIGURE FAILED${normal}"; exit 1)) &&
      if [ -n "$TRAVIS_CVC4_DISTCHECK" ]; then
-       make -j2 distcheck CVC4_REGRESSION_ARGS='--no-early-exit' || (echo; echo "${red}DISTCHECK FAILED${normal}"; echo; exit 1);
+       make -j2 distcheck CVC4_REGRESSION_ARGS='--no-early-exit' || (echo; echo "${red}DISTCHECK (WITH NEWTHEORY TESTS) FAILED${normal}"; echo; exit 1);
      else
        (make -j2 check CVC4_REGRESSION_ARGS='--no-early-exit' || (echo; echo "${red}BUILD/TEST FAILED${normal}"; echo; exit 1)) &&
        (make check BINARY=pcvc4 CVC4_REGRESSION_ARGS='--fallback-sequential --no-early-exit' RUN_REGRESSION_ARGS= || (echo; echo "${red}PORTFOLIO TEST FAILED${normal}"; echo; exit 1)) &&
diff --git a/contrib/alttheoryskel/theory_DIR.cpp b/contrib/alttheoryskel/theory_DIR.cpp
index eca07e909..83d837322 100644
--- a/contrib/alttheoryskel/theory_DIR.cpp
+++ b/contrib/alttheoryskel/theory_DIR.cpp
@@ -11,9 +11,8 @@ Theory$camel::Theory$camel(context::Context* c,
                            context::UserContext* u,
                            OutputChannel& out,
                            Valuation valuation,
-                           const LogicInfo& logicInfo,
-                           QuantifiersEngine* qe) :
-  Theory(THEORY_$alt_id, c, u, out, valuation, logicInfo, qe) {
+                           const LogicInfo& logicInfo) :
+  Theory(THEORY_$alt_id, c, u, out, valuation, logicInfo) {
 }/* Theory$camel::Theory$camel() */
 
 void Theory$camel::check(Effort level) {
diff --git a/contrib/alttheoryskel/theory_DIR.h b/contrib/alttheoryskel/theory_DIR.h
index 9dfb3e614..d8e652b7c 100644
--- a/contrib/alttheoryskel/theory_DIR.h
+++ b/contrib/alttheoryskel/theory_DIR.h
@@ -17,8 +17,7 @@ public:
                context::UserContext* u,
                OutputChannel& out,
                Valuation valuation,
-               const LogicInfo& logicInfo,
-               QuantifiersEngine* qe);
+               const LogicInfo& logicInfo);
 
   void check(Effort);
 
diff --git a/contrib/new-theory b/contrib/new-theory
index c1478a980..1868fecec 100755
--- a/contrib/new-theory
+++ b/contrib/new-theory
@@ -121,10 +121,12 @@ function copyaltskel {
 
 # copy files from the skeleton, with proper replacements
 if $alternate; then
+  alternate01=1
   for file in `ls contrib/alttheoryskel`; do
     copyaltskel "$file"
   done
 else
+  alternate01=0
   for file in `ls contrib/theoryskel`; do
     copyskel "$file"
   done
@@ -150,7 +152,7 @@ echo "Adding sources to src/Makefile.am..."
 
 perl -e '
   while(<>) { print; last if /^libcvc4_la_SOURCES = /; }
-  if('$alternate') {
+  if('$alternate01') {
     while(<>) { if(!/\\$/) { chomp; print "$_ \\\n\ttheory/'"$dir"'/theory_'"$dir"'.h \\\n\ttheory/'"$dir"'/theory_'"$dir"'.cpp\n"; last; } else { print; } }
   } else {
     while(<>) { if(!/\\$/) { chomp; print "$_ \\\n\ttheory/'"$dir"'/theory_'"$dir"'.h \\\n\ttheory/'"$dir"'/theory_'"$dir"'.cpp \\\n\ttheory/'"$dir"'/theory_'"$dir"'_rewriter.h \\\n\ttheory/'"$dir"'/theory_'"$dir"'_type_rules.h\n"; last; } else { print; } }
diff --git a/contrib/theoryskel/theory_DIR.cpp b/contrib/theoryskel/theory_DIR.cpp
index aefa0a2af..72101a5a6 100644
--- a/contrib/theoryskel/theory_DIR.cpp
+++ b/contrib/theoryskel/theory_DIR.cpp
@@ -11,9 +11,8 @@ Theory$camel::Theory$camel(context::Context* c,
                            context::UserContext* u,
                            OutputChannel& out,
                            Valuation valuation,
-                           const LogicInfo& logicInfo,
-                           QuantifiersEngine* qe) :
-  Theory(THEORY_$id, c, u, out, valuation, logicInfo, qe) {
+                           const LogicInfo& logicInfo) :
+  Theory(THEORY_$id, c, u, out, valuation, logicInfo) {
 }/* Theory$camel::Theory$camel() */
 
 void Theory$camel::check(Effort level) {
diff --git a/contrib/theoryskel/theory_DIR.h b/contrib/theoryskel/theory_DIR.h
index 9dfb3e614..d8e652b7c 100644
--- a/contrib/theoryskel/theory_DIR.h
+++ b/contrib/theoryskel/theory_DIR.h
@@ -17,8 +17,7 @@ public:
                context::UserContext* u,
                OutputChannel& out,
                Valuation valuation,
-               const LogicInfo& logicInfo,
-               QuantifiersEngine* qe);
+               const LogicInfo& logicInfo);
 
   void check(Effort);