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)
@@ -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;