1 /********************* */
2 /*! \file reset_assertions.cpp
4 ** Top contributors (to current version):
5 ** Andres Noetzli, 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 test for SmtEngine::resetAssertions()
14 ** This program indirectly also tests some corner cases w.r.t.
15 ** context-dependent datastructures: resetAssertions() pops the contexts to
16 ** zero but some context-dependent datastructures are created at leevel 1,
17 ** which the datastructure needs to handle properly problematic.
23 #include "api/cvc4cpp.h"
25 using namespace CVC4::api
;
30 slv
.setOption("incremental", "true");
32 Sort real
= slv
.getRealSort();
33 Term x
= slv
.mkConst(real
, "x");
34 Term four
= slv
.mkInteger(4);
35 Term xEqFour
= slv
.mkTerm(Kind::EQUAL
, x
, four
);
36 slv
.assertFormula(xEqFour
);
37 std::cout
<< slv
.checkSat() << std::endl
;
39 slv
.resetAssertions();
41 Sort elementType
= slv
.getIntegerSort();
42 Sort indexType
= slv
.getIntegerSort();
43 Sort arrayType
= slv
.mkArraySort(indexType
, elementType
);
44 Term array
= slv
.mkConst(arrayType
, "array");
45 Term arrayAtFour
= slv
.mkTerm(Kind::SELECT
, array
, four
);
46 Term ten
= slv
.mkInteger(10);
47 Term arrayAtFour_eq_ten
= slv
.mkTerm(Kind::EQUAL
, arrayAtFour
, ten
);
48 slv
.assertFormula(arrayAtFour_eq_ten
);
49 std::cout
<< slv
.checkSat() << std::endl
;