25567506028

Committed 08 May 2026 04:40PM UTC coverage: 67.254% (+0.03%) from 67.22%

Build # 25567506028

Build Type

Pull #607

github

Committed by

web-flow

Commit Message

Merge branch 'master' into context_delegates

Pull Request Pull Request #607: QF_BV context delegates (#453): config/param selection, incremental state, assumptions, and delegate regressions

Coverage Stats

105 of 353 new or added lines in 7 files covered. (29.75%)

4 existing lines in 3 files now uncovered.

85236 of 126737 relevant lines covered (67.25%)

1627700.56 hits per line

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

53.33

/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 "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,
};

/*
 * Names of delegate solvers (in lexicographic order)
 */
static const char * const sat_delegate_modes[NUM_SAT_DELEGATES] = {
  "cadical",
  "cryptominisat",
  "kissat",
  "none",
  "y2sat",
};

static const int32_t sat_delegate_code[NUM_SAT_DELEGATES] = {
  SAT_DELEGATE_CADICAL,
  SAT_DELEGATE_CRYPTOMINISAT,
  SAT_DELEGATE_KISSAT,
  SAT_DELEGATE_NONE,
  SAT_DELEGATE_Y2SAT,
};




/*
 * 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:
    v = parse_as_keyword(value, sat_delegate_modes, sat_delegate_code, NUM_SAT_DELEGATES);
    if (v < 0) {
      r = -2;
    } else {
      config->sat_delegate = (sat_delegate_t) v;
    }
    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;

  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) {
  if (a == CTX_ARCH_NOSOLVERS) {
    a = CTX_ARCH_IFW;
  } else {
    a = -1;
  }
  return a;
}

static int32_t arch_add_rfw(int32_t a) {
  if (a == CTX_ARCH_NOSOLVERS) {
    a = CTX_ARCH_RFW;
  } else {
    a = -1;
  }
  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) || 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
}


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

SRI-CSL / yices2 / 25567506028

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