From 9af3f271937cb9389f8e5b8f1b302f48bc6cdd9a Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Mon, 31 Mar 2014 16:07:58 -0400
Subject: Travis-CI test for new-theory script, also related bugfixes.

---
 contrib/alttheoryskel/theory_DIR.cpp | 5 ++---
 contrib/alttheoryskel/theory_DIR.h   | 3 +--
 contrib/new-theory                   | 4 +++-
 contrib/theoryskel/theory_DIR.cpp    | 5 ++---
 contrib/theoryskel/theory_DIR.h      | 3 +--
 5 files changed, 9 insertions(+), 11 deletions(-)

(limited to 'contrib')

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);
 
-- 
cgit v1.2.3