From e256d610ca0db37e964b9a2b4530470e8589b958 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Wed, 24 Apr 2019 11:46:33 -0700 Subject: [PATCH] README: Remove project leaders, history. --- README.md | 50 ++------------------------------------------------ 1 file changed, 2 insertions(+), 48 deletions(-) diff --git a/README.md b/README.md index 09f8a0dcc..faef42e66 100644 --- a/README.md +++ b/README.md @@ -57,7 +57,8 @@ We recommend that you visit our CVC4 tutorials online at: for help getting started using CVC4. If you need help with using CVC4, please refer to -[http://cvc4.stanford.edu/#Technical_Support](http://cvc4.stanford.edu/#Technical_Support). +[http://cvc4.stanford.edu#technical-support]( + http://cvc4.stanford.edu#technical-support). If you are using CVC4 in your work, or incorporating it into software of your own, we'd like to invite you to leave a description and link to your @@ -79,55 +80,8 @@ Contributing Please refer to our [contributing guidelines](CONTRIBUTING.md). -Project Leaders -------------------------------------------------------------------------------- - -* [Clark Barrett](http://theory.stanford.edu/~barrett/) (Stanford University) -* [Cesare Tinelli](http://homepage.cs.uiowa.edu/~tinelli/) (The University of Iowa) - - Authors ------------------------------------------------------------------------------- For a full list of authors, please refer to the [AUTHORS](https://github.com/CVC4/CVC4/blob/master/AUTHORS) file. - -History -------------------------------------------------------------------------------- - -The Cooperating Validity Checker series has a long history. The Stanford -Validity Checker (SVC) came first in 1996, incorporating theories and its own -SAT solver. Its successor, the Cooperating Validity Checker (CVC), had a more -optimized internal design, produced proofs, used the Chaff SAT solver, and -featured a number of usability enhancements. Its name comes from the -cooperative nature of decision procedures in Nelson-Oppen theory combination, -which share amongst each other equalities between shared terms. - -CVC Lite, first made available in 2003, was a rewrite of CVC that attempted to -make CVC more flexible (hence the "lite") while extending the feature set: CVC -Lite supported quantifiers where its predecessors did not. - -CVC3 was a major overhaul of portions of CVC Lite: it added better decision -procedure implementations, added support for using MiniSat in the core, and had -generally better performance. - -CVC4 is the fifth generation of this validity checker line. It represents a -complete re-evaluation of the core architecture to be both performant and to -serve as a cutting-edge research vehicle for the next several years. Rather -than taking CVC3 and redesigning problem parts, we've taken a clean-room -approach, starting from scratch. Before using any designs from CVC3, we have -thoroughly scrutinized, vetted, and updated them. Many parts of CVC4 bear only -a superficial resemblance, if any, to their correspondent in CVC3. - -However, CVC4 is fundamentally similar to CVC3 and many other modern SMT -solvers: it is a DPLL(T) solver, with a SAT solver at its core and a delegation -path to different decision procedure implementations, each in charge of solving -formulas in some background theory. - -The re-evaluation and ground-up rewrite was necessitated, we felt, by the -performance characteristics of CVC3. CVC3 has many useful features, but some -core aspects of the design led to high memory use, and the use of heavyweight -computation (where more nimble engineering approaches could suffice) makes CVC3 -a much slower prover than other tools. As these designs are central to CVC3, a -new version was preferable to a selective re-engineering, which would have -ballooned in short order. -- 2.30.2