Wrap MCSAT as a Nelson-Oppen theory solver in CDCL(T) architecture

src/Makefile

@@ -198,6 +198,7 @@ core_src_c := \
 	solvers/egraph/egraph_explanations.c \
 	solvers/egraph/egraph_utils.c \
 	solvers/egraph/theory_explanations.c \
+	solvers/mcsat_satellite.c \
 	solvers/floyd_warshall/dl_vartable.c \
 	solvers/floyd_warshall/idl_floyd_warshall.c \
 	solvers/floyd_warshall/rdl_floyd_warshall.c \

src/api/context_config.c

@@ -90,6 +90,7 @@ typedef enum ctx_config_key {
   CTX_CONFIG_KEY_ARRAY_SOLVER,
   CTX_CONFIG_KEY_BV_SOLVER,
   CTX_CONFIG_KEY_ARITH_SOLVER,
+  CTX_CONFIG_KEY_MCSAT_SUPPLEMENT,
   CTX_CONFIG_KEY_MODEL_INTERPOLATION,
   CTX_CONFIG_KEY_SAT_DELEGATE,
   CTX_CONFIG_KEY_SAT_DELEGATE_INCREMENTAL_MODE,
@@ -103,6 +104,7 @@ static const char *const config_key_names[NUM_CONFIG_KEYS] = {
   "arith-solver",
   "array-solver",
   "bv-solver",
+  "mcsat-supplement",
   "mode",
   "model-interpolation",
   "sat-delegate",
@@ -117,6 +119,7 @@ static const int32_t config_key[NUM_CONFIG_KEYS] = {
   CTX_CONFIG_KEY_ARITH_SOLVER,
   CTX_CONFIG_KEY_ARRAY_SOLVER,
   CTX_CONFIG_KEY_BV_SOLVER,
+  CTX_CONFIG_KEY_MCSAT_SUPPLEMENT,
   CTX_CONFIG_KEY_MODE,
   CTX_CONFIG_KEY_MODEL_INTERPOLATION,
   CTX_CONFIG_KEY_SAT_DELEGATE,
@@ -258,17 +261,20 @@ static const bool fragment2iflag[NUM_ARITH_FRAGMENTS+1] = {
 static const ctx_config_t default_config = {
   CTX_MODE_PUSHPOP,       // mode
   CTX_SOLVER_TYPE_DPLLT,  // DPLLT solver
+  false,                  // solver type set by user
   SMT_UNKNOWN,            // logic
   CTX_CONFIG_DEFAULT,     // uf
   CTX_CONFIG_DEFAULT,     // array
   CTX_CONFIG_DEFAULT,     // bv
   CTX_CONFIG_DEFAULT,     // arith
   ARITH_LIRA,             // fragment
+  false,                  // mcsat supplement
   false,                  // model interpolation
   SAT_DELEGATE_NONE,      // sat delegate
   SAT_DELEGATE_MODE_REBUILD, // sat delegate incremental mode (unused unless explicitly set)
   false,                  // sat delegate incremental mode set by user
   NULL,                   // trace tags
+  false,                  // mcsat supplement set by user
 };
 
 
@@ -385,6 +391,7 @@ int32_t config_set_field(ctx_config_t *config, const char *key, const char *valu
       r = -2;
     } else {
       config->solver_type = v;
+      config->solver_type_set = true;
     }
     break;
 
@@ -422,6 +429,14 @@ int32_t config_set_field(ctx_config_t *config, const char *key, const char *valu
       config->arith_config = v;
     }
     break;
+  case CTX_CONFIG_KEY_MCSAT_SUPPLEMENT:
+    v = parse_as_boolean(value, &config->mcsat_supplement);
+    if (v < 0) {
+      r = -2;
+    } else {
+      config->mcsat_supplement_set = true;
+    }
+    break;
   case CTX_CONFIG_KEY_MODEL_INTERPOLATION:
     v = parse_as_boolean(value, &config->model_interpolation);
     if (v < 0) {
@@ -604,6 +619,46 @@ static bool arch_is_supported(context_arch_t a) {
 #endif
 }
 
+/*
+ * Check whether architecture a has an E-graph coordinator.
+ */
+static bool arch_has_egraph(context_arch_t a) {
+  switch (a) {
+  case CTX_ARCH_EG:
+  case CTX_ARCH_EGFUN:
+  case CTX_ARCH_EGSPLX:
+  case CTX_ARCH_EGBV:
+  case CTX_ARCH_EGFUNSPLX:
+  case CTX_ARCH_EGFUNBV:
+  case CTX_ARCH_EGSPLXBV:
+  case CTX_ARCH_EGFUNSPLXBV:
+    return true;
+  default:
+    return false;
+  }
+}
+
+/*
+ * CDCL(T) architecture to use when a logic's default backend is MCSAT
+ * but the configuration requests a DPLL(T) top-level solver.
+ */
+static inline context_arch_t mcsat_supplement_arch_for_logic(smt_logic_t logic) {
+  (void) logic;
+  return CTX_ARCH_EGFUNSPLXBV;
+}
+
+static bool mcsat_supplement_is_supported(void) {
+#if HAVE_MCSAT
+  return true;
+#else
+  return false;
+#endif
+}
+
+static bool logic_supported_by_mcsat_config(smt_logic_t code) {
+  return code == SMT_ALL || !logic_has_quantifiers(code);
+}
+
 
 /*
  * Check whether config is valid (and supported by this version of Yices)
@@ -619,11 +674,12 @@ static bool arch_is_supported(context_arch_t a) {
  *  -2 if the config is valid but not currently supported
  *  -3 if the solver combination is valid but does not support the specified mode
  */
-int32_t decode_config(const ctx_config_t *config, smt_logic_t *logic, context_arch_t *arch, context_mode_t *mode, bool *iflag, bool *qflag) {
+int32_t decode_config(const ctx_config_t *config, smt_logic_t *logic, context_arch_t *arch, context_mode_t *mode, bool *iflag, bool *qflag, bool *mcsat_supplement) {
   smt_logic_t logic_code;
   int32_t a, r;
 
   r = 0; // default return code
+  *mcsat_supplement = false;
 
   logic_code = config->logic;
   if (logic_code != SMT_UNKNOWN) {
@@ -655,7 +711,26 @@ int32_t decode_config(const ctx_config_t *config, smt_logic_t *logic, context_ar
       }
     }
 
-    a = logic2arch[logic_code];
+    if (config->solver_type_set && config->solver_type == CTX_SOLVER_TYPE_MCSAT) {
+      if (!arch_is_supported(CTX_ARCH_MCSAT) || !logic_supported_by_mcsat_config(logic_code)) {
+        r = -2;
+        goto done;
+      }
+      a = CTX_ARCH_MCSAT;
+    } else {
+      a = logic2arch[logic_code];
+    }
+
+    if (config->solver_type_set && config->solver_type == CTX_SOLVER_TYPE_DPLLT && a == CTX_ARCH_MCSAT) {
+      if (config->mcsat_supplement_set && !config->mcsat_supplement) {
+        r = -1;
+        goto done;
+      }
+      a = mcsat_supplement_arch_for_logic(logic_code);
+      *mcsat_supplement = true;
+    } else if (config->mcsat_supplement) {
+      *mcsat_supplement = true;
+    }
     if (a < 0 || !arch_is_supported(a)) {
       // not supported
       r = -2;
@@ -668,7 +743,11 @@ int32_t decode_config(const ctx_config_t *config, smt_logic_t *logic, context_ar
       *mode = config->mode;
     }
 
-  } else if (config->solver_type == CTX_SOLVER_TYPE_MCSAT) {
+  } else if (config->solver_type_set && config->solver_type == CTX_SOLVER_TYPE_MCSAT) {
+    if (config->mcsat_supplement) {
+      r = -1;
+      goto done;
+    }
     if (arch_is_supported(CTX_ARCH_MCSAT)) {
       /*
        * MCSAT solver/no logic specified
@@ -699,6 +778,7 @@ int32_t decode_config(const ctx_config_t *config, smt_logic_t *logic, context_ar
       a = arch_add_bv(a);
     }
     a = arch_add_arith(a, config->arith_config);
+    *mcsat_supplement = config->mcsat_supplement;
 
     // a is either -1 or an architecture code
     if (a < 0) {
@@ -716,6 +796,14 @@ int32_t decode_config(const ctx_config_t *config, smt_logic_t *logic, context_ar
     }
   }
 
+  if (r == 0 && *mcsat_supplement) {
+    if (!mcsat_supplement_is_supported()) {
+      r = -2;
+    } else if (*arch == CTX_ARCH_MCSAT || !arch_has_egraph(*arch)) {
+      r = -1;
+    }
+  }
+
  done:
   return r;
 }

src/api/context_config.h

@@ -99,17 +99,20 @@ typedef enum solver_code {
 struct ctx_config_s {
   context_mode_t        mode;
   context_solver_type_t solver_type;
+  bool                  solver_type_set;
   smt_logic_t           logic;
   solver_code_t         uf_config;
   solver_code_t         array_config;
   solver_code_t         bv_config;
   solver_code_t         arith_config;
   arith_fragment_t      arith_fragment;
+  bool                  mcsat_supplement;
   bool                  model_interpolation;
   sat_delegate_t        sat_delegate;
   sat_delegate_incremental_mode_t sat_delegate_incremental_mode;
   bool                  sat_delegate_incremental_mode_set;
   char*                 trace_tags;
+  bool                  mcsat_supplement_set;
 };
 
 
@@ -149,7 +152,7 @@ extern int32_t config_set_logic(ctx_config_t *config, const char *logic);
  *
  * This can't be used to set config->logic: key must be one of "mode",
  * "arith-fragment", "uf-solver", "array-solver", "bv-solver",
- * "arith-solver" or "trace".
+ * "arith-solver", "mcsat-supplement", or "trace".
  *
  * Return code:
  *   -1 if the key is not recognized
@@ -188,7 +191,7 @@ extern int32_t config_set_field(ctx_config_t *config, const char *key, const cha
  *   0 if the config is valid and supported
  */
 extern int32_t decode_config(const ctx_config_t *config, smt_logic_t *logic, context_arch_t *arch,
-                             context_mode_t *mode, bool *iflag, bool *qflag);
+                             context_mode_t *mode, bool *iflag, bool *qflag, bool *mcsat_supplement);
 
 
 

src/api/search_parameters.c

@@ -102,6 +102,7 @@
 #define DEFAULT_USE_BOOL_DYN_ACK      false
 #define DEFAULT_USE_OPTIMISTIC_FCHECK true
 #define DEFAULT_AUX_EQ_RATIO          0.3
+#define DEFAULT_MCSAT_SUPPLEMENT_CHECK MCSAT_SUPPLEMENT_CHECK_BOTH
 
 
 /*
@@ -167,6 +168,7 @@ static const param_t default_settings = {
 
   DEFAULT_MAX_UPDATE_CONFLICTS,
   DEFAULT_MAX_EXTENSIONALITY,
+  DEFAULT_MCSAT_SUPPLEMENT_CHECK,
 };
 
 
@@ -224,9 +226,10 @@ typedef enum param_key {
   // array solver
   PARAM_MAX_UPDATE_CONFLICTS,
   PARAM_MAX_EXTENSIONALITY,
+  PARAM_MCSAT_SUPPLEMENT_CHECK,
 } param_key_t;
 
-#define NUM_PARAM_KEYS (PARAM_MAX_EXTENSIONALITY+1)
+#define NUM_PARAM_KEYS (PARAM_MCSAT_SUPPLEMENT_CHECK+1)
 
 // parameter names in lexicographic ordering
 static const char *const param_key_names[NUM_PARAM_KEYS] = {
@@ -253,6 +256,7 @@ static const char *const param_key_names[NUM_PARAM_KEYS] = {
   "max-extensionality",
   "max-interface-eqs",
   "max-update-conflicts",
+  "mcsat-supplement-check",
   "optimistic-final-check",
   "prop-threshold",
   "r-factor",
@@ -291,6 +295,7 @@ static const int32_t param_code[NUM_PARAM_KEYS] = {
   PARAM_MAX_EXTENSIONALITY,
   PARAM_MAX_INTERFACE_EQS,
   PARAM_MAX_UPDATE_CONFLICTS,
+  PARAM_MCSAT_SUPPLEMENT_CHECK,
   PARAM_OPTIMISTIC_FCHECK,
   PARAM_PROP_THRESHOLD,
   PARAM_R_FACTOR,
@@ -327,6 +332,19 @@ static const int32_t branching_code[NUM_BRANCHING_MODES] = {
   BRANCHING_THEORY,
 };
 
+/*
+ * Supplementary MCSAT checking modes (in lexicographic order)
+ */
+static const char * const mcsat_supplement_check_modes[NUM_MCSAT_SUPPLEMENT_CHECK_MODES] = {
+  "both",
+  "final-only",
+};
+
+static const int32_t mcsat_supplement_check_code[NUM_MCSAT_SUPPLEMENT_CHECK_MODES] = {
+  MCSAT_SUPPLEMENT_CHECK_BOTH,
+  MCSAT_SUPPLEMENT_CHECK_FINAL_ONLY,
+};
+
 /*
  * Names of delegate solvers (in lexicographic order)
  */
@@ -496,7 +514,6 @@ sat_delegate_t effective_sat_delegate_mode(sat_delegate_t config_delegate, const
 
 
 
-
 /****************
  *  FUNCTIONS   *
  ***************/
@@ -552,6 +569,28 @@ static int32_t set_branching_param(const char *value, branch_t *v) {
   return k;
 }
 
+/*
+ * Parse value as supplementary MCSAT check mode. Store the result in *v.
+ * - return 0 if this works
+ * - return -2 otherwise
+ */
+static int32_t set_mcsat_supplement_check_param(const char *value, mcsat_supplement_check_t *v) {
+  int32_t k;
+
+  k = parse_as_keyword(value, mcsat_supplement_check_modes, mcsat_supplement_check_code,
+                       NUM_MCSAT_SUPPLEMENT_CHECK_MODES);
+  assert(k >= 0 || k == -1);
+
+  if (k >= 0) {
+    assert(MCSAT_SUPPLEMENT_CHECK_BOTH <= k && k <= MCSAT_SUPPLEMENT_CHECK_FINAL_ONLY);
+    *v = (mcsat_supplement_check_t) k;
+    k = 0;
+  } else {
+    k = -2;
+  }
+  return k;
+}
+
 /*
  * Parse value as a SAT delegate mode. Store the result in *v
  * - return 0 if this works
@@ -870,6 +909,10 @@ int32_t params_set_field(param_t *parameters, const char *key, const char *value
     }
     break;
 
+  case PARAM_MCSAT_SUPPLEMENT_CHECK:
+    r = set_mcsat_supplement_check_param(value, &parameters->mcsat_supplement_check);
+    break;
+
   default:
     assert(k == -1);
     r = -1;

src/api/search_parameters.h

@@ -45,6 +45,17 @@ typedef enum {
 
 #define NUM_BRANCHING_MODES 6
 
+/*
+ * Supplementary MCSAT check mode (for CDCL(T) mode)
+ */
+typedef enum {
+  MCSAT_SUPPLEMENT_CHECK_BOTH,
+  MCSAT_SUPPLEMENT_CHECK_FINAL_ONLY,
+} mcsat_supplement_check_t;
+
+// keep in sync with mcsat_supplement_check_modes in search_parameters.c
+#define NUM_MCSAT_SUPPLEMENT_CHECK_MODES 2
+
 /*
  * Optional SAT delegate for QF_BV solving.
  */
@@ -212,6 +223,13 @@ struct param_s {
   uint32_t max_update_conflicts;
   uint32_t max_extensionality;
 
+  /*
+   * Supplementary MCSAT checks in CDCL(T)
+   * - BOTH: run in propagate and final_check
+   * - FINAL_ONLY: run in final_check only
+   */
+  mcsat_supplement_check_t mcsat_supplement_check;
+
 };