25686639376

Committed 11 May 2026 05:36PM UTC coverage: 67.164% (-0.09%) from 67.254%

Build # 25686639376

Build Type

push

github

Committed by

disteph

Commit Message

Commit supported by Codex/GPT5.5 and Windsurf/Opus4.7: support Floyd-Warshall E-graph satellites

Add one-shot E-graph satellite support for the IDL and RDL Floyd-Warshall solvers, including tagged atom pointers, E-graph assertion queues, equality-edge explanations, model reconciliation hooks, and context architectures for EG+IFW/RFW with optional BV.

Update API/frontend config selection and documentation, and add API regression coverage for SAT-level FW atoms, logic-config overrides, BV-guarded equality, and disequality interface lemmas.

Coverage Stats

297 of 672 new or added lines in 11 files covered. (44.2%)

9 existing lines in 4 files now uncovered.

85516 of 127324 relevant lines covered (67.16%)

1619036.4 hits per line

Source File
Press 'n' to go to next uncovered line, 'b' for previous

66.08

/src/api/context_config.c

/*
 * This file is part of the Yices SMT Solver.
 * Copyright (C) 2017 SRI International.
 *
 * Yices is free software: you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation, either version 3 of the License, or
 * (at your option) any later version.
 *
 * Yices is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with Yices.  If not, see <http://www.gnu.org/licenses/>.
 */

/*
 * OBJECT TO STORE CONTEXT CONFIGURATIONS
 */

#include <stdbool.h>
#include <assert.h>

#include "api/context_config.h"
#include "api/search_parameters.h"
#include "utils/memalloc.h"
#include "utils/string_utils.h"


/*
 * Mapping from strings to context modes (cf. string_utils.h)
 */
static const char * const mode_names[NUM_MODES] = {
  "interactive",
  "multi-checks",
  "one-shot",
  "push-pop",
};

static const int32_t mode[NUM_MODES] = {
  CTX_MODE_INTERACTIVE,
  CTX_MODE_MULTICHECKS,
  CTX_MODE_ONECHECK,
  CTX_MODE_PUSHPOP,
};

static const char * const solver_type_names[NUM_SOLVER_TYPES] = {
  "dpllt",
  "mcsat"
};

static const int32_t solver_type[NUM_SOLVER_TYPES] = {
  CTX_SOLVER_TYPE_DPLLT,
  CTX_SOLVER_TYPE_MCSAT
};

/*
 * Solver codes
 */
static const char * const solver_code_names[NUM_SOLVER_CODES] = {
  "auto",
  "default",
  "ifw",
  "none",
  "rfw",
  "simplex",
};

static const int32_t solver_code[NUM_SOLVER_CODES] = {
  CTX_CONFIG_AUTO,
  CTX_CONFIG_DEFAULT,
  CTX_CONFIG_ARITH_IFW,
  CTX_CONFIG_NONE,
  CTX_CONFIG_ARITH_RFW,
  CTX_CONFIG_ARITH_SIMPLEX,
};


/*
 * Descriptor fields (other than "logic")
 */
typedef enum ctx_config_key {
  CTX_CONFIG_KEY_MODE,
  CTX_CONFIG_KEY_SOLVER_TYPE,
  CTX_CONFIG_KEY_TRACE_TAGS,
  CTX_CONFIG_KEY_ARITH_FRAGMENT,
  CTX_CONFIG_KEY_UF_SOLVER,
  CTX_CONFIG_KEY_ARRAY_SOLVER,
  CTX_CONFIG_KEY_BV_SOLVER,
  CTX_CONFIG_KEY_ARITH_SOLVER,
  CTX_CONFIG_KEY_MODEL_INTERPOLATION,
  CTX_CONFIG_KEY_SAT_DELEGATE,
  CTX_CONFIG_KEY_SAT_DELEGATE_SELECTOR_FRAMES,
} ctx_config_key_t;

#define NUM_CONFIG_KEYS (CTX_CONFIG_KEY_SAT_DELEGATE_SELECTOR_FRAMES+1)


static const char *const config_key_names[NUM_CONFIG_KEYS] = {
  "arith-fragment",
  "arith-solver",
  "array-solver",
  "bv-solver",
  "mode",
  "model-interpolation",
  "sat-delegate",
  "sat-delegate-selector-frames",
  "solver-type",
  "trace",
  "uf-solver",
};

static const int32_t config_key[NUM_CONFIG_KEYS] = {
  CTX_CONFIG_KEY_ARITH_FRAGMENT,
  CTX_CONFIG_KEY_ARITH_SOLVER,
  CTX_CONFIG_KEY_ARRAY_SOLVER,
  CTX_CONFIG_KEY_BV_SOLVER,
  CTX_CONFIG_KEY_MODE,
  CTX_CONFIG_KEY_MODEL_INTERPOLATION,
  CTX_CONFIG_KEY_SAT_DELEGATE,
  CTX_CONFIG_KEY_SAT_DELEGATE_SELECTOR_FRAMES,
  CTX_CONFIG_KEY_SOLVER_TYPE,
  CTX_CONFIG_KEY_TRACE_TAGS,
  CTX_CONFIG_KEY_UF_SOLVER,
};

/*
 * CONTEXT SETTING FOR A GIVEN LOGIC CODE
 */

/*
 * Conversion of SMT logic code to a default architecture code
 * -1 means not supported
 *
 * We don't use AUTO_IDL, AUTO_RDL, IFW or RFW here since
 * the Floyd-Warshall solvers don't support all use modes.
 *
 * IMPORTANT: this array is used by the API in config_for_logic.
 */
static const int32_t logic2arch[NUM_SMT_LOGICS] = {
  CTX_ARCH_NOSOLVERS,  // NONE

  -1,                  // AX
  -1,                  // BV  (supported by EF)
  -1,                  // FFA
  -1,                  // IDL (supported by EF)
  -1,                  // LIA (supported by EF)
  -1,                  // LRA (supported by EF)
  -1,                  // LIRA
  -1,                  // NIA
  -1,                  // NRA
  -1,                  // NIRA
  -1,                  // RDL
  -1,                  // UF
  -1,                  // ABV
  -1,                  // ALIA
  -1,                  // ALRA
  -1,                  // ALIRA
  -1,                  // ANIA
  -1,                  // ANRA
  -1,                  // ANIRA
  -1,                  // AUF
  -1,                  // BVLRA
  -1,                  // UFBV
  -1,                  // UFBVLIA
  -1,                  // UFIDL
  -1,                  // UFLIA
  -1,                  // UFLRA
  -1,                  // UFLIRA
  -1,                  // UFNIA
  -1,                  // UFNRA
  -1,                  // UFNIRA
  -1,                  // UFRDL
  -1,                  // AUFBV
  -1,                  // AUFBVLIA
  -1,                  // AUFBVNIA
  -1,                  // AUFLIA
  -1,                  // AUFLRA
  -1,                  // AUFLIRA
  -1,                  // AUFNIA
  -1,                  // AUFNRA
  -1,                  // AUFNIRA

  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
  CTX_ARCH_SPLX,       // QF_LIRA
  CTX_ARCH_MCSAT,      // QF_NIA
  CTX_ARCH_MCSAT,      // QF_NRA
  CTX_ARCH_MCSAT,      // QF_NIRA
  CTX_ARCH_SPLX,       // QF_RDL
  CTX_ARCH_EG,         // QF_UF
  CTX_ARCH_EGFUNBV,    // QF_ABV
  CTX_ARCH_EGFUNSPLX,  // QF_ALIA
  CTX_ARCH_EGFUNSPLX,  // QF_ALRA
  CTX_ARCH_EGFUNSPLX,  // QF_ALIRA
  CTX_ARCH_MCSAT,      // QF_ANIA
  CTX_ARCH_MCSAT,      // QF_ANRA
  CTX_ARCH_MCSAT,      // QF_ANIRA
  CTX_ARCH_EGFUN,      // QF_AUF
  CTX_ARCH_EGSPLXBV,   // QF_BVLRA
  CTX_ARCH_EGBV,       // QF_UFBV
  CTX_ARCH_EGSPLXBV,   // QF_UFBVLIA

  CTX_ARCH_EGSPLX,     // QF_UFIDL
  CTX_ARCH_EGSPLX,     // QF_UFLIA
  CTX_ARCH_EGSPLX,     // QF_UFLRA
  CTX_ARCH_EGSPLX,     // QF_UFLIRA
  CTX_ARCH_MCSAT,      // QF_UFNIA
  CTX_ARCH_MCSAT,      // QF_UFNRA
  CTX_ARCH_MCSAT,      // QF_UFNIRA
  CTX_ARCH_EGSPLX,     // QF_UFRDL
  CTX_ARCH_EGFUNBV,    // QF_AUFBV
  CTX_ARCH_EGFUNSPLXBV, // QF_AUFBVLIA
  CTX_ARCH_MCSAT,      // QF_AUFBVNIA
  CTX_ARCH_EGFUNSPLX,  // QF_AUFLIA
  CTX_ARCH_EGFUNSPLX,  // QF_AUFLRA
  CTX_ARCH_EGFUNSPLX,  // QF_AUFLIRA
  CTX_ARCH_MCSAT,      // QF_AUFNIA
  CTX_ARCH_MCSAT,      // QF_AUFNRA
  CTX_ARCH_MCSAT,      // QF_AUFNIRA

  CTX_ARCH_EGFUNSPLXBV,  // ALL interpreted as QF_AUFLIRA + QF_BV
};



/*
 * WHICH ARITHMETIC FRAGMENTS REQUIRE THE DIOPHANTINE SUBSOLVER
 */
static const bool fragment2iflag[NUM_ARITH_FRAGMENTS+1] = {
  false,  // IDL
  false,  // RDL
  true,   // LIA
  false,  // LRA
  true,   // LIRA
  true,   // NIA
  false,  // NRA
  true,   // NIRA
  false,  // FFA
  false,  // no arithmetic
};


/*
 * Default configuration:
 * - enable PUSH/POP
 * - solver type = DPLL(T)
 * - no logic specified
 * - arith fragment = LIRA
 * - all solvers set to defaults
 */
static const ctx_config_t default_config = {
  CTX_MODE_PUSHPOP,       // mode
  CTX_SOLVER_TYPE_DPLLT,  // DPLLT solver
  SMT_UNKNOWN,            // logic
  CTX_CONFIG_DEFAULT,     // uf
  CTX_CONFIG_DEFAULT,     // array
  CTX_CONFIG_DEFAULT,     // bv
  CTX_CONFIG_DEFAULT,     // arith
  ARITH_LIRA,             // fragment
  false,                  // model interpolation
  SAT_DELEGATE_NONE,      // sat delegate
  false,                  // sat delegate selector frames
  NULL,                   // trace tags
};





/*
 * DIRECT CONFIGURATION
 */
int32_t arch_for_logic(smt_logic_t code) {
  assert(code != SMT_UNKNOWN);
  return logic2arch[code];
}

bool iflag_for_logic(smt_logic_t code) {
  assert(code != SMT_UNKNOWN);
  return fragment2iflag[arith_fragment(code)];
}



/*
 * CONFIG OBJECT
 */

/*
 * Initialize config to the default configuration
 */
void init_config_to_defaults(ctx_config_t *config) {
  *config = default_config;
}



/*
 * Set a default configuration to support the given logic
 * - return -1 if the logic name is not recognized
 * - return -2 if we don't support the logic yet
 * - return 0 otherwise
 *
 * If the function returns 0, the logic field is updated.
 * All other fields are left unchanged.
 */
int32_t config_set_logic(ctx_config_t *config, const char *logic) {
  smt_logic_t code;
  int32_t r;

  code = smt_logic_code(logic);
  if (code == SMT_UNKNOWN) {
    r = -1;
  } else if (logic2arch[code] < 0) {
    r = -2;
  } else {
    config->logic = (smt_logic_t) code;
    r = 0;
  }

  return r;
}


/*
 * Convert value to a solver
 */
static int32_t set_solver_code(const char *value, solver_code_t *dest) {
  int32_t v, r;

  v = parse_as_keyword(value, solver_code_names, solver_code, NUM_SOLVER_CODES);
  if (v < 0) {
    r = -2;
  } else if (v >= CTX_CONFIG_AUTO) {
    r = -3;
  } else {
    assert(v == CTX_CONFIG_DEFAULT || v == CTX_CONFIG_NONE);
    *dest = (solver_code_t) v;
    r = 0;
  }

  return r;
}


/*
 * Set an individual field in config
 * - key = field name
 * - value = value for that field
 *
 * Return code:
 *   -1 if the key is not recognized
 *   -2 if the value is not recognized
 *   -3 if the value is not valid for the key
 *    0 otherwise
 */
int32_t config_set_field(ctx_config_t *config, const char *key, const char *value) {
  int32_t k, v, r;
  arith_fragment_t arith;

  r = 0; // return code

  k = parse_as_keyword(key, config_key_names, config_key, NUM_CONFIG_KEYS);
  switch (k) {
  case CTX_CONFIG_KEY_MODE:
    v = parse_as_keyword(value, mode_names, mode, NUM_MODES);
    if (v < 0) {
      r = -2;
    } else {
      config->mode = v;
    }
    break;

  case CTX_CONFIG_KEY_SOLVER_TYPE:
    v = parse_as_keyword(value, solver_type_names, solver_type, NUM_SOLVER_TYPES);
    if (v < 0) {
      r = -2;
    } else {
      config->solver_type = v;
    }
    break;

  case CTX_CONFIG_KEY_TRACE_TAGS:
    config->trace_tags = safe_strdup(value);
    break;

  case CTX_CONFIG_KEY_ARITH_FRAGMENT:
    arith = arith_fragment_code(value);
    if (arith == ARITH_NONE) {
      r = -2;
    } else {
      config->arith_fragment = arith;
    }
    break;

  case CTX_CONFIG_KEY_UF_SOLVER:
    r = set_solver_code(value, &config->uf_config);
    break;

  case CTX_CONFIG_KEY_ARRAY_SOLVER:
    r = set_solver_code(value, &config->array_config);
    break;

  case CTX_CONFIG_KEY_BV_SOLVER:
    r = set_solver_code(value, &config->bv_config);
    break;

  case CTX_CONFIG_KEY_ARITH_SOLVER:
    v = parse_as_keyword(value, solver_code_names, solver_code, NUM_SOLVER_CODES);
    if (v < 0) {
      r = -2;
    } else {
      assert(0 <= v && v <= NUM_SOLVER_CODES);
      config->arith_config = v;
    }
    break;
  case CTX_CONFIG_KEY_MODEL_INTERPOLATION:
    v = parse_as_boolean(value, &config->model_interpolation);
    if (v < 0) {
      r = -2;
    }
    break;
  case CTX_CONFIG_KEY_SAT_DELEGATE:
    if (parse_sat_delegate(value, &config->sat_delegate) < 0) {
      r = -2;
    }
    break;
  case CTX_CONFIG_KEY_SAT_DELEGATE_SELECTOR_FRAMES:
    v = parse_as_boolean(value, &config->sat_delegate_selector_frames);
    if (v < 0) {
      r = -2;
    }
    break;
  default:
    assert(k == -1);
    r = -1;
    break;
  }

  return r;
}



/*
 * Auxiliary functions to build architecture codes incrementally
 * - each function takes an integer a: a is either a valid architecture
 *   code or -1
 * - then the function adds a new solver component to a: this results
 *   in either a new valid code or -1 if the new component is not compatible with a.
 *
 * Important: we assume that the components are added in the following
 * order: egraph, array solver, bitvector solver, arithmetic solver
 */
static inline int32_t arch_add_egraph(int32_t a) {
  if (a == CTX_ARCH_NOSOLVERS) {
    a = CTX_ARCH_EG;
  } else {
    a = -1;
  }
  return a;
}

static int32_t arch_add_array(int32_t a) {
  if (a == CTX_ARCH_EG || a == CTX_ARCH_NOSOLVERS) {
    a = CTX_ARCH_EGFUN; // array requires egraph so we add both implicitly
  } else {
    a = -1;
  }
  return a;
}

static int32_t arch_add_bv(int32_t a) {
  switch (a) {
  case CTX_ARCH_NOSOLVERS:
    a = CTX_ARCH_BV;
    break;

  case CTX_ARCH_EG:
    a = CTX_ARCH_EGBV;
    break;

  case CTX_ARCH_EGFUN:
    a = CTX_ARCH_EGFUNBV;
    break;

  case CTX_ARCH_SPLX:
    a = CTX_ARCH_EGSPLXBV;
    break;

  case CTX_ARCH_EGIFW:
    a = CTX_ARCH_EGBVIFW;
    break;

  case CTX_ARCH_EGRFW:
    a = CTX_ARCH_EGBVRFW;
    break;

  default:
    a = -1;
    break;
  }

  return a;
}

// add the simplex solver
static int32_t arch_add_simplex(int32_t a) {
  switch (a) {
  case CTX_ARCH_NOSOLVERS:
    a = CTX_ARCH_SPLX;
    break;

  case CTX_ARCH_BV:
    a = CTX_ARCH_EGSPLXBV;
    break;

  case CTX_ARCH_EG:
    a = CTX_ARCH_EGSPLX;
    break;

  case CTX_ARCH_EGFUN:
    a = CTX_ARCH_EGFUNSPLX;
    break;

  case CTX_ARCH_EGBV:
    a = CTX_ARCH_EGSPLXBV;
    break;

  case CTX_ARCH_EGFUNBV:
    a = CTX_ARCH_EGFUNSPLXBV;
    break;

  default:
    a = -1;
    break;
  }

  return a;
}

// add a Floyd-Warshall solver
static int32_t arch_add_ifw(int32_t a) {
  switch (a) {
  case CTX_ARCH_NOSOLVERS:
    a = CTX_ARCH_IFW;
    break;

  case CTX_ARCH_EG:
    a = CTX_ARCH_EGIFW;
    break;

  case CTX_ARCH_BV:
  case CTX_ARCH_EGBV:
    a = CTX_ARCH_EGBVIFW;
    break;

  default:
    a = -1;
    break;
  }
  return a;
}

static int32_t arch_add_rfw(int32_t a) {
  switch (a) {
  case CTX_ARCH_NOSOLVERS:
    a = CTX_ARCH_RFW;
    break;

  case CTX_ARCH_EG:
    a = CTX_ARCH_EGRFW;
    break;

  case CTX_ARCH_BV:
  case CTX_ARCH_EGBV:
    a = CTX_ARCH_EGBVRFW;
    break;

  default:
    a = -1;
    break;
  }
  return a;
}


// add solver identified by code c to a
static int32_t arch_add_arith(int32_t a, solver_code_t c) {
  switch (c) {
  case CTX_CONFIG_NONE:  // no arithmetic solver
    break;

  case CTX_CONFIG_DEFAULT:  // simplex is the default
  case CTX_CONFIG_AUTO:     // auto = simplex here too
  case CTX_CONFIG_ARITH_SIMPLEX:
    a = arch_add_simplex(a);
    break;

  case CTX_CONFIG_ARITH_IFW:
    a = arch_add_ifw(a);
    break;

  case CTX_CONFIG_ARITH_RFW:
    a = arch_add_rfw(a);
    break;
  }
  return a;
}


/*
 * Check whether the architecture code a is compatible with mode
 * - current restriction: IFW and RFW don't support PUSH/POP or MULTIPLE CHECKS
 */
static bool arch_supports_mode(context_arch_t a, context_mode_t mode) {
  return (a != CTX_ARCH_IFW && a != CTX_ARCH_RFW &&
          a != CTX_ARCH_EGIFW && a != CTX_ARCH_EGRFW &&
          a != CTX_ARCH_EGBVIFW && a != CTX_ARCH_EGBVRFW) || mode == CTX_MODE_ONECHECK;
}


/*
 * Check whether the architecture is supported.
 */
static bool arch_is_supported(context_arch_t a) {
#if HAVE_MCSAT
  return true; // all architectures are supported
#else
  return a != CTX_ARCH_MCSAT;
#endif
}


/*
 * Architecture selected by an explicit arithmetic-solver setting in a
 * configuration that also specifies a logic.
 */
static int32_t arch_for_logic_and_arith_config(smt_logic_t logic_code, solver_code_t arith_config) {
  switch (arith_config) {
  case CTX_CONFIG_ARITH_IFW:
    if (logic_code == QF_IDL) {
      return CTX_ARCH_IFW;
    } else if (logic_code == QF_UFIDL) {
      return CTX_ARCH_EGIFW;
    }
    return -1;

  case CTX_CONFIG_ARITH_RFW:
    if (logic_code == QF_RDL) {
      return CTX_ARCH_RFW;
    } else if (logic_code == QF_UFRDL) {
      return CTX_ARCH_EGRFW;
    }
    return -1;

  default:
    return logic2arch[logic_code];
  }
}


/*
 * Check whether config is valid (and supported by this version of Yices)
 * and convert it to a tuple (arch, mode, iflag, qflag)
 * - arch = architecture code as defined in context.h
 * - mode = one of the context's modes
 * - iflag = true if the integer solver (in simplex) is required
 * - qflag = true if support for quantifiers is required
 *
 * Return code:
 *   0 if the config is valid and supported
 *  -1 if the config is invalid
 *  -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) {
  smt_logic_t logic_code;
  int32_t a, r;

  r = 0; // default return code

  logic_code = config->logic;
  if (logic_code != SMT_UNKNOWN) {
    /*
     * The intended logic is specified
     */
    assert(0 <= logic_code && logic_code < NUM_SMT_LOGICS);

    /*
     * Special case: difference logic + mode = ONECHECK + arith_config == AUTO
     */
    if (config->arith_config == CTX_CONFIG_AUTO && config->mode == CTX_MODE_ONECHECK) {
      if (logic_code == QF_IDL) {
        *logic = QF_IDL;
        *arch = CTX_ARCH_AUTO_IDL;
        *mode = CTX_MODE_ONECHECK;
        *iflag = false;
        *qflag = false;
        goto done;
      }

      if (logic_code == QF_RDL) {
        *logic = QF_RDL;
        *arch = CTX_ARCH_AUTO_RDL;
        *mode = CTX_MODE_ONECHECK;
        *iflag = false;
        *qflag = false;
        goto done;
      }
    }

    a = arch_for_logic_and_arith_config(logic_code, config->arith_config);
    if (a < 0) {
      // invalid combination of logic and arithmetic solver
      r = -1;
    } else if (!arch_is_supported(a)) {
      // not supported
      r = -2;
    } else if (!arch_supports_mode(a, config->mode)) {
      // mode is not supported by the solvers
      r = -3;
    } else {
      // good configuration
      *logic = logic_code;
      *arch = (context_arch_t) a;
      *iflag = iflag_for_logic(logic_code);
      *qflag = qflag_for_logic(logic_code);
      *mode = config->mode;
    }

  } else if (config->solver_type == CTX_SOLVER_TYPE_MCSAT) {
    if (arch_is_supported(CTX_ARCH_MCSAT)) {
      /*
       * MCSAT solver/no logic specified
       */
      *logic = SMT_UNKNOWN;
      *arch = CTX_ARCH_MCSAT;
      *mode = CTX_MODE_PUSHPOP;
      *iflag = false;
      *qflag = false;
    } else {
      // not compiled with MCSAT support so this is not supported
      r = -2;
    }

  } else {
    /*
     * No logic specified.
     */

    a = CTX_ARCH_NOSOLVERS;
    if (config->uf_config == CTX_CONFIG_DEFAULT) {
      a = arch_add_egraph(a);
    }
    if (config->array_config == CTX_CONFIG_DEFAULT) {
      a = arch_add_array(a);
    }
    if (config->bv_config == CTX_CONFIG_DEFAULT) {
      a = arch_add_bv(a);
    }
    a = arch_add_arith(a, config->arith_config);

    // a is either -1 or an architecture code
    if (a < 0) {
      r = -1; // invalid combination of solvers
    } else if (arch_supports_mode(a, config->mode)) {
      // good configuration
      *logic = SMT_UNKNOWN;
      *arch = (context_arch_t) a;
      *iflag = fragment2iflag[config->arith_fragment];
      *qflag = false;
      *mode = config->mode;
    } else {
      // mode is not supported by the solvers
      r = -3;
    }
  }

 done:
  return r;
}


/*
 * Cleanup a configutation descriptor
 */
void delete_config(ctx_config_t *config) {
  safe_free(config->trace_tags);
}


/*
 * Check whether a logic is supported by the MCSAT solver
 */
bool logic_is_supported_by_mcsat(smt_logic_t code) {
  return code == SMT_ALL || !logic_has_quantifiers(code);
}

/*
 * Check whether a logic requires the MCSAT solver
 */
bool logic_requires_mcsat(smt_logic_t code) {
  return arch_for_logic(code) == CTX_ARCH_MCSAT;
}

/*
 * Check whether a logic is supported by the exists/forall solver
 * - logics with quantifiers and BV or linear arithmetic are supported
 * - logic "NONE" == purely Boolean is supported too
 */
bool logic_is_supported_by_ef(smt_logic_t code) {
  return code == NONE || code == BV || code == IDL || code == LRA || code == RDL || code == LIA || code == UF;
}


/*
 * Context architecture for a logic supported by EF
 */
int32_t ef_arch_for_logic(smt_logic_t code) {
  switch (code) {
  case NONE:
    return CTX_ARCH_NOSOLVERS;

  case UF:
    return CTX_ARCH_EG;

  case BV:
    return CTX_ARCH_BV;

  case IDL:
  case LRA:
  case RDL:
  case LIA:
    return CTX_ARCH_SPLX;

  default:
    return -1;
  }
}

1	/*
2	* This file is part of the Yices SMT Solver.
3	* Copyright (C) 2017 SRI International.
4	*
5	* Yices is free software: you can redistribute it and/or modify
6	* it under the terms of the GNU General Public License as published by
7	* the Free Software Foundation, either version 3 of the License, or
8	* (at your option) any later version.
9	*
10	* Yices is distributed in the hope that it will be useful,
11	* but WITHOUT ANY WARRANTY; without even the implied warranty of
12	* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
13	* GNU General Public License for more details.
14	*
15	* You should have received a copy of the GNU General Public License
16	* along with Yices. If not, see <http://www.gnu.org/licenses/>.
17	*/
18
19	/*
20	* OBJECT TO STORE CONTEXT CONFIGURATIONS
21	*/
22
23	#include <stdbool.h>
24	#include <assert.h>
25
26	#include "api/context_config.h"
27	#include "api/search_parameters.h"
28	#include "utils/memalloc.h"
29	#include "utils/string_utils.h"
30
31
32	/*
33	* Mapping from strings to context modes (cf. string_utils.h)
34	*/
35	static const char * const mode_names[NUM_MODES] = {
36	"interactive",
37	"multi-checks",
38	"one-shot",
39	"push-pop",
40	};
41
42	static const int32_t mode[NUM_MODES] = {
43	CTX_MODE_INTERACTIVE,
44	CTX_MODE_MULTICHECKS,
45	CTX_MODE_ONECHECK,
46	CTX_MODE_PUSHPOP,
47	};
48
49	static const char * const solver_type_names[NUM_SOLVER_TYPES] = {
50	"dpllt",
51	"mcsat"
52	};
53
54	static const int32_t solver_type[NUM_SOLVER_TYPES] = {
55	CTX_SOLVER_TYPE_DPLLT,
56	CTX_SOLVER_TYPE_MCSAT
57	};
58
59	/*
60	* Solver codes
61	*/
62	static const char * const solver_code_names[NUM_SOLVER_CODES] = {
63	"auto",
64	"default",
65	"ifw",
66	"none",
67	"rfw",
68	"simplex",
69	};
70
71	static const int32_t solver_code[NUM_SOLVER_CODES] = {
72	CTX_CONFIG_AUTO,
73	CTX_CONFIG_DEFAULT,
74	CTX_CONFIG_ARITH_IFW,
75	CTX_CONFIG_NONE,
76	CTX_CONFIG_ARITH_RFW,
77	CTX_CONFIG_ARITH_SIMPLEX,
78	};
79
80
81	/*
82	* Descriptor fields (other than "logic")
83	*/
84	typedef enum ctx_config_key {
85	CTX_CONFIG_KEY_MODE,
86	CTX_CONFIG_KEY_SOLVER_TYPE,
87	CTX_CONFIG_KEY_TRACE_TAGS,
88	CTX_CONFIG_KEY_ARITH_FRAGMENT,
89	CTX_CONFIG_KEY_UF_SOLVER,
90	CTX_CONFIG_KEY_ARRAY_SOLVER,
91	CTX_CONFIG_KEY_BV_SOLVER,
92	CTX_CONFIG_KEY_ARITH_SOLVER,
93	CTX_CONFIG_KEY_MODEL_INTERPOLATION,
94	CTX_CONFIG_KEY_SAT_DELEGATE,
95	CTX_CONFIG_KEY_SAT_DELEGATE_SELECTOR_FRAMES,
96	} ctx_config_key_t;
97
98	#define NUM_CONFIG_KEYS (CTX_CONFIG_KEY_SAT_DELEGATE_SELECTOR_FRAMES+1)
99
100
101	static const char *const config_key_names[NUM_CONFIG_KEYS] = {
102	"arith-fragment",
103	"arith-solver",
104	"array-solver",
105	"bv-solver",
106	"mode",
107	"model-interpolation",
108	"sat-delegate",
109	"sat-delegate-selector-frames",
110	"solver-type",
111	"trace",
112	"uf-solver",
113	};
114
115	static const int32_t config_key[NUM_CONFIG_KEYS] = {
116	CTX_CONFIG_KEY_ARITH_FRAGMENT,
117	CTX_CONFIG_KEY_ARITH_SOLVER,
118	CTX_CONFIG_KEY_ARRAY_SOLVER,
119	CTX_CONFIG_KEY_BV_SOLVER,
120	CTX_CONFIG_KEY_MODE,
121	CTX_CONFIG_KEY_MODEL_INTERPOLATION,
122	CTX_CONFIG_KEY_SAT_DELEGATE,
123	CTX_CONFIG_KEY_SAT_DELEGATE_SELECTOR_FRAMES,
124	CTX_CONFIG_KEY_SOLVER_TYPE,
125	CTX_CONFIG_KEY_TRACE_TAGS,
126	CTX_CONFIG_KEY_UF_SOLVER,
127	};
128
129	/*
130	* CONTEXT SETTING FOR A GIVEN LOGIC CODE
131	*/
132
133	/*
134	* Conversion of SMT logic code to a default architecture code
135	* -1 means not supported
136	*
137	* We don't use AUTO_IDL, AUTO_RDL, IFW or RFW here since
138	* the Floyd-Warshall solvers don't support all use modes.
139	*
140	* IMPORTANT: this array is used by the API in config_for_logic.
141	*/
142	static const int32_t logic2arch[NUM_SMT_LOGICS] = {
143	CTX_ARCH_NOSOLVERS, // NONE
144
145	-1, // AX
146	-1, // BV (supported by EF)
147	-1, // FFA
148	-1, // IDL (supported by EF)
149	-1, // LIA (supported by EF)
150	-1, // LRA (supported by EF)
151	-1, // LIRA
152	-1, // NIA
153	-1, // NRA
154	-1, // NIRA
155	-1, // RDL
156	-1, // UF
157	-1, // ABV
158	-1, // ALIA
159	-1, // ALRA
160	-1, // ALIRA
161	-1, // ANIA
162	-1, // ANRA
163	-1, // ANIRA
164	-1, // AUF
165	-1, // BVLRA
166	-1, // UFBV
167	-1, // UFBVLIA
168	-1, // UFIDL
169	-1, // UFLIA
170	-1, // UFLRA
171	-1, // UFLIRA
172	-1, // UFNIA
173	-1, // UFNRA
174	-1, // UFNIRA
175	-1, // UFRDL
176	-1, // AUFBV
177	-1, // AUFBVLIA
178	-1, // AUFBVNIA
179	-1, // AUFLIA
180	-1, // AUFLRA
181	-1, // AUFLIRA
182	-1, // AUFNIA
183	-1, // AUFNRA
184	-1, // AUFNIRA
185
186	CTX_ARCH_EGFUN, // QF_AX
187	CTX_ARCH_BV, // QF_BV
188	CTX_ARCH_MCSAT, // QF_FFA
189	CTX_ARCH_SPLX, // QF_IDL
190	CTX_ARCH_SPLX, // QF_LIA
191	CTX_ARCH_SPLX, // QF_LRA
192	CTX_ARCH_SPLX, // QF_LIRA
193	CTX_ARCH_MCSAT, // QF_NIA
194	CTX_ARCH_MCSAT, // QF_NRA
195	CTX_ARCH_MCSAT, // QF_NIRA
196	CTX_ARCH_SPLX, // QF_RDL
197	CTX_ARCH_EG, // QF_UF
198	CTX_ARCH_EGFUNBV, // QF_ABV
199	CTX_ARCH_EGFUNSPLX, // QF_ALIA
200	CTX_ARCH_EGFUNSPLX, // QF_ALRA
201	CTX_ARCH_EGFUNSPLX, // QF_ALIRA
202	CTX_ARCH_MCSAT, // QF_ANIA
203	CTX_ARCH_MCSAT, // QF_ANRA
204	CTX_ARCH_MCSAT, // QF_ANIRA
205	CTX_ARCH_EGFUN, // QF_AUF
206	CTX_ARCH_EGSPLXBV, // QF_BVLRA
207	CTX_ARCH_EGBV, // QF_UFBV
208	CTX_ARCH_EGSPLXBV, // QF_UFBVLIA
209
210	CTX_ARCH_EGSPLX, // QF_UFIDL
211	CTX_ARCH_EGSPLX, // QF_UFLIA
212	CTX_ARCH_EGSPLX, // QF_UFLRA
213	CTX_ARCH_EGSPLX, // QF_UFLIRA
214	CTX_ARCH_MCSAT, // QF_UFNIA
215	CTX_ARCH_MCSAT, // QF_UFNRA
216	CTX_ARCH_MCSAT, // QF_UFNIRA
217	CTX_ARCH_EGSPLX, // QF_UFRDL
218	CTX_ARCH_EGFUNBV, // QF_AUFBV
219	CTX_ARCH_EGFUNSPLXBV, // QF_AUFBVLIA
220	CTX_ARCH_MCSAT, // QF_AUFBVNIA
221	CTX_ARCH_EGFUNSPLX, // QF_AUFLIA
222	CTX_ARCH_EGFUNSPLX, // QF_AUFLRA
223	CTX_ARCH_EGFUNSPLX, // QF_AUFLIRA
224	CTX_ARCH_MCSAT, // QF_AUFNIA
225	CTX_ARCH_MCSAT, // QF_AUFNRA
226	CTX_ARCH_MCSAT, // QF_AUFNIRA
227
228	CTX_ARCH_EGFUNSPLXBV, // ALL interpreted as QF_AUFLIRA + QF_BV
229	};
230
231
232
233	/*
234	* WHICH ARITHMETIC FRAGMENTS REQUIRE THE DIOPHANTINE SUBSOLVER
235	*/
236	static const bool fragment2iflag[NUM_ARITH_FRAGMENTS+1] = {
237	false, // IDL
238	false, // RDL
239	true, // LIA
240	false, // LRA
241	true, // LIRA
242	true, // NIA
243	false, // NRA
244	true, // NIRA
245	false, // FFA
246	false, // no arithmetic
247	};
248
249
250	/*
251	* Default configuration:
252	* - enable PUSH/POP
253	* - solver type = DPLL(T)
254	* - no logic specified
255	* - arith fragment = LIRA
256	* - all solvers set to defaults
257	*/
258	static const ctx_config_t default_config = {
259	CTX_MODE_PUSHPOP, // mode
260	CTX_SOLVER_TYPE_DPLLT, // DPLLT solver
261	SMT_UNKNOWN, // logic
262	CTX_CONFIG_DEFAULT, // uf
263	CTX_CONFIG_DEFAULT, // array
264	CTX_CONFIG_DEFAULT, // bv
265	CTX_CONFIG_DEFAULT, // arith
266	ARITH_LIRA, // fragment
267	false, // model interpolation
268	SAT_DELEGATE_NONE, // sat delegate
269	false, // sat delegate selector frames
270	NULL, // trace tags
271	};
272
273
274
275
276
277	/*
278	* DIRECT CONFIGURATION
279	*/
280	int32_t arch_for_logic(smt_logic_t code) {	5,458✔
281	assert(code != SMT_UNKNOWN);
282	return logic2arch[code];	5,458✔
283	}
284
285	bool iflag_for_logic(smt_logic_t code) {	2,766✔
286	assert(code != SMT_UNKNOWN);
287	return fragment2iflag[arith_fragment(code)];	2,766✔
288	}
289
290
291
292	/*
293	* CONFIG OBJECT
294	*/
295
296	/*
297	* Initialize config to the default configuration
298	*/
299	void init_config_to_defaults(ctx_config_t *config) {	104✔
300	*config = default_config;	104✔
301	}	104✔
302
303
304
305	/*
306	* Set a default configuration to support the given logic
307	* - return -1 if the logic name is not recognized
308	* - return -2 if we don't support the logic yet
309	* - return 0 otherwise
310	*
311	* If the function returns 0, the logic field is updated.
312	* All other fields are left unchanged.
313	*/
314	int32_t config_set_logic(ctx_config_t config, const char logic) {	33✔
315	smt_logic_t code;
316	int32_t r;
317
318	code = smt_logic_code(logic);	33✔
319	if (code == SMT_UNKNOWN) {	33✔
320	r = -1;	×
321	} else if (logic2arch[code] < 0) {	33✔
322	r = -2;	×
323	} else {
324	config->logic = (smt_logic_t) code;	33✔
325	r = 0;	33✔
326	}
327
328	return r;	33✔
329	}
330
331
332	/*
333	* Convert value to a solver
334	*/
335	static int32_t set_solver_code(const char value, solver_code_t dest) {	15✔
336	int32_t v, r;
337
338	v = parse_as_keyword(value, solver_code_names, solver_code, NUM_SOLVER_CODES);	15✔
339	if (v < 0) {	15✔
340	r = -2;	×
341	} else if (v >= CTX_CONFIG_AUTO) {	15✔
342	r = -3;	×
343	} else {
344	assert(v == CTX_CONFIG_DEFAULT \|\| v == CTX_CONFIG_NONE);
345	*dest = (solver_code_t) v;	15✔
346	r = 0;	15✔
347	}
348
349	return r;	15✔
350	}
351
352
353	/*
354	* Set an individual field in config
355	* - key = field name
356	* - value = value for that field
357	*
358	* Return code:
359	* -1 if the key is not recognized
360	* -2 if the value is not recognized
361	* -3 if the value is not valid for the key
362	* 0 otherwise
363	*/
364	int32_t config_set_field(ctx_config_t config, const char key, const char *value) {	160✔
365	int32_t k, v, r;
366	arith_fragment_t arith;
367
368	r = 0; // return code	160✔
369
370	k = parse_as_keyword(key, config_key_names, config_key, NUM_CONFIG_KEYS);	160✔
371	switch (k) {	160✔
372	case CTX_CONFIG_KEY_MODE:	46✔
373	v = parse_as_keyword(value, mode_names, mode, NUM_MODES);	46✔
374	if (v < 0) {	46✔
375	r = -2;	×
376	} else {
377	config->mode = v;	46✔
378	}
379	break;	46✔
380
381	case CTX_CONFIG_KEY_SOLVER_TYPE:	64✔
382	v = parse_as_keyword(value, solver_type_names, solver_type, NUM_SOLVER_TYPES);	64✔
383	if (v < 0) {	64✔
384	r = -2;	×
385	} else {
386	config->solver_type = v;	64✔
387	}
388	break;	64✔
389
390	case CTX_CONFIG_KEY_TRACE_TAGS:	2✔
391	config->trace_tags = safe_strdup(value);	2✔
392	break;	2✔
393
394	case CTX_CONFIG_KEY_ARITH_FRAGMENT:	8✔
395	arith = arith_fragment_code(value);	8✔
396	if (arith == ARITH_NONE) {	8✔
397	r = -2;	×
398	} else {
399	config->arith_fragment = arith;	8✔
400	}
401	break;	8✔
402
403	case CTX_CONFIG_KEY_UF_SOLVER:	×
404	r = set_solver_code(value, &config->uf_config);	×
405	break;	×
406
407	case CTX_CONFIG_KEY_ARRAY_SOLVER:	8✔
408	r = set_solver_code(value, &config->array_config);	8✔
409	break;	8✔
410
411	case CTX_CONFIG_KEY_BV_SOLVER:	7✔
412	r = set_solver_code(value, &config->bv_config);	7✔
413	break;	7✔
414
415	case CTX_CONFIG_KEY_ARITH_SOLVER:	10✔
416	v = parse_as_keyword(value, solver_code_names, solver_code, NUM_SOLVER_CODES);	10✔
417	if (v < 0) {	10✔
418	r = -2;	×
419	} else {
420	assert(0 <= v && v <= NUM_SOLVER_CODES);
421	config->arith_config = v;	10✔
422	}
423	break;	10✔
424	case CTX_CONFIG_KEY_MODEL_INTERPOLATION:	9✔
425	v = parse_as_boolean(value, &config->model_interpolation);	9✔
426	if (v < 0) {	9✔
427	r = -2;	×
428	}
429	break;	9✔
430	case CTX_CONFIG_KEY_SAT_DELEGATE:	3✔
431	if (parse_sat_delegate(value, &config->sat_delegate) < 0) {	3✔
432	r = -2;	×
433	}
434	break;	3✔
435	case CTX_CONFIG_KEY_SAT_DELEGATE_SELECTOR_FRAMES:	3✔
436	v = parse_as_boolean(value, &config->sat_delegate_selector_frames);	3✔
437	if (v < 0) {	3✔
438	r = -2;	×
439	}
440	break;	3✔
441	default:	×
442	assert(k == -1);
443	r = -1;	×
444	break;	×
445	}
446
447	return r;	160✔
448	}
449
450
451
452	/*
453	* Auxiliary functions to build architecture codes incrementally
454	* - each function takes an integer a: a is either a valid architecture
455	* code or -1
456	* - then the function adds a new solver component to a: this results
457	* in either a new valid code or -1 if the new component is not compatible with a.
458	*
459	* Important: we assume that the components are added in the following
460	* order: egraph, array solver, bitvector solver, arithmetic solver
461	*/
462	static inline int32_t arch_add_egraph(int32_t a) {	12✔
463	if (a == CTX_ARCH_NOSOLVERS) {	12✔
464	a = CTX_ARCH_EG;	12✔
465	} else {
466	a = -1;	×
467	}
468	return a;	12✔
469	}
470
471	static int32_t arch_add_array(int32_t a) {	4✔
472	if (a == CTX_ARCH_EG \|\| a == CTX_ARCH_NOSOLVERS) {	4✔
473	a = CTX_ARCH_EGFUN; // array requires egraph so we add both implicitly	4✔
474	} else {
475	a = -1;	×
476	}
477	return a;	4✔
478	}
479
480	static int32_t arch_add_bv(int32_t a) {	5✔
481	switch (a) {	5✔
482	case CTX_ARCH_NOSOLVERS:	×
483	a = CTX_ARCH_BV;	×
484	break;	×
485
486	case CTX_ARCH_EG:	1✔
487	a = CTX_ARCH_EGBV;	1✔
488	break;	1✔
489
490	case CTX_ARCH_EGFUN:	4✔
491	a = CTX_ARCH_EGFUNBV;	4✔
492	break;	4✔
493
494	case CTX_ARCH_SPLX:	×
495	a = CTX_ARCH_EGSPLXBV;	×
496	break;	×
497
NEW 498	case CTX_ARCH_EGIFW:	×
NEW 499	a = CTX_ARCH_EGBVIFW;	×
NEW 500	break;	×
501
NEW 502	case CTX_ARCH_EGRFW:	×
NEW 503	a = CTX_ARCH_EGBVRFW;	×
NEW 504	break;	×
505
506	default:	×
507	a = -1;	×
508	break;	×
509	}
510
511	return a;	5✔
512	}
513
514	// add the simplex solver
515	static int32_t arch_add_simplex(int32_t a) {	4✔
516	switch (a) {	4✔
517	case CTX_ARCH_NOSOLVERS:	×
518	a = CTX_ARCH_SPLX;	×
519	break;	×
520
521	case CTX_ARCH_BV:	×
522	a = CTX_ARCH_EGSPLXBV;	×
523	break;	×
524
525	case CTX_ARCH_EG:	×
526	a = CTX_ARCH_EGSPLX;	×
527	break;	×
528
529	case CTX_ARCH_EGFUN:	×
530	a = CTX_ARCH_EGFUNSPLX;	×
531	break;	×
532
533	case CTX_ARCH_EGBV:	×
534	a = CTX_ARCH_EGSPLXBV;	×
535	break;	×
536
537	case CTX_ARCH_EGFUNBV:	4✔
538	a = CTX_ARCH_EGFUNSPLXBV;	4✔
539	break;	4✔
540
541	default:	×
542	a = -1;	×
543	break;	×
544	}
545
546	return a;	4✔
547	}
548
549	// add a Floyd-Warshall solver
550	static int32_t arch_add_ifw(int32_t a) {	6✔
551	switch (a) {	6✔
NEW 552	case CTX_ARCH_NOSOLVERS:	×
UNCOV 553	a = CTX_ARCH_IFW;	×
NEW 554	break;	×
555
556	case CTX_ARCH_EG:	5✔
557	a = CTX_ARCH_EGIFW;	5✔
558	break;	5✔
559
560	case CTX_ARCH_BV:	1✔
561	case CTX_ARCH_EGBV:
562	a = CTX_ARCH_EGBVIFW;	1✔
563	break;	1✔
564
NEW 565	default:	×
UNCOV 566	a = -1;	×
NEW 567	break;	×
568	}
569	return a;	6✔
570	}
571
572	static int32_t arch_add_rfw(int32_t a) {	2✔
573	switch (a) {	2✔
NEW 574	case CTX_ARCH_NOSOLVERS:	×
UNCOV 575	a = CTX_ARCH_RFW;	×
NEW 576	break;	×
577
578	case CTX_ARCH_EG:	2✔
579	a = CTX_ARCH_EGRFW;	2✔
580	break;	2✔
581
NEW 582	case CTX_ARCH_BV:	×
583	case CTX_ARCH_EGBV:
NEW 584	a = CTX_ARCH_EGBVRFW;	×
NEW 585	break;	×
586
NEW 587	default:	×
UNCOV 588	a = -1;	×
NEW 589	break;	×
590	}
591	return a;	2✔
592	}
593
594
595	// add solver identified by code c to a
596	static int32_t arch_add_arith(int32_t a, solver_code_t c) {	12✔
597	switch (c) {	12✔
598	case CTX_CONFIG_NONE: // no arithmetic solver	×
599	break;	×
600
601	case CTX_CONFIG_DEFAULT: // simplex is the default	4✔
602	case CTX_CONFIG_AUTO: // auto = simplex here too
603	case CTX_CONFIG_ARITH_SIMPLEX:
604	a = arch_add_simplex(a);	4✔
605	break;	4✔
606
607	case CTX_CONFIG_ARITH_IFW:	6✔
608	a = arch_add_ifw(a);	6✔
609	break;	6✔
610
611	case CTX_CONFIG_ARITH_RFW:	2✔
612	a = arch_add_rfw(a);	2✔
613	break;	2✔
614	}
615	return a;	12✔
616	}
617
618
619	/*
620	* Check whether the architecture code a is compatible with mode
621	* - current restriction: IFW and RFW don't support PUSH/POP or MULTIPLE CHECKS
622	*/
623	static bool arch_supports_mode(context_arch_t a, context_mode_t mode) {	45✔
624	return (a != CTX_ARCH_IFW && a != CTX_ARCH_RFW &&	45✔
625	a != CTX_ARCH_EGIFW && a != CTX_ARCH_EGRFW &&	39✔
626	a != CTX_ARCH_EGBVIFW && a != CTX_ARCH_EGBVRFW) \|\| mode == CTX_MODE_ONECHECK;	90✔
627	}
628
629
630	/*
631	* Check whether the architecture is supported.
632	*/
633	static bool arch_is_supported(context_arch_t a) {	92✔
634	#if HAVE_MCSAT
635	return true; // all architectures are supported	92✔
636	#else
637	return a != CTX_ARCH_MCSAT;
638	#endif
639	}
640
641
642	/*
643	* Architecture selected by an explicit arithmetic-solver setting in a
644	* configuration that also specifies a logic.
645	*/
646	static int32_t arch_for_logic_and_arith_config(smt_logic_t logic_code, solver_code_t arith_config) {	33✔
647	switch (arith_config) {	33✔
648	case CTX_CONFIG_ARITH_IFW:	1✔
649	if (logic_code == QF_IDL) {	1✔
NEW 650	return CTX_ARCH_IFW;	×
651	} else if (logic_code == QF_UFIDL) {	1✔
652	return CTX_ARCH_EGIFW;	1✔
653	}
NEW 654	return -1;	×
655
656	case CTX_CONFIG_ARITH_RFW:	1✔
657	if (logic_code == QF_RDL) {	1✔
NEW 658	return CTX_ARCH_RFW;	×
659	} else if (logic_code == QF_UFRDL) {	1✔
660	return CTX_ARCH_EGRFW;	1✔
661	}
NEW 662	return -1;	×
663
664	default:	31✔
665	return logic2arch[logic_code];	31✔
666	}
667	}
668
669
670	/*
671	* Check whether config is valid (and supported by this version of Yices)
672	* and convert it to a tuple (arch, mode, iflag, qflag)
673	* - arch = architecture code as defined in context.h
674	* - mode = one of the context's modes
675	* - iflag = true if the integer solver (in simplex) is required
676	* - qflag = true if support for quantifiers is required
677	*
678	* Return code:
679	* 0 if the config is valid and supported
680	* -1 if the config is invalid
681	* -2 if the config is valid but not currently supported
682	* -3 if the solver combination is valid but does not support the specified mode
683	*/
684	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) {	104✔
685	smt_logic_t logic_code;
686	int32_t a, r;
687
688	r = 0; // default return code	104✔
689
690	logic_code = config->logic;	104✔
691	if (logic_code != SMT_UNKNOWN) {	104✔
692	/*
693	* The intended logic is specified
694	*/
695	assert(0 <= logic_code && logic_code < NUM_SMT_LOGICS);
696
697	/*
698	* Special case: difference logic + mode = ONECHECK + arith_config == AUTO
699	*/
700	if (config->arith_config == CTX_CONFIG_AUTO && config->mode == CTX_MODE_ONECHECK) {	33✔
701	if (logic_code == QF_IDL) {	×
702	*logic = QF_IDL;	×
703	*arch = CTX_ARCH_AUTO_IDL;	×
704	*mode = CTX_MODE_ONECHECK;	×
705	*iflag = false;	×
706	*qflag = false;	×
707	goto done;	×
708	}
709
710	if (logic_code == QF_RDL) {	×
711	*logic = QF_RDL;	×
712	*arch = CTX_ARCH_AUTO_RDL;	×
713	*mode = CTX_MODE_ONECHECK;	×
714	*iflag = false;	×
715	*qflag = false;	×
716	goto done;	×
717	}
718	}
719
720	a = arch_for_logic_and_arith_config(logic_code, config->arith_config);	33✔
721	if (a < 0) {	33✔
722	// invalid combination of logic and arithmetic solver
NEW 723	r = -1;	×
724	} else if (!arch_is_supported(a)) {	33✔
725	// not supported
726	r = -2;	×
727	} else if (!arch_supports_mode(a, config->mode)) {	33✔
728	// mode is not supported by the solvers
NEW 729	r = -3;	×
730	} else {
731	// good configuration
732	*logic = logic_code;	33✔
733	*arch = (context_arch_t) a;	33✔
734	*iflag = iflag_for_logic(logic_code);	33✔
735	*qflag = qflag_for_logic(logic_code);	33✔
736	*mode = config->mode;	33✔
737	}
738
739	} else if (config->solver_type == CTX_SOLVER_TYPE_MCSAT) {	71✔
740	if (arch_is_supported(CTX_ARCH_MCSAT)) {	59✔
741	/*
742	* MCSAT solver/no logic specified
743	*/
744	*logic = SMT_UNKNOWN;	59✔
745	*arch = CTX_ARCH_MCSAT;	59✔
746	*mode = CTX_MODE_PUSHPOP;	59✔
747	*iflag = false;	59✔
748	*qflag = false;	59✔
749	} else {
750	// not compiled with MCSAT support so this is not supported
751	r = -2;	×
752	}
753
754	} else {
755	/*
756	* No logic specified.
757	*/
758
759	a = CTX_ARCH_NOSOLVERS;	12✔
760	if (config->uf_config == CTX_CONFIG_DEFAULT) {	12✔
761	a = arch_add_egraph(a);	12✔
762	}
763	if (config->array_config == CTX_CONFIG_DEFAULT) {	12✔
764	a = arch_add_array(a);	4✔
765	}
766	if (config->bv_config == CTX_CONFIG_DEFAULT) {	12✔
767	a = arch_add_bv(a);	5✔
768	}
769	a = arch_add_arith(a, config->arith_config);	12✔
770
771	// a is either -1 or an architecture code
772	if (a < 0) {	12✔
773	r = -1; // invalid combination of solvers	×
774	} else if (arch_supports_mode(a, config->mode)) {	12✔
775	// good configuration
776	*logic = SMT_UNKNOWN;	12✔
777	*arch = (context_arch_t) a;	12✔
778	*iflag = fragment2iflag[config->arith_fragment];	12✔
779	*qflag = false;	12✔
780	*mode = config->mode;	12✔
781	} else {
782	// mode is not supported by the solvers
783	r = -3;	×
784	}
785	}
786
787	done:	104✔
788	return r;	104✔
789	}
790
791
792	/*
793	* Cleanup a configutation descriptor
794	*/
795	void delete_config(ctx_config_t *config) {	103✔
796	safe_free(config->trace_tags);	103✔
797	}	103✔
798
799
800	/*
801	* Check whether a logic is supported by the MCSAT solver
802	*/
803	bool logic_is_supported_by_mcsat(smt_logic_t code) {	511✔
804	return code == SMT_ALL \|\| !logic_has_quantifiers(code);	511✔
805	}
806
807	/*
808	* Check whether a logic requires the MCSAT solver
809	*/
810	bool logic_requires_mcsat(smt_logic_t code) {	1,633✔
811	return arch_for_logic(code) == CTX_ARCH_MCSAT;	1,633✔
812	}
813
814	/*
815	* Check whether a logic is supported by the exists/forall solver
816	* - logics with quantifiers and BV or linear arithmetic are supported
817	* - logic "NONE" == purely Boolean is supported too
818	*/
819	bool logic_is_supported_by_ef(smt_logic_t code) {	1,633✔
820	return code == NONE \|\| code == BV \|\| code == IDL \|\| code == LRA \|\| code == RDL \|\| code == LIA \|\| code == UF;	1,633✔
821	}
822
823
824	/*
825	* Context architecture for a logic supported by EF
826	*/
827	int32_t ef_arch_for_logic(smt_logic_t code) {	694✔
828	switch (code) {	694✔
829	case NONE:	×
830	return CTX_ARCH_NOSOLVERS;	×
831
832	case UF:	114✔
833	return CTX_ARCH_EG;	114✔
834
835	case BV:	24✔
836	return CTX_ARCH_BV;	24✔
837
838	case IDL:	556✔
839	case LRA:
840	case RDL:
841	case LIA:
842	return CTX_ARCH_SPLX;	556✔
843
844	default:	×
845	return -1;	×
846	}
847	}

SRI-CSL / yices2 / 25686639376

Source File Press 'n' to go to next uncovered line, 'b' for previous

Source File
Press 'n' to go to next uncovered line, 'b' for previous