Remove references to nyu (cvc5#1721)

timothy-king · Apr 2, 2018 · 75d15b2 · 75d15b2
1 parent a917cc2
commit 75d15b2
Show file tree

Hide file tree

Showing 22 changed files with 28 additions and 124 deletions.
diff --git 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 <[email protected]>  Wed, 02 Jul 2014 14:45:05 -0400
diff --git 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
@@ -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
@@ -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
@@ -1,8 +1,7 @@
 #!/bin/sh
 #
 # get-authors
-# Morgan Deters <[email protected]> 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
diff --git 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
@@ -1,8 +1,7 @@
 #!/usr/bin/perl -w
 #
 # update-copyright.pl
-# Morgan Deters <[email protected]> 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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 <[email protected]>  Tue, 24 Dec 2013 09:12:59 -0500
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
Original file line number	Diff line number	Diff line change
Expand Up		@@ -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 <[email protected]> Wed, 02 Jul 2014 14:45:05 -0400