ff: kinds file and deps (enumerator, type-checker, rewriter)

src/CMakeLists.txt

@@ -693,6 +693,12 @@ libcvc5_add_sources(
   theory/evaluator.h
   theory/ext_theory.cpp
   theory/ext_theory.h
+  theory/ff/theory_ff.cpp
+  theory/ff/theory_ff.h
+  theory/ff/theory_ff_rewriter.cpp
+  theory/ff/theory_ff_rewriter.h
+  theory/ff/theory_ff_type_rules.cpp
+  theory/ff/theory_ff_type_rules.h
   theory/fp/fp_word_blaster.cpp
   theory/fp/fp_word_blaster.h
   theory/fp/fp_expand_defs.cpp
@@ -1296,6 +1302,7 @@ set(KINDS_FILES
   ${PROJECT_SOURCE_DIR}/src/theory/uf/kinds
   ${PROJECT_SOURCE_DIR}/src/theory/arith/kinds
   ${PROJECT_SOURCE_DIR}/src/theory/bv/kinds
+  ${PROJECT_SOURCE_DIR}/src/theory/ff/kinds
   ${PROJECT_SOURCE_DIR}/src/theory/fp/kinds
   ${PROJECT_SOURCE_DIR}/src/theory/arrays/kinds
   ${PROJECT_SOURCE_DIR}/src/theory/datatypes/kinds

src/expr/node_manager_template.cpp

@@ -31,6 +31,7 @@
 #include "expr/type_checker.h"
 #include "expr/type_properties.h"
 #include "util/bitvector.h"
+#include "util/finite_field.h"
 #include "util/poly_util.h"
 #include "util/rational.h"
 #include "util/resource_manager.h"
@@ -180,6 +181,11 @@ TypeNode NodeManager::mkBitVectorType(unsigned size)
   return mkTypeConst<BitVectorSize>(BitVectorSize(size));
 }
 
+TypeNode NodeManager::mkFiniteFieldType(const Integer& modulus)
+{
+  return mkTypeConst<FiniteFieldSize>(FiniteFieldSize(modulus));
+}
+
 TypeNode NodeManager::sExprType()
 {
   return mkTypeConst<TypeConstant>(SEXPR_TYPE);
@@ -1314,6 +1320,13 @@ Node NodeManager::mkConstRealOrInt(const Rational& r)
   return mkConstReal(r);
 }
 
+Node NodeManager::mkConstFiniteFieldElem(const Integer& v, const TypeNode& type)
+{
+  Assert(type.isFiniteField());
+  return mkConst(kind::CONST_FINITE_FIELD,
+                 FiniteField(v, type.getFiniteFieldSize()));
+}
+
 Node NodeManager::mkConstRealOrInt(const TypeNode& tn, const Rational& r)
 {
   Assert(tn.isRealOrInt()) << "Expected real or int for mkConstRealOrInt, got "

src/expr/node_manager_template.h

@@ -31,6 +31,7 @@
 #include "expr/node_builder.h"
 #include "expr/node_value.h"
 #include "util/floatingpoint_size.h"
+#include "util/integer.h"
 
 namespace cvc5 {
 
@@ -449,6 +450,9 @@ class NodeManager
   /** Make the type of bitvectors of size <code>size</code> */
   TypeNode mkBitVectorType(unsigned size);
 
+  /** Make the type of finite field elements modulo <code>modulus</code> */
+  TypeNode mkFiniteFieldType(const Integer& modulus);
+
   /** Make the type of arrays with the given parameterization */
   TypeNode mkArrayType(TypeNode indexType, TypeNode constituentType);
 
@@ -661,6 +665,13 @@ class NodeManager
    */
   Node mkConstInt(const Rational& r);
 
+  /**
+   * Make a contant finite field element.
+   *
+   * Given the integer value of the element and its type.
+   */
+  Node mkConstFiniteFieldElem(const Integer& v, const TypeNode& type);
+
   /**
    * Make constant real or int, which calls one of the above methods based
    * on whether r is integral.

src/expr/type_node.cpp

@@ -24,6 +24,7 @@
 #include "theory/type_enumerator.h"
 #include "util/bitvector.h"
 #include "util/cardinality.h"
+#include "util/finite_field.h"
 
 using namespace std;
 
@@ -99,8 +100,8 @@ CardinalityClass TypeNode::getCardinalityClass()
   {
     ret = CardinalityClass::INTERPRETED_ONE;
   }
-  else if (isBoolean() || isBitVector() || isFloatingPoint()
-           || isRoundingMode())
+  else if (isBoolean() || isBitVector() || isFloatingPoint() || isRoundingMode()
+           || isFiniteField())
   {
     ret = CardinalityClass::FINITE;
   }
@@ -552,6 +553,12 @@ uint32_t TypeNode::getBitVectorSize() const
   return getConst<BitVectorSize>();
 }
 
+Integer TypeNode::getFiniteFieldSize() const
+{
+  Assert(getKind() == kind::FINITE_FIELD_TYPE);
+  return getConst<FiniteFieldSize>();
+}
+
 TypeNode TypeNode::getRangeType() const
 {
   if (isDatatypeTester())

src/expr/type_node.h

@@ -30,6 +30,7 @@
 #include "expr/metakind.h"
 #include "expr/node_value.h"
 #include "util/cardinality_class.h"
+#include "util/integer.h"
 
 namespace cvc5::internal {
 
@@ -457,6 +458,9 @@ class TypeNode {
   /** Is this an array type? */
   bool isArray() const;
 
+  /** Is this an array type? */
+  bool isFiniteField() const;
+
   /** Is this a Set type? */
   bool isSet() const;
 
@@ -653,6 +657,9 @@ class TypeNode {
   /** Get the size of this bit-vector type. */
   uint32_t getBitVectorSize() const;
 
+  /** Get the field cardinality (order) of this finite-field type. */
+  Integer getFiniteFieldSize() const;
+
   /** Is this a sort kind? */
   bool isUninterpretedSort() const;
 
@@ -877,6 +884,11 @@ inline bool TypeNode::isArray() const {
   return getKind() == kind::ARRAY_TYPE;
 }
 
+inline bool TypeNode::isFiniteField() const
+{
+  return getKind() == kind::FINITE_FIELD_TYPE;
+}
+
 inline TypeNode TypeNode::getArrayIndexType() const {
   Assert(isArray());
   return (*this)[0];

src/theory/ff/kinds

@@ -0,0 +1,56 @@
+# kinds                                                               -*- sh -*-
+#
+# For documentation on this file format, please refer to
+# src/theory/builtin/kinds.
+#
+
+theory THEORY_FF \
+    ::cvc5::internal::theory::ff::TheoryFiniteFields \
+    "theory/ff/theory_ff.h"
+typechecker "theory/ff/theory_ff_type_rules.h"
+rewriter ::cvc5::internal::theory::ff::TheoryFiniteFieldsRewriter \
+    "theory/ff/theory_ff_rewriter.h"
+
+properties parametric
+properties check presolve
+
+# Finite Fields
+# operator FINITE_FIELD_TYPE 1 "finite-field type"
+constant FINITE_FIELD_TYPE \
+  struct \
+  FiniteFieldSize \
+  "::cvc5::internal::FiniteFieldSizeHashFunction" \
+  "util/finite_field.h" \
+  "finite field type"
+
+cardinality FINITE_FIELD_TYPE \
+    "::cvc5::internal::theory::ff::FiniteFieldProperties::computeCardinality(%TYPE%)" \
+    "theory/ff/theory_ff_type_rules.h"
+
+enumerator FINITE_FIELD_TYPE \
+    "::cvc5::internal::theory::ff::FiniteFieldEnumerator" \
+    "theory/ff/type_enumerator.h"
+
+well-founded FINITE_FIELD_TYPE \
+    true \
+    "(*cvc5::internal::theory::TypeEnumerator(%TYPE%))" \
+    "theory/type_enumerator.h"
+
+constant CONST_FINITE_FIELD \
+  class \
+  FiniteField \
+  ::cvc5::internal::FiniteFieldHashFunction \
+  "util/finite_field.h" \
+  "a finite-field constant; payload is an instance of the cvc5::internal::FiniteField class"
+
+## ffmetic kinds
+operator FINITE_FIELD_MULT 2: "multiplication of two or more field elements"
+operator FINITE_FIELD_NEG 1 "unary negation of a field element"
+operator FINITE_FIELD_ADD 2: "addition of two or more field elements"
+
+typerule CONST_FINITE_FIELD ::cvc5::internal::theory::ff::FiniteFieldConstantTypeRule
+typerule FINITE_FIELD_MULT ::cvc5::internal::theory::ff::FiniteFieldFixedFieldTypeRule
+typerule FINITE_FIELD_NEG ::cvc5::internal::theory::ff::FiniteFieldFixedFieldTypeRule
+typerule FINITE_FIELD_ADD ::cvc5::internal::theory::ff::FiniteFieldFixedFieldTypeRule
+
+endtheory

src/theory/ff/theory_ff.cpp

@@ -0,0 +1,153 @@
+/******************************************************************************
+ * 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.
+ * ****************************************************************************
+ *
+ * Finite fields theory
+ */
+
+#include "theory/ff/theory_ff.h"
+
+#include <cerrno>
+#include <fstream>
+#include <iostream>
+#include <numeric>
+#include <sstream>
+#include <unordered_map>
+
+#include "expr/node_manager_attributes.h"
+#include "expr/node_traversal.h"
+#include "theory/theory_model.h"
+#include "theory/trust_substitutions.h"
+#include "util/statistics_registry.h"
+#include "util/utility.h"
+
+using namespace cvc5::internal::kind;
+
+namespace cvc5::internal {
+namespace theory {
+namespace ff {
+
+void noCoCoA()
+{
+  throw LogicException(
+      "cvc5 can't solve field problems since it was not configured with "
+      "--cocoa");
+}
+
+TheoryFiniteFields::TheoryFiniteFields(Env& env,
+                                       OutputChannel& out,
+                                       Valuation valuation)
+    : Theory(THEORY_FF, env, out, valuation),
+      d_state(env, valuation),
+      d_im(env, *this, d_state, getStatsPrefix(THEORY_FF)),
+      d_eqNotify(d_im)
+{
+  d_theoryState = &d_state;
+  d_inferManager = &d_im;
+}
+
+TheoryFiniteFields::~TheoryFiniteFields() {}
+
+TheoryRewriter* TheoryFiniteFields::getTheoryRewriter() { return &d_rewriter; }
+
+ProofRuleChecker* TheoryFiniteFields::getProofChecker() { return nullptr; }
+
+bool TheoryFiniteFields::needsEqualityEngine(EeSetupInfo& esi)
+{
+  esi.d_notify = &d_eqNotify;
+  esi.d_name = "theory::ff::ee";
+  // TODO: not needed, I think
+  // esi.d_notifyNewClass = true;
+  // esi.d_notifyMerge = true;
+  // esi.d_notifyDisequal = true;
+  return true;
+}
+
+void TheoryFiniteFields::finishInit()
+{
+  Assert(d_equalityEngine != nullptr);
+
+  d_equalityEngine->addFunctionKind(Kind::FINITE_FIELD_MULT);
+  d_equalityEngine->addFunctionKind(Kind::FINITE_FIELD_NEG);
+  d_equalityEngine->addFunctionKind(Kind::FINITE_FIELD_ADD);
+}
+
+void TheoryFiniteFields::postCheck(Effort level)
+{
+  // TODO
+}
+
+void TheoryFiniteFields::notifyFact(TNode atom,
+                                    bool polarity,
+                                    TNode fact,
+                                    bool isInternal)
+{
+  // TODO
+}
+
+bool TheoryFiniteFields::collectModelValues(TheoryModel* m,
+                                            const std::set<Node>& termSet)
+{
+  // TODO
+  return true;
+}
+
+void TheoryFiniteFields::computeCareGraph()
+{
+  // TODO
+}
+
+TrustNode TheoryFiniteFields::explain(TNode node)
+{
+  // TODO
+  return TrustNode::null();
+}
+
+Node TheoryFiniteFields::getModelValue(TNode node)
+{
+  // TODO
+  return Node::null();
+}
+
+void TheoryFiniteFields::preRegisterTerm(TNode node)
+{
+  // TODO
+}
+
+TrustNode TheoryFiniteFields::ppRewrite(TNode n, std::vector<SkolemLemma>& lems)
+{
+  // TODO
+  return TrustNode::null();
+}
+
+Theory::PPAssertStatus TheoryFiniteFields::ppAssert(
+    TrustNode tin, TrustSubstitutionMap& outSubstitutions)
+{
+  TNode in = tin.getNode();
+  Trace("ff::pp") << "ff::ppAssert : " << in << std::endl;
+  Theory::PPAssertStatus status = Theory::PP_ASSERT_STATUS_UNSOLVED;
+  return status;
+}
+
+void TheoryFiniteFields::presolve()
+{
+  // TODO
+}
+
+bool TheoryFiniteFields::isEntailed(Node n, bool pol)
+{
+  // TODO
+  return false;
+}
+
+}  // namespace ff
+}  // namespace theory
+}  // namespace cvc5::internal