ff: add resource limits & fix UNSAT core bug (cvc5#10653)

Now we take resource limits into account during our searches and while calling into CoCoA.

Along the way, I found an UNSAT core bug related to the CoCoA encoder and fixed it.

src/theory/ff/cocoa_encoder.cpp

@@ -214,6 +214,16 @@ FiniteFieldValue CocoaEncoder::cocoaFfToFfVal(const Scalar& elem)
   return ff::cocoaFfToFfVal(elem, size());
 }
 
+const Node& CocoaEncoder::polyFact(const Poly& poly) const
+{
+  return d_polyFacts.at(extractStr(poly));
+}
+
+bool CocoaEncoder::polyHasFact(const Poly& poly) const
+{
+  return d_polyFacts.count(extractStr(poly));
+}
+
 const Poly& CocoaEncoder::symPoly(CoCoA::symbol s) const
 {
   Assert(d_symPolys.count(extractStr(s)));
@@ -293,21 +303,24 @@ void CocoaEncoder::encodeFact(const Node& f)
 {
   Assert(d_stage == Stage::Encode);
   Assert(isFfFact(f, size()));
+  Poly p;
   // ==
   if (f.getKind() == Kind::EQUAL)
   {
     encodeTerm(f[0]);
     encodeTerm(f[1]);
-    d_cache.insert({f, d_cache.at(f[0]) - d_cache.at(f[1])});
+    p = d_cache.at(f[0]) - d_cache.at(f[1]);
   }
   // !=
   else
   {
     encodeTerm(f[0][0]);
     encodeTerm(f[0][1]);
     Poly diff = d_cache.at(f[0][0]) - d_cache.at(f[0][1]);
-    d_cache.insert({f, diff * symPoly(d_diseqSyms.at(f)) - 1});
+    p = diff * symPoly(d_diseqSyms.at(f)) - 1;
   }
+  d_cache.insert({f, p});
+  d_polyFacts.insert({extractStr(p), f});
 }
 
 }  // namespace ff

src/theory/ff/cocoa_encoder.h

@@ -33,6 +33,7 @@
 // internal includes
 #include "expr/node.h"
 #include "theory/ff/cocoa_util.h"
+#include "theory/ff/core.h"
 #include "theory/ff/util.h"
 
 namespace cvc5::internal {
@@ -103,6 +104,14 @@ class CocoaEncoder : public FieldObj
    * Convert a (coefficient) Scalar to a FiniteFieldValue.
    */
   FiniteFieldValue cocoaFfToFfVal(const Scalar& elem);
+  /**
+   * Does some fact that imply this poly?
+   */
+  bool polyHasFact(const Poly& poly) const;
+  /**
+   * Get the fact that implies this poly.
+   */
+  const Node& polyFact(const Poly& poly) const;
 
  private:
   /**
@@ -168,6 +177,8 @@ class CocoaEncoder : public FieldObj
   std::vector<Poly> d_polys{};
   /** bitsum polynomials that must be zero */
   std::vector<Poly> d_bitsumPolys{};
+  /** polys to the facts that imply them */
+  std::unordered_map<std::string, Node> d_polyFacts{};
 };
 
 }  // namespace ff

src/theory/ff/cocoa_util.cpp

@@ -21,6 +21,8 @@
 #include <CoCoA/BigIntOps.H>
 #include <CoCoA/SparsePolyIter.H>
 #include <CoCoA/SparsePolyOps-RingElem.H>
+#include <CoCoA/SparsePolyOps-ideal.H>
+#include <CoCoA/TmpGPoly.H>
 
 // std includes
 
@@ -88,6 +90,33 @@ CoCoA::BigInt intToCocoa(const Integer& i)
   return CoCoA::BigIntFromString(i.toString());
 }
 
+const std::vector<Poly>& GBasisTimeout(const CoCoA::ideal& ideal,
+                                       const ResourceManager* rm)
+{
+  if (rm == nullptr)
+  {
+    return CoCoA::GBasis(ideal);
+  }
+  double sec = static_cast<double>(rm->getRemainingTime()) / 1e3;
+  Trace("ff::gb") << "Computing a GB; limit " << sec << "s" << std::endl;
+  try
+  {
+    if (sec == 0)
+    {
+      return CoCoA::GBasis(ideal);
+    }
+    else
+    {
+      return CoCoA::GBasis(ideal, CoCoA::CpuTimeLimit(sec));
+    }
+  }
+  catch (CoCoA::TimeoutException& t)
+  {
+    CoCoA::handlersEnabled = false;
+    throw FfTimeoutException("GBasis");
+  }
+}
+
 }  // namespace ff
 }  // namespace theory
 }  // namespace cvc5::internal

src/theory/ff/cocoa_util.h

@@ -30,8 +30,10 @@
 #include <vector>
 
 // internal includes
+#include "theory/ff/util.h"
 #include "util/finite_field_value.h"
 #include "util/integer.h"
+#include "util/resource_manager.h"
 
 namespace cvc5::internal {
 namespace theory {
@@ -76,6 +78,13 @@ std::string extractStr(const T& t)
   return o.str();
 }
 
+/**
+ * Compute a GB, with timeout given by `rm`.
+ * Throws an FfTimeoutException if the timeout is exceeded.
+ */
+const std::vector<Poly>& GBasisTimeout(const CoCoA::ideal& ideal,
+                                       const ResourceManager* rm);
+
 }  // namespace ff
 }  // namespace theory
 }  // namespace cvc5::internal

src/theory/ff/multi_roots.cpp

@@ -30,7 +30,10 @@
 #include <sstream>
 
 #include "smt/assertions.h"
+#include "theory/ff/cocoa_util.h"
 #include "theory/ff/uni_roots.h"
+#include "theory/ff/util.h"
+#include "util/resource_manager.h"
 
 namespace cvc5::internal {
 namespace theory {
@@ -135,6 +138,7 @@ std::pair<size_t, CoCoA::RingElem> extractAssignment(
 std::unordered_set<std::string> assignedVars(const CoCoA::ideal& ideal)
 {
   std::unordered_set<std::string> ret{};
+  Assert(CoCoA::HasGBasis(ideal));
   for (const auto& g : CoCoA::GBasis(ideal))
   {
     if (CoCoA::deg(g) == 1)
@@ -160,6 +164,7 @@ std::unique_ptr<AssignmentEnumerator> applyRule(const CoCoA::ideal& ideal)
   CoCoA::ring polyRing = ideal->myRing();
   Assert(!isUnsat(ideal));
   // first, we look for super-linear univariate polynomials.
+  Assert(CoCoA::HasGBasis(ideal));
   const auto& gens = CoCoA::GBasis(ideal);
   for (const auto& p : gens)
   {
@@ -208,7 +213,8 @@ std::unique_ptr<AssignmentEnumerator> applyRule(const CoCoA::ideal& ideal)
   }
 }
 
-std::vector<CoCoA::RingElem> findZero(const CoCoA::ideal& initialIdeal)
+std::vector<CoCoA::RingElem> findZero(const CoCoA::ideal& initialIdeal,
+                                      const Env& env)
 {
   CoCoA::ring polyRing = initialIdeal->myRing();
   // We maintain two stacks:
@@ -242,8 +248,16 @@ std::vector<CoCoA::RingElem> findZero(const CoCoA::ideal& initialIdeal)
   // while some ideal might have a zero.
   while (!ideals.empty())
   {
-    // choose one
+    // check for timeout
+    if (env.getResourceManager()->outOfTime())
+    {
+      throw FfTimeoutException("findZero");
+    }
+    // choose one ideal
     const auto& ideal = ideals.back();
+    // make sure we have a GBasis:
+    GBasisTimeout(ideal, env.getResourceManager());
+    Assert(CoCoA::HasGBasis(ideal));
     // If the ideal is UNSAT, drop it.
     if (isUnsat(ideal))
     {
@@ -254,6 +268,7 @@ std::vector<CoCoA::RingElem> findZero(const CoCoA::ideal& initialIdeal)
     else if (allVarsAssigned(ideal))
     {
       std::unordered_map<size_t, CoCoA::RingElem> varNumToValue{};
+      Assert(CoCoA::HasGBasis(ideal));
       const auto& gens = CoCoA::GBasis(ideal);
       size_t numIndets = CoCoA::NumIndets(polyRing);
       Assert(gens.size() == numIndets);
@@ -296,6 +311,7 @@ std::vector<CoCoA::RingElem> findZero(const CoCoA::ideal& initialIdeal)
             << "level: " << branchers.size()
             << ", brancher: " << branchers.back()->name()
             << ", branch: " << choicePoly.value() << std::endl;
+        Assert(CoCoA::HasGBasis(ideal));
         std::vector<CoCoA::RingElem> newGens = CoCoA::GBasis(ideal);
         newGens.push_back(choicePoly.value());
         ideals.push_back(CoCoA::ideal(newGens));

src/theory/ff/multi_roots.h

@@ -32,6 +32,7 @@
 #include <vector>
 
 #include "expr/node.h"
+#include "smt/env.h"
 
 namespace cvc5::internal {
 namespace theory {
@@ -40,7 +41,7 @@ namespace ff {
 /**
  * Find a common zero for all poynomials in this ideal. Figure 5 from [OKTB23].
  */
-std::vector<CoCoA::RingElem> findZero(const CoCoA::ideal& ideal);
+std::vector<CoCoA::RingElem> findZero(const CoCoA::ideal& ideal, const Env& env);
 
 /**
  * Enumerates **assignment**s: monic, degree-one, univariate polynomials.

src/theory/ff/split_gb.cpp

@@ -31,13 +31,14 @@
 // internal includes
 #include "base/output.h"
 #include "theory/ff/parse.h"
+#include "util/resource_manager.h"
 
 namespace cvc5::internal {
 namespace theory {
 namespace ff {
 
 std::optional<std::unordered_map<Node, FiniteFieldValue>> split(
-    const std::vector<Node>& facts, const FfSize& size)
+    const std::vector<Node>& facts, const FfSize& size, const Env& env)
 {
   std::unordered_set<Node> bits{};
   CocoaEncoder enc(size);
@@ -64,7 +65,7 @@ std::optional<std::unordered_map<Node, FiniteFieldValue>> split(
   BitProp bitProp(facts, enc);
 
   std::vector<Polys> splitGens = {lGens, nlGens};
-  SplitGb splitBasis = splitGb(splitGens, bitProp);
+  SplitGb splitBasis = splitGb(splitGens, bitProp, env);
   if (std::any_of(splitBasis.begin(), splitBasis.end(), [](const auto& b) {
         return b.isWholeRing();
       }))
@@ -73,7 +74,7 @@ std::optional<std::unordered_map<Node, FiniteFieldValue>> split(
   }
 
   std::optional<Point> root =
-      splitFindZero(std::move(splitBasis), enc.polyRing(), bitProp);
+      splitFindZero(std::move(splitBasis), enc.polyRing(), bitProp, env);
   if (root.has_value())
   {
     std::unordered_map<Node, FiniteFieldValue> model;
@@ -89,7 +90,9 @@ std::optional<std::unordered_map<Node, FiniteFieldValue>> split(
   return {};
 }
 
-SplitGb splitGb(const std::vector<Polys>& generatorSets, BitProp& bitProp)
+SplitGb splitGb(const std::vector<Polys>& generatorSets,
+                BitProp& bitProp,
+                const Env& env)
 {
   size_t k = generatorSets.size();
   std::vector<Polys> newPolys(generatorSets);
@@ -108,7 +111,7 @@ SplitGb splitGb(const std::vector<Polys>& generatorSets, BitProp& bitProp)
         std::copy(newPolys[i].begin(),
                   newPolys[i].end(),
                   std::back_inserter(newGens));
-        splitBasis[i] = Gb(newGens);
+        splitBasis[i] = Gb(newGens, env.getResourceManager());
         newPolys[i].clear();
       }
     }
@@ -146,7 +149,8 @@ bool admit(size_t i, const Poly& p)
 
 std::optional<Point> splitFindZero(SplitGb&& splitBasisIn,
                                    CoCoA::ring polyRing,
-                                   BitProp& bitProp)
+                                   BitProp& bitProp,
+                                   const Env& env)
 {
   SplitGb splitBasis = std::move(splitBasisIn);
   while (true)
@@ -159,7 +163,7 @@ std::optional<Point> splitFindZero(SplitGb&& splitBasisIn,
     }
     PartialPoint nullPartialRoot(CoCoA::NumIndets(polyRing));
     auto result = splitZeroExtend(
-        allGens, SplitGb(splitBasis), std::move(nullPartialRoot), bitProp);
+        allGens, SplitGb(splitBasis), std::move(nullPartialRoot), bitProp, env);
     if (std::holds_alternative<Poly>(result))
     {
       auto conflict = std::get<Poly>(result);
@@ -172,7 +176,7 @@ std::optional<Point> splitFindZero(SplitGb&& splitBasisIn,
                   std::back_inserter(gens.back()));
         gens.back().push_back(conflict);
       }
-      splitBasis = splitGb(gens, bitProp);
+      splitBasis = splitGb(gens, bitProp, env);
     }
     else if (std::holds_alternative<bool>(result))
     {
@@ -188,7 +192,8 @@ std::optional<Point> splitFindZero(SplitGb&& splitBasisIn,
 std::variant<Point, Poly, bool> splitZeroExtend(const Polys& origPolys,
                                                 const SplitGb&& curBases,
                                                 const PartialPoint&& curR,
-                                                const BitProp& bitProp)
+                                                const BitProp& bitProp,
+                                                const Env& env)
 {
   Assert(origPolys.size());
   CoCoA::ring polyRing = CoCoA::owner(origPolys[0]);
@@ -211,6 +216,11 @@ std::variant<Point, Poly, bool> splitZeroExtend(const Polys& origPolys,
     return false;
   }
 
+  if (env.getResourceManager()->outOfTime())
+  {
+    throw FfTimeoutException("splitZeroExtend");
+  }
+
   if (nAssigned == CoCoA::NumIndets(CoCoA::owner(origPolys[0])))
   {
     Point out;
@@ -242,9 +252,9 @@ std::variant<Point, Poly, bool> splitZeroExtend(const Polys& origPolys,
       newSplitGens.back().push_back(*next);
     }
     BitProp bitPropCopy = bitProp;
-    SplitGb newBases = splitGb(newSplitGens, bitPropCopy);
+    SplitGb newBases = splitGb(newSplitGens, bitPropCopy, env);
     auto result = splitZeroExtend(
-        origPolys, std::move(newBases), std::move(newR), bitPropCopy);
+        origPolys, std::move(newBases), std::move(newR), bitPropCopy, env);
     if (!std::holds_alternative<bool>(result))
     {
       return result;
@@ -333,12 +343,13 @@ void checkZero(const SplitGb& origBases, const Point& zero)
 }
 
 Gb::Gb() : d_ideal(), d_basis(){};
-Gb::Gb(const Polys& generators) : d_ideal(), d_basis()
+Gb::Gb(const std::vector<Poly>& generators, const ResourceManager* rm)
+    : d_ideal(), d_basis()
 {
   if (generators.size())
   {
     d_ideal.emplace(CoCoA::ideal(generators));
-    d_basis = CoCoA::GBasis(d_ideal.value());
+    d_basis = GBasisTimeout(d_ideal.value(), rm);
   }
 }