diff options
| author | Nick Smallbone <nick@smallbone.se> | 2019-03-23 08:17:49 +0700 |
|---|---|---|
| committer | Willy Sudiarto Raharjo <willysr@slackbuilds.org> | 2019-03-23 08:17:49 +0700 |
| commit | 3015af4e8716f1776cb6dba21b091cfee90be735 (patch) | |
| tree | b79f505845cead7e571d98920b4d750e994dae45 /academic/cvc4/README | |
| parent | 2e6a13ec85a6924a37de5e58148508c32f11f07f (diff) | |
academic/cvc4: Added (Theorem Solver).
Signed-off-by: Willy Sudiarto Raharjo <willysr@slackbuilds.org>
Diffstat (limited to 'academic/cvc4/README')
| -rw-r--r-- | academic/cvc4/README | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/academic/cvc4/README b/academic/cvc4/README new file mode 100644 index 0000000000000..830c7394fbd80 --- /dev/null +++ b/academic/cvc4/README @@ -0,0 +1,7 @@ +CVC4 is an automated theorem prover and satisfiability modulo theories +(SMT) solver. Given a formula in first-order logic, it attempts to +either prove the formula or find a counterexample. CVC4 supports +arithmetic, reasoning about arrays, and several other built-in +theories. Input problems are written in SMT-LIB format. + +This package includes the cvc4 program as well as libraries. |