examples/simple_vc_quant_cxx.cpp

   1 /*********************                                                        */
   2 /*! \file simple_vc_quant_cxx.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andres Noetzli, Andrew Reynolds, 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 for quantifiers
  13  **
  14  ** A simple demonstration of the C++ interface for quantifiers.
  15  **/
  16
  17 #include <cvc4/api/cvc4cpp.h>
  18
  19 #include <iostream>
  20
  21 using namespace CVC4::api;
  22
  23 int main() {
  24   Solver slv;
  25
  26   // Prove that the following is unsatisfiable:
  27   //   forall x. P( x ) ^ ~P( 5 )
  28
  29   Sort integer = slv.getIntegerSort();
  30   Sort boolean = slv.getBooleanSort();
  31   Sort integerPredicate = slv.mkFunctionSort(integer, boolean);
  32
  33   Term p = slv.mkConst(integerPredicate, "P");
  34   Term x = slv.mkVar(integer, "x");
  35
  36   // make forall x. P( x )
  37   Term var_list = slv.mkTerm(Kind::BOUND_VAR_LIST, x);
  38   Term px = slv.mkTerm(Kind::APPLY_UF, p, x);
  39   Term quantpospx = slv.mkTerm(Kind::FORALL, var_list, px);
  40   std::cout << "Made expression : " << quantpospx << std::endl;
  41
  42   //make ~P( 5 )
  43   Term five = slv.mkInteger(5);
  44   Term pfive = slv.mkTerm(Kind::APPLY_UF, p, five);
  45   Term negpfive = slv.mkTerm(Kind::NOT, pfive);
  46   std::cout << "Made expression : " << negpfive << std::endl;
  47
  48   Term formula = slv.mkTerm(Kind::AND, quantpospx, negpfive);
  49
  50   slv.assertFormula(formula);
  51
  52   std::cout << "Checking SAT after asserting " << formula << " to CVC4."
  53             << std::endl;
  54   std::cout << "CVC4 should report unsat." << std::endl;
  55   std::cout << "Result from CVC4 is: " << slv.checkSat() << std::endl;
  56
  57   slv.resetAssertions();
  58
  59   // this version has a pattern e.g. in smt2 syntax (forall ((x Int)) (! (P x ) :pattern ((P x))))
  60   Term pattern = slv.mkTerm(Kind::INST_PATTERN, px);
  61   Term pattern_list = slv.mkTerm(Kind::INST_PATTERN_LIST, pattern);
  62   Term quantpospx_pattern =
  63       slv.mkTerm(Kind::FORALL, var_list, px, pattern_list);
  64   std::cout << "Made expression : " << quantpospx_pattern << std::endl;
  65
  66   Term formula_pattern = slv.mkTerm(Kind::AND, quantpospx_pattern, negpfive);
  67
  68   slv.assertFormula(formula_pattern);
  69
  70   std::cout << "Checking SAT after asserting " << formula_pattern << " to CVC4."
  71             << std::endl;
  72   std::cout << "CVC4 should report unsat." << std::endl;
  73   std::cout << "Result from CVC4 is: " << slv.checkSat() << std::endl;
  74
  75   return 0;
  76 }