ff: connect sub-theories to main solver & test (#9218)

Organizing the PR a bit:

we hook up the subtheories to TheoryFf
we expose FF-related things via the C++/Pytohn API and SMT-LIB2 interface.
we add a bunch of tests against these interfaces.

NEWS.md

@@ -12,8 +12,18 @@ This file contains a summary of important user-visible changes.
   * `BITVECTOR_USUBO` unsigned subtraction overflow detection
   * `BITVECTOR_SSUBO` signed subtraction overflow detection
   * `BITVECTOR_SDIVO` signed division overflow detection
-
 - Support for Web Assembly compilation using Emscripten.
+- Support for the theory of (prime-order) finite fields:
+  * Sorts are created with
+    * C++: `Solver::makeFiniteFieldSort`
+    * SMT-LIB: `(_ FiniteField P)` for prime order `P`
+  * Constants are created with
+    * C++: `Solver::makeFiniteFieldElem`
+    * SMT-LIB: `(as ffN F)` for integer `N` and field sort `F`
+  * The operators are multiplication, addition and negation
+    * C++: kinds `FF_MUL`, `FF_ADD`, and `FF_NEG`
+    * SMT-LIB: operators `ff.mul`, `ff.add`, and `ff.neg`
+  * The only predicate is equality
 
 **Changes**
 

cmake/deps-utils/CoCoALib-0.99800-trace.patch

@@ -22,6 +22,28 @@ index 4c4d51e..efe50f7 100644
 
  typedef std::list<GPoly> GPolyList;
 
+diff --git a/src/AlgebraicCore/PolyRing-content.C b/src/AlgebraicCore/PolyRing-content.C
+index c5d0a0a..36d6d2b 100644
+--- a/src/AlgebraicCore/PolyRing-content.C
++++ b/src/AlgebraicCore/PolyRing-content.C
+@@ -33,6 +33,7 @@
+ #include "CoCoA/convert.H"
+ #include "CoCoA/error.H"
+ #include "CoCoA/utils.H"  // for len
++#include "CoCoA/TmpGPoly.H"
+
+
+ #include <vector>
+@@ -128,7 +129,9 @@ namespace CoCoA
+   {
+     const PolyRing Rx = owner(f);
+     RingElem ans(Rx);
++    if (handlersEnabled) reductionStartHandler(f);
+     Rx->myMonic(raw(ans), raw(f));
++    if (handlersEnabled) reductionEndHandler(ans);
+     return ans;
+   }
+
 diff --git a/src/AlgebraicCore/SparsePolyOps-reduce.C b/src/AlgebraicCore/SparsePolyOps-reduce.C
 index b5b8b43..11687f0 100644
 --- a/src/AlgebraicCore/SparsePolyOps-reduce.C

examples/api/cpp/CMakeLists.txt

@@ -35,6 +35,10 @@ foreach(example ${CVC5_EXAMPLES_API})
   cvc5_add_example(${example} "" "api/cpp")
 endforeach()
 
+if(USE_COCOA)
+  cvc5_add_example(finite_field "" "api/cpp")
+endif()
+
 set(SYGUS_EXAMPLES_API
   sygus-fun
   sygus-grammar

examples/api/cpp/finite_field.cpp

@@ -0,0 +1,67 @@
+/******************************************************************************
+ * 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 example of solving finite field problems with cvc5's cpp API
+ */
+
+#include <cvc5/cvc5.h>
+
+#include <cassert>
+#include <iostream>
+
+using namespace std;
+using namespace cvc5;
+
+int main()
+{
+  Solver solver;
+  solver.setOption("produce-models", "true");
+
+  Sort f5 = solver.mkFiniteFieldSort("5");
+  Term a = solver.mkConst(f5, "a");
+  Term b = solver.mkConst(f5, "b");
+  Term z = solver.mkFiniteFieldElem("0", f5);
+
+  Term inv =
+      solver.mkTerm(EQUAL,
+                    {solver.mkTerm(FINITE_FIELD_ADD,
+                                   {solver.mkTerm(FINITE_FIELD_MULT, {a, b}),
+                                    solver.mkFiniteFieldElem("-1", f5)}),
+                     z});
+  Term aIsTwo = solver.mkTerm(
+      EQUAL,
+      {solver.mkTerm(FINITE_FIELD_ADD, {a, solver.mkFiniteFieldElem("-2", f5)}),
+       z});
+  // ab - 1 = 0
+  solver.assertFormula(inv);
+  // a = 2
+  solver.assertFormula(aIsTwo);
+
+  // should be SAT, with b = 2^(-1)
+  Result r = solver.checkSat();
+  assert(r.isSat());
+
+  cout << "a = " << solver.getValue(a) << endl;
+  cout << "b = " << solver.getValue(b) << endl;
+
+  // b = 2
+  Term bIsTwo = solver.mkTerm(
+      EQUAL,
+      {solver.mkTerm(FINITE_FIELD_ADD, {b, solver.mkFiniteFieldElem("-2", f5)}),
+       z});
+
+  // should be UNSAT, 2*2 - 1 != 0
+  solver.assertFormula(bIsTwo);
+
+  r = solver.checkSat();
+  assert(!r.isSat());
+}

examples/api/java/CMakeLists.txt

@@ -37,7 +37,7 @@ set(EXAMPLES_API_JAVA
    UnsatCores
 )
 
-foreach(example ${EXAMPLES_API_JAVA})
+function(add_java_example example)
   add_jar(${example} ${example}.java
           INCLUDE_JARS "${CVC5_JAR}"
           OUTPUT_DIR "${CMAKE_BINARY_DIR}/bin/api/java")
@@ -53,4 +53,12 @@ foreach(example ${EXAMPLES_API_JAVA})
         ${example}
   )
   set_tests_properties(${EXAMPLE_TEST_NAME} PROPERTIES SKIP_RETURN_CODE 77)
+endfunction()
+
+foreach(example ${EXAMPLES_API_JAVA})
+  add_java_example(${example})
 endforeach()
+
+if(USE_COCOA)
+  add_java_example(FiniteField)
+endif()

examples/api/java/FiniteField.java

@@ -0,0 +1,70 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Alex Ozdemir, Mudathir Mohamed, Liana Hadarean, Morgan Deters
+ *
+ * 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 example of solving finite field problems with cvc5's Java API
+ *
+ */
+
+import io.github.cvc5.*;
+import java.util.*;
+
+public class FiniteField
+{
+  public static void main(String args[]) throws CVC5ApiException
+  {
+    Solver slv = new Solver();
+    {
+      slv.setLogic("QF_FF"); // Set the logic
+
+      Sort f5 = slv.mkFiniteFieldSort("5");
+      Term a = slv.mkConst(f5, "a");
+      Term b = slv.mkConst(f5, "b");
+      Term z = slv.mkFiniteFieldElem("0", f5);
+
+      System.out.println("is ff: " + f5.isFiniteField());
+      System.out.println("ff size: " + f5.getFiniteFieldSize());
+      System.out.println("is ff value: " + z.isFiniteFieldValue());
+      System.out.println("ff value: " + z.getFiniteFieldValue());
+
+      Term inv =
+        slv.mkTerm(Kind.EQUAL,
+            slv.mkTerm(Kind.FINITE_FIELD_ADD,
+              slv.mkTerm(Kind.FINITE_FIELD_MULT, a, b),
+              slv.mkFiniteFieldElem("-1", f5)),
+            z);
+
+      Term aIsTwo =
+        slv.mkTerm(Kind.EQUAL,
+            slv.mkTerm(Kind.FINITE_FIELD_ADD,
+              a,
+              slv.mkFiniteFieldElem("-2", f5)),
+            z);
+
+      slv.assertFormula(inv);
+      slv.assertFormula(aIsTwo);
+
+      Result r = slv.checkSat();
+      System.out.println("is sat: " + r.isSat());
+
+      Term bIsTwo =
+        slv.mkTerm(Kind.EQUAL,
+            slv.mkTerm(Kind.FINITE_FIELD_ADD,
+              b,
+              slv.mkFiniteFieldElem("-2", f5)),
+            z);
+
+      slv.assertFormula(bIsTwo);
+      r = slv.checkSat();
+      System.out.println("is sat: " + r.isSat());
+    }
+  }
+}

examples/api/python/CMakeLists.txt

@@ -48,7 +48,7 @@ execute_process(COMMAND
                 OUTPUT_VARIABLE PYTHON_MODULE_PATH
                 OUTPUT_STRIP_TRAILING_WHITESPACE)
 
-foreach(example ${EXAMPLES_API_PYTHON})
+function(create_python_example example)
   set(example_test example/api/python/${example})
   add_test(
     NAME ${example_test}
@@ -58,4 +58,12 @@ foreach(example ${EXAMPLES_API_PYTHON})
   set_tests_properties(${example_test} PROPERTIES
     LABELS "example"
     ENVIRONMENT PYTHONPATH=${PYTHON_MODULE_PATH}:${CMAKE_SOURCE_DIR}/api/python)
+endfunction()
+
+foreach(example ${EXAMPLES_API_PYTHON})
+  create_python_example(${example})
 endforeach()
+
+if(USE_COCOA)
+  create_python_example("finite_field")
+endif()

examples/api/python/finite_field.py

@@ -0,0 +1,59 @@
+###############################################################################
+# Top contributors (to current version):
+#   Andrew Reynolds, 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 simple test for cvc5's finite field solver.
+#
+##
+
+import cvc5
+from cvc5 import Kind
+
+if __name__ == "__main__":
+    slv = cvc5.Solver()
+    slv.setOption("produce-models", "true")
+    F = slv.mkFiniteFieldSort("5")
+    a = slv.mkConst(F, "a")
+    b = slv.mkConst(F, "b")
+
+    inv = slv.mkTerm(
+        Kind.EQUAL,
+        slv.mkTerm(Kind.FINITE_FIELD_MULT, a, b),
+        slv.mkFiniteFieldElem("1", F),
+    )
+    aIsTwo = slv.mkTerm(
+        Kind.EQUAL,
+        a,
+        slv.mkFiniteFieldElem("2", F),
+    )
+    # ab - 1 = 0
+    slv.assertFormula(inv)
+    # a = 2
+    slv.assertFormula(aIsTwo)
+    r = slv.checkSat()
+
+    # should be SAT, with b = 2^(-1)
+    assert r.isSat()
+    print(slv.getValue(a).toPythonObj())
+    assert slv.getValue(b).toPythonObj() == -2
+
+    bIsTwo = slv.mkTerm(
+        Kind.EQUAL,
+        b,
+        slv.mkFiniteFieldElem("2", F),
+    )
+
+    # b = 2
+    slv.assertFormula(bIsTwo)
+    r = slv.checkSat()
+
+    # should be UNSAT, since 2*2 - 1 != 0
+    assert not r.isSat()