1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andres Noetzli, Mudathir Mohamed, Aina Niemetz |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
7 |
|
* Copyright (c) 2009-2021 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. |
11 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* A simple test for SmtEngine::resetAssertions() |
14 |
|
* |
15 |
|
* This program indirectly also tests some corner cases w.r.t. |
16 |
|
* context-dependent datastructures: resetAssertions() pops the contexts to |
17 |
|
* zero but some context-dependent datastructures are created at leevel 1, |
18 |
|
* which the datastructure needs to handle properly problematic. |
19 |
|
*/ |
20 |
|
|
21 |
|
#include <iostream> |
22 |
|
#include <sstream> |
23 |
|
|
24 |
|
#include "api/cpp/cvc5.h" |
25 |
|
|
26 |
|
using namespace cvc5::api; |
27 |
|
|
28 |
1 |
int main() |
29 |
|
{ |
30 |
2 |
Solver slv; |
31 |
1 |
slv.setOption("incremental", "true"); |
32 |
|
|
33 |
2 |
Sort real = slv.getRealSort(); |
34 |
2 |
Term x = slv.mkConst(real, "x"); |
35 |
2 |
Term four = slv.mkInteger(4); |
36 |
2 |
Term xEqFour = slv.mkTerm(Kind::EQUAL, x, four); |
37 |
1 |
slv.assertFormula(xEqFour); |
38 |
1 |
std::cout << slv.checkSat() << std::endl; |
39 |
|
|
40 |
1 |
slv.resetAssertions(); |
41 |
|
|
42 |
2 |
Sort elementType = slv.getIntegerSort(); |
43 |
2 |
Sort indexType = slv.getIntegerSort(); |
44 |
2 |
Sort arrayType = slv.mkArraySort(indexType, elementType); |
45 |
2 |
Term array = slv.mkConst(arrayType, "array"); |
46 |
2 |
Term arrayAtFour = slv.mkTerm(Kind::SELECT, array, four); |
47 |
2 |
Term ten = slv.mkInteger(10); |
48 |
2 |
Term arrayAtFour_eq_ten = slv.mkTerm(Kind::EQUAL, arrayAtFour, ten); |
49 |
1 |
slv.assertFormula(arrayAtFour_eq_ten); |
50 |
1 |
std::cout << slv.checkSat() << std::endl; |
51 |
4 |
} |