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

diff --git a/.travis.yml b/.travis.yml
index 9b8482c000505aecc6b825a60126d27127dca5a8..10eea921bcddfa92b84158b4781e734abf620944 100644 (file)
--- 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 eca07e90917b07a1c847b52075e9a6f8fe491770..83d837322bf0862ebb48c34bfef5bc6221a1e1dc 100644 (file)
--- 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 9dfb3e614302a90670e37b299735d77fb33e5493..d8e652b7c75083cdd1a3e0f2e16ce5b8435f6a5a 100644 (file)
--- 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 c1478a980beb24c68c3cae1d1ae4bff2d7e00497..1868fecec0c4314bd4746ee1f042186a5eb59cb3 100755 (executable)
--- 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 aefa0a2af1fea7823624f988d66924233814d499..72101a5a660ac08b01769f86056458d6d23c3a8b 100644 (file)
--- 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 9dfb3e614302a90670e37b299735d77fb33e5493..d8e652b7c75083cdd1a3e0f2e16ce5b8435f6a5a 100644 (file)
--- 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);