1 /********************* */
2 /*! \file simple_vc_quant_cxx.cpp
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
12 ** \brief A simple demonstration of the C++ interface for quantifiers
14 ** A simple demonstration of the C++ interface for quantifiers.
17 #include <cvc4/api/cvc4cpp.h>
21 using namespace CVC4::api
;
26 // Prove that the following is unsatisfiable:
27 // forall x. P( x ) ^ ~P( 5 )
29 Sort integer
= slv
.getIntegerSort();
30 Sort boolean
= slv
.getBooleanSort();
31 Sort integerPredicate
= slv
.mkFunctionSort(integer
, boolean
);
33 Term p
= slv
.mkConst(integerPredicate
, "P");
34 Term x
= slv
.mkVar(integer
, "x");
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
;
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
;
48 Term formula
= slv
.mkTerm(Kind::AND
, quantpospx
, negpfive
);
50 slv
.assertFormula(formula
);
52 std::cout
<< "Checking SAT after asserting " << formula
<< " to CVC4."
54 std::cout
<< "CVC4 should report unsat." << std::endl
;
55 std::cout
<< "Result from CVC4 is: " << slv
.checkSat() << std::endl
;
57 slv
.resetAssertions();
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
;
66 Term formula_pattern
= slv
.mkTerm(Kind::AND
, quantpospx_pattern
, negpfive
);
68 slv
.assertFormula(formula_pattern
);
70 std::cout
<< "Checking SAT after asserting " << formula_pattern
<< " to CVC4."
72 std::cout
<< "CVC4 should report unsat." << std::endl
;
73 std::cout
<< "Result from CVC4 is: " << slv
.checkSat() << std::endl
;