Skip site navigation (1)Skip section navigation (2)

FreeBSD Manual Pages


home | help
CVC4(1)				 User Manuals			       CVC4(1)

       cvc4, pcvc4 - an	automated theorem prover

       cvc4 [ options ]	[ file ]

       pcvc4 [ options ] [ file	]

       cvc4  is	 an automated theorem prover for first-order formulas with re-
       spect to	background theories of interest.  pcvc4	is CVC4's  "portfolio"
       variant,	 which is capable of running multiple CVC4 instances in	paral-
       lel, 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 na-
       tive "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 presenta-
       tion language is	assumed).  If file is unspecified  and	CVC4  is  con-
       nected to a terminal, interactive mode is assumed.

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



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

       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 Stanford Validity Checker (SVC) in 1996.

       SVC's successor,	the Cooperating	Validity Checker (CVC),	had a more op-
       timized	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

       CVC  Lite,  first made available	in 2003, was a rewrite of CVC that at-
       tempted 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 Min-
       iSat 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  fea-
       tures,  but some	core aspects of	the design led to high memory use, and
       the use of heavyweight computation (where more nimble  engineering  ap-
       proaches	 could	suffice)  makes	 CVC3  a much slower prover than other
       tools.  As these	designs	are central to CVC3, a new version was prefer-
       able to a selective re-engineering, which would have ballooned in short

       This manual page	refers to CVC4 version CVC4_RELEASE_STRING.

       An  issue   tracker   for   the	 CVC4	project	  is   maintained   at

       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.

       libcvc4(3), libcvc4parser(3)

       Additionally,  the  CVC4	wiki contains useful information about the de-
       sign and	internals of CVC4.  It is maintained  at  http://cvc4.cs.stan-

CVC4 release CVC4_RELEASE_STRING  2020-08-08			       CVC4(1)


Want to link to this manual page? Use this URL:

home | help