ff: hook up SplitGB solver (cvc5#10274)

src/CMakeLists.txt

@@ -74,6 +74,8 @@ libcvc5_add_sources(
   preprocessing/passes/extended_rewriter_pass.h
   preprocessing/passes/ff_bitsum.cpp
   preprocessing/passes/ff_bitsum.h
+  preprocessing/passes/ff_disjunctive_bit.cpp
+  preprocessing/passes/ff_disjunctive_bit.h
   preprocessing/passes/foreign_theory_rewrite.cpp
   preprocessing/passes/foreign_theory_rewrite.h
   preprocessing/passes/fun_def_fmf.cpp

src/options/ff_options.toml

@@ -16,3 +16,34 @@ name   = "Finite Field Theory"
   type       = "bool"
   default    = "false"
   help       = "include field polynomials in Groebner basis computation; don't do this"
+
+[[option]]
+  name       = "ffDisjunctiveBit"
+  category   = "expert"
+  long       = "ff-disjunctive-bit"
+  type       = "bool"
+  default    = "false"
+  help       = "leave disjunctive bit constraints (or (= x 1) (= x 0)) alone; otherwise, preprocess to (= (* x x) x)"
+
+[[option]]
+  name       = "ffBitsum"
+  category   = "expert"
+  long       = "ff-bitsum"
+  type       = "bool"
+  default    = "false"
+  help       = "parse bitsums"
+[[option]]
+  name       = "ffSolver"
+  category   = "expert"
+  long       = "ff-solver=MODE"
+  type       = "FfSolver"
+  default    = "GB"
+  help       = "which field solver (default: 'gb'; see --ff-solver=help)"
+  help_mode  = "Which field solver"
+[[option.mode.GB]]
+  name = "gb"
+  help = "use a groebner basis for the whole system"
+[[option.mode.SPLIT_GB]]
+  name = "split"
+  help = "use multiple groebner bases for partitions of the system"
+

src/preprocessing/passes/ff_disjunctive_bit.cpp

@@ -0,0 +1,57 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Alex Ozdemir
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2023 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.
+ * ****************************************************************************
+ *
+ * replace disjunctive bit constraints with polynomial bit constraints
+ *
+ * example: x = 0 OR x = 1 becomes x * x = x
+ */
+
+#include "preprocessing/passes/ff_disjunctive_bit.h"
+
+// external includes
+
+// std includes
+
+// internal includes
+#include "preprocessing/assertion_pipeline.h"
+#include "theory/ff/parse.h"
+
+namespace cvc5::internal {
+namespace preprocessing {
+namespace passes {
+
+FfDisjunctiveBit::FfDisjunctiveBit(PreprocessingPassContext* preprocContext)
+    : PreprocessingPass(preprocContext, "ff-disjunctive-bit")
+{
+}
+
+PreprocessingPassResult FfDisjunctiveBit::applyInternal(
+    AssertionPipeline* assertionsToPreprocess)
+{
+  auto nm = NodeManager::currentNM();
+  for (uint64_t i = 0, n = assertionsToPreprocess->size(); i < n; ++i)
+  {
+    Node fact = (*assertionsToPreprocess)[i];
+    std::optional<Node> var = theory::ff::parse::disjunctiveBitConstraint(fact);
+    if (var.has_value())
+    {
+      Trace("ff::disjunctive-bit") << "rw bit constr: " << *var << std::endl;
+      Node var2 = nm->mkNode(Kind::FINITE_FIELD_MULT, *var, *var);
+      assertionsToPreprocess->replace(i, var2.eqNode(*var));
+    }
+  }
+  return PreprocessingPassResult::NO_CONFLICT;
+}
+
+}  // namespace passes
+}  // namespace preprocessing
+}  // namespace cvc5::internal

src/preprocessing/passes/ff_disjunctive_bit.h

@@ -0,0 +1,49 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Alex Ozdemir
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2023 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.
+ * ****************************************************************************
+ *
+ * replace disjunctive bit constraints with polynomial bit constraints
+ *
+ * example: x = 0 OR x = 1 becomes x * x = x
+ */
+
+#include "cvc5_private.h"
+
+#ifndef CVC5__PREPROCESSING__PASSES__FF_DISJUNCTIVE_BIT_H
+#define CVC5__PREPROCESSING__PASSES__FF_DISJUNCTIVE_BIT_H
+
+// external includes
+
+// std includes
+
+// internal includes
+#include "preprocessing/preprocessing_pass.h"
+#include "preprocessing/preprocessing_pass_context.h"
+
+namespace cvc5::internal {
+namespace preprocessing {
+namespace passes {
+
+class FfDisjunctiveBit : public PreprocessingPass
+{
+ public:
+  FfDisjunctiveBit(PreprocessingPassContext* preprocContext);
+
+ protected:
+  PreprocessingPassResult applyInternal(
+      AssertionPipeline* assertionsToPreprocess) override;
+};
+
+}  // namespace passes
+}  // namespace preprocessing
+}  // namespace cvc5::internal
+
+#endif /* CVC5__PREPROCESSING__PASSES__FF_DISJUNCTIVE_BIT_H */

src/preprocessing/preprocessing_pass_registry.cpp

@@ -33,6 +33,8 @@
 #include "preprocessing/passes/bv_to_bool.h"
 #include "preprocessing/passes/bv_to_int.h"
 #include "preprocessing/passes/extended_rewriter_pass.h"
+#include "preprocessing/passes/ff_bitsum.h"
+#include "preprocessing/passes/ff_disjunctive_bit.h"
 #include "preprocessing/passes/foreign_theory_rewrite.h"
 #include "preprocessing/passes/fun_def_fmf.h"
 #include "preprocessing/passes/global_negate.h"
@@ -81,6 +83,7 @@ void PreprocessingPassRegistry::registerPassInfo(
 PreprocessingPass* PreprocessingPassRegistry::createPass(
     PreprocessingPassContext* ppCtx, const std::string& name)
 {
+  Assert(d_ppInfo.count(name));
   return d_ppInfo[name](ppCtx);
 }
 
@@ -126,6 +129,8 @@ PreprocessingPassRegistry::PreprocessingPassRegistry()
   registerPassInfo("global-negate", callCtor<GlobalNegate>);
   registerPassInfo("int-to-bv", callCtor<IntToBV>);
   registerPassInfo("bv-to-int", callCtor<BVToInt>);
+  registerPassInfo("ff-bitsum", callCtor<FfBitsum>);
+  registerPassInfo("ff-disjunctive-bit", callCtor<FfDisjunctiveBit>);
   registerPassInfo("learned-rewrite", callCtor<LearnedRewrite>);
   registerPassInfo("foreign-theory-rewrite", callCtor<ForeignTheoryRewrite>);
   registerPassInfo("synth-rr", callCtor<SynthRewRulesPass>);

src/smt/process_assertions.cpp

@@ -20,6 +20,7 @@
 #include "options/arith_options.h"
 #include "options/base_options.h"
 #include "options/bv_options.h"
+#include "options/ff_options.h"
 #include "options/quantifiers_options.h"
 #include "options/sep_options.h"
 #include "options/smt_options.h"
@@ -314,6 +315,16 @@ bool ProcessAssertions::apply(AssertionPipeline& ap)
                << endl;
   Trace("smt") << " assertions     : " << ap.size() << endl;
 
+  // ff
+  if (options().ff.ffDisjunctiveBit)
+  {
+    applyPass("ff-disjunctive-bit", ap);
+  }
+  if (options().ff.ffBitsum || options().ff.ffSolver == options::FfSolver::SPLIT_GB)
+  {
+    applyPass("ff-bitsum", ap);
+  }
+
   // ensure rewritten
   applyPass("rewrite", ap);
 

src/theory/ff/sub_theory.cpp

@@ -35,6 +35,7 @@
 #include "theory/ff/cocoa_encoder.h"
 #include "theory/ff/core.h"
 #include "theory/ff/multi_roots.h"
+#include "theory/ff/split_gb.h"
 #include "util/cocoa_globals.h"
 #include "util/finite_field_value.h"
 
@@ -59,94 +60,119 @@ Result SubTheory::postCheck(Theory::Effort e)
   if (e == Theory::EFFORT_FULL)
   {
     if (d_facts.empty()) return Result::SAT;
-    CocoaEncoder enc(size());
-    // collect leaves
-    for (const Node& node : d_facts)
+    if (options().ff.ffSolver == options::FfSolver::SPLIT_GB)
     {
-      enc.addFact(node);
+      std::vector<Node> facts{};
+      std::copy(d_facts.begin(), d_facts.end(), std::back_inserter(facts));
+      auto result = split(facts, size());
+      if (result.has_value())
+      {
+        const auto nm = NodeManager::currentNM();
+        for (const auto& [var, val] : result.value())
+        {
+          d_model.insert({var, nm->mkConst<FiniteFieldValue>(val)});
+        }
+        return Result::SAT;
+      }
+      std::copy(d_facts.begin(), d_facts.end(), std::back_inserter(d_conflict));
+      return Result::UNSAT;
     }
-    enc.endScan();
-    // assert facts
-    for (const Node& node : d_facts)
+    else if (options().ff.ffSolver == options::FfSolver::GB)
     {
-      enc.addFact(node);
-    }
+      CocoaEncoder enc(size());
+      // collect leaves
+      for (const Node& node : d_facts)
+      {
+        enc.addFact(node);
+      }
+      enc.endScan();
+      // assert facts
+      for (const Node& node : d_facts)
+      {
+        enc.addFact(node);
+      }
 
-    // compute a GB
-    std::vector<CoCoA::RingElem> generators;
-    generators.insert(generators.end(), enc.polys().begin(), enc.polys().end());
-    generators.insert(
-        generators.end(), enc.bitsumPolys().begin(), enc.bitsumPolys().end());
-    size_t nNonFieldPolyGens = generators.size();
-    if (options().ff.ffFieldPolys)
-    {
-      for (const auto& var : CoCoA::indets(enc.polyRing()))
+      // compute a GB
+      std::vector<CoCoA::RingElem> generators;
+      generators.insert(
+          generators.end(), enc.polys().begin(), enc.polys().end());
+      generators.insert(
+          generators.end(), enc.bitsumPolys().begin(), enc.bitsumPolys().end());
+      size_t nNonFieldPolyGens = generators.size();
+      if (options().ff.ffFieldPolys)
       {
-        CoCoA::BigInt characteristic = CoCoA::characteristic(coeffRing());
-        long power = CoCoA::LogCardinality(coeffRing());
-        CoCoA::BigInt size = CoCoA::power(characteristic, power);
-        generators.push_back(CoCoA::power(var, size) - var);
+        for (const auto& var : CoCoA::indets(enc.polyRing()))
+        {
+          CoCoA::BigInt characteristic = CoCoA::characteristic(coeffRing());
+          long power = CoCoA::LogCardinality(coeffRing());
+          CoCoA::BigInt size = CoCoA::power(characteristic, power);
+          generators.push_back(CoCoA::power(var, size) - var);
+        }
       }
-    }
-    Tracer tracer(generators);
-    if (options().ff.ffTraceGb) tracer.setFunctionPointers();
-    CoCoA::ideal ideal = CoCoA::ideal(generators);
-    const auto basis = CoCoA::GBasis(ideal);
-    if (options().ff.ffTraceGb) tracer.unsetFunctionPointers();
-
-    // if it is trivial, create a conflict
-    bool is_trivial = basis.size() == 1 && CoCoA::deg(basis.front()) == 0;
-    if (is_trivial)
-    {
-      Trace("ff::gb") << "Trivial GB" << std::endl;
-      if (options().ff.ffTraceGb)
+      Tracer tracer(generators);
+      if (options().ff.ffTraceGb) tracer.setFunctionPointers();
+      CoCoA::ideal ideal = CoCoA::ideal(generators);
+      const auto basis = CoCoA::GBasis(ideal);
+      if (options().ff.ffTraceGb) tracer.unsetFunctionPointers();
+
+      // if it is trivial, create a conflict
+      bool is_trivial = basis.size() == 1 && CoCoA::deg(basis.front()) == 0;
+      if (is_trivial)
       {
-        std::vector<size_t> coreIndices = tracer.trace(basis.front());
-        Assert(d_conflict.empty());
-        for (size_t i : coreIndices)
+        Trace("ff::gb") << "Trivial GB" << std::endl;
+        if (options().ff.ffTraceGb)
         {
-          // omit field polys from core
-          if (i < nNonFieldPolyGens)
+          std::vector<size_t> coreIndices = tracer.trace(basis.front());
+          Assert(d_conflict.empty());
+          for (size_t i : coreIndices)
           {
-            Trace("ff::core") << "Core: " << d_facts[i] << std::endl;
-            d_conflict.push_back(d_facts[i]);
+            // omit field polys from core
+            if (i < nNonFieldPolyGens)
+            {
+              Trace("ff::core") << "Core: " << d_facts[i] << std::endl;
+              d_conflict.push_back(d_facts[i]);
+            }
           }
         }
+        else
+        {
+          setTrivialConflict();
+        }
       }
       else
       {
-        setTrivialConflict();
-      }
-    }
-    else
-    {
-      Trace("ff::gb") << "Non-trivial GB" << std::endl;
+        Trace("ff::gb") << "Non-trivial GB" << std::endl;
 
-      // common root (vec of CoCoA base ring elements)
-      std::vector<CoCoA::RingElem> root = findZero(ideal);
+        // common root (vec of CoCoA base ring elements)
+        std::vector<CoCoA::RingElem> root = findZero(ideal);
 
-      if (root.empty())
-      {
-        // UNSAT
-        setTrivialConflict();
-      }
-      else
-      {
-        // SAT: populate d_model from the root
-        Assert(d_model.empty());
-        const auto nm = NodeManager::currentNM();
-        for (const auto& [idx, node] : enc.nodeIndets())
+        if (root.empty())
+        {
+          // UNSAT
+          setTrivialConflict();
+        }
+        else
         {
-          if (isFfLeaf(node))
+          // SAT: populate d_model from the root
+          Assert(d_model.empty());
+          const auto nm = NodeManager::currentNM();
+          for (const auto& [idx, node] : enc.nodeIndets())
           {
-            Node value = nm->mkConst(enc.cocoaFfToFfVal(root[idx]));
-            Trace("ff::model")
-                << "Model: " << node << " = " << value << std::endl;
-            d_model.emplace(node, value);
+            if (isFfLeaf(node))
+            {
+              Node value = nm->mkConst(enc.cocoaFfToFfVal(root[idx]));
+              Trace("ff::model")
+                  << "Model: " << node << " = " << value << std::endl;
+              d_model.emplace(node, value);
+            }
           }
         }
       }
     }
+    else
+    {
+      Unreachable() << options().ff.ffSolver << std::endl;
+    }
     AlwaysAssert((!d_conflict.empty() ^ !d_model.empty()) || d_facts.empty());
     return d_facts.empty() || d_conflict.empty() ? Result::SAT : Result::UNSAT;
   }