Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Alex Ozdemir, Daniel Larraz, Andrew Reynolds
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 : : * A field-specific theory.
14 : : * That is, the sub-theory for GF(p) for some fixed p.
15 : : * Implements Figure 2, "DecisionProcedure" from [OKTB23].
16 : : *
17 : : * [OKTB23]: https://doi.org/10.1007/978-3-031-37703-7_8
18 : : */
19 : :
20 : : #ifdef CVC5_USE_COCOA
21 : :
22 : : #include "theory/ff/sub_theory.h"
23 : :
24 : : #include <CoCoA/BigInt.H>
25 : : #include <CoCoA/CpuTimeLimit.H>
26 : : #include <CoCoA/QuotientRing.H>
27 : : #include <CoCoA/RingZZ.H>
28 : : #include <CoCoA/SparsePolyOps-ideal.H>
29 : : #include <CoCoA/ring.H>
30 : :
31 : : #include <numeric>
32 : :
33 : : #include "expr/node_traversal.h"
34 : : #include "options/ff_options.h"
35 : : #include "smt/env_obj.h"
36 : : #include "theory/ff/cocoa_encoder.h"
37 : : #include "theory/ff/core.h"
38 : : #include "theory/ff/multi_roots.h"
39 : : #include "theory/ff/split_gb.h"
40 : : #include "theory/ff/util.h"
41 : : #include "util/cocoa_globals.h"
42 : : #include "util/finite_field_value.h"
43 : : #include "util/resource_manager.h"
44 : :
45 : : namespace cvc5::internal {
46 : : namespace theory {
47 : : namespace ff {
48 : :
49 : 253 : SubTheory::SubTheory(Env& env, FfStatistics* stats, Integer modulus)
50 : : : EnvObj(env),
51 : : FieldObj(nodeManager(), modulus),
52 : 253 : d_facts(context()),
53 : 506 : d_stats(stats)
54 : : {
55 [ - + ][ - + ]: 253 : AlwaysAssert(modulus.isProbablePrime()) << "non-prime fields are unsupported";
[ - - ]
56 : : // must be initialized before using CoCoA.
57 : 253 : initCocoaGlobalManager();
58 : 253 : }
59 : :
60 : 23871 : void SubTheory::notifyFact(TNode fact) { d_facts.emplace_back(fact); }
61 : :
62 : 12906 : Result SubTheory::postCheck(Theory::Effort e)
63 : : {
64 : 12906 : d_conflict.clear();
65 : 12906 : d_model.clear();
66 : : // on some branches, we'll overwrite this result
67 : : Result result = {
68 : 25812 : Result::UNKNOWN, UnknownExplanation::UNKNOWN_REASON, "internal"};
69 [ + + ]: 12906 : if (e == Theory::EFFORT_FULL)
70 : : {
71 : : try
72 : : {
73 [ + + ]: 2649 : if (d_facts.empty()) return Result::SAT;
74 [ + + ]: 2639 : if (options().ff.ffSolver == options::FfSolver::SPLIT_GB)
75 : : {
76 : 836 : std::vector<Node> facts{};
77 : 836 : std::copy(d_facts.begin(), d_facts.end(), std::back_inserter(facts));
78 : 836 : const auto optModel = split(facts, size(), d_env);
79 [ + + ]: 836 : if (optModel.has_value())
80 : : {
81 : 25 : const auto nm = nodeManager();
82 [ + + ]: 122 : for (const auto& [var, val] : optModel.value())
83 : : {
84 : 97 : d_model.insert({var, nm->mkConst<FiniteFieldValue>(val)});
85 : : }
86 : 25 : return Result::SAT;
87 : : }
88 : 811 : std::copy(
89 : 811 : d_facts.begin(), d_facts.end(), std::back_inserter(d_conflict));
90 : 811 : return Result::UNSAT;
91 : 836 : }
92 [ + - ]: 1803 : else if (options().ff.ffSolver == options::FfSolver::GB)
93 : : {
94 : 1803 : CocoaEncoder enc(nodeManager(), size());
95 : : // collect leaves
96 [ + + ]: 46669 : for (const Node& node : d_facts)
97 : : {
98 : 44866 : enc.addFact(node);
99 : : }
100 : 1803 : enc.endScan();
101 : : // assert facts
102 [ + + ]: 46669 : for (const Node& node : d_facts)
103 : : {
104 : 44866 : enc.addFact(node);
105 : : }
106 : :
107 : : // compute a GB
108 : 1803 : std::vector<CoCoA::RingElem> generators;
109 : 5409 : generators.insert(
110 : 5409 : generators.end(), enc.polys().begin(), enc.polys().end());
111 : 3606 : generators.insert(generators.end(),
112 : 1803 : enc.bitsumPolys().begin(),
113 : 1803 : enc.bitsumPolys().end());
114 [ + + ]: 1803 : if (options().ff.ffFieldPolys)
115 : : {
116 : 11 : CoCoA::PolyRing polyRing(enc.polyRing());
117 [ + + ]: 24 : for (const auto& var : CoCoA::indets(polyRing))
118 : : {
119 : 13 : CoCoA::BigInt characteristic = CoCoA::characteristic(coeffRing());
120 : 13 : const long power = CoCoA::LogCardinality(coeffRing());
121 : 13 : CoCoA::BigInt size = CoCoA::power(characteristic, power);
122 : 13 : generators.push_back(CoCoA::power(var, size) - var);
123 : 13 : }
124 : 11 : }
125 : 1803 : Tracer tracer(generators);
126 [ + - ]: 1803 : if (options().ff.ffTraceGb) tracer.setFunctionPointers();
127 : 1803 : CoCoA::ideal ideal = CoCoA::ideal(generators);
128 : 1803 : const auto basis = GBasisTimeout(ideal, d_env.getResourceManager());
129 [ + - ]: 1803 : if (options().ff.ffTraceGb) tracer.unsetFunctionPointers();
130 : :
131 : : // if it is trivial, create a conflict
132 [ + + ][ + + ]: 1803 : bool is_trivial = basis.size() == 1 && CoCoA::deg(basis.front()) == 0;
133 [ + + ]: 1803 : if (is_trivial)
134 : : {
135 [ + - ]: 1695 : Trace("ff::gb") << "Trivial GB" << std::endl;
136 : 1695 : result = Result::UNSAT;
137 [ + - ]: 1695 : if (options().ff.ffTraceGb)
138 : : {
139 : 1695 : std::vector<size_t> coreIndices = tracer.trace(basis.front());
140 [ - + ][ - + ]: 1695 : Assert(d_conflict.empty());
[ - - ]
141 [ + + ]: 46162 : for (size_t i = 0, n = d_facts.size(); i < n; ++i)
142 : : {
143 [ + - ]: 88934 : Trace("ff::core")
144 : 44467 : << "In " << i << " : " << d_facts[i] << std::endl;
145 : : }
146 [ + + ]: 13610 : for (size_t i : coreIndices)
147 : : {
148 : : // omit (field polys, bitsum polys, ...) from core
149 [ + + ]: 11915 : if (enc.polyHasFact(generators[i]))
150 : : {
151 [ + - ]: 23806 : Trace("ff::core")
152 : 11903 : << "Core: " << i << " : " << d_facts[i] << std::endl;
153 : 11903 : d_conflict.push_back(enc.polyFact(generators[i]));
154 : : }
155 : : }
156 : 1695 : }
157 : : else
158 : : {
159 : 0 : setTrivialConflict();
160 : : }
161 : : }
162 : : else
163 : : {
164 [ + - ]: 108 : Trace("ff::gb") << "Non-trivial GB" << std::endl;
165 : :
166 : : // common root (vec of CoCoA base ring elements)
167 : 108 : std::vector<CoCoA::RingElem> root = findZero(ideal, d_env);
168 : :
169 [ + + ]: 108 : if (root.empty())
170 : : {
171 : 9 : result = Result::UNSAT;
172 : 9 : setTrivialConflict();
173 : : }
174 : : else
175 : : {
176 : 99 : result = Result::SAT;
177 : : // populate d_model from the root
178 [ - + ][ - + ]: 99 : Assert(d_model.empty());
[ - - ]
179 : 99 : const auto nm = nodeManager();
180 [ + - ]: 99 : Trace("ff::model") << "Model GF(" << size() << "):" << std::endl;
181 [ + + ]: 378 : for (const auto& [idx, node] : enc.nodeIndets())
182 : : {
183 [ + - ]: 279 : if (isFfLeaf(node))
184 : : {
185 : 279 : Node value = nm->mkConst(enc.cocoaFfToFfVal(root[idx]));
186 [ + - ]: 558 : Trace("ff::model")
187 : 279 : << " " << node << " = " << value << std::endl;
188 : 279 : d_model.emplace(node, value);
189 : 279 : }
190 : 99 : }
191 : : }
192 : 108 : }
193 : 1803 : }
194 : : else
195 : : {
196 : 0 : Unreachable() << options().ff.ffSolver << std::endl;
197 : : }
198 [ - + ][ - + ]: 1803 : AlwaysAssert(result.getStatus() != Result::UNKNOWN);
[ - - ]
199 : 1803 : return result;
200 : : }
201 [ - - ]: 0 : catch (FfTimeoutException& exc)
202 : : {
203 : 0 : return {Result::UNKNOWN, UnknownExplanation::TIMEOUT, exc.getMessage()};
204 : 0 : }
205 : : }
206 : 10257 : return {Result::UNKNOWN, UnknownExplanation::REQUIRES_FULL_CHECK, ""};
207 : 12906 : }
208 : :
209 : 9 : void SubTheory::setTrivialConflict()
210 : : {
211 : 9 : std::copy(d_facts.begin(), d_facts.end(), std::back_inserter(d_conflict));
212 : 9 : }
213 : :
214 : 2515 : bool SubTheory::inConflict() const { return !d_conflict.empty(); }
215 : :
216 : 2515 : const std::vector<Node>& SubTheory::conflict() const { return d_conflict; }
217 : :
218 : 47 : const std::unordered_map<Node, Node>& SubTheory::model() const
219 : : {
220 : 47 : return d_model;
221 : : }
222 : :
223 : : } // namespace ff
224 : : } // namespace theory
225 : : } // namespace cvc5::internal
226 : :
227 : : #endif /* CVC5_USE_COCOA */
|
