Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Haniel Barbosa, Andrew Reynolds, Aina Niemetz
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2025 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 : : * The RealToInt preprocessing pass.
14 : : *
15 : : * Converts real operations into integer operations.
16 : : */
17 : :
18 : : #include "preprocessing/passes/real_to_int.h"
19 : :
20 : : #include <string>
21 : :
22 : : #include "expr/skolem_manager.h"
23 : : #include "preprocessing/assertion_pipeline.h"
24 : : #include "preprocessing/preprocessing_pass_context.h"
25 : : #include "theory/arith/arith_msum.h"
26 : : #include "theory/rewriter.h"
27 : : #include "theory/theory_model.h"
28 : : #include "util/rational.h"
29 : :
30 : : using namespace cvc5::internal::kind;
31 : : using namespace cvc5::internal::theory;
32 : :
33 : : namespace cvc5::internal {
34 : : namespace preprocessing {
35 : : namespace passes {
36 : :
37 : 50592 : RealToInt::RealToInt(PreprocessingPassContext* preprocContext)
38 : 50592 : : PreprocessingPass(preprocContext, "real-to-int"), d_cache(userContext())
39 : : {
40 : 50592 : }
41 : :
42 : 241 : Node RealToInt::realToIntInternal(TNode n, NodeMap& cache, std::vector<Node>& var_eq)
43 : : {
44 [ + - ]: 241 : Trace("real-as-int-debug") << "Convert : " << n << std::endl;
45 : 241 : NodeMap::iterator find = cache.find(n);
46 [ + + ]: 241 : if (find != cache.end())
47 : : {
48 : 53 : return (*find).second;
49 : : }
50 : : else
51 : : {
52 : 188 : NodeManager* nm = nodeManager();
53 : 188 : SkolemManager* sm = nm->getSkolemManager();
54 : 188 : Node ret = n;
55 [ + + ]: 188 : if (n.getNumChildren() > 0)
56 : : {
57 : 127 : if ((n.getKind() == Kind::EQUAL && n[0].getType().isReal())
58 [ + + ][ + - ]: 98 : || n.getKind() == Kind::GEQ || n.getKind() == Kind::LT
59 [ + + ][ + - ]: 218 : || n.getKind() == Kind::GT || n.getKind() == Kind::LEQ)
[ - + ][ + + ]
60 : : {
61 : 43 : ret = rewrite(n);
62 [ + - ]: 43 : Trace("real-as-int-debug") << "Now looking at : " << ret << std::endl;
63 [ + - ]: 43 : if (!ret.isConst())
64 : : {
65 [ - + ]: 43 : Node ret_lit = ret.getKind() == Kind::NOT ? ret[0] : ret;
66 : 43 : bool ret_pol = ret.getKind() != Kind::NOT;
67 : 43 : std::map<Node, Node> msum;
68 [ + - ]: 43 : if (ArithMSum::getMonomialSumLit(ret_lit, msum))
69 : : {
70 : : // get common coefficient
71 : 43 : std::vector<Node> coeffs;
72 : 43 : for (std::map<Node, Node>::iterator itm = msum.begin();
73 [ + + ]: 120 : itm != msum.end();
74 : 77 : ++itm)
75 : : {
76 : 77 : Node v = itm->first;
77 : 77 : Node c = itm->second;
78 [ + + ]: 77 : if (!c.isNull())
79 : : {
80 [ - + ][ - + ]: 51 : Assert(c.isConst());
[ - - ]
81 : 51 : coeffs.push_back(nm->mkConstInt(
82 : 102 : Rational(c.getConst<Rational>().getDenominator())));
83 : : }
84 : 77 : }
85 : 43 : Node cc = coeffs.empty()
86 : : ? Node::null()
87 : 67 : : (coeffs.size() == 1 ? coeffs[0]
88 [ - - ]: 9 : : rewrite(nodeManager()->mkNode(
89 [ + + ][ + + ]: 128 : Kind::MULT, coeffs)));
[ + + ][ + + ]
[ - - ]
90 : 43 : std::vector<Node> sum;
91 : 43 : for (std::map<Node, Node>::iterator itm = msum.begin();
92 [ + + ]: 120 : itm != msum.end();
93 : 77 : ++itm)
94 : : {
95 : 77 : Node v = itm->first;
96 : 77 : Node c = itm->second;
97 : 77 : Node s;
98 [ + + ]: 77 : if (c.isNull())
99 : : {
100 [ + + ][ + + ]: 26 : c = cc.isNull() ? nodeManager()->mkConstInt(Rational(1)) : cc;
[ - - ]
101 : : }
102 : : else
103 : : {
104 [ + - ]: 51 : if (!cc.isNull())
105 : : {
106 : 102 : c = nm->mkConstInt(c.getConst<Rational>()
107 : 153 : * cc.getConst<Rational>());
108 : : }
109 : : }
110 [ - + ][ - + ]: 77 : Assert(c.getType().isInteger());
[ - - ]
111 [ + + ]: 77 : if (v.isNull())
112 : : {
113 : 17 : sum.push_back(c);
114 : : }
115 : : else
116 : : {
117 : 60 : Node vv = realToIntInternal(v, cache, var_eq);
118 [ + - ]: 60 : if (vv.getType().isInteger())
119 : : {
120 : 60 : sum.push_back(nodeManager()->mkNode(Kind::MULT, c, vv));
121 : : }
122 : : else
123 : : {
124 : 0 : throw TypeCheckingExceptionPrivate(
125 : : v,
126 : 0 : std::string("Cannot translate to Int: ") + v.toString());
127 : : }
128 : 60 : }
129 : 77 : }
130 : : Node sumt =
131 : 43 : sum.empty()
132 [ - + ][ - - ]: 43 : ? nm->mkConstInt(Rational(0))
133 [ - + ][ + + ]: 43 : : (sum.size() == 1 ? sum[0] : nm->mkNode(Kind::ADD, sum));
134 : 86 : ret = nm->mkNode(
135 : 129 : ret_lit.getKind(), sumt, nm->mkConstInt(Rational(0)));
136 [ - + ]: 43 : if (!ret_pol)
137 : : {
138 : 0 : ret = ret.negate();
139 : : }
140 [ + - ]: 43 : Trace("real-as-int") << "Convert : " << std::endl;
141 [ + - ]: 43 : Trace("real-as-int") << " " << n << std::endl;
142 [ + - ]: 43 : Trace("real-as-int") << " " << ret << std::endl;
143 : 43 : }
144 : 43 : }
145 : : }
146 : : else
147 : : {
148 : 66 : bool childChanged = false;
149 : 66 : std::vector<Node> children;
150 : 66 : Kind k = n.getKind();
151 : 66 : bool preserveTypes = true;
152 : : // We change Real equalities to Int equalities, we handle other kinds
153 : : // here as well.
154 [ + + ][ + - ]: 66 : if (k==Kind::EQUAL || k==Kind::MULT || k==Kind::NONLINEAR_MULT ||
[ + + ][ + - ]
155 [ + - ][ - + ]: 47 : k==Kind::ADD || k==Kind::SUB || k==Kind::NEG)
156 : : {
157 : 19 : preserveTypes = false;
158 : : }
159 [ + + ]: 158 : for (size_t i = 0; i < n.getNumChildren(); i++)
160 : : {
161 : 92 : Node nc = realToIntInternal(n[i], cache, var_eq);
162 : : // must preserve types if we don't belong to arithmetic, cast back
163 [ + + ]: 92 : if (preserveTypes)
164 : : {
165 : 52 : if (!n[i].getType().isInteger() && nc.getType().isInteger())
166 : : {
167 : 4 : nc = nm->mkNode(Kind::TO_REAL, nc);
168 : : }
169 : : }
170 [ + + ][ + + ]: 92 : childChanged = childChanged || nc != n[i];
[ + + ][ - - ]
171 : 92 : children.push_back(nc);
172 : 92 : }
173 [ + + ]: 66 : if (childChanged)
174 : : {
175 [ + + ]: 56 : if (n.getMetaKind() == kind::metakind::PARAMETERIZED)
176 : : {
177 : 2 : children.insert(children.begin(), n.getOperator());
178 : : }
179 : 56 : ret = nm->mkNode(k, children);
180 : : }
181 : 66 : }
182 : : }
183 : : else
184 : : {
185 : 79 : TypeNode tn = n.getType();
186 [ + + ]: 79 : if (tn.isReal())
187 : : {
188 [ - + ]: 36 : if (n.getKind() == Kind::BOUND_VARIABLE)
189 : : {
190 : : // cannot change the type of quantified variables, since this leads
191 : : // to incompleteness.
192 : 0 : throw TypeCheckingExceptionPrivate(
193 : : n,
194 : 0 : std::string("Cannot translate bound variable to Int: ")
195 : 0 : + n.toString());
196 : : }
197 [ + + ]: 36 : else if (n.isVar())
198 : : {
199 : 35 : Node toIntN = nm->mkNode(Kind::TO_INTEGER, n);
200 : 35 : ret = sm->mkPurifySkolem(toIntN);
201 : 35 : Node retToReal = nm->mkNode(Kind::TO_REAL, ret);
202 : 35 : var_eq.push_back(n.eqNode(retToReal));
203 : : // add the substitution to the preprocessing context, which ensures
204 : : // the model for n is correct, as well as substituting it in the input
205 : : // assertions when necessary.
206 : : // The model value for the Real variable n we are eliminating is
207 : : // (to_real k), where k is the Int skolem whose unpurified form is
208 : : // (to_int n).
209 : 35 : d_preprocContext->addSubstitution(n, retToReal);
210 : 35 : }
211 : : }
212 : 79 : }
213 : 188 : cache[n] = ret;
214 : 188 : return ret;
215 : 188 : }
216 : : }
217 : :
218 : 31 : PreprocessingPassResult RealToInt::applyInternal(
219 : : AssertionPipeline* assertionsToPreprocess)
220 : : {
221 : 31 : std::vector<Node> var_eq;
222 [ + + ]: 120 : for (unsigned i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
223 : : {
224 : 89 : Node a = (*assertionsToPreprocess)[i];
225 : 89 : Node ac = realToIntInternal(a, d_cache, var_eq);
226 [ + + ]: 89 : if (ac != a)
227 : : {
228 : : // this pass is refutation unsound, "unsat" will be "unknown"
229 : 47 : assertionsToPreprocess->markRefutationUnsound();
230 [ + - ]: 47 : Trace("real-to-int") << "Converted " << a << " to " << ac << std::endl;
231 : 47 : assertionsToPreprocess->replace(
232 : : i, ac, nullptr, TrustId::PREPROCESS_REAL_TO_INT);
233 : 47 : assertionsToPreprocess->ensureRewritten(i);
234 [ - + ]: 47 : if (assertionsToPreprocess->isInConflict())
235 : : {
236 : 0 : return PreprocessingPassResult::CONFLICT;
237 : : }
238 : : }
239 [ + - ][ + - ]: 89 : }
240 : 31 : return PreprocessingPassResult::NO_CONFLICT;
241 : 31 : }
242 : :
243 : :
244 : : } // namespace passes
245 : : } // namespace preprocessing
246 : : } // namespace cvc5::internal
|
