CVC4 - Revision history

Clark Barrett at 01:27, 1 December 2012

2012-12-01T01:27:39Z

Mdeters at 22:09, 17 September 2012

2012-09-17T22:09:28Z

Mdeters at 20:48, 17 September 2012

2012-09-17T20:48:43Z

Mdeters at 20:41, 17 September 2012

2012-09-17T20:41:23Z

Mdeters: moved CVC Portal to CVC4

2012-09-17T20:37:10Z

moved CVC Portal to CVC4

Clark Barrett at 17:49, 16 May 2012

2012-05-16T17:49:02Z

Mdeters at 16:16, 10 February 2012

2012-02-10T16:16:26Z

Mdeters at 04:06, 22 July 2011

2011-07-22T04:06:15Z

Lianah at 20:11, 30 March 2011

2011-03-30T20:11:45Z

Mdeters at 20:52, 18 March 2011

2011-03-18T20:52:53Z

@@ Line 9: / Line 9: @@
 * an interactive text-based interface;
 * a rich [http://church.cims.nyu.edu/cvc4-builds/documentation/public/latest/ C++ API] for embedding in other systems;
-* proof and model generation abilities;
+* model generation abilities;
-* predicate subtyping;
+* source compatibility with much of the CVC3 API via a "compatibility library";
 * source compatibility with much the CVC3 API via a "compatibility library";
 * essentially no limit on its use for research or commercial purposes (see [http://church.cims.nyu.edu/cvc4-builds/documentation/public/latest/COPYING_source.html license]).

@@ Line 8: / Line 8: @@
 * support for quantifiers;
 * an interactive text-based interface;
-* a rich C++ API for embedding in other systems;
+* a rich [http://church.cims.nyu.edu/cvc4-builds/documentation/public/latest/ C++ API] for embedding in other systems;
 * proof and model generation abilities;
 * predicate subtyping;
 * source compatibility with much the CVC3 API via a "compatibility library";
 * essentially no limit on its use for research or commercial purposes (see [http://church.cims.nyu.edu/cvc4-builds/documentation/public/latest/COPYING_source.html license]).

@@ Line 12: / Line 12: @@
 * predicate subtyping;
 * source compatibility with much the CVC3 API via a "compatibility library";
-* essentially no limit on its use for research or commercial purposes (see [[CVC4 License|license]]).
+* essentially no limit on its use for research or commercial purposes (see [http://church.cims.nyu.edu/cvc4-builds/documentation/public/latest/COPYING_source.html license]).

@@ Line 1: / Line 1: @@
-Welcome to the CVC portal and CVC4 developers' wiki.  This service is only intended for the developers of CVC4 at [http://www.nyu.edu/ NYU] and [http://www.uiowa.edu/ UIowa].
+CVC4 is an automatic theorem prover for Satisfiability Modulo Theories (SMT) problems. It can be used to prove the validity (or, dually, the satisfiability) of first-order formulas in a large number of built-in logical theories and their combination.
-A valid login is required for many of these links.
+CVC4 is the most recent of a series of popular SMT provers, which originated at Stanford University with the SVC system. CVC4 is a from-scratch redesign and reimplementation of earlier solvers; it is designed for flexibility as a research tool and performance as an industrial SMT solver.
-'''Relevant to CVC4 development:'''
+CVC4 works with a version of first-order logic and has a wide variety of features including:
-* [[Developer Meeting Minutes]]<ul>{{#ifexist: Meeting Minutes - {{#timel:F j, Y}}|<li>[[Meeting Minutes - {{#timel:F j, Y}}|'''Today's meeting''' - {{#timel:D M j}}]]</li>}}{{#if: {{mtglinks_recent}}|<li>'''Recent meetings:''' {{mtglinks_recent}}</li>}}{{#if: {{mtglinks_upcoming}}|<li>'''Upcoming meetings:''' {{mtglinks_upcoming}}</li>}}</ul>
-* [http://church.cims.nyu.edu/~mdeters/cvc4-devel.logs/ cvc4-devel IRC logs]
-* [[CVC4 Contest|CVC4 Contest]]
-* [[CVC4 Wishlist|CVC4 wishlist]]
-* [[Developer's Guide]]
-* [[User's Manual]]
-* [[How do I... ?]]
-* [[Library|Our library: bibliographical references of interest]]
-* [[To Discuss|Items "yet to discuss"]]
-* [[CVC4 Parsing]]
-* [[How to write a theory in CVC4]]
-'''Some CVC3 resources:'''
+* several built-in base theories: rational and integer linear arithmetic, arrays, tuples, records, inductive data types, bit vectors, and equality over uninterpreted function symbols;
-* [http://www.cs.nyu.edu/acsys/bugs/ CVC3 Bugzilla]
+* support for quantifiers;
-* [http://www.cs.nyu.edu/acsys/cvc3/wiki CVC3 Wiki]
+* an interactive text-based interface;
-* [http://cs.nyu.edu/mailman/listinfo/cvc-devel Mailing list]
+* a rich C++ API for embedding in other systems;
-* [http://cs.nyu.edu/acsys/cvc3/ CVC3 public page]
+* proof and model generation abilities;
-* [[Fuzz-testing, October 2009|Results of Fuzz-testing CVC3 prior to release]]
+* predicate subtyping;
+* source compatibility with much the CVC3 API via a "compatibility library";
-'''Some CVC4 resources:'''
+* essentially no limit on its use for research or commercial purposes (see [[CVC4 License|license]]).
-* [http://church.cims.nyu.edu/bugzilla/ CVC4 Bugzilla]
-* [http://cs.nyu.edu/mailman/listinfo/cvc4-devel Mailing list]
-<!--* [[CVC3 Benchmarking|CVC3 benchmarking useful for CVC4 design]] {{NEW}}-->
-−
-'''Relevant to this wiki:'''
-* [[User Registration|User registration]]
-* [[Developer Resources|Developer resources]]
-* [[Using SSL with Church]]
-−
-To register as a new user, or recommend someone for an account, contact [http://cs.nyu.edu/~dejan/ Dejan] or [http://cs.nyu.edu/~mdeters/ Morgan].

@@ Line 5: / Line 5: @@
 '''Relevant to CVC4 development:'''
 * [[Developer Meeting Minutes]]<ul>{{#ifexist: Meeting Minutes - {{#timel:F j, Y}}|<li>[[Meeting Minutes - {{#timel:F j, Y}}|'''Today's meeting''' - {{#timel:D M j}}]]</li>}}{{#if: {{mtglinks_recent}}|<li>'''Recent meetings:''' {{mtglinks_recent}}</li>}}{{#if: {{mtglinks_upcoming}}|<li>'''Upcoming meetings:''' {{mtglinks_upcoming}}</li>}}</ul>
 * [[CVC4 Contest|CVC4 Contest]]
 * [[CVC4 Wishlist|CVC4 wishlist]]

← Older revision	Revision as of 20:37, 17 September 2012
(No difference)