examples/api/linear_arith.cpp

   1 /*********************                                                        */
   2 /*! \file linear_arith.cpp
   3  ** \verbatim
   4  ** Original author: Tim King
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): Morgan Deters
   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
  11  **
  12  ** \brief A simple demonstration of the linear arithmetic capabilities of CVC4
  13  **
  14  ** A simple demonstration of the linear arithmetic solving capabilities and
  15  ** the push pop of CVC4. This also gives an example option.
  16  **/
  17
  18 #include <iostream>
  19
  20 //#include <cvc4/cvc4.h> // use this after CVC4 is properly installed
  21 #include "smt/smt_engine.h"
  22
  23 using namespace std;
  24 using namespace CVC4;
  25
  26 int main() {
  27   ExprManager em;
  28   SmtEngine smt(&em);
  29   smt.setLogic("QF_LIRA"); // Set the logic
  30
  31   // Prove that if given x (Integer) and y (Real) then
  32   // the maximum value of y - x is 2/3
  33
  34   // Types
  35   Type real = em.realType();
  36   Type integer = em.integerType();
  37
  38   // Variables
  39   Expr x = em.mkVar("x", integer);
  40   Expr y = em.mkVar("y", real);
  41
  42   // Constants
  43   Expr three = em.mkConst(Rational(3));
  44   Expr neg2 = em.mkConst(Rational(-2));
  45   Expr two_thirds = em.mkConst(Rational(2,3));
  46
  47   // Terms
  48   Expr three_y = em.mkExpr(kind::MULT, three, y);
  49   Expr diff = em.mkExpr(kind::MINUS, y, x);
  50
  51   // Formulas
  52   Expr x_geq_3y = em.mkExpr(kind::GEQ, x, three_y);
  53   Expr x_leq_y = em.mkExpr(kind::LEQ, x, y);
  54   Expr neg2_lt_x = em.mkExpr(kind::LT, neg2, x);
  55
  56   Expr assumptions =
  57     em.mkExpr(kind::AND, x_geq_3y, x_leq_y, neg2_lt_x);
  58
  59   cout << "Given the assumptions " << assumptions << endl;
  60   smt.assertFormula(assumptions);
  61
  62
  63   smt.push();
  64   Expr diff_leq_two_thirds = em.mkExpr(kind::LEQ, diff, two_thirds);
  65   cout << "Prove that " << diff_leq_two_thirds << " with CVC4." << endl;
  66   cout << "CVC4 should report VALID." << endl;
  67   cout << "Result from CVC4 is: " << smt.query(diff_leq_two_thirds) << endl;
  68   smt.pop();
  69
  70   cout << endl;
  71
  72   smt.push();
  73   Expr diff_is_two_thirds = em.mkExpr(kind::EQUAL, diff, two_thirds);
  74   smt.assertFormula(diff_is_two_thirds);
  75   cout << "Show that the asserts are consistent with " << endl;
  76   cout << diff_is_two_thirds << " with CVC4." << endl;
  77   cout << "CVC4 should report SAT." << endl;
  78   cout << "Result from CVC4 is: " << smt.checkSat(em.mkConst(true)) << endl;
  79   smt.pop();
  80
  81   cout << "Thus the maximum value of (y - x) is 2/3."<< endl;
  82
  83   return 0;
  84 }