1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
|
/******************************************************************************
* Top contributors (to current version):
* Andrew Reynolds, Aina Niemetz
*
* This file is part of the cvc5 project.
*
* Copyright (c) 2009-2025 by the authors listed in the file AUTHORS
* in the top-level source directory and their institutional affiliations.
* All rights reserved. See the file COPYING in the top-level source
* directory for licensing information.
* ****************************************************************************
*
* Test for project issue #655
*
*/
#include <cvc5/cvc5.h>
using namespace cvc5;
int main(void)
{
TermManager tm;
Solver solver(tm);
solver.setOption("incremental", "false");
solver.setOption("produce-abducts", "true");
Sort s0 = tm.getBooleanSort();
DatatypeDecl d1 = tm.mkDatatypeDecl("_dt0");
DatatypeConstructorDecl dtcd2 = tm.mkDatatypeConstructorDecl("_cons7");
dtcd2.addSelectorSelf("_sel4");
dtcd2.addSelector("_sel5", s0);
dtcd2.addSelector("_sel6", s0);
d1.addConstructor(dtcd2);
DatatypeConstructorDecl dtcd3 = tm.mkDatatypeConstructorDecl("_cons12");
dtcd3.addSelectorSelf("_sel8");
dtcd3.addSelector("_sel9", s0);
dtcd3.addSelector("_sel10", s0);
dtcd3.addSelector("_sel11", s0);
d1.addConstructor(dtcd3);
DatatypeConstructorDecl dtcd4 = tm.mkDatatypeConstructorDecl("_cons17");
dtcd4.addSelector("_sel13", s0);
dtcd4.addSelector("_sel14", s0);
dtcd4.addSelector("_sel15", s0);
dtcd4.addSelector("_sel16", s0);
d1.addConstructor(dtcd4);
DatatypeDecl d5 = tm.mkDatatypeDecl("_dt1");
DatatypeConstructorDecl dtcd6 = tm.mkDatatypeConstructorDecl("_cons19");
dtcd6.addSelectorSelf("_sel18");
d5.addConstructor(dtcd6);
DatatypeConstructorDecl dtcd7 = tm.mkDatatypeConstructorDecl("_cons21");
dtcd7.addSelector("_sel20", s0);
d5.addConstructor(dtcd7);
DatatypeConstructorDecl dtcd8 = tm.mkDatatypeConstructorDecl("_cons22");
d5.addConstructor(dtcd8);
Sort s9 = tm.mkParamSort("_p3");
DatatypeDecl d10 = tm.mkDatatypeDecl("_dt2", {s9});
DatatypeConstructorDecl dtcd11 = tm.mkDatatypeConstructorDecl("_cons27");
dtcd11.addSelector("_sel23", s9);
dtcd11.addSelector("_sel24", s0);
dtcd11.addSelector("_sel25", s0);
dtcd11.addSelector("_sel26", s9);
d10.addConstructor(dtcd11);
DatatypeConstructorDecl dtcd12 = tm.mkDatatypeConstructorDecl("_cons30");
dtcd12.addSelector("_sel28", s9);
dtcd12.addSelector("_sel29", s0);
d10.addConstructor(dtcd12);
DatatypeConstructorDecl dtcd13 = tm.mkDatatypeConstructorDecl("_cons33");
dtcd13.addSelectorSelf("_sel31");
dtcd13.addSelector("_sel32", s0);
d10.addConstructor(dtcd13);
DatatypeConstructorDecl dtcd14 = tm.mkDatatypeConstructorDecl("_cons36");
dtcd14.addSelector("_sel34", s0);
dtcd14.addSelectorSelf("_sel35");
d10.addConstructor(dtcd14);
std::vector<Sort> v15 = tm.mkDatatypeSorts({d1, d5, d10});
Sort s16 = v15[0];
Sort s17 = v15[1];
Sort s18 = v15[2];
Term t19 = tm.mkConst(s16, "_x66");
Datatype dt20 = s16.getDatatype();
DatatypeConstructor dtc21 = dt20.operator[]("_cons17");
Term t22 = dtc21.getTesterTerm();
Sort s23 = t22.getSort();
Term t24 = tm.mkTerm(Kind::APPLY_TESTER, {t22, t19});
Term t25 = solver.getAbduct(t24);
return 0;
}
|
