examples/simple_vc_cxx.cpp

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Andres Noetzli, Morgan Deters, Mudathir Mohamed
   4  *
   5  * This file is part of the cvc5 project.
   6  *
   7  * Copyright (c) 2009-2021 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.
  11  * ****************************************************************************
  12  *
  13  * A simple demonstration of the C++ interface
  14  *
  15  * Compare to the Java interface in SimpleVC.java; they are virtually
  16  * line-by-line identical.
  17  */
  18
  19 #include <cvc5/cvc5.h>
  20
  21 #include <iostream>
  22
  23 using namespace cvc5;
  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::ADD, {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 = slv.mkTerm(Kind::AND, {x_positive, y_positive})
  48                      .impTerm(twox_plus_y_geq_3);
  49
  50   std::cout << "Checking entailment of formula " << formula << " with cvc5."
  51             << std::endl;
  52   std::cout << "cvc5 should report UNSAT." << std::endl;
  53   std::cout << "Result from cvc5 is: "
  54             << slv.checkSatAssuming(formula.notTerm()) << std::endl;
  55
  56   return 0;
  57 }