1 /********************* */
2 /*! \file simple_vc_cxx.cpp
4 ** Original author: Morgan Deters
5 ** Major contributors: Dejan Jovanovic
6 ** Minor contributors (to current version): none
7 ** This file is part of the CVC4 project.
8 ** Copyright (c) 2009-2013 New York University and The University of Iowa
9 ** See the file COPYING in the top-level source directory for licensing
10 ** 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> // use this after CVC4 is properly installed
22 #include "smt/smt_engine.h"
31 // Prove that for integers x and y:
32 // x > 0 AND y > 0 => 2x + y >= 3
34 Type integer
= em
.integerType();
36 Expr x
= em
.mkVar("x", integer
);
37 Expr y
= em
.mkVar("y", integer
);
38 Expr zero
= em
.mkConst(Rational(0));
40 Expr x_positive
= em
.mkExpr(kind::GT
, x
, zero
);
41 Expr y_positive
= em
.mkExpr(kind::GT
, y
, zero
);
43 Expr two
= em
.mkConst(Rational(2));
44 Expr twox
= em
.mkExpr(kind::MULT
, two
, x
);
45 Expr twox_plus_y
= em
.mkExpr(kind::PLUS
, twox
, y
);
47 Expr three
= em
.mkConst(Rational(3));
48 Expr twox_plus_y_geq_3
= em
.mkExpr(kind::GEQ
, twox_plus_y
, three
);
51 em
.mkExpr(kind::AND
, x_positive
, y_positive
).
52 impExpr(twox_plus_y_geq_3
);
54 cout
<< "Checking validity of formula " << formula
<< " with CVC4." << endl
;
55 cout
<< "CVC4 should report VALID." << endl
;
56 cout
<< "Result from CVC4 is: " << smt
.query(formula
) << endl
;