doc/cvc4.1_template.in

   1 .\" Process this file with
   2 .\" groff -man -Tascii cvc4.1
   3 .\"
   4 .TH CVC4 1 "@MAN_DATE@" "CVC4 release @VERSION@" "User Manuals"
   5 .SH NAME
   6 cvc4, pcvc4 \- an automated theorem prover
   7 .SH SYNOPSIS
   8 .B cvc4 [
   9 .I options
  10 .B ] [
  11 .I file
  12 .B ]
  13 .P
  14 .B pcvc4 [
  15 .I options
  16 .B ] [
  17 .I file
  18 .B ]
  19 .SH DESCRIPTION
  20 .B cvc4
  21 is an automated theorem prover for first-order formulas with respect
  22 to background theories of interest.
  23 .B pcvc4
  24 is CVC4's "portfolio" variant, which is capable of running multiple
  25 CVC4 instances in parallel, configured differently.
  26
  27 With
  28 .I file
  29 , commands are read from
  30 .I file
  31 and executed.  CVC4 supports the SMT-LIB (versions 1.2 and 2.0) input
  32 format, as well as its own native \(lqpresentation language\(rq (see
  33 .BR cvc4 (5)
  34 ), which is similar in many respects to CVC3's presentation language,
  35 but not identical.
  36
  37 If
  38 .I file
  39 is unspecified, standard input is read (and the
  40 .B CVC4
  41 presentation language is assumed).  If
  42 .I file
  43 is unspecified and
  44 .B CVC4
  45 is connected to a terminal, interactive mode is assumed.
  46
  47 .SH COMMON OPTIONS
  48 ${common_manpage_documentation}
  49
  50 ${remaining_manpage_documentation}
  51
  52 .\".SH FILES
  53 .\".SH ENVIRONMENT
  54 .SH DIAGNOSTICS
  55 .B CVC4
  56 reports all syntactic and semantic errors on standard error.
  57 .SH HISTORY
  58 The
  59 .B CVC4
  60 effort is the culmination of fifteen years of theorem proving
  61 research, starting with the
  62 .I Stanford Validity Checker (SVC)
  63 in 1996.
  64
  65 SVC's successor, the
  66 .I Cooperating Validity Checker (CVC),
  67 had a more optimized internal design, produced proofs, used the
  68 .I Chaff
  69 SAT solver, and featured a number of usability
  70 enhancements.  Its name comes from the cooperative nature of
  71 decision procedures in Nelson-Oppen theory combination,
  72 which share amongst each other equalities between shared terms.
  73
  74 CVC Lite, first made available in 2003, was a rewrite of CVC
  75 that attempted to make CVC
  76 more flexible (hence the \(lqlite\(rq) while extending the feature set:
  77 CVCLite supported quantifiers where its predecessors did not.
  78 CVC3 was a major overhaul of portions of CVC Lite: it added
  79 better decision procedure implementations, added support for using
  80 MiniSat in the core, and had generally better performance.
  81
  82 CVC4 is the new version, the fifth generation of this validity
  83 checker line that is now celebrating fifteen years of heritage.
  84 It represents a complete re-evaluation of
  85 the core architecture to be both performant and to serve as a cutting-edge research vehicle
  86 for the next several years.  Rather than taking CVC3
  87 and redesigning problem parts, we've taken a clean-room approach,
  88 starting from scratch.  Before using any designs from CVC3, we have
  89 thoroughly scrutinized, vetted, and updated them.  Many parts of CVC4
  90 bear only a superficial resemblance, if any, to their correspondent in CVC3.
  91
  92 However, CVC4 is fundamentally similar to CVC3 and many other
  93 modern SMT solvers: it is a DPLL(
  94 .I T
  95 ) solver,
  96 with a SAT solver at its core and a delegation path to different decision
  97 procedure implementations, each in charge of solving formulas in some
  98 background theory.
  99
 100 The re-evaluation and ground-up rewrite was necessitated, we felt, by
 101 the performance characteristics of CVC3.  CVC3 has many useful
 102 features, but some core aspects of the design led to high memory use, and
 103 the use of heavyweight computation (where more nimble engineering
 104 approaches could suffice) makes CVC3 a much slower prover than other tools.
 105 As these designs are central to CVC3, a new version was preferable to a
 106 selective re-engineering, which would have ballooned in short order.
 107 .SH VERSION
 108 This manual page refers to
 109 .B CVC4
 110 version @VERSION@.
 111 .SH BUGS
 112 A Bugzilla for the CVC4 project is maintained at
 113 .BR http://goedel.cs.nyu.edu/bugzilla3/ .
 114 .SH AUTHORS
 115 .B CVC4
 116 is developed by a team of researchers at New York University
 117 and the University of Iowa.
 118 See the AUTHORS file in the distribution for a full list of
 119 contributors.
 120 .SH "SEE ALSO"
 121 .BR libcvc4 (3),
 122 .BR libcvc4parser (3),
 123 .BR libcvc4compat (3)
 124
 125 Additionally, the CVC4 wiki contains useful information about the
 126 design and internals of CVC4.  It is maintained at
 127 .BR http://goedel.cs.nyu.edu/wiki/ .