1 files changed, 127 insertions, 0 deletions
diff --git a/doc/cvc4.1_template.in b/doc/cvc4.1_template.in
new file mode 100644
index 000000000..23eff6110
--- /dev/null
+++ b/doc/cvc4.1_template.in
@@ -0,0 +1,127 @@
+.\" Process this file with
+.\" groff -man -Tascii cvc4.1
+.\"
+.TH CVC4 1 "@MAN_DATE@" "CVC4 release @VERSION@" "User Manuals"
+.SH NAME
+cvc4, pcvc4 \- an automated theorem prover
+.SH SYNOPSIS
+.B cvc4 [
+.I options
+.B ] [
+.I file
+.B ]
+.P
+.B pcvc4 [
+.I options
+.B ] [
+.I file
+.B ]
+.SH DESCRIPTION
+.B cvc4
+is an automated theorem prover for first-order formulas with respect
+to background theories of interest.
+.B pcvc4
+is CVC4's "portfolio" variant, which is capable of running multiple
+CVC4 instances in parallel, configured differently.
+
+With
+.I file
+, commands are read from
+.I file
+and executed.  CVC4 supports the SMT-LIB (versions 1.2 and 2.0) input
+format, as well as its own native \(lqpresentation language\(rq (see
+.BR cvc4 (5)
+), which is similar in many respects to CVC3's presentation language,
+but not identical.
+
+If
+.I file
+is unspecified, standard input is read (and the
+.B CVC4
+presentation language is assumed).  If
+.I file
+is unspecified and
+.B CVC4
+is connected to a terminal, interactive mode is assumed.
+
+.SH COMMON OPTIONS
+${common_manpage_documentation}
+
+${remaining_manpage_documentation}
+
+.\".SH FILES
+.\".SH ENVIRONMENT
+.SH DIAGNOSTICS
+.B CVC4
+reports all syntactic and semantic errors on standard error.
+.SH HISTORY
+The
+.B CVC4
+effort is the culmination of fifteen years of theorem proving
+research, starting with the
+.I Stanford Validity Checker (SVC)
+in 1996.
+
+SVC's successor, the
+.I Cooperating Validity Checker (CVC),
+had a more optimized internal design, produced proofs, used the
+.I Chaff
+SAT solver, and featured a number of usability
+enhancements.  Its name comes from the cooperative nature of
+decision procedures in Nelson-Oppen theory combination,
+which share amongst each other equalities between shared terms.
+
+CVC Lite, first made available in 2003, was a rewrite of CVC
+that attempted to make CVC
+more flexible (hence the \(lqlite\(rq) while extending the feature set:
+CVCLite supported quantifiers where its predecessors did not.
+CVC3 was a major overhaul of portions of CVC Lite: it added
+better decision 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 fifteen 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(
+.I T
+) solver,
+with a SAT solver at its core and a delegation path to different decision
+procedure implementations, each in charge of solving formulas in some
+background theory.
+
+The re-evaluation and ground-up rewrite was necessitated, we felt, by
+the performance characteristics of CVC3.  CVC3 has many useful
+features, but some core aspects of the design led to high memory use, and
+the use of heavyweight computation (where more nimble engineering
+approaches could suffice) makes CVC3 a much slower prover than other tools.
+As these designs are central to CVC3, a new version was preferable to a
+selective re-engineering, which would have ballooned in short order.
+.SH VERSION
+This manual page refers to
+.B CVC4
+version @VERSION@.
+.SH BUGS
+A Bugzilla for the CVC4 project is maintained at
+.BR http://goedel.cs.nyu.edu/bugzilla3/ .
+.SH AUTHORS
+.B CVC4
+is developed by a team of researchers at New York University
+and the University of Iowa.
+See the AUTHORS file in the distribution for a full list of
+contributors.
+.SH "SEE ALSO"
+.BR libcvc4 (3),
+.BR libcvc4parser (3),
+.BR libcvc4compat (3)
+
+Additionally, the CVC4 wiki contains useful information about the
+design and internals of CVC4.  It is maintained at
+.BR http://goedel.cs.nyu.edu/wiki/ .