Finite Field support

Makefile.build

@@ -89,7 +89,7 @@ srcsubdirs = mt io terms utils solvers solvers/floyd_warshall \
     solvers/funs solvers/bv solvers/egraph solvers/cdcl solvers/simplex solvers/quant \
     parser_utils model api frontend frontend/common \
     frontend/smt1 frontend/yices frontend/smt2 context exists_forall \
-    mcsat mcsat/eq mcsat/weq mcsat/uf mcsat/bool mcsat/ite mcsat/nra mcsat/bv \
+    mcsat mcsat/eq mcsat/weq mcsat/uf mcsat/bool mcsat/ite mcsat/nra mcsat/ff mcsat/bv \
     mcsat/bv/explain mcsat/utils
 
 testdir = tests/unit

src/Makefile

@@ -349,14 +349,19 @@ mcsat_src_c := \
 	mcsat/model.c \
 	mcsat/trail.c \
 	mcsat/conflict.c \
+	mcsat/unit_info.c \
 	mcsat/gc.c \
 	mcsat/eq/equality_graph.c \
 	mcsat/eq/merge_queue.c \
 	mcsat/weq/weak_eq_graph.c \
 	mcsat/utils/int_mset.c \
 	mcsat/utils/int_lset.c \
+	mcsat/utils/lp_data.c \
+	mcsat/utils/lp_utils.c \
+	mcsat/utils/lp_constraint_db.c \
 	mcsat/utils/value_hash_map.c \
 	mcsat/utils/value_vector.c \
+	mcsat/utils/value_version_set.c \
 	mcsat/utils/scope_holder.c \
 	mcsat/utils/statistics.c \
 	mcsat/utils/substitution.c \
@@ -368,9 +373,13 @@ mcsat_src_c := \
 	mcsat/nra/nra_plugin.c \
 	mcsat/nra/nra_plugin_internal.c \
 	mcsat/nra/nra_plugin_explain.c \
-	mcsat/nra/libpoly_utils.c \
-	mcsat/nra/poly_constraint.c \
+	mcsat/nra/nra_libpoly.c \
 	mcsat/nra/feasible_set_db.c \
+	mcsat/ff/ff_plugin.c \
+	mcsat/ff/ff_plugin_internal.c \
+	mcsat/ff/ff_plugin_explain.c \
+	mcsat/ff/ff_libpoly.c \
+	mcsat/ff/ff_feasible_set_db.c \
 	mcsat/ite/ite_plugin.c \
 	mcsat/bv/bv_plugin.c \
 	mcsat/bv/bv_bdd_manager.c \

src/api/context_config.c

@@ -140,6 +140,7 @@ static const int32_t logic2arch[NUM_SMT_LOGICS] = {
 
   -1,                  // AX
   -1,                  // BV  (supported by EF)
+  -1,                  // FFA
   -1,                  // IDL (supported by EF)
   -1,                  // LIA (supported by EF)
   -1,                  // LRA (supported by EF)
@@ -179,6 +180,7 @@ static const int32_t logic2arch[NUM_SMT_LOGICS] = {
 
   CTX_ARCH_EGFUN,      // QF_AX
   CTX_ARCH_BV,         // QF_BV
+  CTX_ARCH_MCSAT,      // QF_FFA
   CTX_ARCH_SPLX,       // QF_IDL
   CTX_ARCH_SPLX,       // QF_LIA
   CTX_ARCH_SPLX,       // QF_LRA
@@ -234,6 +236,7 @@ static const bool fragment2iflag[NUM_ARITH_FRAGMENTS+1] = {
   true,   // NIA
   false,  // NRA
   true,   // NIRA
+  false,  // NFFA
   false,  // no arithmetic
 };
 

src/api/smt_logic_codes.c

@@ -53,6 +53,7 @@ static const char * const smt_logic_names[NUM_SMT_LOGIC_NAMES] = {
   "AUFNRA",
   "AX",
   "BV",
+  "FFA",
   "IDL",
   "LIA",
   "LIRA",
@@ -80,6 +81,7 @@ static const char * const smt_logic_names[NUM_SMT_LOGIC_NAMES] = {
   "QF_AUFNRA",
   "QF_AX",
   "QF_BV",
+  "QF_FFA",
   "QF_IDL",
   "QF_LIA",
   "QF_LIRA",
@@ -140,6 +142,7 @@ static const smt_logic_t smt_code[NUM_SMT_LOGIC_NAMES] = {
   AUFNRA,
   AX,
   BV,
+  FFA,
   IDL,
   LIA,
   LIRA,
@@ -167,6 +170,7 @@ static const smt_logic_t smt_code[NUM_SMT_LOGIC_NAMES] = {
   QF_AUFNRA,
   QF_AX,
   QF_BV,
+  QF_FFA,
   QF_IDL,
   QF_LIA,
   QF_LIRA,
@@ -286,6 +290,7 @@ static const uint8_t has_arrays[NUM_SMT_LOGICS] = {
 
   true,   // AX
   false,  // BV
+  false,  // FFA
   false,  // IDL
   false,  // LIA
   false,  // LRA
@@ -325,6 +330,7 @@ static const uint8_t has_arrays[NUM_SMT_LOGICS] = {
 
   true,   // QF_AX
   false,  // QF_BV
+  false,  // QF_FFA
   false,  // QF_IDL
   false,  // QF_LIA
   false,  // QF_LRA
@@ -370,6 +376,7 @@ static const uint8_t has_bv[NUM_SMT_LOGICS] = {
 
   false,  // AX
   true,   // BV
+  false,  // FFA
   false,  // IDL
   false,  // LIA
   false,  // LRA
@@ -409,6 +416,7 @@ static const uint8_t has_bv[NUM_SMT_LOGICS] = {
 
   false,  // QF_AX
   true,   // QF_BV
+  false,  // QF_FFA
   false,  // QF_IDL
   false,  // QF_LIA
   false,  // QF_LRA
@@ -454,6 +462,7 @@ static const uint8_t has_quantifiers[NUM_SMT_LOGICS] = {
 
   true,   // AX
   true,   // BV
+  true,   // FFA
   true,   // IDL
   true,   // LIA
   true,   // LRA
@@ -493,6 +502,7 @@ static const uint8_t has_quantifiers[NUM_SMT_LOGICS] = {
 
   false,  // QF_AX
   false,  // QF_BV
+  false,  // QF_FFA
   false,  // QF_IDL
   false,  // QF_LIA
   false,  // QF_LRA
@@ -538,6 +548,7 @@ static const uint8_t has_uf[NUM_SMT_LOGICS] = {
 
   false,  // AX
   false,  // BV
+  false,  // FFA
   false,  // IDL
   false,  // LIA
   false,  // LRA
@@ -577,6 +588,7 @@ static const uint8_t has_uf[NUM_SMT_LOGICS] = {
 
   false,  // QF_AX
   false,  // QF_BV
+  false,  // QF_FFA
   false,  // QF_IDL
   false,  // QF_LIA
   false,  // QF_LRA
@@ -622,6 +634,7 @@ static const uint8_t arith_frag[NUM_SMT_LOGICS] = {
 
   ARITH_NONE,   // AX
   ARITH_NONE,   // BV
+  ARITH_FFA,    // FFA
   ARITH_IDL,    // IDL
   ARITH_LIA,    // LIA
   ARITH_LRA,    // LRA
@@ -661,6 +674,7 @@ static const uint8_t arith_frag[NUM_SMT_LOGICS] = {
 
   ARITH_NONE,   // QF_AX
   ARITH_NONE,   // QF_BV
+  ARITH_FFA,    // QF_FFA
   ARITH_IDL,    // QF_IDL
   ARITH_LIA,    // QF_LIA
   ARITH_LRA,    // QF_LRA
@@ -747,6 +761,7 @@ static const smt_logic_t logic2qf[NUM_SMT_LOGICS] = {
    */
   QF_AX,
   QF_BV,
+  QF_FFA,
   QF_IDL,
   QF_LIA,
   QF_LRA,
@@ -789,6 +804,7 @@ static const smt_logic_t logic2qf[NUM_SMT_LOGICS] = {
    */
   QF_AX,
   QF_BV,
+  QF_FFA,
   QF_IDL,
   QF_LIA,
   QF_LRA,
@@ -847,6 +863,7 @@ static const bool is_official[NUM_SMT_LOGICS] = {
 
   false,  // AX
   true,   // BV
+  false,  // FFA
   false,  // IDL
   true,   // LIA
   true,   // LRA
@@ -886,6 +903,7 @@ static const bool is_official[NUM_SMT_LOGICS] = {
 
   true,   // QF_AX
   true,   // QF_BV
+  false,  // QF_FFA
   true,   // QF_IDL
   true,   // QF_LIA
   true,   // QF_LRA

src/api/smt_logic_codes.h

@@ -67,6 +67,7 @@ typedef enum smt_logic {
    */
   AX,          // arrays
   BV,          // bitvectors
+  FFA,         // finite fields
   IDL,         // integer difference logic
   LIA,         // linear integer arithmetic
   LRA,         // linear real arithmetic
@@ -115,6 +116,7 @@ typedef enum smt_logic {
    */
   QF_AX,       // arrays
   QF_BV,       // bitvectors
+  QF_FFA,      // finite fields
   QF_IDL,      // integer difference logic
   QF_LIA,      // linear integer arithmetic
   QF_LRA,      // linear real arithmetic
@@ -189,6 +191,7 @@ typedef enum arith_fragment {
   ARITH_NIA,   // non-linear integer arithmetic
   ARITH_NRA,   // non-linear real arithmetic
   ARITH_NIRA,  // non-linear mixed arithmetic
+  ARITH_FFA,   // finite field arithmetic
   ARITH_NONE,  // no arithmetic
 } arith_fragment_t;
 

src/api/yices_api.c

@@ -1577,6 +1577,17 @@ static inline void type_vector_push(type_vector_t *v, type_t tau) {
  * Otherwise they return false and set the error code and diagnostic data.
  */
 
+// Check whether n (as mpz) is positive
+static bool check_positive_mpz(mpz_t n) {
+  if (mpz_sgn(n) != 1) {
+    error_report_t *error = get_yices_error();
+    error->code = POS_INT_REQUIRED;
+    error->badval = mpz_fits_slong_p(n) ? mpz_get_si(n) : -1;
+    return false;
+  }
+  return true;
+}
+
 // Check whether n is positive
 static bool check_positive(uint32_t n) {
   if (n == 0) {
@@ -1912,6 +1923,21 @@ static bool check_integer_term(term_manager_t *mngr, term_t t) {
 }
 #endif
 
+// Check whether t is a finitefield term, t must be valid.
+static bool check_arith_ff_term(term_manager_t *mngr, term_t t) {
+  term_table_t *tbl;
+
+  tbl = term_manager_get_terms(mngr);
+
+  if (! is_finitefield_term(tbl, t)) {
+    error_report_t *error = get_yices_error();
+    error->code = ARITHTERM_REQUIRED;
+    error->term1 = t;
+    return false;
+  }
+  return true;
+}
+
 // Check whether t is a real term, t must be valid.
 static bool check_real_term(term_manager_t *mngr, term_t t) {
   term_table_t *tbl;
@@ -2740,6 +2766,7 @@ static bool check_elim_vars(term_manager_t *mngr, uint32_t n, const term_t *var)
     case BOOL_TYPE:
     case INT_TYPE:
     case REAL_TYPE:
+    case FF_TYPE:
     case BITVECTOR_TYPE:
     case SCALAR_TYPE:
       break;
@@ -2840,6 +2867,16 @@ type_t _o_yices_bv_type(uint32_t size) {
   return bv_type(__yices_globals.types, size);
 }
 
+type_t _o_yices_ff_type(mpz_t order) {
+  if (! check_positive_mpz(order)) {
+    return NULL_TYPE;
+  }
+  if (! mpz_probab_prime_p(order, 18)) {
+    return NULL_TYPE;
+  }
+  return ff_type(__yices_globals.types, order);
+}
+
 EXPORTED type_t yices_new_uninterpreted_type(void) {
   MT_PROTECT(type_t, __yices_globals.lock, _o_yices_new_uninterpreted_type());
 }
@@ -7192,6 +7229,19 @@ int32_t _o_yices_rational_const_value(term_t t, mpq_t q) {
   return 0;
 }
 
+EXPORTED int32_t yices_finitefield_const_value(term_t t, mpz_t z) {
+  MT_PROTECT(int32_t,  __yices_globals.lock, _o_yices_finitefield_const_value(t, z));
+}
+
+int32_t _o_yices_finitefield_const_value(term_t t, mpz_t z) {
+  if (! check_good_term(__yices_globals.manager, t) ||
+      ! check_constructor(__yices_globals.terms, t, YICES_ARITH_FF_CONSTANT)) {
+    return -1;
+  }
+  arith_ff_const_value(__yices_globals.terms, t, z);
+  return 0;
+}
+
 
 /*
  * Components of a sum t
@@ -7207,6 +7257,7 @@ EXPORTED int32_t yices_sum_component(term_t t, int32_t i, mpq_t coeff, term_t *t
 int32_t _o_yices_sum_component(term_t t, int32_t i, mpq_t coeff, term_t *term) {
   if (! check_good_term(__yices_globals.manager, t) ||
       ! check_constructor(__yices_globals.terms, t, YICES_ARITH_SUM) ||
+      ! check_constructor(__yices_globals.terms, t, YICES_ARITH_FF_SUM) ||
       ! check_child_idx(__yices_globals.terms, t, i)) {
     return -1;
   }
@@ -7283,6 +7334,14 @@ term_t arith_buffer_get_lt0_atom(rba_buffer_t *b) {
   return mk_arith_lt0(__yices_globals.manager, b);
 }
 
+term_t arith_ff_buffer_get_term(rba_buffer_t *b, rational_t *mod) {
+  return mk_arith_ff_term(__yices_globals.manager, b, mod);
+}
+
+term_t arith_ff_buffer_get_eq0_atom(rba_buffer_t *b, rational_t *mod) {
+  return mk_arith_ff_eq0(__yices_globals.manager, b, mod);
+}
+
 term_t bvlogic_buffer_get_term(bvlogic_buffer_t *b) {
   return mk_bvlogic_term(__yices_globals.manager, b);
 }
@@ -7309,6 +7368,10 @@ term_t yices_bvconst64_term(uint32_t n, uint64_t c) {
   return bv64_constant(__yices_globals.terms, n, c);
 }
 
+term_t yices_ffconst_term(rational_t *q, rational_t *mod) {
+  return arith_ff_constant(__yices_globals.terms, q, mod);
+}
+
 term_t yices_rational_term(rational_t *q) {
   return arith_constant(__yices_globals.terms, q);
 }
@@ -7351,6 +7414,21 @@ bool yices_check_arith_term(term_t t) {
   return check_good_term(__yices_globals.manager, t) && check_arith_term(__yices_globals.manager, t);
 }
 
+/*
+ * Check whether t is a valid finite field arithmetic term
+ * - if not set the internal error report:
+ *
+ * If t is not a valid term:
+ *   code = INVALID_TERM
+ *   term1 = t
+ *   index = -1
+ * If t is not an arithmetic term;
+ *   code = ARITHTERM_REQUIRED
+ *   term1 = t
+ */
+bool yices_check_arith_ff_term(term_t t) {
+  return check_good_term(__yices_globals.manager, t) && check_arith_ff_term(__yices_globals.manager, t);
+}
 
 /*
  * Check for degree overflow in the product (b * t)
@@ -7369,7 +7447,7 @@ bool yices_check_mul_term(rba_buffer_t *b, term_t t) {
 
   tbl = __yices_globals.terms;
 
-  assert(good_term(tbl, t) && is_arithmetic_term(tbl, t));
+  assert(good_term(tbl, t) && (is_arithmetic_term(tbl, t) || is_finitefield_term(tbl, t)));
 
   d1 = rba_buffer_degree(b);
   d2 = term_degree(tbl, t);