From 9b50072a191b32be0e49446df413f983c1332cc5 Mon Sep 17 00:00:00 2001 From: Alex Ozdemir Date: Mon, 10 Oct 2022 13:11:32 -0700 Subject: [PATCH 1/5] ff: sub-theory This patch adds a "sub-theory" of FF. * a sub-theory is initialized with a field size, and responsible only for the field of that size. * its interface is a restriction of the general SMT theory interface * the full FF solver essentially just multiplexes between the sub-theories --- src/CMakeLists.txt | 2 + src/options/ff_options.toml | 18 ++ src/theory/ff/sub_theory.cpp | 342 +++++++++++++++++++++++++++++++++++ src/theory/ff/sub_theory.h | 148 +++++++++++++++ 4 files changed, 510 insertions(+) create mode 100644 src/theory/ff/sub_theory.cpp create mode 100644 src/theory/ff/sub_theory.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index fa7f216838a..299ab38439d 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -697,6 +697,8 @@ libcvc5_add_sources( theory/ff/roots.h theory/ff/stats.cpp theory/ff/stats.h + theory/ff/sub_theory.cpp + theory/ff/sub_theory.h theory/ff/theory_ff.cpp theory/ff/theory_ff.h theory/ff/theory_ff_rewriter.cpp diff --git a/src/options/ff_options.toml b/src/options/ff_options.toml index d6e12a25d8a..b2b46e6a8d9 100644 --- a/src/options/ff_options.toml +++ b/src/options/ff_options.toml @@ -9,6 +9,24 @@ name = "Finite Field Theory" default = "true" help = "use a traced groebner basis engine" +[[option]] + name = "ffIncrementality" + category = "expert" + long = "ff-incrementality=MODE" + type = "FfIncrementality" + default = "NONINCREMENTAL" + help = "how incrementally to compute Groebner bases, see --ff-incrementality=help" + help_mode = "how incrementally to compute Groebner bases" +[[option.mode.NONINCREMENTAL]] + name = "nonincremental" + help = "Bases are computed at full-effort, no bases are saved" +[[option.mode.LAZY]] + name = "lazy" + help = "Bases are computed at full-effort, per-context bases are saved" +[[option.mode.EAGER]] + name = "eager" + help = "Bases are computed at standard-effort, per-context bases are saved" + [[option]] name = "ffFieldPolys" category = "expert" diff --git a/src/theory/ff/sub_theory.cpp b/src/theory/ff/sub_theory.cpp new file mode 100644 index 00000000000..b454a141650 --- /dev/null +++ b/src/theory/ff/sub_theory.cpp @@ -0,0 +1,342 @@ +/****************************************************************************** + * Top contributors (to current version): + * Alex Ozdemir + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * A field-specific theory + */ + +#ifdef CVC5_USE_COCOA + +#include "theory/ff/sub_theory.h" + +#include +#include +#include +#include + +#include + +#include "expr/node_manager_attributes.h" +#include "expr/node_traversal.h" +#include "options/ff_options.h" +#include "smt/env_obj.h" +#include "util/cocoa_globals.h" +#include "util/ff_val.h" + +namespace cvc5::internal { +namespace theory { +namespace ff { + +SubTheory::SubTheory(Env& env, FfStatistics* stats, Integer modulus) + : EnvObj(env), + context::ContextNotifyObj(context()), + d_facts(context()), + d_vars(userContext()), + d_atoms(userContext()), + d_stats(stats), + d_baseRing(CoCoA::NewZZmod(CoCoA::BigIntFromString(modulus.toString()))), + d_modulus(modulus) +{ + AlwaysAssert(modulus.isProbablePrime()) << "non-prime fields are unsupported"; + // must be initialized before using CoCoA. + initCocoaGlobalManager(); +} + +void SubTheory::preRegisterTerm(TNode n) +{ + if (n.isVar()) + { + clearPolyRing(); + d_vars.push_back(n); + } + else if (n.getKind() == Kind::EQUAL) + { + d_atoms.push_back(n); + } +} + +// CoCoA symbols must start with a letter and contain only letters and +// underscores. +// +// Thus, our encoding is: v_ESCAPED where any underscore or invalid character +// in NAME is replace in ESCAPED with an underscore followed by a base-16 +// encoding of its ASCII code using alphabet abcde fghij klmno p, followed by +// another _. +// +// Sorry. It sucks, but we don't have much to work with here... +std::string varNameToSymName(const std::string& varName) +{ + std::ostringstream o; + o << "v_"; + for (const auto c : varName) + { + if (('a' <= c && c <= 'z') || ('A' <= c && c <= 'Z')) + { + o << c; + } + else + { + uint8_t code = c; + o << "_" + << "abcdefghijklmnop"[code & 0x0f] + << "abcdefghijklmnop"[(code >> 4) & 0x0f] << "_"; + } + } + return o.str(); +} + +void SubTheory::ensureInitPolyRing() +{ + if (!d_polyRing.has_value()) + { + std::vector symbols; + for (const auto& v : d_vars) + { + symbols.push_back( + CoCoA::symbol(varNameToSymName(v.getAttribute(expr::VarNameAttr())))); + } + for (size_t i = 0; i < d_atoms.size(); ++i) + { + symbols.push_back(CoCoA::symbol("i", i)); + } + d_polyRing = CoCoA::NewPolyRing(d_baseRing, symbols); + size_t i = 0; + Assert(d_translationCache.empty()); + Assert(d_symbolIdxVars.empty()); + for (const auto& v : d_vars) + { + d_translationCache.insert({v, CoCoA::indet(d_polyRing.value(), i)}); + d_symbolIdxVars.insert({i, v}); + ++i; + } + Assert(d_atomInverses.empty()); + for (const auto& a : d_atoms) + { + d_atomInverses.insert({a, CoCoA::indet(d_polyRing.value(), i)}); + Trace("ff::trans") << "inverse for " << a << std::endl; + ++i; + } + Assert(!d_incrementalIdeal.has_value()); + Assert(d_updateIndices.empty()); + d_incrementalIdeal.emplace(d_env, d_polyRing.value()); + d_updateIndices.push_back(0); + } +} + +void SubTheory::clearPolyRing() +{ + d_polyRing.reset(); + d_checkIndices.clear(); + d_atomInverses.clear(); + d_translationCache.clear(); + d_incrementalIdeal.reset(); + d_symbolIdxVars.clear(); + d_updateIndices.clear(); +} + +void SubTheory::notifyFact(TNode fact) +{ + ensureInitPolyRing(); + d_facts.emplace_back(fact); + d_model.clear(); +} + +void SubTheory::postCheck(Theory::Effort e) +{ + d_checkIndices.push_back(d_facts.size()); + auto inc = options().ff.ffIncrementality; + if (e == Theory::EFFORT_STANDARD) + { + if (inc == options::FfIncrementality::EAGER) + { + computeBasis(d_facts.size()); + } + } + else if (e == Theory::EFFORT_FULL) + { + if (inc == options::FfIncrementality::EAGER + || inc == options::FfIncrementality::LAZY) + { + for (size_t i : d_checkIndices) + { + if (i > d_updateIndices.back()) + { + computeBasis(i); + if (inConflict()) return; + } + } + } + else + { + computeBasis(d_facts.size()); + } + if (!inConflict()) + { + extractModel(); + } + } +} + +bool SubTheory::inConflict() const { return !d_conflict.empty(); } + +const std::vector& SubTheory::conflict() const { return d_conflict; } + +const std::unordered_map& SubTheory::model() const +{ + return d_model; +} + +void SubTheory::contextNotifyPop() +{ + Trace("ff::context") << "Pop " << context()->getLevel() << std::endl; + while (d_updateIndices.back() > d_facts.size()) + { + d_updateIndices.pop_back(); + d_incrementalIdeal.value().pop(); + d_conflict.clear(); + } + while (d_checkIndices.size() > 0 && d_checkIndices.back() > d_facts.size()) + { + d_checkIndices.pop_back(); + } +} + +void SubTheory::computeBasis(size_t factIndex) +{ + Assert(d_conflict.empty()); + Assert(d_updateIndices.size() > 0); + Assert(factIndex > d_updateIndices.back()); + IncrementalIdeal& ideal = d_incrementalIdeal.value(); + std::vector newGens; + for (size_t i = d_updateIndices.back(); i < factIndex; ++i) + { + TNode fact = d_facts[i]; + translate(fact); + newGens.push_back(d_translationCache.at(fact)); + } + { + CodeTimer reductionTimer(d_stats->d_reductionTime); + ideal.pushGenerators(std::move(newGens)); + d_stats->d_numReductions += 1; + } + d_updateIndices.push_back(factIndex); + if (ideal.idealIsTrivial()) + { + for (size_t i : ideal.trivialCoreIndices()) + { + d_conflict.push_back(d_facts[i]); + } + Trace("ff::conflict") << "conflict " << ideal.trivialCoreIndices().size() + << "/" << d_facts.size() << " facts" << std::endl; + if (TraceChannel.isOn("ff::conflict")) + { + Trace("ff::conflict::debug") + << "conflict " << NodeManager::currentNM()->mkAnd(d_conflict) + << std::endl; + } + } +} + +void SubTheory::extractModel() +{ + CodeTimer modelTimer(d_stats->d_modelConstructionTime); + IncrementalIdeal& ideal = d_incrementalIdeal.value(); + Trace("ff::model") << "constructing model" << std::endl; + d_model.clear(); + if (ideal.hasSolution()) + { + Trace("ff::model") << "found model" << std::endl; + const auto& values = ideal.solution(); + NodeManager* nm = NodeManager::currentNM(); + for (size_t i = 0, numVars = d_vars.size(); i < numVars; ++i) + { + std::ostringstream symName; + symName << CoCoA::indet(d_polyRing.value(), i); + Node var = d_symbolIdxVars.at(i); + std::ostringstream valStr; + valStr << values[i]; + Integer integer(valStr.str(), 10); + FfVal literal(integer, d_modulus); + Node value = nm->mkConst(literal); + + Trace("ff::model") << var << ": " << value << std::endl; + d_model.emplace(var, value); + } + } + else + { + ++d_stats->d_numConstructionErrors; + d_conflict.insert(d_conflict.begin(), d_facts.begin(), d_facts.end()); + } +} + +void SubTheory::translate(TNode t) +{ + auto& cache = d_translationCache; + // Build polynomials for terms + for (const auto& node : + NodeDfsIterable(t, VisitOrder::POSTORDER, [&cache](TNode nn) { + return cache.count(nn) > 0; + })) + { + if (node.getType().isFiniteField() || node.getKind() == Kind::EQUAL + || node.getKind() == Kind::NOT) + { + CoCoA::RingElem poly; + std::vector subPolys; + std::transform(node.begin(), + node.end(), + std::back_inserter(subPolys), + [&cache](Node n) { return cache[n]; }); + switch (node.getKind()) + { + // FF-term cases: + case Kind::FINITE_FIELD_ADD: + poly = std::accumulate( + subPolys.begin(), + subPolys.end(), + CoCoA::RingElem(d_polyRing.value()->myZero()), + [](CoCoA::RingElem a, CoCoA::RingElem b) { return a + b; }); + break; + case Kind::FINITE_FIELD_NEG: poly = -subPolys[0]; break; + case Kind::FINITE_FIELD_MULT: + poly = std::accumulate( + subPolys.begin(), + subPolys.end(), + CoCoA::RingElem(d_polyRing.value()->myOne()), + [](CoCoA::RingElem a, CoCoA::RingElem b) { return a * b; }); + break; + case Kind::CONST_FINITE_FIELD: + poly = d_polyRing.value()->myOne() + * CoCoA::BigIntFromString( + node.getConst().getValue().toString()); + break; + // fact cases: + case Kind::EQUAL: poly = subPolys[0] - subPolys[1]; break; + case Kind::NOT: + Assert(node[0].getKind() == Kind::EQUAL); + poly = subPolys[0] * d_atomInverses.at(node[0]) - 1; + break; + default: + Unreachable() << "Invalid finite field kind: " << node.getKind(); + } + Trace("ff::trans") + << "Translated " << node << "\t-> " << poly << std::endl; + cache.insert(std::make_pair(node, poly)); + } + } +} + +} // namespace ff +} // namespace theory +} // namespace cvc5::internal + +#endif /* CVC5_USE_COCOA */ diff --git a/src/theory/ff/sub_theory.h b/src/theory/ff/sub_theory.h new file mode 100644 index 00000000000..d153e5d70eb --- /dev/null +++ b/src/theory/ff/sub_theory.h @@ -0,0 +1,148 @@ +/****************************************************************************** + * Top contributors (to current version): + * Alex Ozdemir + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * A field-specific theory + */ + +#include "cvc5_private.h" + +#ifdef CVC5_USE_COCOA + +#ifndef CVC5__THEORY__FF__SUB_THEORY_H +#define CVC5__THEORY__FF__SUB_THEORY_H + +#include + +#include +#include +#include +#include +#include + +#include "context/cdlist_forward.h" +#include "context/cdo.h" +#include "context/context.h" +#include "expr/node.h" +#include "options/ff_options.h" +#include "smt/env_obj.h" +#include "theory/ff/core.h" +#include "theory/ff/groebner.h" +#include "theory/ff/stats.h" +#include "theory/theory.h" +#include "util/integer.h" + +namespace cvc5::internal { +namespace theory { +namespace ff { + +class SubTheory : EnvObj, context::ContextNotifyObj +{ + public: + // Create a new sub-theory. + // + // Parameters: + // * modulus: the size of this field for this theory, a prime. + SubTheory(Env& env, FfStatistics* stats, Integer modulus); + + // Notify this theory of a node it may need to handle. + // + // All nodes this theory sees in the future must be pre-registered. + void preRegisterTerm(TNode); + + // Assert a fact to this theory. + void notifyFact(TNode fact); + + // Check the current facts. + void postCheck(Theory::Effort); + + // Has a conflict been detected? + bool inConflict() const; + + // What is that conflict? + const std::vector& conflict() const; + + // Get a model. + const std::unordered_map& model() const; + + private: + // Called on SAT pop; we pop the incremental ideal if needed. + void contextNotifyPop() override; + + // Compute a Groebner basis for the facts up to (not including) this index. + void computeBasis(size_t factIndex); + + void extractModel(); + + // Initialize the polynomial ring, set up post-registration data structures. + void ensureInitPolyRing(); + + // Uninitialize the polynomial ring, clear post-registration data structures. + void clearPolyRing(); + + // Translate t to CoCoA, and cache the result. + void translate(TNode t); + + // Is registration done and the polynomial ring initialized? + bool d_registrationDone(); + + // Manages the incremental GB. + std::optional d_incrementalIdeal{}; + + // For an atom x == y, contains the potential inverse of (x - y). + // + // Used to make x != y. + std::unordered_map d_atomInverses{}; + + // Facts, in notification order. + // + // Uses SAT context. + context::CDList d_facts; + + // The length of that fact list at each check. + std::vector d_checkIndices{}; + + // The length of that fact list at each point where we updated the ideal. + std::vector d_updateIndices{}; + + // Non-empty if we're in a conflict. + std::vector d_conflict{}; + + // Cache from nodes to CoCoA polynomials. + std::unordered_map d_translationCache{}; + + // A model, if we've found one. A map from variable nodes to their constant + // values. + std::unordered_map d_model{}; + + // Variables + context::CDList d_vars; + + // Variables + std::unordered_map d_symbolIdxVars{}; + + // Atoms + context::CDList d_atoms; + + FfStatistics* d_stats; + CoCoA::ring d_baseRing; + Integer d_modulus; + // Set after registration is done. + std::optional d_polyRing{}; +}; + +} // namespace ff +} // namespace theory +} // namespace cvc5::internal + +#endif /* CVC5__THEORY__FF__SUB_THEORY_H */ + +#endif /* CVC5_USE_COCOA */ From 64af7df513fdd8cc7fa9f650d00698fec3b3a519 Mon Sep 17 00:00:00 2001 From: Alex Ozdemir Date: Mon, 10 Oct 2022 14:02:53 -0700 Subject: [PATCH 2/5] Update src/theory/ff/sub_theory.h Co-authored-by: Andrew Reynolds --- src/theory/ff/sub_theory.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/theory/ff/sub_theory.h b/src/theory/ff/sub_theory.h index d153e5d70eb..63e4a415e9c 100644 --- a/src/theory/ff/sub_theory.h +++ b/src/theory/ff/sub_theory.h @@ -44,7 +44,7 @@ namespace cvc5::internal { namespace theory { namespace ff { -class SubTheory : EnvObj, context::ContextNotifyObj +class SubTheory : protected EnvObj, protected context::ContextNotifyObj { public: // Create a new sub-theory. From 7df6ceb33954bef16fbab917a6b5504af6127c30 Mon Sep 17 00:00:00 2001 From: Alex Ozdemir Date: Mon, 10 Oct 2022 14:07:49 -0700 Subject: [PATCH 3/5] document more --- src/theory/ff/sub_theory.h | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/src/theory/ff/sub_theory.h b/src/theory/ff/sub_theory.h index 63e4a415e9c..1385f191ccb 100644 --- a/src/theory/ff/sub_theory.h +++ b/src/theory/ff/sub_theory.h @@ -44,6 +44,18 @@ namespace cvc5::internal { namespace theory { namespace ff { +/** + * A solver for a specific, known finite field. + * + * While the main ff solver is responsible for all elements in any finite field, + * this solver just considers a single field. The main ff solver essentially + * just multiplexes between different sub-solvers. + * + * The solver only exposes a subset of the standard SMT theory interface. See + * the methods below. + * + * For now, our implementation assumes that the finite field has prime order. + */ class SubTheory : protected EnvObj, protected context::ContextNotifyObj { public: @@ -132,8 +144,16 @@ class SubTheory : protected EnvObj, protected context::ContextNotifyObj // Atoms context::CDList d_atoms; + // Statistics shared among all finite-field sub-theories. FfStatistics* d_stats; + // The base field of the multivariate polynomial ring. + // + // That is, the field that the polynomial coefficients live in/the + // finite-field constants live in. + // + // For now, we assume this is a prime-order finite-field. CoCoA::ring d_baseRing; + // The prime modulus for the base field. Integer d_modulus; // Set after registration is done. std::optional d_polyRing{}; From b637cf25d698e371aece4ec01345fb756a6c80bb Mon Sep 17 00:00:00 2001 From: Alex Ozdemir Date: Mon, 10 Oct 2022 15:12:27 -0700 Subject: [PATCH 4/5] doc getModel precondition --- src/theory/ff/sub_theory.h | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/theory/ff/sub_theory.h b/src/theory/ff/sub_theory.h index 1385f191ccb..d38fef9b178 100644 --- a/src/theory/ff/sub_theory.h +++ b/src/theory/ff/sub_theory.h @@ -83,6 +83,9 @@ class SubTheory : protected EnvObj, protected context::ContextNotifyObj const std::vector& conflict() const; // Get a model. + // + // Can only be called after a full-effort post-check + // if inConflict is false. const std::unordered_map& model() const; private: From a55f498fcd9a372061fe5db9451a5449f60637e0 Mon Sep 17 00:00:00 2001 From: Alex Ozdemir Date: Tue, 11 Oct 2022 07:59:09 -0700 Subject: [PATCH 5/5] more doc --- src/theory/ff/sub_theory.h | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/theory/ff/sub_theory.h b/src/theory/ff/sub_theory.h index d38fef9b178..f0f21ef9745 100644 --- a/src/theory/ff/sub_theory.h +++ b/src/theory/ff/sub_theory.h @@ -119,6 +119,8 @@ class SubTheory : protected EnvObj, protected context::ContextNotifyObj // Facts, in notification order. // + // Contains only the facts in *this specific field*. + // // Uses SAT context. context::CDList d_facts;