summaryrefslogtreecommitdiff
path: root/math/cvcl/pkg-descr
diff options
context:
space:
mode:
Diffstat (limited to 'math/cvcl/pkg-descr')
-rw-r--r--math/cvcl/pkg-descr8
1 files changed, 8 insertions, 0 deletions
diff --git a/math/cvcl/pkg-descr b/math/cvcl/pkg-descr
new file mode 100644
index 000000000000..bd68d695f4d1
--- /dev/null
+++ b/math/cvcl/pkg-descr
@@ -0,0 +1,8 @@
+CVC Lite is an automatic theorem prover for the Satisfiability Modulo
+Theories (SMT) problem. Its features include: support for a variety of
+theories; interactive as well as C and C++ library interfaces; proof and
+model generation abilities; predicate subtyping; and suppport for quantifiers.
+In addition, there are essentially no limits on its use for research or
+commercial purposes (see license).
+
+WWW: http://www.cs.nyu.edu/acsys/cvcl/