Branch data Line data Source code
1 : : /******************************************************************************
2 : : * This file is part of the cvc5 project.
3 : : *
4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 : : * in the top-level source directory and their institutional affiliations.
6 : : * All rights reserved. See the file COPYING in the top-level source
7 : : * directory for licensing information.
8 : : * ****************************************************************************
9 : : *
10 : : * encoding Nodes as cocoa ring elements.
11 : : */
12 : :
13 : : #ifdef CVC5_USE_COCOA
14 : :
15 : : #include "theory/ff/cocoa_encoder.h"
16 : :
17 : : // external includes
18 : : #include <CoCoA/BigInt.H>
19 : : #include <CoCoA/QuotientRing.H>
20 : : #include <CoCoA/SparsePolyIter.H>
21 : : #include <CoCoA/SparsePolyOps-RingElem.H>
22 : : #include <CoCoA/SparsePolyRing.H>
23 : :
24 : : // std includes
25 : : #include <sstream>
26 : :
27 : : // internal includes
28 : : #include "expr/node_traversal.h"
29 : : #include "theory/ff/cocoa_util.h"
30 : : #include "theory/theory.h"
31 : :
32 : : namespace cvc5::internal {
33 : : namespace theory {
34 : : namespace ff {
35 : :
36 : : #define LETTER(c) (('a' <= c && c <= 'z') || ('A' <= c && c <= 'Z'))
37 : :
38 : : // CoCoA symbols must start with a letter and contain only letters, numbers, and
39 : : // underscores.
40 : : //
41 : : // Our encoding is described within
42 : 28437 : CoCoA::symbol cocoaSym(const std::string& varName, std::optional<size_t> index)
43 : : {
44 : 28437 : std::ostringstream o;
45 [ + + ]: 143275 : for (const auto c : varName)
46 : : {
47 : : // letters and numbers as themselves
48 : 114838 : uint8_t code = c;
49 [ + + ][ - + ]: 114838 : if (LETTER(c) || ('0' <= c && c <= '9'))
[ + + ][ + - ]
[ + - ][ + + ]
50 : : {
51 : 110242 : o << c;
52 : : }
53 : : // _ as __
54 [ + + ]: 4596 : else if ('_' == c)
55 : : {
56 : 3058 : o << "__";
57 : : }
58 : : // other as _xXX (XX is hex)
59 : : else
60 : : {
61 : : o << "_x"
62 : 1538 : << "0123456789abcdef"[code & 0x0f]
63 : 1538 : << "0123456789abcdef"[(code >> 4) & 0x0f];
64 : : }
65 : : }
66 : : // if we're starting with something bad, prepend u__; note that the above
67 : : // never produces __.
68 : 28437 : std::string s = o.str();
69 [ + + ][ - + ]: 28437 : if (!LETTER(s[0]))
[ + + ][ + - ]
[ + + ]
70 : : {
71 : 4346 : s.insert(0, "u__");
72 : : }
73 [ + + ]: 56874 : return index.has_value() ? CoCoA::symbol(s, *index) : CoCoA::symbol(s);
74 : 28437 : }
75 : :
76 : 1941 : CocoaEncoder::CocoaEncoder(NodeManager* nm, const FfSize& size)
77 : 1941 : : FieldObj(nm, size)
78 : : {
79 : 1941 : }
80 : :
81 : 27085 : CoCoA::symbol CocoaEncoder::freshSym(const std::string& varName,
82 : : std::optional<size_t> index)
83 : : {
84 [ + - ]: 27085 : Trace("ff::cocoa::sym") << "CoCoA sym for " << varName;
85 [ + + ]: 27085 : if (index.has_value())
86 : : {
87 [ + - ]: 16863 : Trace("ff::cocoa::sym") << "[" << *index << "]";
88 : : }
89 [ + - ]: 27085 : Trace("ff::cocoa::sym") << std::endl;
90 [ - + ][ - + ]: 27085 : Assert(d_stage == Stage::Scan);
[ - - ]
91 : 27085 : std::optional<size_t> suffix = {};
92 : 54170 : CoCoA::symbol sym("dummy");
93 : 27085 : std::string symString;
94 : : do
95 : : {
96 : 28437 : std::string n = suffix.has_value()
97 : 31141 : ? varName + "_" + std::to_string(suffix.value())
98 [ + + ]: 29789 : : varName;
99 : 28437 : sym = cocoaSym(n, index);
100 : 28437 : symString = extractStr(sym);
101 [ + + ]: 28437 : if (suffix.has_value())
102 : : {
103 : 1352 : *suffix += 1;
104 : : }
105 : : else
106 : : {
107 : 27085 : suffix = std::make_optional(0);
108 : : }
109 [ + + ]: 28437 : } while (d_vars.count(symString));
110 : 27085 : d_vars.insert(symString);
111 : 27085 : d_syms.push_back(sym);
112 : 54170 : return sym;
113 : 27085 : }
114 : :
115 : 1941 : void CocoaEncoder::endScan()
116 : : {
117 [ - + ][ - + ]: 1941 : Assert(d_stage == Stage::Scan);
[ - - ]
118 : 1941 : d_stage = Stage::Encode;
119 : 1941 : d_coeffRing = CoCoA::NewZZmod(intToCocoa(size()));
120 : 1941 : d_polyRing = CoCoA::NewPolyRing(*d_coeffRing, d_syms);
121 [ + + ]: 29026 : for (size_t i = 0, n = d_syms.size(); i < n; ++i)
122 : : {
123 : 27085 : d_symPolys.insert({extractStr(d_syms[i]), CoCoA::indet(*d_polyRing, i)});
124 : : }
125 : 1941 : }
126 : :
127 : 63750 : void CocoaEncoder::addFact(const Node& fact)
128 : : {
129 [ - + ][ - + ]: 63750 : Assert(isFfFact(fact, size()));
[ - - ]
130 [ + + ]: 63750 : if (d_stage == Stage::Scan)
131 : : {
132 : 31875 : for (const auto& node :
133 : 138177 : NodeDfsIterable(fact, VisitOrder::POSTORDER, [this](TNode nn) {
134 : 138177 : return d_scanned.count(nn);
135 [ + + ]: 139605 : }))
136 : : {
137 [ - + ]: 75855 : if (!d_scanned.insert(node).second)
138 : : {
139 : 0 : continue;
140 : : }
141 [ + + ][ + + ]: 75855 : if (isFfLeaf(node, size()) && !node.isConst())
[ + - ][ + + ]
[ - - ]
142 : : {
143 [ + - ]: 10222 : Trace("ff::cocoa") << "CoCoA var sym for " << node << std::endl;
144 : 10222 : CoCoA::symbol sym = freshSym(node.getName());
145 [ - + ][ - + ]: 10222 : Assert(!d_varSyms.count(node));
[ - - ]
146 [ - + ][ - + ]: 10222 : Assert(!d_symNodes.count(extractStr(sym)));
[ - - ]
147 : 10222 : d_varSyms.insert({node, sym});
148 : 10222 : d_symNodes.insert({extractStr(sym), node});
149 : 10222 : }
150 [ + + ][ + - ]: 65633 : else if (node.getKind() == Kind::NOT && isFfFact(node, size()))
[ + + ][ + + ]
[ - - ]
151 : : {
152 [ + - ]: 16467 : Trace("ff::cocoa") << "CoCoA != sym for " << node << std::endl;
153 : 32934 : CoCoA::symbol sym = freshSym("diseq", d_diseqSyms.size());
154 : 16467 : d_diseqSyms.insert({node, sym});
155 : 16467 : }
156 [ + + ]: 49166 : else if (node.getKind() == Kind::FINITE_FIELD_BITSUM)
157 : : {
158 [ + - ]: 396 : Trace("ff::cocoa") << "CoCoA bitsum sym for " << node << std::endl;
159 : 792 : CoCoA::symbol sym = freshSym("bitsum", d_bitsumSyms.size());
160 : 396 : d_bitsumSyms.insert({node, sym});
161 : 396 : d_symNodes.insert({extractStr(sym), node});
162 : 396 : }
163 : 31875 : }
164 : : }
165 : : else
166 : : {
167 [ - + ][ - + ]: 31875 : Assert(d_stage == Stage::Encode);
[ - - ]
168 : 31875 : encodeFact(fact);
169 : 31875 : d_polys.push_back(d_cache.at(fact));
170 : : }
171 : 63750 : }
172 : :
173 : 755 : std::vector<Node> CocoaEncoder::bitsums() const
174 : : {
175 : 755 : std::vector<Node> bs;
176 [ + + ]: 1144 : for (const auto& [b, _] : d_bitsumSyms)
177 : : {
178 : 389 : bs.push_back(b);
179 : : }
180 : 755 : return bs;
181 : 0 : }
182 : :
183 : 373 : const Node& CocoaEncoder::symNode(CoCoA::symbol s) const
184 : : {
185 [ - + ][ - + ]: 373 : Assert(d_symNodes.count(extractStr(s)));
[ - - ]
186 : 373 : return d_symNodes.at(extractStr(s));
187 : : }
188 : :
189 : 498 : bool CocoaEncoder::hasNode(CoCoA::symbol s) const
190 : : {
191 : 498 : return d_symNodes.count(extractStr(s));
192 : : }
193 : :
194 : 124 : std::vector<std::pair<size_t, Node>> CocoaEncoder::nodeIndets() const
195 : : {
196 : 124 : std::vector<std::pair<size_t, Node>> out;
197 [ + + ]: 622 : for (size_t i = 0, end = d_syms.size(); i < end; ++i)
198 : : {
199 [ + + ]: 498 : if (hasNode(d_syms[i]))
200 : : {
201 : 373 : Node n = symNode(d_syms[i]);
202 : : // skip indets for !=
203 [ + + ]: 373 : if (isFfLeaf(n, size()))
204 : : {
205 : 366 : out.emplace_back(i, n);
206 : : }
207 : 373 : }
208 : : }
209 : 124 : return out;
210 : 0 : }
211 : :
212 : 1151 : FiniteFieldValue CocoaEncoder::cocoaFfToFfVal(const Scalar& elem) const
213 : : {
214 [ - + ][ - + ]: 1151 : Assert(d_coeffRing.has_value());
[ - - ]
215 [ - + ][ - + ]: 1151 : Assert(CoCoA::owner(elem) == d_coeffRing);
[ - - ]
216 : 1151 : return ff::cocoaFfToFfVal(elem, size());
217 : : }
218 : :
219 : 6893 : const Node& CocoaEncoder::polyFact(const Poly& poly) const
220 : : {
221 : 6893 : return d_polyFacts.at(extractStr(poly));
222 : : }
223 : :
224 : 6906 : bool CocoaEncoder::polyHasFact(const Poly& poly) const
225 : : {
226 : 6906 : return d_polyFacts.count(extractStr(poly));
227 : : }
228 : :
229 : 27085 : const Poly& CocoaEncoder::symPoly(CoCoA::symbol s) const
230 : : {
231 [ - + ][ - + ]: 27085 : Assert(d_symPolys.count(extractStr(s)));
[ - - ]
232 : 27085 : return d_symPolys.at(extractStr(s));
233 : : }
234 : :
235 : 63750 : void CocoaEncoder::encodeTerm(const Node& t)
236 : : {
237 [ - + ][ - + ]: 63750 : Assert(d_stage == Stage::Encode);
[ - - ]
238 : :
239 : : // for all un-encoded descendents:
240 : 63750 : for (const auto& node :
241 : 93297 : NodeDfsIterable(t, VisitOrder::POSTORDER, [this](TNode nn) {
242 : 93297 : return d_cache.count(nn);
243 [ + + ]: 155013 : }))
244 : : {
245 : : // a rule must put the encoding here
246 : 27513 : Poly elem;
247 : 27513 : if (isFfFact(node, size()) || isFfTerm(node, size()))
248 : : {
249 [ + - ]: 27507 : Trace("ff::cocoa::enc") << "Encode " << node;
250 : : // ff leaf
251 [ + + ][ + + ]: 27507 : if (isFfLeaf(node, size()) && !node.isConst())
[ + - ][ + + ]
[ - - ]
252 : : {
253 : 10222 : elem = symPoly(d_varSyms.at(node));
254 : : }
255 : : // ff.add
256 [ + + ]: 17285 : else if (node.getKind() == Kind::FINITE_FIELD_ADD)
257 : : {
258 : 4254 : elem = CoCoA::zero(*d_polyRing);
259 [ + + ]: 17188 : for (const auto& c : node)
260 : : {
261 : 12934 : elem += d_cache[c];
262 : 12934 : }
263 : : }
264 : : // ff.mul
265 [ + + ]: 13031 : else if (node.getKind() == Kind::FINITE_FIELD_MULT)
266 : : {
267 : 7152 : elem = CoCoA::one(*d_polyRing);
268 [ + + ]: 23232 : for (const auto& c : node)
269 : : {
270 : 16080 : elem *= d_cache[c];
271 : 16080 : }
272 : : }
273 : : // ff.bitsum
274 [ + + ]: 5879 : else if (node.getKind() == Kind::FINITE_FIELD_BITSUM)
275 : : {
276 : 396 : Poly sum = CoCoA::zero(*d_polyRing);
277 : 396 : Poly two = CoCoA::one(*d_polyRing) * 2;
278 : 396 : Poly twoPow = CoCoA::one(*d_polyRing);
279 [ + + ]: 1577 : for (const auto& c : node)
280 : : {
281 : 1181 : sum += twoPow * d_cache[c];
282 : 1181 : twoPow *= two;
283 : 1181 : }
284 : 396 : elem = symPoly(d_bitsumSyms.at(node));
285 : 396 : d_bitsumPolys.push_back(sum - elem);
286 : 396 : }
287 : : // ff constant
288 [ + - ]: 5483 : else if (node.getKind() == Kind::CONST_FINITE_FIELD)
289 : : {
290 : 5483 : elem = CoCoA::one(*d_polyRing)
291 : 10966 : * intToCocoa(node.getConst<FiniteFieldValue>().getValue());
292 : : }
293 : : // !!
294 : : else
295 : : {
296 : 0 : Unimplemented() << node;
297 : : }
298 : : }
299 : : // cache the encoding
300 : 27513 : d_cache.insert({node, elem});
301 : 91263 : }
302 : 63750 : }
303 : :
304 : 31875 : void CocoaEncoder::encodeFact(const Node& f)
305 : : {
306 [ - + ][ - + ]: 31875 : Assert(d_stage == Stage::Encode);
[ - - ]
307 [ - + ][ - + ]: 31875 : Assert(isFfFact(f, size()));
[ - - ]
308 : 31875 : Poly p;
309 : : // ==
310 [ + + ]: 31875 : if (f.getKind() == Kind::EQUAL)
311 : : {
312 : 15408 : encodeTerm(f[0]);
313 : 15408 : encodeTerm(f[1]);
314 : 15408 : p = d_cache.at(f[0]) - d_cache.at(f[1]);
315 : : }
316 : : // !=
317 : : else
318 : : {
319 : 16467 : encodeTerm(f[0][0]);
320 : 16467 : encodeTerm(f[0][1]);
321 : 32934 : Poly diff = d_cache.at(f[0][0]) - d_cache.at(f[0][1]);
322 : 16467 : p = diff * symPoly(d_diseqSyms.at(f)) - 1;
323 : 16467 : }
324 [ + + ]: 31875 : if (!CoCoA::IsZero(p))
325 : : {
326 : : // normalize; if we don't do it, CoCoA will in GB input, confusing our
327 : : // tracer.
328 : 31869 : p = p / CoCoA::LC(p);
329 : : }
330 : 31875 : d_cache.insert({f, p});
331 : 31875 : d_polyFacts.insert({extractStr(p), f});
332 : 31875 : }
333 : :
334 : : } // namespace ff
335 : : } // namespace theory
336 : : } // namespace cvc5::internal
337 : :
338 : : #endif /* CVC5_USE_COCOA */
|
