e2558df28ef96312adc713813b5deb432a221c82
1 /********************* */
4 ** Top contributors (to current version):
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2019 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 solving capabilities of the CVC4
19 #include <cvc4/cvc4.h>
27 smt
.setLogic("QF_BV"); // Set the logic
29 Type bitvector32
= em
.mkBitVectorType(32);
31 Expr x
= em
.mkVar("a", bitvector32
);
33 Expr ext_31_1
= em
.mkConst(CVC4::BitVectorExtract(31,1));
34 Expr x_31_1
= em
.mkExpr(ext_31_1
, x
);
36 Expr ext_30_0
= em
.mkConst(CVC4::BitVectorExtract(30,0));
37 Expr x_30_0
= em
.mkExpr(ext_30_0
, x
);
39 Expr ext_31_31
= em
.mkConst(CVC4::BitVectorExtract(31,31));
40 Expr x_31_31
= em
.mkExpr(ext_31_31
, x
);
42 Expr ext_0_0
= em
.mkConst(CVC4::BitVectorExtract(0,0));
43 Expr x_0_0
= em
.mkExpr(ext_0_0
, x
);
45 Expr eq
= em
.mkExpr(kind::EQUAL
, x_31_1
, x_30_0
);
46 cout
<< " Asserting: " << eq
<< endl
;
47 smt
.assertFormula(eq
);
49 Expr eq2
= em
.mkExpr(kind::EQUAL
, x_31_31
, x_0_0
);
50 cout
<< " Querying: " << eq2
<< endl
;
51 cout
<< " Expect entailed. " << endl
;
52 cout
<< " CVC4: " << smt
.checkEntailed(eq2
) << endl
;