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

FreeBSD Manual Pages

  
 
  

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

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

COMMON OPTIONS
       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.

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

       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
       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 de-
       sign and	internals of CVC4.  It is maintained  at  http://cvc4.cs.stan-
       ford.edu/wiki/.

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

NAME | SYNOPSIS | DESCRIPTION | COMMON OPTIONS | DIAGNOSTICS | HISTORY | VERSION | BUGS | AUTHORS | SEE ALSO

Want to link to this manual page? Use this URL:
<https://www.freebsd.org/cgi/man.cgi?query=cvc4&sektion=1&manpath=FreeBSD+12.2-RELEASE+and+Ports>

home | help