Finite Field support (#513)

* Symbols created, eval_ff_* to be done

* Added ff_plugin stub

* Registered ff plugin to mcsat

* Added further type support for FF type

* Added printing support for the ff type

* fixed warning

* actual missing error strings

* Parsing of (as (_ ff3 13) FF0) done

* reformat indentions

* reformat indentions

* Front-end parsing done

* mod_rba_buffer_t and TAG_ARITH_FF_BUFFER

* Code Formatting

* Finite Field term generation done

* Fixed print_elem in term_stack2.c

* Code Formatting

* Removed unnecessary todos

* Support arbitrary finite field size

* Some optimization for ff eq term generation

* Code Formatting and Warning fixes

* Added exceptions when ff is solved with non-mcsat context.

* fixed model_eval to handle finite field terms (and return unknown).

* Term manager update (added further ff code to term_manager)

* Added FF support to MCSAT preprocessor

* Added FF support to model printing

* fix

* Fixed printing and added value_ff_t.

* WIP: ff_plugin_new_term_notify

* Code Formatting fixes

* extracted lp_data handling from NRA plugin

* moved trail_variable_compare to trail and added lp_data in ff_plugin

* extracted poly_constraint from nra to lp_constraint_db

* fixed bug in non mcsat part

* using lp_data in explanation

* store term_t in lp_data instead of variable_t

* Consolidated libpoly_utils.c

* update nra_plugin_explain to support lp_data

* fixed context_config bug

* added mcsat only checks to makefile

* rework done: extracted lib_poly code from nra.

* rework done: extracted unit_info from nra and bv

* implementation of term_notify in ff done

* fixed Makefile whitespaces

* ff_poly_constraint_create implemented and minor improvements in the nra plugin.

* Build system update to use static libpoly for all builds when configured

* fixed term printing issue

* make lp_data_t finite field order aware

* throw exception on multiple ff orders

* extracted constraint_unit_info_demote

* Fixed typos

* minor code rework to enable the compiler to remove nra_plugin_check_assignment for release builds

* implemented pop/push and parts of propagate

* Typos and minor code fixes

* Added feasible_int_set_db files

* value_version_set done

* Renamed to ff_feasible_set_db

* Attach/Detach lp_int_ring_t in ff_feasible_set

* added ff_feasible_set_db to ff_plugin

* Typos and minor code fixes

* ffsat propagation done

* fixed two assertions

* value_hash_map made first and next record operate on const value.

* value_version_set fixed bugs

* Implemented ff_plugin_decide and some minor fixes

* Added calls to ff_feasible_set_db_pop/_push

* Using new libpoly features

* Fixed zero finding and some printing issues

* Typos and minor code fixes

* Implemented ff_plugin_explain_propagation and ff_plugin_explain_evaluation (taken from nra)

* Created functions for ff explain

* Typos and minor code fixes

* Prepared to plug explanation in

* Added explanation procedure

* Update ff_plugin_explain.c to avoid polynomial copying.

* Added plugin_ctx to lp_data

* fixed trace printing in ff_plugin_explain

* Fixed some stuff

* Fixed bugs in testing

* Moved some code, addes some asserts

* Some optimizations

* fixup

* fixed some bugs

* added last_reason_unsat conflict core minimization

* added gc sweep in lp_data.c

* added irreducible factor calculation to ff_plugin_explain.c

* added common factor removal

* added :dump-model option

* fixed ff model printing

* Typos and minor code fixes

* allowed ff-1

* added todos/comments/ideas

* Fixed warnings in release build

* added libpoly root finding

* fixed duplicated function

* fixed missing case in mcsat solver.c

* code format

* Fixed todos in explain

* added debugging code

* report out of memory if rb and lp don't agree

* Update Readme with special build steps

* Update readme

* Update readme

* Fixed compile warnings

* Fixed compile warnings in release build.

* Fixed typos

* rename int_queue_t size with capacity

* enhanced int_queue

* added queue for next decision

* Clear hint queue on conflict

* Added two queues (top and hint)

* fixed bug

* added solver hints in NRA

* model_interpolation questions

* model_interpolation does not perform request_top_decision

* Remove shortcut variables from the queue

* regression prints execution time

* nra_plugin.c hint only on real solution

* variable selection forces decision on hint

* fix random decision

* trace printing

* changed the gold of a model interpolant

* added option for test issue204.smt2

* Added ff regression tests

* Added hint queue in ff

* Added fintie field cases in substitution.c

* Added const to rational functions

* Made ff order (rational_t *mod) const

* Some code rework and fixed missing mod calculation in arith_ff_buffer_to_term

* renamed srs to lp_polynomial_subres in libpoly

* removed changes to build system (align with master)

* minor reworks in feasible_set_db and nra_plugin

* Integrated lp_feasibility_set_int in ff_plugin

* Added quickxplain to ff_feasible_set_db

* Added pointer to nra_plugin in feasible_set_db

* Changed the finite field logic from FF to FFA

* Code Formatting fixes

* Minor code cleanup

* Added comment

* Reverted README.md

* Removed broken runtime estimate from check.sh

* added more const

* Fixed false-positive warning in gcc

* Removed non-passing test

* Removed additional check code, since issue 520 is fixed

* Fixed typos

* Added missing FFA in arith framgemt_names

* run_test.sh: removed tailing } in filenames

* Adaptions to feedback, part 1

* Minor rework

* Adaptions to feedback, part 2

* Removed unused value_version_set

* Updated FFA error printing

* Update comments

* fixed test gold file

---------

Co-authored-by: Thomas Hader <thomas.hader@sri.com>
Co-authored-by: Thomas Hader <tom@hader.email>
Co-authored-by: Thomas Hader <thader@drei.at>

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,12 +349,16 @@ 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/scope_holder.c \
@@ -368,9 +372,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)
@@ -180,6 +181,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
@@ -236,6 +238,7 @@ static const bool fragment2iflag[NUM_ARITH_FRAGMENTS+1] = {
   true,   // NIA
   false,  // NRA
   true,   // NIRA
+  false,  // FFA
   false,  // no arithmetic
 };
 

src/api/smt_logic_codes.c

@@ -54,6 +54,7 @@ static const char * const smt_logic_names[NUM_SMT_LOGIC_NAMES] = {
   "AX",
   "BV",
   "BVLRA",
+  "FFA",
   "IDL",
   "LIA",
   "LIRA",
@@ -82,6 +83,7 @@ static const char * const smt_logic_names[NUM_SMT_LOGIC_NAMES] = {
   "QF_AX",
   "QF_BV",
   "QF_BVLRA",
+  "QF_FFA",
   "QF_IDL",
   "QF_LIA",
   "QF_LIRA",
@@ -142,6 +144,7 @@ static const smt_logic_t smt_code[NUM_SMT_LOGIC_NAMES] = {
   AUFNRA,
   AX,
   BV,
+  FFA,
   BVLRA,
   IDL,
   LIA,
@@ -171,6 +174,7 @@ static const smt_logic_t smt_code[NUM_SMT_LOGIC_NAMES] = {
   QF_AX,
   QF_BV,
   QF_BVLRA,
+  QF_FFA,
   QF_IDL,
   QF_LIA,
   QF_LIRA,
@@ -237,6 +241,7 @@ smt_logic_t smt_logic_code(const char *logic_name) {
  */
 static const char * const fragment_names[NUM_ARITH_FRAGMENTS] = {
   "IDL",
+  "FFA",
   "LIA",
   "LIRA",
   "LRA",
@@ -248,6 +253,7 @@ static const char * const fragment_names[NUM_ARITH_FRAGMENTS] = {
 
 static const arith_fragment_t fragment_code[NUM_ARITH_FRAGMENTS] = {
   ARITH_IDL,
+  ARITH_FFA,
   ARITH_LIA,
   ARITH_LIRA,
   ARITH_LRA,
@@ -290,6 +296,7 @@ static const uint8_t has_arrays[NUM_SMT_LOGICS] = {
 
   true,   // AX
   false,  // BV
+  false,  // FFA
   false,  // IDL
   false,  // LIA
   false,  // LRA
@@ -330,6 +337,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
@@ -376,6 +384,7 @@ static const uint8_t has_bv[NUM_SMT_LOGICS] = {
 
   false,  // AX
   true,   // BV
+  false,  // FFA
   false,  // IDL
   false,  // LIA
   false,  // LRA
@@ -416,6 +425,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
@@ -462,6 +472,7 @@ static const uint8_t has_quantifiers[NUM_SMT_LOGICS] = {
 
   true,   // AX
   true,   // BV
+  true,   // FFA
   true,   // IDL
   true,   // LIA
   true,   // LRA
@@ -502,6 +513,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
@@ -548,6 +560,7 @@ static const uint8_t has_uf[NUM_SMT_LOGICS] = {
 
   false,  // AX
   false,  // BV
+  false,  // FFA
   false,  // IDL
   false,  // LIA
   false,  // LRA
@@ -588,6 +601,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
@@ -634,6 +648,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
@@ -674,6 +689,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
@@ -761,6 +777,7 @@ static const smt_logic_t logic2qf[NUM_SMT_LOGICS] = {
    */
   QF_AX,
   QF_BV,
+  QF_FFA,
   QF_IDL,
   QF_LIA,
   QF_LRA,
@@ -804,6 +821,7 @@ static const smt_logic_t logic2qf[NUM_SMT_LOGICS] = {
    */
   QF_AX,
   QF_BV,
+  QF_FFA,
   QF_IDL,
   QF_LIA,
   QF_LRA,
@@ -863,6 +881,7 @@ static const bool is_official[NUM_SMT_LOGICS] = {
 
   false,  // AX
   true,   // BV
+  false,  // FFA
   false,  // IDL
   true,   // LIA
   true,   // LRA
@@ -903,6 +922,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
@@ -118,6 +119,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
@@ -195,6 +197,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);