Provided by: cvc4_1.8-3_amd64 bug

NAME

       cvc4, pcvc4 - an automated theorem prover

SYNOPSIS

       cvc4 [ options ] [ file ]

       pcvc4 [ options ] [ file ]

DESCRIPTION

       cvc4  is  an  automated theorem prover for first-order formulas with respect to background
       theories of interest.  pcvc4 is CVC4's "portfolio" variant, which is  capable  of  running
       multiple CVC4 instances in parallel, configured differently.

       With file , commands are read from file and executed.  CVC4 supports the SMT-LIB (versions
       1.2 and 2.0) input format, as well as its own native “presentation language” (see  cvc4(5)
       ), which is similar in many respects to CVC3's presentation language, but not identical.

       If  file  is  unspecified,  standard  input is read (and the CVC4 presentation language is
       assumed).  If file is unspecified and CVC4 is connected to a terminal, interactive mode is
       assumed.

COMMON OPTIONS

       Each option marked with [*] has a --no-OPTIONNAME variant, which reverses the sense of the
       option.

              $

              $

       Each option marked with [*] has a --no-OPTIONNAME variant, which reverses the sense of the
       option.

DIAGNOSTICS

       CVC4 reports all syntactic and semantic errors on standard error.

HISTORY

       The  CVC4 effort is the culmination of fifteen years of theorem proving research, starting
       with the Stanford Validity Checker (SVC) in 1996.

       SVC's successor, the Cooperating Validity Checker (CVC), had  a  more  optimized  internal
       design,  produced  proofs,  used  the 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  “lite”)  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(  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.

VERSION

       This manual page refers to CVC4 version CVC4_RELEASE_STRING.

BUGS

       An     issue     tracker     for     the     CVC4     project     is     maintained     at
       https://github.com/CVC4/CVC4/issues.

AUTHORS

       CVC4  is  developed  by a team of researchers at Stanford University and the University of
       Iowa.  See the AUTHORS file in the distribution for a full list of contributors.

SEE ALSO

       libcvc4(3), libcvc4parser(3)

       Additionally, the CVC4 wiki contains useful information about the design and internals  of
       CVC4.  It is maintained at http://cvc4.cs.stanford.edu/wiki/.