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 : 51808 : CoCoA::symbol cocoaSym(const std::string& varName, std::optional<size_t> index)
43 : : {
44 : 51808 : std::ostringstream o;
45 [ + + ]: 253927 : for (const auto c : varName)
46 : : {
47 : : // letters and numbers as themselves
48 : 202119 : uint8_t code = c;
49 [ + + ][ - + ]: 202119 : if (LETTER(c) || ('0' <= c && c <= '9'))
[ + + ][ + - ]
[ + - ][ + + ]
50 : : {
51 : 194466 : o << c;
52 : : }
53 : : // _ as __
54 [ + + ]: 7653 : else if ('_' == c)
55 : : {
56 : 6191 : o << "__";
57 : : }
58 : : // other as _xXX (XX is hex)
59 : : else
60 : : {
61 : : o << "_x"
62 : 1462 : << "0123456789abcdef"[code & 0x0f]
63 : 1462 : << "0123456789abcdef"[(code >> 4) & 0x0f];
64 : : }
65 : : }
66 : : // if we're starting with something bad, prepend u__; note that the above
67 : : // never produces __.
68 : 51808 : std::string s = o.str();
69 [ + + ][ - + ]: 51808 : if (!LETTER(s[0]))
[ + + ][ + - ]
[ + + ]
70 : : {
71 : 9566 : s.insert(0, "u__");
72 : : }
73 [ + + ]: 103616 : return index.has_value() ? CoCoA::symbol(s, *index) : CoCoA::symbol(s);
74 : 51808 : }
75 : :
76 : 2613 : CocoaEncoder::CocoaEncoder(NodeManager* nm, const FfSize& size)
77 : 2613 : : FieldObj(nm, size)
78 : : {
79 : 2613 : }
80 : :
81 : 47264 : CoCoA::symbol CocoaEncoder::freshSym(const std::string& varName,
82 : : std::optional<size_t> index)
83 : : {
84 [ + - ]: 47264 : Trace("ff::cocoa::sym") << "CoCoA sym for " << varName;
85 [ + + ]: 47264 : if (index.has_value())
86 : : {
87 [ + - ]: 32392 : Trace("ff::cocoa::sym") << "[" << *index << "]";
88 : : }
89 [ + - ]: 47264 : Trace("ff::cocoa::sym") << std::endl;
90 [ - + ][ - + ]: 47264 : Assert(d_stage == Stage::Scan);
[ - - ]
91 : 47264 : std::optional<size_t> suffix = {};
92 : 94528 : CoCoA::symbol sym("dummy");
93 : 47264 : std::string symString;
94 : : do
95 : : {
96 : 51808 : std::string n = suffix.has_value()
97 : 60896 : ? varName + "_" + std::to_string(suffix.value())
98 [ + + ]: 56352 : : varName;
99 : 51808 : sym = cocoaSym(n, index);
100 : 51808 : symString = extractStr(sym);
101 [ + + ]: 51808 : if (suffix.has_value())
102 : : {
103 : 4544 : *suffix += 1;
104 : : }
105 : : else
106 : : {
107 : 47264 : suffix = std::make_optional(0);
108 : : }
109 [ + + ]: 51808 : } while (d_vars.count(symString));
110 : 47264 : d_vars.insert(symString);
111 : 47264 : d_syms.push_back(sym);
112 : 94528 : return sym;
113 : 47264 : }
114 : :
115 : 2613 : void CocoaEncoder::endScan()
116 : : {
117 [ - + ][ - + ]: 2613 : Assert(d_stage == Stage::Scan);
[ - - ]
118 : 2613 : d_stage = Stage::Encode;
119 : 2613 : d_coeffRing = CoCoA::NewZZmod(intToCocoa(size()));
120 : 2613 : d_polyRing = CoCoA::NewPolyRing(*d_coeffRing, d_syms);
121 [ + + ]: 49877 : for (size_t i = 0, n = d_syms.size(); i < n; ++i)
122 : : {
123 : 47264 : d_symPolys.insert({extractStr(d_syms[i]), CoCoA::indet(*d_polyRing, i)});
124 : : }
125 : 2613 : }
126 : :
127 : 112638 : void CocoaEncoder::addFact(const Node& fact)
128 : : {
129 [ - + ][ - + ]: 112638 : Assert(isFfFact(fact, size()));
[ - - ]
130 [ + + ]: 112638 : if (d_stage == Stage::Scan)
131 : : {
132 : 56319 : for (const auto& node :
133 : 240832 : NodeDfsIterable(fact, VisitOrder::POSTORDER, [this](TNode nn) {
134 : 240832 : return d_scanned.count(nn);
135 [ + + ]: 242282 : }))
136 : : {
137 [ - + ]: 129644 : if (!d_scanned.insert(node).second)
138 : : {
139 : 0 : continue;
140 : : }
141 [ + + ][ + + ]: 129644 : if (isFfLeaf(node, size()) && !node.isConst())
[ + - ][ + + ]
[ - - ]
142 : : {
143 [ + - ]: 14872 : Trace("ff::cocoa") << "CoCoA var sym for " << node << std::endl;
144 : 14872 : CoCoA::symbol sym = freshSym(node.getName());
145 [ - + ][ - + ]: 14872 : Assert(!d_varSyms.count(node));
[ - - ]
146 [ - + ][ - + ]: 14872 : Assert(!d_symNodes.count(extractStr(sym)));
[ - - ]
147 : 14872 : d_varSyms.insert({node, sym});
148 : 14872 : d_symNodes.insert({extractStr(sym), node});
149 : 14872 : }
150 [ + + ][ + - ]: 114772 : else if (node.getKind() == Kind::NOT && isFfFact(node, size()))
[ + + ][ + + ]
[ - - ]
151 : : {
152 [ + - ]: 31924 : Trace("ff::cocoa") << "CoCoA != sym for " << node << std::endl;
153 : 63848 : CoCoA::symbol sym = freshSym("diseq", d_diseqSyms.size());
154 : 31924 : d_diseqSyms.insert({node, sym});
155 : 31924 : }
156 [ + + ]: 82848 : else if (node.getKind() == Kind::FINITE_FIELD_BITSUM)
157 : : {
158 [ + - ]: 468 : Trace("ff::cocoa") << "CoCoA bitsum sym for " << node << std::endl;
159 : 936 : CoCoA::symbol sym = freshSym("bitsum", d_bitsumSyms.size());
160 : 468 : d_bitsumSyms.insert({node, sym});
161 : 468 : d_symNodes.insert({extractStr(sym), node});
162 : 468 : }
163 : 56319 : }
164 : : }
165 : : else
166 : : {
167 [ - + ][ - + ]: 56319 : Assert(d_stage == Stage::Encode);
[ - - ]
168 : 56319 : encodeFact(fact);
169 : 56319 : d_polys.push_back(d_cache.at(fact));
170 : : }
171 : 112638 : }
172 : :
173 : 840 : std::vector<Node> CocoaEncoder::bitsums() const
174 : : {
175 : 840 : std::vector<Node> bs;
176 [ + + ]: 1301 : for (const auto& [b, _] : d_bitsumSyms)
177 : : {
178 : 461 : bs.push_back(b);
179 : : }
180 : 840 : return bs;
181 : 0 : }
182 : :
183 : 385 : const Node& CocoaEncoder::symNode(CoCoA::symbol s) const
184 : : {
185 [ - + ][ - + ]: 385 : Assert(d_symNodes.count(extractStr(s)));
[ - - ]
186 : 385 : return d_symNodes.at(extractStr(s));
187 : : }
188 : :
189 : 512 : bool CocoaEncoder::hasNode(CoCoA::symbol s) const
190 : : {
191 : 512 : return d_symNodes.count(extractStr(s));
192 : : }
193 : :
194 : 116 : std::vector<std::pair<size_t, Node>> CocoaEncoder::nodeIndets() const
195 : : {
196 : 116 : std::vector<std::pair<size_t, Node>> out;
197 [ + + ]: 628 : for (size_t i = 0, end = d_syms.size(); i < end; ++i)
198 : : {
199 [ + + ]: 512 : if (hasNode(d_syms[i]))
200 : : {
201 : 385 : Node n = symNode(d_syms[i]);
202 : : // skip indets for !=
203 [ + + ]: 385 : if (isFfLeaf(n, size()))
204 : : {
205 : 378 : out.emplace_back(i, n);
206 : : }
207 : 385 : }
208 : : }
209 : 116 : return out;
210 : 0 : }
211 : :
212 : 1307 : FiniteFieldValue CocoaEncoder::cocoaFfToFfVal(const Scalar& elem) const
213 : : {
214 [ - + ][ - + ]: 1307 : Assert(d_coeffRing.has_value());
[ - - ]
215 [ - + ][ - + ]: 1307 : Assert(CoCoA::owner(elem) == d_coeffRing);
[ - - ]
216 : 1307 : return ff::cocoaFfToFfVal(elem, size());
217 : : }
218 : :
219 : 11867 : const Node& CocoaEncoder::polyFact(const Poly& poly) const
220 : : {
221 : 11867 : return d_polyFacts.at(extractStr(poly));
222 : : }
223 : :
224 : 11879 : bool CocoaEncoder::polyHasFact(const Poly& poly) const
225 : : {
226 : 11879 : return d_polyFacts.count(extractStr(poly));
227 : : }
228 : :
229 : 47264 : const Poly& CocoaEncoder::symPoly(CoCoA::symbol s) const
230 : : {
231 [ - + ][ - + ]: 47264 : Assert(d_symPolys.count(extractStr(s)));
[ - - ]
232 : 47264 : return d_symPolys.at(extractStr(s));
233 : : }
234 : :
235 : 112638 : void CocoaEncoder::encodeTerm(const Node& t)
236 : : {
237 [ - + ][ - + ]: 112638 : Assert(d_stage == Stage::Encode);
[ - - ]
238 : :
239 : : // for all un-encoded descendents:
240 : 112638 : for (const auto& node :
241 : 161469 : NodeDfsIterable(t, VisitOrder::POSTORDER, [this](TNode nn) {
242 : 161469 : return d_cache.count(nn);
243 [ + + ]: 266677 : }))
244 : : {
245 : : // a rule must put the encoding here
246 : 41401 : Poly elem;
247 : 41401 : if (isFfFact(node, size()) || isFfTerm(node, size()))
248 : : {
249 [ + - ]: 41395 : Trace("ff::cocoa::enc") << "Encode " << node;
250 : : // ff leaf
251 [ + + ][ + + ]: 41395 : if (isFfLeaf(node, size()) && !node.isConst())
[ + - ][ + + ]
[ - - ]
252 : : {
253 : 14872 : elem = symPoly(d_varSyms.at(node));
254 : : }
255 : : // ff.add
256 [ + + ]: 26523 : else if (node.getKind() == Kind::FINITE_FIELD_ADD)
257 : : {
258 : 5743 : elem = CoCoA::zero(*d_polyRing);
259 [ + + ]: 23990 : for (const auto& c : node)
260 : : {
261 : 18247 : elem += d_cache[c];
262 : 18247 : }
263 : : }
264 : : // ff.mul
265 [ + + ]: 20780 : else if (node.getKind() == Kind::FINITE_FIELD_MULT)
266 : : {
267 : 12757 : elem = CoCoA::one(*d_polyRing);
268 [ + + ]: 41183 : for (const auto& c : node)
269 : : {
270 : 28426 : elem *= d_cache[c];
271 : 28426 : }
272 : : }
273 : : // ff.bitsum
274 [ + + ]: 8023 : else if (node.getKind() == Kind::FINITE_FIELD_BITSUM)
275 : : {
276 : 468 : Poly sum = CoCoA::zero(*d_polyRing);
277 : 468 : Poly two = CoCoA::one(*d_polyRing) * 2;
278 : 468 : Poly twoPow = CoCoA::one(*d_polyRing);
279 [ + + ]: 1857 : for (const auto& c : node)
280 : : {
281 : 1389 : sum += twoPow * d_cache[c];
282 : 1389 : twoPow *= two;
283 : 1389 : }
284 : 468 : elem = symPoly(d_bitsumSyms.at(node));
285 : 468 : d_bitsumPolys.push_back(sum - elem);
286 : 468 : }
287 : : // ff constant
288 [ + - ]: 7555 : else if (node.getKind() == Kind::CONST_FINITE_FIELD)
289 : : {
290 : 7555 : elem = CoCoA::one(*d_polyRing)
291 : 15110 : * intToCocoa(node.getConst<FiniteFieldValue>().getValue());
292 : : }
293 : : // !!
294 : : else
295 : : {
296 : 0 : Unimplemented() << node;
297 : : }
298 : : }
299 : : // cache the encoding
300 : 41401 : d_cache.insert({node, elem});
301 : 154039 : }
302 : 112638 : }
303 : :
304 : 56319 : void CocoaEncoder::encodeFact(const Node& f)
305 : : {
306 [ - + ][ - + ]: 56319 : Assert(d_stage == Stage::Encode);
[ - - ]
307 [ - + ][ - + ]: 56319 : Assert(isFfFact(f, size()));
[ - - ]
308 : 56319 : Poly p;
309 : : // ==
310 [ + + ]: 56319 : if (f.getKind() == Kind::EQUAL)
311 : : {
312 : 24395 : encodeTerm(f[0]);
313 : 24395 : encodeTerm(f[1]);
314 : 24395 : p = d_cache.at(f[0]) - d_cache.at(f[1]);
315 : : }
316 : : // !=
317 : : else
318 : : {
319 : 31924 : encodeTerm(f[0][0]);
320 : 31924 : encodeTerm(f[0][1]);
321 : 63848 : Poly diff = d_cache.at(f[0][0]) - d_cache.at(f[0][1]);
322 : 31924 : p = diff * symPoly(d_diseqSyms.at(f)) - 1;
323 : 31924 : }
324 [ + + ]: 56319 : if (!CoCoA::IsZero(p))
325 : : {
326 : : // normalize; if we don't do it, CoCoA will in GB input, confusing our
327 : : // tracer.
328 : 56313 : p = p / CoCoA::LC(p);
329 : : }
330 : 56319 : d_cache.insert({f, p});
331 : 56319 : d_polyFacts.insert({extractStr(p), f});
332 : 56319 : }
333 : :
334 : : } // namespace ff
335 : : } // namespace theory
336 : : } // namespace cvc5::internal
337 : :
338 : : #endif /* CVC5_USE_COCOA */
|
