Merge branch 'master' of https://github.com/CVC4/CVC4

[cvc5.git] / examples / simple_vc_cxx.cpp

diff --git a/examples/simple_vc_cxx.cpp b/examples/simple_vc_cxx.cpp
index 819b1fc9704872da28fa0232113f389a336c87eb..5b1f36f402b6616aa90d7ca30ab13adadab8d395 100644 (file)
--- a/examples/simple_vc_cxx.cpp
+++ b/examples/simple_vc_cxx.cpp
@@ -1,13 +1,11 @@
 /*********************                                                        */
 /*! \file simple_vc_cxx.cpp
  ** \verbatim
- ** Original author: mdeters
- ** Major contributors: none
+ ** Original author: Morgan Deters
+ ** Major contributors: Dejan Jovanovic
  ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
@@ -20,7 +18,7 @@
 
 #include <iostream>
 
-//#include <cvc4.h> // use this after CVC4 is properly installed
+//#include <cvc4/cvc4.h> // use this after CVC4 is properly installed
 #include "smt/smt_engine.h"
 
 using namespace std;
@@ -37,21 +35,21 @@ int main() {
 
   Expr x = em.mkVar("x", integer);
   Expr y = em.mkVar("y", integer);
-  Expr zero = em.mkConst(Integer(0));
+  Expr zero = em.mkConst(Rational(0));
 
   Expr x_positive = em.mkExpr(kind::GT, x, zero);
   Expr y_positive = em.mkExpr(kind::GT, y, zero);
 
-  Expr two = em.mkConst(Integer(2));
+  Expr two = em.mkConst(Rational(2));
   Expr twox = em.mkExpr(kind::MULT, two, x);
   Expr twox_plus_y = em.mkExpr(kind::PLUS, twox, y);
 
-  Expr three = em.mkConst(Integer(3));
+  Expr three = em.mkConst(Rational(3));
   Expr twox_plus_y_geq_3 = em.mkExpr(kind::GEQ, twox_plus_y, three);
 
-  BoolExpr formula =
-    BoolExpr(em.mkExpr(kind::AND, x_positive, y_positive)).
-    impExpr(BoolExpr(twox_plus_y_geq_3));
+  Expr formula =
+    em.mkExpr(kind::AND, x_positive, y_positive).
+    impExpr(twox_plus_y_geq_3);
 
   cout << "Checking validity of formula " << formula << " with CVC4." << endl;
   cout << "CVC4 should report VALID." << endl;