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

FreeBSD Manual Pages

  
 
  

home | help
LIBCVC4(3)		    CVC4 Library Interfaces		    LIBCVC4(3)

NAME
       libcvc4 - a library interface for the CVC4 theorem prover

SYNOPSIS
       A small program like:

	      #include <iostream>
	      #include "expr/expr_manager.h"
	      #include "smt/smt_engine.h"

	      using namespace CVC4;

	      int main() {
		ExprManager em;
		SmtEngine smt(&em);
		Expr onePlusTwo	= em.mkExpr(kind::PLUS,
					    em.mkConst(Rational(1)),
					    em.mkConst(Rational(2)));
		std::cout << language::SetLanguage(language::output::LANG_CVC4)
			  << smt.getInfo("name")
			  << " says that 1 + 2 = "
			  << smt.simplify(onePlusTwo)
			  << std::endl;

		return 0;
	      }

       gives the output:

	      "cvc4" says that 1 + 2 = 3

DESCRIPTION
       The  main classes of interest in	CVC4's API are ExprManager, SmtEngine,
       and a few related ones like Expr	and Type.

       The ExprManager is used to build	up  expressions	 and  types,  and  the
       SmtEngine  is  used  primarily  to  make	assertions, check satisfiabil-
       ity/validity, and extract models	and proofs.

SEE ALSO
       cvc4(1),	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			    LIBCVC4(3)

NAME | SYNOPSIS | DESCRIPTION | SEE ALSO

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

home | help