examples/simple_vc_cxx.cpp

   1 /*********************                                                        */
   2 /*! \file simple_vc_cxx.cpp
   3  ** \verbatim
   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
  11  **
  12  ** \brief A simple demonstration of the C++ interface
  13  **
  14  ** A simple demonstration of the C++ interface.  Compare to the Java
  15  ** interface in SimpleVC.java; they are virtually line-by-line
  16  ** identical.
  17  **/
  18
  19 #include <cvc4/api/cvc4cpp.h>
  20
  21 #include <iostream>
  22
  23 using namespace CVC4::api;
  24
  25 int main() {
  26   Solver slv;
  27
  28   // Prove that for integers x and y:
  29   //   x > 0 AND y > 0  =>  2x + y >= 3
  30
  31   Sort integer = slv.getIntegerSort();
  32
  33   Term x = slv.mkConst(integer, "x");
  34   Term y = slv.mkConst(integer, "y");
  35   Term zero = slv.mkInteger(0);
  36
  37   Term x_positive = slv.mkTerm(Kind::GT, x, zero);
  38   Term y_positive = slv.mkTerm(Kind::GT, y, zero);
  39
  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);
  43
  44   Term three = slv.mkInteger(3);
  45   Term twox_plus_y_geq_3 = slv.mkTerm(Kind::GEQ, twox_plus_y, three);
  46
  47   Term formula =
  48       slv.mkTerm(Kind::AND, x_positive, y_positive).impTerm(twox_plus_y_geq_3);
  49
  50   std::cout << "Checking entailment of formula " << formula << " with CVC4."
  51             << std::endl;
  52   std::cout << "CVC4 should report ENTAILED." << std::endl;
  53   std::cout << "Result from CVC4 is: " << slv.checkEntailed(formula)
  54             << std::endl;
  55
  56   return 0;
  57 }