File: proj-issue573.cpp

package info (click to toggle)
cvc5 1.1.2-3
  • links: PTS, VCS
  • area: main
  • in suites: forky, sid
  • size: 80,856 kB
  • sloc: cpp: 339,634; java: 10,248; python: 10,063; sh: 6,726; ansic: 1,622; lisp: 763; perl: 207; makefile: 33
file content (144 lines) | stat: -rw-r--r-- 5,886 bytes parent folder | download | duplicates (2)
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
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2023 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 #573
 *
 */
#include <cvc5/cvc5.h>

using namespace cvc5;
int main(void)
{
  Solver solver;
  solver.setOption("incremental", "false");
  solver.setOption("produce-models", "true");
  Sort s0 = solver.getRoundingModeSort();
  Sort s1 = solver.mkFloatingPointSort(5, 11);
  Sort s2 = solver.mkBitVectorSort(1);
  Sort s3 = solver.mkBitVectorSort(5);
  Sort s4 = solver.mkBitVectorSort(10);
  Sort s5 = solver.mkBitVectorSort(16);
  Sort s6 = solver.mkFloatingPointSort(11, 53);
  Sort s7 = solver.mkBitVectorSort(1);
  Sort s8 = solver.mkBitVectorSort(11);
  Sort s9 = solver.mkBitVectorSort(52);
  Sort s10 = solver.mkBitVectorSort(64);
  DatatypeDecl d11 = solver.mkDatatypeDecl("_dt0");
  DatatypeConstructorDecl dtcd12 = solver.mkDatatypeConstructorDecl("_cons2");
  dtcd12.addSelector("_sel1", s8);
  d11.addConstructor(dtcd12);
  std::vector<Sort> v13 = solver.mkDatatypeSorts({d11});
  Sort s14 = v13[0];
  Term t15 = solver.mkRoundingMode(cvc5::RoundingMode::ROUND_TOWARD_ZERO);
  Term t16 = solver.mkVar(s5, "_f3_0");
  Term t17 = solver.mkVar(s8, "_f3_1");
  Term t18 = solver.mkVar(s5, "_f3_2");
  Op o19 = solver.mkOp(Kind::EQUAL);
  Term t20 = solver.mkTerm(o19, {t15, t15});
  Sort s21 = t20.getSort();
  Term t22 = solver.mkTerm(Kind::DISTINCT, {t20, t20});
  Term t23 = solver.mkTerm(Kind::AND, {t22, t22});
  Op o24 = solver.mkOp(Kind::SET_SINGLETON);
  Term t25 = solver.mkTerm(o24, {t20});
  Sort s26 = t25.getSort();
  Op o27 = solver.mkOp(Kind::SET_CHOOSE);
  Term t28 = solver.mkTerm(o27, {t25});
  Op o29 = solver.mkOp(Kind::SET_INSERT);
  Term t30 = solver.mkTerm(o29, {t20, t25});
  Op o31 = solver.mkOp(Kind::IMPLIES);
  Term t32 = solver.mkTerm(o31, {t20, t23});
  Op o33 = solver.mkOp(Kind::SET_INSERT);
  Term t34 = solver.mkTerm(o29, {t32, t25});
  Term t35 = solver.mkTerm(Kind::SET_CHOOSE, {t34});
  Term t36 = solver.mkVar(s14, "_f4_0");
  Term t37 = solver.mkVar(s9, "_f4_1");
  Op o38 = solver.mkOp(Kind::SET_CHOOSE);
  Term t39 = solver.mkTerm(o27, {t25});
  Op o40 = solver.mkOp(Kind::APPLY_SELECTOR);
  Datatype dt41 = s14.getDatatype();
  DatatypeConstructor dtc42 = dt41.operator[]("_cons2");
  DatatypeSelector dts43 = dtc42.getSelector("_sel1");
  Term t44 = dts43.getTerm();
  Sort s45 = t44.getSort();
  Term t46 = solver.mkTerm(o40, {t44, t36});
  Op o47 = solver.mkOp(Kind::APPLY_UPDATER);
  Datatype dt48 = s14.getDatatype();
  DatatypeConstructor dtc49 = dt41.operator[]("_cons2");
  DatatypeSelector dts50 = dtc42.getSelector("_sel1");
  Term t51 = dts43.getUpdaterTerm();
  Sort s52 = t51.getSort();
  Term t53 = solver.mkTerm(o47, {t51, t36, t46});
  Op o54 = solver.mkOp(Kind::SET_CHOOSE);
  Term t55 = solver.mkTerm(o27, {t25});
  Op o56 = solver.mkOp(Kind::APPLY_UPDATER);
  Datatype dt57 = s14.getDatatype();
  DatatypeConstructor dtc58 = dt41.operator[]("_cons2");
  DatatypeSelector dts59 = dtc42.getSelector("_sel1");
  Term t60 = dts43.getUpdaterTerm();
  Term t61 = solver.mkTerm(o47, {t51, t53, t46});
  Op o62 = solver.mkOp(Kind::DISTINCT);
  Term t63 = solver.mkTerm(o62, {t25, t25});
  Term t64 = solver.mkVar(s10, "_f5_0");
  Term t65 = solver.mkVar(s21, "_f5_1");
  Term t66 = solver.mkTerm(Kind::SET_CHOOSE, {t25});
  Op o67 = solver.mkOp(Kind::ITE);
  Term t68 = t20.iteTerm(t25, t25);
  Op o69 = solver.mkOp(Kind::SET_CHOOSE);
  Term t70 = solver.mkTerm(o27, {t25});
  Term t71 = solver.mkTerm(Kind::EQUAL, {t25, t25});
  Term t72 = solver.mkVar(s6, "_f6_0");
  Term t73 = solver.mkVar(s9, "_f6_1");
  Op o74 = solver.mkOp(Kind::SET_CHOOSE);
  Term t75 = solver.mkTerm(o27, {t25});
  Op o76 = solver.mkOp(Kind::FLOATINGPOINT_DIV);
  Term t77 = solver.mkTerm(o76, {t15, t72, t72});
  Op o78 = solver.mkOp(Kind::SET_CHOOSE);
  Term t79 = solver.mkTerm(o27, {t25});
  Op o80 = solver.mkOp(Kind::FLOATINGPOINT_REM);
  Term t81 = solver.mkTerm(o80, {t77, t72});
  Op o82 = solver.mkOp(Kind::ITE);
  Term t83 = solver.mkTerm(o67, {t20, t73, t73});
  Op o84 = solver.mkOp(Kind::FLOATINGPOINT_TO_FP_FROM_UBV, {11, 53});
  Term t85 = solver.mkTerm(o84, {t15, t83});
  Op o86 = solver.mkOp(Kind::SET_CHOOSE);
  Term t87 = solver.mkTerm(o27, {t25});
  Op o88 = solver.mkOp(Kind::FLOATINGPOINT_MIN);
  Term t89 = solver.mkTerm(o88, {t77, t77});
  Op o90 = solver.mkOp(Kind::SET_CHOOSE);
  Term t91 = solver.mkTerm(o27, {t25});
  Op o92 = solver.mkOp(Kind::SET_CHOOSE);
  Term t93 = solver.mkTerm(o27, {t25});
  Op o94 = solver.mkOp(Kind::FLOATINGPOINT_MIN);
  Term t95 = solver.mkTerm(o88, {t77, t77});
  Op o96 = solver.mkOp(Kind::SET_CHOOSE);
  Term t97 = solver.mkTerm(o27, {t25});
  Op o98 = solver.mkOp(Kind::FLOATINGPOINT_FMA);
  Term t99 = solver.mkTerm(o98, {t15, t77, t77, t77});
  Op o100 = solver.mkOp(Kind::ITE);
  Term t101 = solver.mkTerm(o67, {t35, t20, t20});
  Op o102 = solver.mkOp(Kind::SET_CHOOSE);
  Term t103 = solver.mkTerm(o27, {t25});
  Op o104 = solver.mkOp(Kind::SET_CHOOSE);
  Term t105 = solver.mkTerm(o27, {t25});
  Op o106 = solver.mkOp(Kind::FLOATINGPOINT_NEG);
  Term t107 = solver.mkTerm(o106, {t77});
  Op o108 = solver.mkOp(Kind::ITE);
  Term t109 = solver.mkTerm(o67, {t101, t101, t20});
  Term t110 = solver.mkVar(s26, "_f7_0");
  Term t111 = solver.mkVar(s4, "_f7_1");
  Term t112 = solver.mkVar(s8, "_f7_2");
  solver.assertFormula(t109);
  solver.checkSat();
  solver.blockModel(cvc5::modes::BlockModelsMode::LITERALS);

  return 0;
}