From 75d15b2cd923f92fd26020e0c8d1786b4396d608 Mon Sep 17 00:00:00 2001 From: Clark Barrett Date: Mon, 2 Apr 2018 13:35:24 -0700 Subject: [PATCH] Remove references to nyu (#1721) --- NEWS | 1 - configure.ac | 2 +- contrib/alttheoryskel/README.WHATS-NEXT | 8 +- contrib/cvc-mode.el | 2 +- contrib/get-authors | 3 +- contrib/get-bug-attachments | 92 ------------------- contrib/theoryskel/README.WHATS-NEXT | 11 ++- contrib/update-copyright.pl | 3 +- doc/SmtEngine.3cvc_template.in | 2 +- doc/cvc4.1_template.in | 2 +- doc/cvc4.5.in | 2 +- doc/libcvc4.3.in | 2 +- doc/libcvc4compat.3.in | 2 +- doc/libcvc4parser.3.in | 2 +- doc/mainpage.md | 2 +- doc/options.3cvc_template.in | 2 +- examples/README | 3 +- src/parser/cvc/Cvc.g | 3 +- src/smt/smt_engine.cpp | 2 +- test/regress/regress1/auflia/bug330.smt2 | 2 +- test/regress/regress1/rewriterules/read5.smt2 | 2 +- test/regress/regress3/pp-regfile.smt | 2 +- 22 files changed, 28 insertions(+), 124 deletions(-) delete mode 100755 contrib/get-bug-attachments 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 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 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 -# 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 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 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 -- 2.30.2