1 /********************* */
2 /*! \file simple_vc_quant_cxx.cpp
4 ** Top contributors (to current version):
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.
19 #include <cvc4/cvc4.h>
28 // Prove that the following is unsatisfiable:
29 // forall x. P( x ) ^ ~P( 5 )
31 Type integer
= em
.integerType();
32 Type boolean
= em
.booleanType();
33 Type integerPredicate
= em
.mkFunctionType(integer
, boolean
);
35 Expr p
= em
.mkVar("P", integerPredicate
);
36 Expr x
= em
.mkBoundVar("x", integer
);
38 // make forall x. P( x )
39 Expr var_list
= em
.mkExpr(kind::BOUND_VAR_LIST
, x
);
40 Expr px
= em
.mkExpr(kind::APPLY_UF
, p
, x
);
41 Expr quantpospx
= em
.mkExpr(kind::FORALL
, var_list
, px
);
42 cout
<< "Made expression : " << quantpospx
<< endl
;
45 Expr five
= em
.mkConst(Rational(5));
46 Expr pfive
= em
.mkExpr(kind::APPLY_UF
, p
, five
);
47 Expr negpfive
= em
.mkExpr(kind::NOT
, pfive
);
48 cout
<< "Made expression : " << negpfive
<< endl
;
50 Expr formula
= em
.mkExpr(kind::AND
, quantpospx
, negpfive
);
52 smt
.assertFormula(formula
);
54 cout
<< "Checking SAT after asserting " << formula
<< " to CVC4." << endl
;
55 cout
<< "CVC4 should report unsat." << endl
;
56 cout
<< "Result from CVC4 is: " << smt
.checkSat() << endl
;
61 // this version has a pattern e.g. in smt2 syntax (forall ((x Int)) (! (P x ) :pattern ((P x))))
62 Expr pattern
= em
.mkExpr(kind::INST_PATTERN
, px
);
63 Expr pattern_list
= em
.mkExpr(kind::INST_PATTERN_LIST
, pattern
);
64 Expr quantpospx_pattern
= em
.mkExpr(kind::FORALL
, var_list
, px
, pattern_list
);
65 cout
<< "Made expression : " << quantpospx_pattern
<< endl
;
67 Expr formula_pattern
= em
.mkExpr(kind::AND
, quantpospx_pattern
, negpfive
);
69 smtp
.assertFormula(formula_pattern
);
71 cout
<< "Checking SAT after asserting " << formula_pattern
<< " to CVC4." << endl
;
72 cout
<< "CVC4 should report unsat." << endl
;
73 cout
<< "Result from CVC4 is: " << smtp
.checkSat() << endl
;