Remove references to nyu (#1721)

22 files changed, 28 insertions, 124 deletions

diff --git a/NEWS b/NEWS
index ff135d1ce..f23833bb6 100644
--- a/NEWS
+++ b/NEWS
@@ -126,4 +126,3 @@ Changes since 1.0
   "unsat") as well.  Now, single -q silences messages and warnings, and
   double -qq silences all output (except on exception or signal).
 
--- Morgan Deters <mdeters@cs.nyu.edu>  Wed, 02 Jul 2014 14:45:05 -0400
diff --git a/configure.ac b/configure.ac
index a279da5cb..fb225b688 100644
--- a/configure.ac
+++ b/configure.ac
@@ -11,7 +11,7 @@ dnl Preprocess CL args. Defined in config/cvc4.m4
 CVC4_AC_INIT
 
 AC_PREREQ([2.61])
-AC_INIT([cvc4], _CVC4_RELEASE_STRING, [cvc-bugs@cs.nyu.edu])
+AC_INIT([cvc4], _CVC4_RELEASE_STRING, [cvc4-bugs@cs.stanford.edu])
 AC_CONFIG_SRCDIR([src/include/cvc4_public.h])
 AC_CONFIG_AUX_DIR([config])
 AC_CONFIG_MACRO_DIR([config])
diff --git a/contrib/alttheoryskel/README.WHATS-NEXT b/contrib/alttheoryskel/README.WHATS-NEXT
index c6ad91c3f..c0237c300 100644
--- a/contrib/alttheoryskel/README.WHATS-NEXT
+++ b/contrib/alttheoryskel/README.WHATS-NEXT
@@ -13,13 +13,13 @@ Your next steps will likely be:
 
 You'll probably find the Developer's wiki useful:
 
-  http://cvc4.cs.nyu.edu/wiki/
+  http://cvc4.cs.stanford.edu/wiki/
 
-...and in particular the Developer's Guide:
+...and the Developer's Guide:
 
-  http://cvc4.cs.nyu.edu/wiki/Developer%27s_Guide
+  https://github.com/CVC4/CVC4/wiki/Developer-Guide
 
 which contains coding guidelines for the CVC4 project.
 
-Good luck, and please contact cvc4-devel@cs.nyu.edu for assistance
+Good luck, and please contact cvc4-devel@cs.stanford.edu for assistance
 should you need it!
diff --git a/contrib/cvc-mode.el b/contrib/cvc-mode.el
index f159944dd..e32c0c439 100644
--- a/contrib/cvc-mode.el
+++ b/contrib/cvc-mode.el
@@ -644,7 +644,7 @@ process will leave its output. Currently, each run of CVC clears the
 compilation buffer. If you need to save multiple runs, save them one
 at a time.
 
-Please report bugs to barrett@cs.nyu.edu."
+Please report bugs to barrett@cs.stanford.edu."
   (interactive)
   (use-local-map cvc-mode-map)
 ;;; Disable asking for the compile command
diff --git a/contrib/get-authors b/contrib/get-authors
index a888d38f3..59187a81c 100755
--- a/contrib/get-authors
+++ b/contrib/get-authors
@@ -1,8 +1,7 @@
 #!/bin/sh
 #
 # get-authors
-# Morgan Deters <mdeters@cs.nyu.edu> for CVC4
-# Copyright (c) 2009-2014  The CVC4 Project
+# Copyright (c) 2009-2018  The CVC4 Project
 #
 # usage: get-authors [ files... ]
 #
diff --git a/contrib/get-bug-attachments b/contrib/get-bug-attachments
deleted file mode 100755
index 80205baff..000000000
--- a/contrib/get-bug-attachments
+++ /dev/null
@@ -1,92 +0,0 @@
-#!/bin/bash
-#
-# get-bug-attachments
-# Morgan Deters <mdeters@cs.nyu.edu>
-# Wed, 26 Sep 2012 09:40:10 -0400
-#
-
-if [ $# -lt 1 ]; then
-  echo "usage: `basename $0` bugids.." >&2
-  exit 1
-fi
-
-while [ $# -gt 0 ]; do
-
-bugid="$1"
-shift
-
-function webcat {
-  if which wget &>/dev/null; then
-    wget -O - "$1"
-  elif which curl &>/dev/null; then
-    curl "$1"
-  else
-    echo "Please install wget or curl." >&2;
-    exit 1
-  fi
-}
-
-function webget {
-  if which wget &>/dev/null; then
-    tmpfile="$(mktemp get_bug_attach.$$.XXXXXXXX)"
-    filename="$(wget -qS -O "$tmpfile" "$1" 2>&1 | grep -i 'Content-disposition: attachment' | sed 's,.*filename="\(.*\)".*,\1,')"
-    ext="$(echo "$filename" | sed 's,.*\.\(.*\),\1,')"
-    if [ -e "$2.$ext" ] && ! diff -q "$tmpfile" "$2.$ext" &>/dev/null; then
-      c=a
-      while [ -e "$2$c.$ext" ] && ! diff -q "$tmpfile" "$2$c.$ext" &>/dev/null; do
-        c=$(echo $c | tr a-y b-z)
-      done
-      mkdir -p "$(dirname "$2")"
-      mv "$tmpfile" "$2$c.$ext"
-      echo "$2$c.$ext"
-    else
-      mkdir -p "$(dirname "$2")"
-      mv "$tmpfile" "$2.$ext"
-      echo "$2.$ext"
-    fi
-  elif which curl &>/dev/null; then
-    tmpfile="$(mktemp get_bug_attach.$$.XXXXXXXX)"
-    filename="$(curl --head "$1" 2>&1 | grep -i 'Content-disposition: attachment' | sed 's,.*filename="\(.*\)".*,\1,')"
-    curl "$1" >"$tmpfile" 2>/dev/null
-    ext="$(echo "$filename" | sed 's,.*\.\(.*\),\1,')"
-    if [ -e "$2.$ext" ] && ! diff -q "$tmpfile" "$2.$ext" &>/dev/null; then
-      c=a
-      while [ -e "$2$c.$ext" ] && ! diff -q "$tmpfile" "$2$c.$ext" &>/dev/null; do
-        c=$(echo $c | tr a-y b-z)
-      done
-      mkdir -p "$(dirname "$2")"
-      mv "$tmpfile" "$2$c.$ext"
-      echo "$2$c.$ext"
-    else
-      mkdir -p "$(dirname "$2")"
-      mv "$tmpfile" "$2.$ext"
-      echo "$2.$ext"
-    fi
-  else
-    echo "Please install wget or curl." >&2;
-    exit 1
-  fi
-}
-
-count=0
-for attachment in $(\
-  webcat "http://cvc4.cs.nyu.edu/bugs/show_bug.cgi?id=$bugid" 2>/dev/null \
-  | grep ' href="attachment.cgi?id=[0-9][0-9]*' \
-  | sed 's,.* href="attachment.cgi?id=\([0-9][0-9]*\).*,\1,' \
-  | sort -nu); do
-
-  let count++
-  printf "%-30s " "Downloading attachment $attachment..."
-  webget "http://cvc4.cs.nyu.edu/bugs/attachment.cgi?id=$attachment" "test/regress/regress0/bug$bugid"
-
-done
-
-if [ $count -eq 0 ]; then
-  echo "There are no bug attachments for bug #$bugid."
-else
-  s=s
-  [ $count -eq 1 ] && s=
-  echo "Downloaded $count bug attachment$s for bug #$bugid."
-fi
-
-done
diff --git a/contrib/theoryskel/README.WHATS-NEXT b/contrib/theoryskel/README.WHATS-NEXT
index 17affade4..213004d5b 100644
--- a/contrib/theoryskel/README.WHATS-NEXT
+++ b/contrib/theoryskel/README.WHATS-NEXT
@@ -17,7 +17,8 @@ Your next steps will likely be:
 * to write parser rules in src/parser/cvc/Cvc.g to support the CVC input
   language, src/parser/smt/Smt.g to support the (deprecated) SMT-LIBv1
   language, and src/parser/smt2/Smt2.g to support SMT-LIBv2
-* to write printer code in src/printer/*/*_printer* to support printing
+* to write printer code in
+src/printer/*/*_printer* to support printing
   your theory terms and types in various output languages
 
 and finally:
@@ -33,13 +34,13 @@ and finally:
 
 You'll probably find the Developer's wiki useful:
 
-  http://cvc4.cs.nyu.edu/wiki/
+  http://cvc4.cs.stanford.edu/wiki/
 
-...and in particular the Developer's Guide:
+...and the Developer's Guide:
 
-  http://cvc4.cs.nyu.edu/wiki/Developer%27s_Guide
+  https://github.com/CVC4/CVC4/wiki/Developer-Guide
 
 which contains coding guidelines for the CVC4 project.
 
-Good luck, and please contact cvc4-devel@cs.nyu.edu for assistance
+Good luck, and please contact cvc4-devel@cs.stanford.edu for assistance
 should you need it!
diff --git a/contrib/update-copyright.pl b/contrib/update-copyright.pl
index d0dd33cbb..e052430c7 100755
--- a/contrib/update-copyright.pl
+++ b/contrib/update-copyright.pl
@@ -1,8 +1,7 @@
 #!/usr/bin/perl -w
 #
 # update-copyright.pl
-# Morgan Deters <mdeters@cs.nyu.edu> for CVC4
-# Copyright (c) 2009-2014  The CVC4 Project
+# Copyright (c) 2009-2018  The CVC4 Project
 #
 # usage: update-copyright [-m] [files/directories...]
 #        update-copyright [-h | --help]
diff --git a/doc/SmtEngine.3cvc_template.in b/doc/SmtEngine.3cvc_template.in
index b240dd8d2..7eaa69cf1 100644
--- a/doc/SmtEngine.3cvc_template.in
+++ b/doc/SmtEngine.3cvc_template.in
@@ -52,4 +52,4 @@ contributors.
 
 Additionally, the CVC4 wiki contains useful information about the
 design and internals of CVC4.  It is maintained at
-.BR http://cvc4.cs.nyu.edu/wiki/ .
+.BR http://cvc4.cs.stanford.edu/wiki/ .
diff --git a/doc/cvc4.1_template.in b/doc/cvc4.1_template.in
index a0535553b..90ae938ab 100644
--- a/doc/cvc4.1_template.in
+++ b/doc/cvc4.1_template.in
@@ -129,4 +129,4 @@ contributors.
 
 Additionally, the CVC4 wiki contains useful information about the
 design and internals of CVC4.  It is maintained at
-.BR http://cvc4.cs.nyu.edu/wiki/ .
+.BR http://cvc4.cs.stanford.edu/wiki/ .
diff --git a/doc/cvc4.5.in b/doc/cvc4.5.in
index b54f23560..c8629bffa 100644
--- a/doc/cvc4.5.in
+++ b/doc/cvc4.5.in
@@ -18,4 +18,4 @@ to background theories of interest.
 
 Additionally, the CVC4 wiki contains useful information about the
 design and internals of CVC4.  It is maintained at
-.BR http://cvc4.cs.nyu.edu/wiki/ .
+.BR http://cvc4.cs.stanford.edu/wiki/ .
diff --git a/doc/libcvc4.3.in b/doc/libcvc4.3.in
index f85a909dd..bf5fde577 100644
--- a/doc/libcvc4.3.in
+++ b/doc/libcvc4.3.in
@@ -62,4 +62,4 @@ is used primarily to make assertions, check satisfiability/validity, and extract
 
 Additionally, the CVC4 wiki contains useful information about the
 design and internals of CVC4.  It is maintained at
-.BR http://goedel.cs.nyu.edu/wiki/ .
+.BR http://goedel.cs.stanford.edu/wiki/ .
diff --git a/doc/libcvc4compat.3.in b/doc/libcvc4compat.3.in
index 3aa58b712..fbb21e6a8 100644
--- a/doc/libcvc4compat.3.in
+++ b/doc/libcvc4compat.3.in
@@ -12,4 +12,4 @@ libcvc4compat \- a CVC3 compatibility library interface for the CVC4 theorem pro
 
 Additionally, the CVC4 wiki contains useful information about the
 design and internals of CVC4.  It is maintained at
-.BR http://cvc4.cs.nyu.edu/wiki/ .
+.BR http://cvc4.cs.stanford.edu/wiki/ .
diff --git a/doc/libcvc4parser.3.in b/doc/libcvc4parser.3.in
index 09fea23f1..7971a8822 100644
--- a/doc/libcvc4parser.3.in
+++ b/doc/libcvc4parser.3.in
@@ -12,4 +12,4 @@ libcvc4parser \- a parser library interface for the CVC4 theorem prover
 
 Additionally, the CVC4 wiki contains useful information about the
 design and internals of CVC4.  It is maintained at
-.BR http://cvc4.cs.nyu.edu/wiki/ .
+.BR http://cvc4.cs.stanford.edu/wiki/ .
diff --git a/doc/mainpage.md b/doc/mainpage.md
index 8c801aa14..13005e023 100644
--- a/doc/mainpage.md
+++ b/doc/mainpage.md
@@ -8,7 +8,7 @@ The main classes of the CVC4 API are:
 - CVC4::SmtEngine - the SMT interface, permits making assertions and checking satisfiability (create one of these for your application)
 
 There are numerous examples of the use of the C++ API in the examples/api directory of the CVC4 source distribution.  There is also a discussion on our CVC4 Wiki at
-http://cvc4.cs.nyu.edu/wiki/Tutorials#C.2B.2B_API
+http://cvc4.cs.stanford.edu/wiki/Tutorials#C.2B.2B_API
 
 Using the CVC4 API from Java
 
diff --git a/doc/options.3cvc_template.in b/doc/options.3cvc_template.in
index e72363b62..477963036 100644
--- a/doc/options.3cvc_template.in
+++ b/doc/options.3cvc_template.in
@@ -40,4 +40,4 @@ contributors.
 
 Additionally, the CVC4 wiki contains useful information about the
 design and internals of CVC4.  It is maintained at
-.BR http://cvc4.cs.nyu.edu/wiki/ .
+.BR http://cvc4.cs.stanford.edu/wiki/ .
diff --git a/examples/README b/examples/README
index 5f5bb0980..df8cffe73 100644
--- a/examples/README
+++ b/examples/README
@@ -1,6 +1,6 @@
 This directory contains usage examples of CVC4's different language
 bindings, library APIs, and also tutorial examples from the tutorials
-available at http://cvc4.cs.nyu.edu/wiki/Tutorials
+available at http://cvc4.cs.stanford.edu/wiki/Tutorials
 
 *** Files named SimpleVC*, simple_vc*
 
@@ -31,4 +31,3 @@ source.  After building CVC4, you can run "make examples".  You'll
 find the built binaries in builds/examples (or just in "examples" if
 you configured a build directory outside of the source tree).
 
--- Morgan Deters <mdeters@cs.nyu.edu>  Tue, 24 Dec 2013 09:12:59 -0500
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 6337fb5f6..47bee5740 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -1729,8 +1729,7 @@ postfixTerm[CVC4::Expr& f]
       /* left- or right-shift */
     | ( LEFTSHIFT_TOK { left = true; }
       | RIGHTSHIFT_TOK { left = false; } ) k=numeral
-      { // Defined in:
-        // http://www.cs.nyu.edu/acsys/cvc3/doc/user_doc.html#user_doc_pres_lang_expr_bit
+      { 
         if(left) {
           f = MK_EXPR(kind::BITVECTOR_CONCAT, f, MK_CONST(BitVector(k)));
         } else {
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 8450307db..a329541e5 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -4563,7 +4563,7 @@ void SmtEnginePrivate::processAssertions() {
         d_assertions[d_realAssertionsEnd - 1] = Rewriter::rewrite(Node(builder));
       }
       // TODO(b/1256): For some reason this is needed for some benchmarks, such as
-      // http://cvc4.cs.nyu.edu/benchmarks/smtlib2/QF_AUFBV/dwp_formulas/try5_small_difret_functions_dwp_tac.re_node_set_remove_at.il.dwp.smt2
+      // QF_AUFBV/dwp_formulas/try5_small_difret_functions_dwp_tac.re_node_set_remove_at.il.dwp.smt2
       removeITEs();
       applySubstitutionsToAssertions();
       //      Assert(iteRewriteAssertionsEnd == d_assertions.size());
diff --git a/test/regress/regress1/auflia/bug330.smt2 b/test/regress/regress1/auflia/bug330.smt2
index d05a8b2a0..ce787e2e7 100644
--- a/test/regress/regress1/auflia/bug330.smt2
+++ b/test/regress/regress1/auflia/bug330.smt2
@@ -1,7 +1,7 @@
 (set-logic QF_AUFLIA)
 (set-info :source |
 Translated from old SVC processor verification benchmarks.  Contact Clark
-Barrett at barrett@cs.nyu.edu for more information.
+Barrett at barrett@cs.stanford.edu for more information.
 
 This benchmark was automatically translated into SMT-LIB format from
 CVC format using CVC Lite
diff --git a/test/regress/regress1/rewriterules/read5.smt2 b/test/regress/regress1/rewriterules/read5.smt2
index 2cd6eb244..0f92effcb 100644
--- a/test/regress/regress1/rewriterules/read5.smt2
+++ b/test/regress/regress1/rewriterules/read5.smt2
@@ -2,7 +2,7 @@
 (set-logic AUF)
 (set-info :source |
 Translated from old SVC processor verification benchmarks.  Contact Clark
-Barrett at barrett@cs.nyu.edu for more information.
+Barrett at barrett@cs.stanford.edu for more information.
 
 This benchmark was automatically translated into SMT-LIB format from
 CVC format using CVC Lite
diff --git a/test/regress/regress3/pp-regfile.smt b/test/regress/regress3/pp-regfile.smt
index e60be055a..0b9d07b84 100644
--- a/test/regress/regress3/pp-regfile.smt
+++ b/test/regress/regress3/pp-regfile.smt
@@ -1,7 +1,7 @@
 (benchmark pp_regfile.smt
   :source {
 Translated from old SVC processor verification benchmarks.  Contact Clark
-Barrett at barrett@cs.nyu.edu for more information.
+Barrett at barrett@cs.stanford.edu for more information.
 
 This benchmark was automatically translated into SMT-LIB format from
 CVC format using CVC Lite