cvc4, pcvc4 - an automated theorem prover

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.

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

       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.

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.

CVC4 reports all syntactic and semantic errors on standard error.

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

       SVC's  successor,  the CooperatingValidityChecker(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.

       cvc4, pcvc4 - an automated theorem prover

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/.

CVC4 release CVC4_RELEASE_STRING                   2024-03-31                                            CVC4(1)

cvc4[options][file]pcvc4[options][file]

       This manual page refers to CVC4 version CVC4_RELEASE_STRING.