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 #573
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("produce-models", "true");
25 : 2 : Sort s0 = tm.getRoundingModeSort();
26 : 2 : Sort s1 = tm.mkFloatingPointSort(5, 11);
27 : 2 : Sort s2 = tm.mkBitVectorSort(1);
28 : 2 : Sort s3 = tm.mkBitVectorSort(5);
29 : 2 : Sort s4 = tm.mkBitVectorSort(10);
30 : 2 : Sort s5 = tm.mkBitVectorSort(16);
31 : 2 : Sort s6 = tm.mkFloatingPointSort(11, 53);
32 : 2 : Sort s7 = tm.mkBitVectorSort(1);
33 : 2 : Sort s8 = tm.mkBitVectorSort(11);
34 : 2 : Sort s9 = tm.mkBitVectorSort(52);
35 : 2 : Sort s10 = tm.mkBitVectorSort(64);
36 : 3 : DatatypeDecl d11 = tm.mkDatatypeDecl("_dt0");
37 : 3 : DatatypeConstructorDecl dtcd12 = tm.mkDatatypeConstructorDecl("_cons2");
38 : 1 : dtcd12.addSelector("_sel1", s8);
39 : 1 : d11.addConstructor(dtcd12);
40 : 4 : std::vector<Sort> v13 = tm.mkDatatypeSorts({d11});
41 : 2 : Sort s14 = v13[0];
42 : 2 : Term t15 = tm.mkRoundingMode(cvc5::RoundingMode::ROUND_TOWARD_ZERO);
43 : 2 : Term t16 = tm.mkVar(s5, "_f3_0");
44 : 2 : Term t17 = tm.mkVar(s8, "_f3_1");
45 : 2 : Term t18 = tm.mkVar(s5, "_f3_2");
46 : 2 : Op o19 = tm.mkOp(Kind::EQUAL);
47 : 5 : Term t20 = tm.mkTerm(o19, {t15, t15});
48 : 2 : Sort s21 = t20.getSort();
49 : 5 : Term t22 = tm.mkTerm(Kind::DISTINCT, {t20, t20});
50 : 5 : Term t23 = tm.mkTerm(Kind::AND, {t22, t22});
51 : 2 : Op o24 = tm.mkOp(Kind::SET_SINGLETON);
52 : 4 : Term t25 = tm.mkTerm(o24, {t20});
53 : 2 : Sort s26 = t25.getSort();
54 : 2 : Op o27 = tm.mkOp(Kind::SET_CHOOSE);
55 : 4 : Term t28 = tm.mkTerm(o27, {t25});
56 : 2 : Op o29 = tm.mkOp(Kind::SET_INSERT);
57 : 5 : Term t30 = tm.mkTerm(o29, {t20, t25});
58 : 2 : Op o31 = tm.mkOp(Kind::IMPLIES);
59 : 5 : Term t32 = tm.mkTerm(o31, {t20, t23});
60 : 2 : Op o33 = tm.mkOp(Kind::SET_INSERT);
61 : 5 : Term t34 = tm.mkTerm(o29, {t32, t25});
62 : 4 : Term t35 = tm.mkTerm(Kind::SET_CHOOSE, {t34});
63 : 2 : Term t36 = tm.mkVar(s14, "_f4_0");
64 : 2 : Term t37 = tm.mkVar(s9, "_f4_1");
65 : 2 : Op o38 = tm.mkOp(Kind::SET_CHOOSE);
66 : 4 : Term t39 = tm.mkTerm(o27, {t25});
67 : 2 : Op o40 = tm.mkOp(Kind::APPLY_SELECTOR);
68 : 2 : Datatype dt41 = s14.getDatatype();
69 : 3 : DatatypeConstructor dtc42 = dt41.operator[]("_cons2");
70 : 3 : DatatypeSelector dts43 = dtc42.getSelector("_sel1");
71 : 2 : Term t44 = dts43.getTerm();
72 : 2 : Sort s45 = t44.getSort();
73 : 5 : Term t46 = tm.mkTerm(o40, {t44, t36});
74 : 2 : Op o47 = tm.mkOp(Kind::APPLY_UPDATER);
75 : 2 : Datatype dt48 = s14.getDatatype();
76 : 3 : DatatypeConstructor dtc49 = dt41.operator[]("_cons2");
77 : 3 : DatatypeSelector dts50 = dtc42.getSelector("_sel1");
78 : 2 : Term t51 = dts43.getUpdaterTerm();
79 : 2 : Sort s52 = t51.getSort();
80 : 6 : Term t53 = tm.mkTerm(o47, {t51, t36, t46});
81 : 2 : Op o54 = tm.mkOp(Kind::SET_CHOOSE);
82 : 4 : Term t55 = tm.mkTerm(o27, {t25});
83 : 2 : Op o56 = tm.mkOp(Kind::APPLY_UPDATER);
84 : 2 : Datatype dt57 = s14.getDatatype();
85 : 3 : DatatypeConstructor dtc58 = dt41.operator[]("_cons2");
86 : 3 : DatatypeSelector dts59 = dtc42.getSelector("_sel1");
87 : 2 : Term t60 = dts43.getUpdaterTerm();
88 : 6 : Term t61 = tm.mkTerm(o47, {t51, t53, t46});
89 : 2 : Op o62 = tm.mkOp(Kind::DISTINCT);
90 : 5 : Term t63 = tm.mkTerm(o62, {t25, t25});
91 : 2 : Term t64 = tm.mkVar(s10, "_f5_0");
92 : 2 : Term t65 = tm.mkVar(s21, "_f5_1");
93 : 4 : Term t66 = tm.mkTerm(Kind::SET_CHOOSE, {t25});
94 : 2 : Op o67 = tm.mkOp(Kind::ITE);
95 : 2 : Term t68 = t20.iteTerm(t25, t25);
96 : 2 : Op o69 = tm.mkOp(Kind::SET_CHOOSE);
97 : 4 : Term t70 = tm.mkTerm(o27, {t25});
98 : 5 : Term t71 = tm.mkTerm(Kind::EQUAL, {t25, t25});
99 : 2 : Term t72 = tm.mkVar(s6, "_f6_0");
100 : 2 : Term t73 = tm.mkVar(s9, "_f6_1");
101 : 2 : Op o74 = tm.mkOp(Kind::SET_CHOOSE);
102 : 4 : Term t75 = tm.mkTerm(o27, {t25});
103 : 2 : Op o76 = tm.mkOp(Kind::FLOATINGPOINT_DIV);
104 : 6 : Term t77 = tm.mkTerm(o76, {t15, t72, t72});
105 : 2 : Op o78 = tm.mkOp(Kind::SET_CHOOSE);
106 : 4 : Term t79 = tm.mkTerm(o27, {t25});
107 : 2 : Op o80 = tm.mkOp(Kind::FLOATINGPOINT_REM);
108 : 5 : Term t81 = tm.mkTerm(o80, {t77, t72});
109 : 2 : Op o82 = tm.mkOp(Kind::ITE);
110 : 6 : Term t83 = tm.mkTerm(o67, {t20, t73, t73});
111 : 2 : Op o84 = tm.mkOp(Kind::FLOATINGPOINT_TO_FP_FROM_UBV, {11, 53});
112 : 5 : Term t85 = tm.mkTerm(o84, {t15, t83});
113 : 2 : Op o86 = tm.mkOp(Kind::SET_CHOOSE);
114 : 4 : Term t87 = tm.mkTerm(o27, {t25});
115 : 2 : Op o88 = tm.mkOp(Kind::FLOATINGPOINT_MIN);
116 : 5 : Term t89 = tm.mkTerm(o88, {t77, t77});
117 : 2 : Op o90 = tm.mkOp(Kind::SET_CHOOSE);
118 : 4 : Term t91 = tm.mkTerm(o27, {t25});
119 : 2 : Op o92 = tm.mkOp(Kind::SET_CHOOSE);
120 : 4 : Term t93 = tm.mkTerm(o27, {t25});
121 : 2 : Op o94 = tm.mkOp(Kind::FLOATINGPOINT_MIN);
122 : 5 : Term t95 = tm.mkTerm(o88, {t77, t77});
123 : 2 : Op o96 = tm.mkOp(Kind::SET_CHOOSE);
124 : 4 : Term t97 = tm.mkTerm(o27, {t25});
125 : 2 : Op o98 = tm.mkOp(Kind::FLOATINGPOINT_FMA);
126 : 7 : Term t99 = tm.mkTerm(o98, {t15, t77, t77, t77});
127 : 2 : Op o100 = tm.mkOp(Kind::ITE);
128 : 6 : Term t101 = tm.mkTerm(o67, {t35, t20, t20});
129 : 2 : Op o102 = tm.mkOp(Kind::SET_CHOOSE);
130 : 4 : Term t103 = tm.mkTerm(o27, {t25});
131 : 2 : Op o104 = tm.mkOp(Kind::SET_CHOOSE);
132 : 4 : Term t105 = tm.mkTerm(o27, {t25});
133 : 2 : Op o106 = tm.mkOp(Kind::FLOATINGPOINT_NEG);
134 : 4 : Term t107 = tm.mkTerm(o106, {t77});
135 : 2 : Op o108 = tm.mkOp(Kind::ITE);
136 : 6 : Term t109 = tm.mkTerm(o67, {t101, t101, t20});
137 : 2 : Term t110 = tm.mkVar(s26, "_f7_0");
138 : 2 : Term t111 = tm.mkVar(s4, "_f7_1");
139 : 1 : Term t112 = tm.mkVar(s8, "_f7_2");
140 : 1 : solver.assertFormula(t109);
141 : 1 : solver.checkSat();
142 : 1 : solver.blockModel(cvc5::modes::BlockModelsMode::LITERALS);
143 : :
144 : 1 : return 0;
145 : : }
|
