From: Andres Nötzli Date: Tue, 4 Jul 2017 05:56:10 +0000 (-0700) Subject: Update README for 1.5 release (#182) X-Git-Tag: cvc5-1.0.0~5749 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c1723f63f0124635a017295502f16c5e7739bec4;p=cvc5.git Update README for 1.5 release (#182) --- diff --git a/README b/README index ac3068536..da2457fed 100644 --- a/README +++ b/README @@ -1,15 +1,15 @@ This is CVC4 release version 1.5. For build and installation notes, please see the INSTALL file included with this distribution. -The project leaders are Clark Barrett (Stanford University) and Cesare Tinelli -(The University of Iowa). For a full list of authors, please refer to the -AUTHORS file in the source distribution. +The project leaders are Clark Barrett (Stanford University) and Cesare +Tinelli (The University of Iowa). For a full list of authors, please +refer to the AUTHORS file in the source distribution. CVC4 is a tool for determining the satisfiability of a first order formula modulo a first order theory (or a combination of such -theories). It is the fourth in the Cooperating Validity Checker family -of tools (CVC, CVC Lite, CVC3) but does not directly incorporate code -from any previous version. +theories). It is the fourth in the Cooperating Validity Checker +family of tools (CVC, CVC Lite, CVC3) but does not directly +incorporate code from any previous version. CVC4 is intended to be an open and extensible SMT engine. It can be used as a stand-alone tool or as a library. It has been designed to @@ -37,20 +37,21 @@ We are always happy to hear feedback from our users: http://cvc4.stanford.edu/#Technical_Support. * if you need to report a bug with CVC4, or make a feature request, - please visit our bugtracker at http://cvc4.cs.stanford.edu/bugs/ or write - to the cvc-bugs@cs.stanford.edu mailing list. We are very grateful for - bug reports, as they help us improve CVC4, and patches are generally - reviewed and accepted quickly. + please visit our bugtracker at http://cvc4.cs.stanford.edu/bugs/ or + write to the cvc-bugs@cs.stanford.edu mailing list. We are very + grateful for bug reports, as they help us improve CVC4, and patches + are generally reviewed and accepted quickly. * 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 project/software on our "Third Party Applications" - page at http://cvc4.cs.stanford.edu/wiki/Public:Third_Party_Applications + page at + http://cvc4.cs.stanford.edu/wiki/Public:Third_Party_Applications -* if you are interested in contributing code (for example, a new decision - procedure implementation) to the CVC4 project, please contact one of the - project leaders. We'd be happy to point you to some internals documentation - to help you out. +* if you are interested in contributing code (for example, a new + decision procedure implementation) to the CVC4 project, please + contact one of the project leaders. We'd be happy to point you to + some internals documentation to help you out. Thank you for using CVC4! @@ -72,14 +73,14 @@ procedure implementations, added support for using MiniSat in the core, and had generally better performance. CVC4 is the new version, the fifth generation of this validity checker -line that is now celebrating sixteen years of heritage. 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. +line that is now celebrating twenty-one years of heritage. 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 @@ -97,4 +98,5 @@ in short order. *** For more information -More information about CVC4 is available at: http://cvc4.cs.stanford.edu/ +More information about CVC4 is available at: +http://cvc4.cs.stanford.edu/