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 : : d_facts(context()),
53 : 253 : 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 : 38718 : 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 : 1672 : std::vector<Node> facts{};
77 : 836 : std::copy(d_facts.begin(), d_facts.end(), std::back_inserter(facts));
78 : 1672 : 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 : : std::copy(
89 : 811 : d_facts.begin(), d_facts.end(), std::back_inserter(d_conflict));
90 : 811 : return Result::UNSAT;
91 : : }
92 [ + - ]: 1803 : else if (options().ff.ffSolver == options::FfSolver::GB)
93 : : {
94 : 3606 : 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 : 3606 : std::vector<CoCoA::RingElem> generators;
109 : : generators.insert(
110 : 1803 : generators.end(), enc.polys().begin(), enc.polys().end());
111 : 1803 : generators.insert(generators.end(),
112 : 1803 : enc.bitsumPolys().begin(),
113 : 5409 : enc.bitsumPolys().end());
114 [ + + ]: 1803 : if (options().ff.ffFieldPolys)
115 : : {
116 [ + + ]: 24 : for (const auto& var : CoCoA::indets(enc.polyRing()))
117 : : {
118 : 26 : CoCoA::BigInt characteristic = CoCoA::characteristic(coeffRing());
119 : 13 : const long power = CoCoA::LogCardinality(coeffRing());
120 : 13 : CoCoA::BigInt size = CoCoA::power(characteristic, power);
121 : 13 : generators.push_back(CoCoA::power(var, size) - var);
122 : : }
123 : : }
124 : 3606 : Tracer tracer(generators);
125 [ + - ]: 1803 : if (options().ff.ffTraceGb) tracer.setFunctionPointers();
126 : 3606 : CoCoA::ideal ideal = CoCoA::ideal(generators);
127 : 3606 : const auto basis = GBasisTimeout(ideal, d_env.getResourceManager());
128 [ + - ]: 1803 : if (options().ff.ffTraceGb) tracer.unsetFunctionPointers();
129 : :
130 : : // if it is trivial, create a conflict
131 [ + + ][ + + ]: 1803 : bool is_trivial = basis.size() == 1 && CoCoA::deg(basis.front()) == 0;
132 [ + + ]: 1803 : if (is_trivial)
133 : : {
134 [ + - ]: 1695 : Trace("ff::gb") << "Trivial GB" << std::endl;
135 : 1695 : result = Result::UNSAT;
136 [ + - ]: 1695 : if (options().ff.ffTraceGb)
137 : : {
138 : 3390 : std::vector<size_t> coreIndices = tracer.trace(basis.front());
139 [ - + ][ - + ]: 1695 : Assert(d_conflict.empty());
[ - - ]
140 [ + + ]: 46162 : for (size_t i = 0, n = d_facts.size(); i < n; ++i)
141 : : {
142 [ + - ]: 88934 : Trace("ff::core")
143 : 44467 : << "In " << i << " : " << d_facts[i] << std::endl;
144 : : }
145 [ + + ]: 13610 : for (size_t i : coreIndices)
146 : : {
147 : : // omit (field polys, bitsum polys, ...) from core
148 [ + + ]: 11915 : if (enc.polyHasFact(generators[i]))
149 : : {
150 [ + - ]: 23806 : Trace("ff::core")
151 : 11903 : << "Core: " << i << " : " << d_facts[i] << std::endl;
152 : 11903 : d_conflict.push_back(enc.polyFact(generators[i]));
153 : : }
154 : : }
155 : : }
156 : : else
157 : : {
158 : 0 : setTrivialConflict();
159 : : }
160 : : }
161 : : else
162 : : {
163 [ + - ]: 108 : Trace("ff::gb") << "Non-trivial GB" << std::endl;
164 : :
165 : : // common root (vec of CoCoA base ring elements)
166 : 216 : std::vector<CoCoA::RingElem> root = findZero(ideal, d_env);
167 : :
168 [ + + ]: 108 : if (root.empty())
169 : : {
170 : 9 : result = Result::UNSAT;
171 : 9 : setTrivialConflict();
172 : : }
173 : : else
174 : : {
175 : 99 : result = Result::SAT;
176 : : // populate d_model from the root
177 [ - + ][ - + ]: 99 : Assert(d_model.empty());
[ - - ]
178 : 99 : const auto nm = nodeManager();
179 [ + - ]: 99 : Trace("ff::model") << "Model GF(" << size() << "):" << std::endl;
180 [ + + ]: 378 : for (const auto& [idx, node] : enc.nodeIndets())
181 : : {
182 [ + - ]: 279 : if (isFfLeaf(node))
183 : : {
184 : 558 : Node value = nm->mkConst(enc.cocoaFfToFfVal(root[idx]));
185 [ + - ]: 558 : Trace("ff::model")
186 : 279 : << " " << node << " = " << value << std::endl;
187 : 279 : d_model.emplace(node, value);
188 : : }
189 : : }
190 : : }
191 : : }
192 : : }
193 : : else
194 : : {
195 : 0 : Unreachable() << options().ff.ffSolver << std::endl;
196 : : }
197 [ - + ][ - + ]: 1803 : AlwaysAssert(result.getStatus() != Result::UNKNOWN);
[ - - ]
198 : 1803 : return result;
199 : : }
200 : 0 : catch (FfTimeoutException& exc)
201 : : {
202 : 0 : return {Result::UNKNOWN, UnknownExplanation::TIMEOUT, exc.getMessage()};
203 : : }
204 : : }
205 : 10257 : return {Result::UNKNOWN, UnknownExplanation::REQUIRES_FULL_CHECK, ""};
206 : : }
207 : :
208 : 9 : void SubTheory::setTrivialConflict()
209 : : {
210 : 9 : std::copy(d_facts.begin(), d_facts.end(), std::back_inserter(d_conflict));
211 : 9 : }
212 : :
213 : 2515 : bool SubTheory::inConflict() const { return !d_conflict.empty(); }
214 : :
215 : 2515 : const std::vector<Node>& SubTheory::conflict() const { return d_conflict; }
216 : :
217 : 47 : const std::unordered_map<Node, Node>& SubTheory::model() const
218 : : {
219 : 47 : return d_model;
220 : : }
221 : :
222 : : } // namespace ff
223 : : } // namespace theory
224 : : } // namespace cvc5::internal
225 : :
226 : : #endif /* CVC5_USE_COCOA */
|
