diff options
| -rw-r--r-- | .travis.yml | 8 | ||||
| -rw-r--r-- | contrib/alttheoryskel/theory_DIR.cpp | 5 | ||||
| -rw-r--r-- | contrib/alttheoryskel/theory_DIR.h | 3 | ||||
| -rwxr-xr-x | contrib/new-theory | 4 | ||||
| -rw-r--r-- | contrib/theoryskel/theory_DIR.cpp | 5 | ||||
| -rw-r--r-- | contrib/theoryskel/theory_DIR.h | 3 |
6 files changed, 16 insertions, 12 deletions
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); |