1 /********************* */
2 /*! \file simple_vc_cxx.cpp
4 ** Top contributors (to current version):
5 ** Andres Noetzli, Morgan Deters, Mudathir Mohamed
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
8 ** in the top-level source directory and their institutional affiliations.
9 ** All rights reserved. See the file COPYING in the top-level source
10 ** directory for licensing information.\endverbatim
12 ** \brief A simple demonstration of the C++ interface
14 ** A simple demonstration of the C++ interface. Compare to the Java
15 ** interface in SimpleVC.java; they are virtually line-by-line
19 #include <cvc4/api/cvc4cpp.h>
23 using namespace CVC4::api
;
28 // Prove that for integers x and y:
29 // x > 0 AND y > 0 => 2x + y >= 3
31 Sort integer
= slv
.getIntegerSort();
33 Term x
= slv
.mkConst(integer
, "x");
34 Term y
= slv
.mkConst(integer
, "y");
35 Term zero
= slv
.mkInteger(0);
37 Term x_positive
= slv
.mkTerm(Kind::GT
, x
, zero
);
38 Term y_positive
= slv
.mkTerm(Kind::GT
, y
, zero
);
40 Term two
= slv
.mkInteger(2);
41 Term twox
= slv
.mkTerm(Kind::MULT
, two
, x
);
42 Term twox_plus_y
= slv
.mkTerm(Kind::PLUS
, twox
, y
);
44 Term three
= slv
.mkInteger(3);
45 Term twox_plus_y_geq_3
= slv
.mkTerm(Kind::GEQ
, twox_plus_y
, three
);
48 slv
.mkTerm(Kind::AND
, x_positive
, y_positive
).impTerm(twox_plus_y_geq_3
);
50 std::cout
<< "Checking entailment of formula " << formula
<< " with CVC4."
52 std::cout
<< "CVC4 should report ENTAILED." << std::endl
;
53 std::cout
<< "Result from CVC4 is: " << slv
.checkEntailed(formula
)