Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Aina Niemetz, Andrew Reynolds
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2024 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 : : * Test for project issue #575
14 : : *
15 : : */
16 : : #include <cvc5/cvc5.h>
17 : :
18 : : using namespace cvc5;
19 : 1 : int main(void)
20 : : {
21 : 2 : TermManager tm;
22 : 2 : Solver solver(tm);
23 : 1 : solver.setOption("incremental", "false");
24 : 1 : solver.setOption("preprocess-only", "true");
25 : 1 : solver.setOption("produce-models", "true");
26 : 2 : Sort s0 = tm.mkBitVectorSort(48);
27 : 2 : Sort s1 = tm.getIntegerSort();
28 : 2 : Sort s2 = tm.getRoundingModeSort();
29 : 3 : DatatypeDecl d3 = tm.mkDatatypeDecl("_dt0");
30 : 3 : DatatypeConstructorDecl dtcd4 = tm.mkDatatypeConstructorDecl("_cons5");
31 : 1 : dtcd4.addSelector("_sel1", s0);
32 : 1 : dtcd4.addSelector("_sel2", s1);
33 : 1 : dtcd4.addSelector("_sel3", s1);
34 : 1 : dtcd4.addSelector("_sel4", s1);
35 : 1 : d3.addConstructor(dtcd4);
36 : 3 : DatatypeConstructorDecl dtcd5 = tm.mkDatatypeConstructorDecl("_cons9");
37 : 1 : dtcd5.addSelector("_sel6", s2);
38 : 1 : dtcd5.addSelector("_sel7", s1);
39 : 1 : dtcd5.addSelector("_sel8", s2);
40 : 1 : d3.addConstructor(dtcd5);
41 : 3 : DatatypeConstructorDecl dtcd6 = tm.mkDatatypeConstructorDecl("_cons13");
42 : 1 : dtcd6.addSelector("_sel10", s2);
43 : 1 : dtcd6.addSelector("_sel11", s1);
44 : 1 : dtcd6.addSelector("_sel12", s1);
45 : 1 : d3.addConstructor(dtcd6);
46 : 6 : Sort s7 = solver.declareDatatype("_dt0", {dtcd4, dtcd5, dtcd6});
47 : 3 : DatatypeDecl d8 = tm.mkDatatypeDecl("_dt14");
48 : 3 : DatatypeConstructorDecl dtcd9 = tm.mkDatatypeConstructorDecl("_cons24");
49 : 1 : dtcd9.addSelector("_sel19", s0);
50 : 1 : dtcd9.addSelector("_sel20", s0);
51 : 1 : dtcd9.addSelector("_sel21", s7);
52 : 1 : dtcd9.addSelector("_sel22", s1);
53 : 1 : dtcd9.addSelector("_sel23", s7);
54 : 1 : d8.addConstructor(dtcd9);
55 : 2 : Sort s10 = tm.mkParamSort("_p16");
56 : 2 : Sort s11 = tm.mkParamSort("_p17");
57 : 5 : DatatypeDecl d12 = tm.mkDatatypeDecl("_dt15", {s10, s11});
58 : 3 : DatatypeConstructorDecl dtcd13 = tm.mkDatatypeConstructorDecl("_cons29");
59 : 1 : dtcd13.addSelector("_sel25", s11);
60 : 1 : dtcd13.addSelector("_sel26", s0);
61 : 1 : dtcd13.addSelector("_sel27", s10);
62 : 1 : dtcd13.addSelector("_sel28", s7);
63 : 1 : d12.addConstructor(dtcd13);
64 : 3 : DatatypeConstructorDecl dtcd14 = tm.mkDatatypeConstructorDecl("_cons31");
65 : 1 : dtcd14.addSelector("_sel30", s10);
66 : 1 : d12.addConstructor(dtcd14);
67 : 3 : DatatypeDecl d15 = tm.mkDatatypeDecl("_dt18");
68 : 3 : DatatypeConstructorDecl dtcd16 = tm.mkDatatypeConstructorDecl("_cons34");
69 : 1 : dtcd16.addSelector("_sel32", s0);
70 : 1 : dtcd16.addSelector("_sel33", s1);
71 : 1 : d15.addConstructor(dtcd16);
72 : 3 : DatatypeConstructorDecl dtcd17 = tm.mkDatatypeConstructorDecl("_cons36");
73 : 1 : dtcd17.addSelectorSelf("_sel35");
74 : 1 : d15.addConstructor(dtcd17);
75 : 3 : DatatypeConstructorDecl dtcd18 = tm.mkDatatypeConstructorDecl("_cons37");
76 : 1 : d15.addConstructor(dtcd18);
77 : 3 : DatatypeConstructorDecl dtcd19 = tm.mkDatatypeConstructorDecl("_cons41");
78 : 1 : dtcd19.addSelector("_sel38", s1);
79 : 1 : dtcd19.addSelectorSelf("_sel39");
80 : 1 : dtcd19.addSelector("_sel40", s2);
81 : 1 : d15.addConstructor(dtcd19);
82 : 6 : std::vector<Sort> v20 = tm.mkDatatypeSorts({d8, d12, d15});
83 : 2 : Sort s21 = v20[0];
84 : 2 : Sort s22 = v20[1];
85 : 2 : Sort s23 = v20[2];
86 : 2 : Sort s24 = tm.getRealSort();
87 : 2 : Sort s25 = tm.mkUninterpretedSort("_u42");
88 : 2 : Sort s26 = tm.mkUninterpretedSort("_u43");
89 : 2 : Sort s27 = tm.mkFloatingPointSort(5, 11);
90 : 2 : Sort s28 = tm.mkBitVectorSort(1);
91 : 2 : Sort s29 = tm.mkBitVectorSort(5);
92 : 2 : Sort s30 = tm.mkBitVectorSort(10);
93 : 2 : Sort s31 = tm.mkBitVectorSort(16);
94 : 3 : DatatypeDecl d32 = tm.mkDatatypeDecl("_dt44");
95 : 3 : DatatypeConstructorDecl dtcd33 = tm.mkDatatypeConstructorDecl("_cons45");
96 : 1 : d32.addConstructor(dtcd33);
97 : 3 : DatatypeConstructorDecl dtcd34 = tm.mkDatatypeConstructorDecl("_cons47");
98 : 1 : dtcd34.addSelector("_sel46", s7);
99 : 1 : d32.addConstructor(dtcd34);
100 : 5 : Sort s35 = solver.declareDatatype("_dt44", {dtcd33, dtcd34});
101 : 4 : Sort s36 = tm.mkFunctionSort({s27}, s31);
102 : 2 : Sort s37 = tm.getRoundingModeSort();
103 : 2 : Sort s38 = tm.mkUninterpretedSort("_u48");
104 : 2 : Sort s39 = tm.getRoundingModeSort();
105 : 2 : Term t40 = tm.mkConst(s36, "_x49");
106 : 2 : Term t41 = tm.mkConst(s23, "_x50");
107 : 2 : Term t42 = tm.mkConst(s21, "_x51");
108 : 2 : Term t43 = tm.mkConst(s27, "_x52");
109 : 2 : Term t44 = tm.mkConst(s25, "_x53");
110 : 2 : Term t45 = tm.mkVar(s31, "_x54");
111 : 2 : Term t46 = tm.mkVar(s25, "_x55");
112 : 2 : Term t47 = tm.mkConst(s1, "_x56");
113 : 2 : Term t48 = tm.mkConst(s27, "_x57");
114 : 2 : Term t49 = tm.mkConst(s23, "_x58");
115 : 2 : Term t50 = tm.mkConst(s2, "_x59");
116 : 2 : Term t51 = tm.mkFloatingPointPosZero(5, 11);
117 : 2 : Term t52 = tm.mkConst(s24, "_x61");
118 : 3 : Term t53 = tm.mkBitVector(16, "1011011010000101", 2);
119 : 2 : Term t54 = tm.mkFloatingPoint(5, 11, t53);
120 : 2 : Term t55 = tm.mkVar(s26, "_x62");
121 : 6 : Term t56 = tm.mkTerm(Kind::EQUAL, {t52, t52, t52});
122 : 2 : Sort s57 = t56.getSort();
123 : 2 : Op o58 = tm.mkOp(Kind::ADD);
124 : 5 : Term t59 = tm.mkTerm(o58, {t47, t47});
125 : 2 : Op o60 = tm.mkOp(Kind::NOT);
126 : 4 : Term t61 = tm.mkTerm(o60, {t56});
127 : 5 : Term t62 = tm.mkTerm(Kind::APPLY_UF, {t40, t51});
128 : 4 : Term t63 = tm.mkTerm(Kind::LT, {t47, t47});
129 : 1 : solver.assertFormula(t61);
130 : 1 : solver.checkSat();
131 : 1 : solver.blockModel(cvc5::modes::BlockModelsMode::LITERALS);
132 : :
133 : 1 : return 0;
134 : : }
|
