README

Go to the documentation of this file.

/*!\page README README

This is a distribution of the CVC Lite source code.  Its use is
governed by the terms set forth in the accompanying file \ref LICENSE.

For instructions on compiling and installing the code, see \ref INSTALL.

<!--<h2>Feedback</h2>

We appreciate any feedback and bug reports from the users.  Please contact 

.  Bug
reports should be filed through our Savannah interface at:

<pre>
   http://chicory.stanford.edu/savannah/bugs/?func=addbug&group=cvcl
</pre>

or submitted to <tt>cvcl-bugs@verify.stanford.edu</tt> (the Savannah
interface is preferred).

Other questions, comments, or suggestions should be sent to

<pre>
   cvcl-support@verify.stanford.edu
</pre>

To learn about updates and important announcements regarding CVC Lite,
please subscribe to the mailing list:

<pre>
   cvcl-announce@verify.stanford.edu
</pre>

This list has a very low traffic (one or two messages a month or so).

Another mailing list serves as an open forum for CVC Lite users:

<pre>
   cvcl-users@verify.stanford.edu
</pre>

You can subscribe to these lists by visiting the corresponding
<em>list information page</em> links at:

<pre>
   http://verify.stanford.edu/savannah/mail/?group=cvcl
</pre>

Other information and related links can be found at the CVC Lite home
page:

<pre>
   http://verify.stanford.edu/CVCL
</pre>

and at the CVC Lite project page in the Savannah interface:

<pre>
   http://verify.stanford.edu/savannah/projects/cvcl/
</pre>

<h2>
Bugs
</h2>

Yes, we have bugs... :-)

Some of the known bugs in this release are listed below.

- [bug #13] Some array expressions do not fully simplify in one pass.
  This causes an assert-failure in the debug build, and might
  potentially cause an infinite loop or failure in other build types.
  This should be fixed soon.

- CVC Lite is still rather slow (algorithmically) on non-CNF formulas,
  especially if they involve many nested IF-THEN-ELSE operators and
  a heavy mixture of decision procedures.  Fixing this is a complex
  but interesting research problem, and we are actively working on it.

- The integrated SAT solver is algorithmically about as efficient as
  Chaff, but 10x to 100x slower in raw speed, depending on the
  problem.  A cleaner and faster SAT solver, as well as more efficient
  underlying data structures, are under development, and will be
  available soon in the next release.
-->
*/

---