ff: groebner bases for incremental ideals

src/CMakeLists.txt

@@ -687,6 +687,8 @@ libcvc5_add_sources(
   theory/evaluator.h
   theory/ext_theory.cpp
   theory/ext_theory.h
+  theory/ff/groebner.cpp
+  theory/ff/groebner.h
   theory/ff/core.cpp
   theory/ff/core.h
   theory/ff/model.cpp
@@ -1243,6 +1245,7 @@ set(options_toml_files
   options/datatypes_options.toml
   options/decision_options.toml
   options/expr_options.toml
+  options/ff_options.toml
   options/fp_options.toml
   options/main_options.toml
   options/parallel_options.toml

src/options/ff_options.toml

@@ -0,0 +1,18 @@
+id     = "FF"
+name   = "Finite Field Theory"
+
+[[option]]
+  name       = "ffTraceGb"
+  category   = "expert"
+  long       = "ff-trace-gb"
+  type       = "bool"
+  default    = "true"
+  help       = "use a traced groebner basis engine"
+
+[[option]]
+  name       = "ffFieldPolys"
+  category   = "expert"
+  long       = "ff-field-polys"
+  type       = "bool"
+  default    = "false"
+  help       = "include field polynomials in Groebner basis computation"

src/theory/ff/groebner.cpp

@@ -0,0 +1,204 @@
+/******************************************************************************
+ * 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.
+ * ****************************************************************************
+ *
+ * An incremental groebner basis engine.
+ */
+
+#ifdef CVC5_USE_COCOA
+
+#include "theory/ff/groebner.h"
+
+#include <CoCoA/BigInt.H>
+#include <CoCoA/QuotientRing.H>
+#include <CoCoA/RingZZ.H>
+#include <CoCoA/SparsePolyOps-ideal.H>
+#include <CoCoA/ring.H>
+
+#include <numeric>
+
+#include "expr/node_manager_attributes.h"
+#include "expr/node_traversal.h"
+#include "options/ff_options.h"
+#include "theory/ff/model.h"
+
+namespace cvc5::internal {
+namespace theory {
+namespace ff {
+
+IncrementalIdeal::IncrementalIdeal(Env& env, CoCoA::ring polyRing)
+    : EnvObj(env),
+      d_context(std::make_unique<context::Context>()),
+      d_polyRing(polyRing),
+      d_gens(d_context.get()),
+      d_basis(d_context.get()),
+      d_hasCore(d_context.get()),
+      d_core(d_context.get()),
+      d_hasSolution(d_context.get()),
+      d_solution(d_context.get())
+{
+  if (options().ff.ffFieldPolys)
+  {
+    for (const auto& var : CoCoA::indets(polyRing))
+    {
+      CoCoA::BigInt characteristic =
+          CoCoA::characteristic(polyRing->myBaseRing());
+      long power = CoCoA::LogCardinality(polyRing->myBaseRing());
+      CoCoA::BigInt size = CoCoA::power(characteristic, power);
+      d_gens.push_back(CoCoA::power(var, size) - var);
+      d_tracer.addInput(d_gens.back());
+    }
+    std::vector<CoCoA::RingElem> firstBasis;
+    for (const auto& fieldPoly : d_gens)
+    {
+      firstBasis.push_back(fieldPoly);
+    }
+    d_basis = std::move(firstBasis);
+  }
+}
+
+void IncrementalIdeal::pushGenerators(std::vector<CoCoA::RingElem>&& gens)
+{
+  d_context->push();
+  d_tracer.push();
+  std::vector<CoCoA::RingElem> theseGens = d_basis.get();
+  for (auto& g : gens)
+  {
+    d_gens.emplace_back(std::move(g));
+    d_tracer.addInput(d_gens.back());
+    theseGens.push_back(d_gens.back());
+  }
+  d_tracer.setFunctionPointers();
+  if (TraceIsOn("ff::groebner::push"))
+  {
+    for (const auto& b : theseGens)
+    {
+      Trace("ff::groebner::push") << "gens: " << b << std::endl;
+    }
+  }
+  CoCoA::ideal ideal = CoCoA::ideal(theseGens);
+  d_basis = CoCoA::GBasis(ideal);
+  if (TraceIsOn("ff::groebner::push"))
+  {
+    for (const auto& b : d_basis.get())
+    {
+      Trace("ff::groebner::push") << "basis: " << b << std::endl;
+    }
+  }
+  d_hasCore.set(false);
+  d_hasSolution.set({});
+}
+
+bool IncrementalIdeal::idealIsTrivial()
+{
+  return d_basis.get().size() == 1 && CoCoA::deg(d_basis.get().front()) == 0;
+}
+
+const std::vector<size_t>& IncrementalIdeal::trivialCoreIndices()
+{
+  Assert(idealIsTrivial());
+  if (!d_hasCore.get())
+  {
+    std::vector<size_t> indices;
+    if (options().ff.ffTraceGb)
+    {
+      indices = d_tracer.trace(d_basis.get().front());
+      if (options().ff.ffFieldPolys)
+      {
+        // we must shift out the field polynomial indices.
+        std::vector<size_t> indicesWithoutFieldPolys;
+        size_t numVars = CoCoA::NumIndets(d_polyRing);
+        for (size_t i : indices)
+        {
+          if (i >= numVars)
+          {
+            indicesWithoutFieldPolys.push_back(i - numVars);
+          }
+        }
+        indices = indicesWithoutFieldPolys;
+      }
+    }
+    else
+    {
+      indices.clear();
+      size_t numGens = d_gens.size();
+      if (options().ff.ffFieldPolys)
+      {
+        numGens -= CoCoA::NumIndets(d_polyRing);
+      }
+      for (size_t i = 0; i < numGens; ++i)
+      {
+        indices.push_back(i);
+      }
+    }
+    d_core = std::move(indices);
+    d_hasCore.set(true);
+  }
+  return d_core.get();
+}
+
+std::vector<CoCoA::RingElem> IncrementalIdeal::trivialCore()
+{
+  std::vector<CoCoA::RingElem> r;
+  for (size_t i : trivialCoreIndices())
+  {
+    r.push_back(d_gens[i]);
+  }
+  return r;
+}
+
+bool IncrementalIdeal::hasSolution()
+{
+  if (idealIsTrivial())
+  {
+    return false;
+  }
+  else
+  {
+    ensureSolution();
+  }
+  return d_hasSolution.get().value();
+}
+
+void IncrementalIdeal::ensureSolution()
+{
+  if (!d_hasSolution.get().has_value())
+  {
+    std::vector<CoCoA::RingElem> root = commonRoot(CoCoA::ideal(d_basis.get()));
+    if (root.empty())
+    {
+      d_hasSolution.set({false});
+    }
+    else
+    {
+      d_hasSolution.set({true});
+      d_solution.set(root);
+    }
+  }
+}
+
+const std::vector<CoCoA::RingElem>& IncrementalIdeal::solution()
+{
+  ensureSolution();
+  return d_solution.get();
+}
+
+void IncrementalIdeal::pop()
+{
+  d_context->pop();
+  d_tracer.pop();
+}
+
+}  // namespace ff
+}  // namespace theory
+}  // namespace cvc5::internal
+
+#endif /* CVC5_USE_COCOA */

src/theory/ff/groebner.h

@@ -0,0 +1,114 @@
+/******************************************************************************
+ * 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.
+ * ****************************************************************************
+ *
+ * An incremental groebner basis engine.
+ */
+
+#include "cvc5_private.h"
+
+#ifdef CVC5_USE_COCOA
+
+#ifndef CVC5__THEORY__FF__GROEBNER_H
+#define CVC5__THEORY__FF__GROEBNER_H
+
+#include <CoCoA/RingFp.H>
+#include <CoCoA/SparsePolyRing.H>
+
+#include <optional>
+#include <vector>
+
+#include "context/cdlist_forward.h"
+#include "context/cdo.h"
+#include "context/context.h"
+#include "expr/node.h"
+#include "smt/env_obj.h"
+#include "theory/ff/core.h"
+
+namespace cvc5::internal {
+namespace theory {
+namespace ff {
+
+// Class for constructing a polynomial ideal for an incremental source of
+// generators.
+//
+// Essentially, you can pass a sequence of generators to this class:
+//
+//     p1, p2, p3, p4, p5, p6, p7
+//
+// in chunks. E.g., p1, p2 and then p3, p4, p5, p6, p7. After each chunk, you
+// can:
+//
+// * check if the whole sequence generates a trivial ideal
+//   * if so, get a subset of the generators that cause triviality
+// * if not, check if the variety (common zero set) for the sequence is empty
+// * if not, get a common zero
+//
+// The class support backtracking/popping: you can remove a chunk of generators
+// at any time.
+class IncrementalIdeal : EnvObj
+{
+ public:
+  IncrementalIdeal(Env& env, CoCoA::ring polyRing);
+  // Add new generators
+  void pushGenerators(std::vector<CoCoA::RingElem>&& gens);
+  // Is the ideal the whole ring?
+  bool idealIsTrivial();
+  // For a trivial ideal, return a (sub)list of generator indices that generate it.
+  const std::vector<size_t>& trivialCoreIndices();
+  // For a trivial ideal, return a (sub)list of generators that generate it.
+  std::vector<CoCoA::RingElem> trivialCore();
+  // For a non-trivial idea, check whether there is a base-field variety member.
+  bool hasSolution();
+  // For a non-trivial idea with a base-field variety member, get it.
+  const std::vector<CoCoA::RingElem>& solution();
+  // Remove the last batch of generators
+  void pop();
+
+ private:
+  // Run common-root extraction, ensuring a common root is found if one exists.
+  void ensureSolution();
+
+  // Used to manage the sequence of generators. A new context is pushed for
+  // each new chunk of generators, and popped when they are removed.
+  //
+  // With this context, other data structures are automatically updated as
+  // generators are added/removed.
+  std::unique_ptr<context::Context> d_context;
+
+  // The ring that generators/the ideal live in
+  CoCoA::ring d_polyRing;
+  // Used to record steps in the ideal membership calculus.
+  IncrementalTracer d_tracer{};
+  // The sequence of generators
+  context::CDList<CoCoA::RingElem> d_gens;
+  // A GB for the current generators.
+  context::CDO<std::vector<CoCoA::RingElem>> d_basis;
+  // Whether we've already computed a core for ideal triviality.
+  context::CDO<bool> d_hasCore;
+  // What that core is.
+  context::CDO<std::vector<size_t>> d_core;
+  // Whether we've search for a common root, and whether we found one.
+  //
+  // Empty if we haven't searched. True if we found one, False if not.
+  context::CDO<std::optional<bool>> d_hasSolution;
+
+  // What the common root is.
+  context::CDO<std::vector<CoCoA::RingElem>> d_solution;
+};
+
+}  // namespace ff
+}  // namespace theory
+}  // namespace cvc5::internal
+
+#endif /* CVC5__THEORY__FF__GROEBNER_H */
+
+#endif /* CVC5_USE_COCOA */

test/unit/theory/CMakeLists.txt

@@ -33,6 +33,7 @@ cvc5_add_unit_test_white(theory_bv_opt_white theory)
 cvc5_add_unit_test_white(theory_bv_int_blaster_white theory)
 cvc5_add_unit_test_white(theory_engine_white theory)
 cvc5_add_unit_test_black(theory_ff_model_black theory)
+cvc5_add_unit_test_black(theory_ff_groebner_black theory)
 cvc5_add_unit_test_black(theory_ff_roots_black theory)
 cvc5_add_unit_test_black(theory_ff_core_black theory)
 cvc5_add_unit_test_white(theory_int_opt_white theory)