"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
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])
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!
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
#!/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... ]
#
+++ /dev/null
-#!/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
* 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:
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!
#!/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]
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/ .
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/ .
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/ .
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/ .
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/ .
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/ .
- 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
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/ .
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*
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
/* 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 {
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());
(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
(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
(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
projects / cvc5.git / commitdiff