1 /********************* */
2 /*! \file simple_vc_cxx.cpp
4 ** Original author: mdeters
5 ** Major contributors: none
6 ** Minor contributors (to current version): none
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
9 ** Courant Institute of Mathematical Sciences
10 ** New York University
11 ** See the file COPYING in the top-level source directory for licensing
12 ** information.\endverbatim
14 ** \brief A simple demonstration of the C++ interface
16 ** A simple demonstration of the C++ interface. Compare to the Java
17 ** interface in SimpleVC.java; they are virtually line-by-line
23 //#include <cvc4.h> // use this after CVC4 is properly installed
24 #include "smt/smt_engine.h"
33 // Prove that for integers x and y:
34 // x > 0 AND y > 0 => 2x + y >= 3
36 Type integer
= em
.integerType();
38 Expr x
= em
.mkVar("x", integer
);
39 Expr y
= em
.mkVar("y", integer
);
40 Expr zero
= em
.mkConst(Rational(0));
42 Expr x_positive
= em
.mkExpr(kind::GT
, x
, zero
);
43 Expr y_positive
= em
.mkExpr(kind::GT
, y
, zero
);
45 Expr two
= em
.mkConst(Rational(2));
46 Expr twox
= em
.mkExpr(kind::MULT
, two
, x
);
47 Expr twox_plus_y
= em
.mkExpr(kind::PLUS
, twox
, y
);
49 Expr three
= em
.mkConst(Rational(3));
50 Expr twox_plus_y_geq_3
= em
.mkExpr(kind::GEQ
, twox_plus_y
, three
);
53 em
.mkExpr(kind::AND
, x_positive
, y_positive
).
54 impExpr(twox_plus_y_geq_3
);
56 cout
<< "Checking validity of formula " << formula
<< " with CVC4." << endl
;
57 cout
<< "CVC4 should report VALID." << endl
;
58 cout
<< "Result from CVC4 is: " << smt
.query(formula
) << endl
;