1 /********************* */
2 /*! \file simple_vc_cxx.cpp
4 ** Top contributors (to current version):
5 ** Morgan Deters, Dejan Jovanovic
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2019 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
21 #include <cvc4/cvc4.h>
30 // Prove that for integers x and y:
31 // x > 0 AND y > 0 => 2x + y >= 3
33 Type integer
= em
.integerType();
35 Expr x
= em
.mkVar("x", integer
);
36 Expr y
= em
.mkVar("y", integer
);
37 Expr zero
= em
.mkConst(Rational(0));
39 Expr x_positive
= em
.mkExpr(kind::GT
, x
, zero
);
40 Expr y_positive
= em
.mkExpr(kind::GT
, y
, zero
);
42 Expr two
= em
.mkConst(Rational(2));
43 Expr twox
= em
.mkExpr(kind::MULT
, two
, x
);
44 Expr twox_plus_y
= em
.mkExpr(kind::PLUS
, twox
, y
);
46 Expr three
= em
.mkConst(Rational(3));
47 Expr twox_plus_y_geq_3
= em
.mkExpr(kind::GEQ
, twox_plus_y
, three
);
50 em
.mkExpr(kind::AND
, x_positive
, y_positive
).
51 impExpr(twox_plus_y_geq_3
);
53 cout
<< "Checking entailment of formula " << formula
<< " with CVC4." << endl
;
54 cout
<< "CVC4 should report ENTAILED." << endl
;
55 cout
<< "Result from CVC4 is: " << smt
.checkEntailed(formula
) << endl
;