1 /********************* */
2 /*! \file extract-new.cpp
4 ** Top contributors (to current version):
5 ** Aina Niemetz, Makai Mann
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/api/cvc4cpp.h>
22 using namespace CVC4::api
;
27 slv
.setLogic("QF_BV"); // Set the logic
29 Sort bitvector32
= slv
.mkBitVectorSort(32);
31 Term x
= slv
.mkConst(bitvector32
, "a");
33 OpTerm ext_31_1
= slv
.mkOpTerm(BITVECTOR_EXTRACT_OP
, 31, 1);
34 Term x_31_1
= slv
.mkTerm(BITVECTOR_EXTRACT
, ext_31_1
, x
);
36 OpTerm ext_30_0
= slv
.mkOpTerm(BITVECTOR_EXTRACT_OP
, 30, 0);
37 Term x_30_0
= slv
.mkTerm(BITVECTOR_EXTRACT
, ext_30_0
, x
);
39 OpTerm ext_31_31
= slv
.mkOpTerm(BITVECTOR_EXTRACT_OP
, 31, 31);
40 Term x_31_31
= slv
.mkTerm(BITVECTOR_EXTRACT
, ext_31_31
, x
);
42 OpTerm ext_0_0
= slv
.mkOpTerm(BITVECTOR_EXTRACT_OP
, 0, 0);
43 Term x_0_0
= slv
.mkTerm(BITVECTOR_EXTRACT
, ext_0_0
, x
);
45 Term eq
= slv
.mkTerm(EQUAL
, x_31_1
, x_30_0
);
46 cout
<< " Asserting: " << eq
<< endl
;
47 slv
.assertFormula(eq
);
49 Term eq2
= slv
.mkTerm(EQUAL
, x_31_31
, x_0_0
);
50 cout
<< " Check validity assuming: " << eq2
<< endl
;
51 cout
<< " Expect valid. " << endl
;
52 cout
<< " CVC4: " << slv
.checkValidAssuming(eq2
) << endl
;