26675300141

Committed 29 May 2026 08:46PM UTC coverage: 68.798% (+3.4%) from 65.375%

Build # 26675300141

Build Type

push

github

Committed by

ahmed-irfan

Commit Message

Rework clause-deletion heuristic to CaDiCaL-style schedule

Replace the geometric, learned-clause-count-triggered reduce schedule
with a CaDiCaL-style one: trigger on conflict count and rebase the
reduction bound to num_conflicts + r-interval * sqrt(num_conflicts).

- context_solver.c: factor the reduce step into try_reduce_heuristic();
  trigger on num_conflicts instead of num_learned_clauses; widen the
  running reduce_threshold to uint64_t (conflict count is unbounded).
- search_parameters: drop r-threshold/r-fraction/r-factor, add
  r-initial-threshold and r-interval (defaults 300 / 25, matching
  CaDiCaL's reduceinit / reduceint).
- Update doc/YICES-LANGUAGE, doc/sphinx parameters table, and the
  interactive (help ...) entries for the renamed parameters.

Coverage Stats

10 of 10 new or added lines in 1 file covered. (100.0%)

8005 existing lines in 44 files now uncovered.

87475 of 127148 relevant lines covered (68.8%)

1646632.75 hits per line

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

54.2

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

#define NUM_CONFIG_KEYS (CTX_CONFIG_KEY_SAT_DELEGATE_INCREMENTAL_MODE+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-incremental-mode",
  "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_INCREMENTAL_MODE,
  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
  SAT_DELEGATE_MODE_REBUILD, // sat delegate incremental mode (unused unless explicitly set)
  false,                  // sat delegate incremental mode set by user
  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_INCREMENTAL_MODE:
    if (parse_sat_delegate_incremental_mode(value, &config->sat_delegate_incremental_mode) < 0) {
      r = -2;
    } else {
      config->sat_delegate_incremental_mode_set = true;
    }
    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 "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_INCREMENTAL_MODE,
96	} ctx_config_key_t;
97
98	#define NUM_CONFIG_KEYS (CTX_CONFIG_KEY_SAT_DELEGATE_INCREMENTAL_MODE+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-incremental-mode",
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_INCREMENTAL_MODE,
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	SAT_DELEGATE_MODE_REBUILD, // sat delegate incremental mode (unused unless explicitly set)
270	false, // sat delegate incremental mode set by user
271	NULL, // trace tags
272	};
273
274
275
276
277
278	/*
279	* DIRECT CONFIGURATION
280	*/
281	int32_t arch_for_logic(smt_logic_t code) {	5,519✔
282	assert(code != SMT_UNKNOWN);
283	return logic2arch[code];	5,519✔
284	}
285
286	bool iflag_for_logic(smt_logic_t code) {	2,812✔
287	assert(code != SMT_UNKNOWN);
288	return fragment2iflag[arith_fragment(code)];	2,812✔
289	}
290
291
292
293	/*
294	* CONFIG OBJECT
295	*/
296
297	/*
298	* Initialize config to the default configuration
299	*/
300	void init_config_to_defaults(ctx_config_t *config) {	126✔
301	*config = default_config;	126✔
302	}	126✔
303
304
305
306	/*
307	* Set a default configuration to support the given logic
308	* - return -1 if the logic name is not recognized
309	* - return -2 if we don't support the logic yet
310	* - return 0 otherwise
311	*
312	* If the function returns 0, the logic field is updated.
313	* All other fields are left unchanged.
314	*/
315	int32_t config_set_logic(ctx_config_t config, const char logic) {	59✔
316	smt_logic_t code;
317	int32_t r;
318
319	code = smt_logic_code(logic);	59✔
320	if (code == SMT_UNKNOWN) {	59✔
UNCOV 321	r = -1;	×
322	} else if (logic2arch[code] < 0) {	59✔
UNCOV 323	r = -2;	×
324	} else {
325	config->logic = (smt_logic_t) code;	59✔
326	r = 0;	59✔
327	}
328
329	return r;	59✔
330	}
331
332
333	/*
334	* Convert value to a solver
335	*/
336	static int32_t set_solver_code(const char value, solver_code_t dest) {	×
337	int32_t v, r;
338
339	v = parse_as_keyword(value, solver_code_names, solver_code, NUM_SOLVER_CODES);	×
340	if (v < 0) {	×
UNCOV 341	r = -2;	×
UNCOV 342	} else if (v >= CTX_CONFIG_AUTO) {	×
343	r = -3;	×
344	} else {
345	assert(v == CTX_CONFIG_DEFAULT \|\| v == CTX_CONFIG_NONE);
UNCOV 346	*dest = (solver_code_t) v;	×
UNCOV 347	r = 0;	×
348	}
349
UNCOV 350	return r;	×
351	}
352
353
354	/*
355	* Set an individual field in config
356	* - key = field name
357	* - value = value for that field
358	*
359	* Return code:
360	* -1 if the key is not recognized
361	* -2 if the value is not recognized
362	* -3 if the value is not valid for the key
363	* 0 otherwise
364	*/
365	int32_t config_set_field(ctx_config_t config, const char key, const char *value) {	184✔
366	int32_t k, v, r;
367	arith_fragment_t arith;
368
369	r = 0; // return code	184✔
370
371	k = parse_as_keyword(key, config_key_names, config_key, NUM_CONFIG_KEYS);	184✔
372	switch (k) {	184✔
373	case CTX_CONFIG_KEY_MODE:	67✔
374	v = parse_as_keyword(value, mode_names, mode, NUM_MODES);	67✔
375	if (v < 0) {	67✔
376	r = -2;	×
377	} else {
378	config->mode = v;	67✔
379	}
380	break;	67✔
381
382	case CTX_CONFIG_KEY_SOLVER_TYPE:	67✔
383	v = parse_as_keyword(value, solver_type_names, solver_type, NUM_SOLVER_TYPES);	67✔
384	if (v < 0) {	67✔
385	r = -2;	×
386	} else {
387	config->solver_type = v;	67✔
388	}
389	break;	67✔
390
391	case CTX_CONFIG_KEY_TRACE_TAGS:	2✔
392	config->trace_tags = safe_strdup(value);	2✔
393	break;	2✔
394
395	case CTX_CONFIG_KEY_ARITH_FRAGMENT:	×
UNCOV 396	arith = arith_fragment_code(value);	×
397	if (arith == ARITH_NONE) {	×
398	r = -2;	×
399	} else {
UNCOV 400	config->arith_fragment = arith;	×
401	}
402	break;	×
403
UNCOV 404	case CTX_CONFIG_KEY_UF_SOLVER:	×
405	r = set_solver_code(value, &config->uf_config);	×
406	break;	×
407
UNCOV 408	case CTX_CONFIG_KEY_ARRAY_SOLVER:	×
409	r = set_solver_code(value, &config->array_config);	×
410	break;	×
411
412	case CTX_CONFIG_KEY_BV_SOLVER:	×
UNCOV 413	r = set_solver_code(value, &config->bv_config);	×
UNCOV 414	break;	×
415
UNCOV 416	case CTX_CONFIG_KEY_ARITH_SOLVER:	×
417	v = parse_as_keyword(value, solver_code_names, solver_code, NUM_SOLVER_CODES);	×
418	if (v < 0) {	×
419	r = -2;	×
420	} else {
421	assert(0 <= v && v <= NUM_SOLVER_CODES);
UNCOV 422	config->arith_config = v;	×
423	}
424	break;	×
425	case CTX_CONFIG_KEY_MODEL_INTERPOLATION:	9✔
426	v = parse_as_boolean(value, &config->model_interpolation);	9✔
427	if (v < 0) {	9✔
UNCOV 428	r = -2;	×
429	}
430	break;	9✔
431	case CTX_CONFIG_KEY_SAT_DELEGATE:	22✔
432	if (parse_sat_delegate(value, &config->sat_delegate) < 0) {	22✔
UNCOV 433	r = -2;	×
434	}
435	break;	22✔
436	case CTX_CONFIG_KEY_SAT_DELEGATE_INCREMENTAL_MODE:	16✔
437	if (parse_sat_delegate_incremental_mode(value, &config->sat_delegate_incremental_mode) < 0) {	16✔
UNCOV 438	r = -2;	×
439	} else {
440	config->sat_delegate_incremental_mode_set = true;	16✔
441	}
442	break;	16✔
443	default:	1✔
444	assert(k == -1);
445	r = -1;	1✔
446	break;	1✔
447	}
448
449	return r;	184✔
450	}
451
452
453
454	/*
455	* Auxiliary functions to build architecture codes incrementally
456	* - each function takes an integer a: a is either a valid architecture
457	* code or -1
458	* - then the function adds a new solver component to a: this results
459	* in either a new valid code or -1 if the new component is not compatible with a.
460	*
461	* Important: we assume that the components are added in the following
462	* order: egraph, array solver, bitvector solver, arithmetic solver
463	*/
464	static inline int32_t arch_add_egraph(int32_t a) {	4✔
465	if (a == CTX_ARCH_NOSOLVERS) {	4✔
466	a = CTX_ARCH_EG;	4✔
467	} else {
UNCOV 468	a = -1;	×
469	}
470	return a;	4✔
471	}
472
473	static int32_t arch_add_array(int32_t a) {	4✔
474	if (a == CTX_ARCH_EG \|\| a == CTX_ARCH_NOSOLVERS) {	4✔
475	a = CTX_ARCH_EGFUN; // array requires egraph so we add both implicitly	4✔
476	} else {
477	a = -1;	×
478	}
479	return a;	4✔
480	}
481
482	static int32_t arch_add_bv(int32_t a) {	4✔
483	switch (a) {	4✔
UNCOV 484	case CTX_ARCH_NOSOLVERS:	×
UNCOV 485	a = CTX_ARCH_BV;	×
486	break;	×
487
UNCOV 488	case CTX_ARCH_EG:	×
UNCOV 489	a = CTX_ARCH_EGBV;	×
490	break;	×
491
492	case CTX_ARCH_EGFUN:	4✔
493	a = CTX_ARCH_EGFUNBV;	4✔
494	break;	4✔
495
496	case CTX_ARCH_SPLX:	×
497	a = CTX_ARCH_EGSPLXBV;	×
498	break;	×
499
500	default:	×
501	a = -1;	×
502	break;	×
503	}
504
505	return a;	4✔
506	}
507
508	// add the simplex solver
509	static int32_t arch_add_simplex(int32_t a) {	4✔
510	switch (a) {	4✔
UNCOV 511	case CTX_ARCH_NOSOLVERS:	×
512	a = CTX_ARCH_SPLX;	×
513	break;	×
514
UNCOV 515	case CTX_ARCH_BV:	×
516	a = CTX_ARCH_EGSPLXBV;	×
517	break;	×
518
UNCOV 519	case CTX_ARCH_EG:	×
UNCOV 520	a = CTX_ARCH_EGSPLX;	×
521	break;	×
522
UNCOV 523	case CTX_ARCH_EGFUN:	×
UNCOV 524	a = CTX_ARCH_EGFUNSPLX;	×
525	break;	×
526
527	case CTX_ARCH_EGBV:	×
UNCOV 528	a = CTX_ARCH_EGSPLXBV;	×
529	break;	×
530
531	case CTX_ARCH_EGFUNBV:	4✔
532	a = CTX_ARCH_EGFUNSPLXBV;	4✔
533	break;	4✔
534
535	default:	×
536	a = -1;	×
UNCOV 537	break;	×
538	}
539
540	return a;	4✔
541	}
542
543	// add a Floyd-Warshall solver
UNCOV 544	static int32_t arch_add_ifw(int32_t a) {	×
545	if (a == CTX_ARCH_NOSOLVERS) {	×
546	a = CTX_ARCH_IFW;	×
547	} else {
548	a = -1;	×
549	}
550	return a;	×
551	}
552
553	static int32_t arch_add_rfw(int32_t a) {	×
554	if (a == CTX_ARCH_NOSOLVERS) {	×
UNCOV 555	a = CTX_ARCH_RFW;	×
556	} else {
557	a = -1;	×
558	}
UNCOV 559	return a;	×
560	}
561
562
563	// add solver identified by code c to a
564	static int32_t arch_add_arith(int32_t a, solver_code_t c) {	4✔
565	switch (c) {	4✔
UNCOV 566	case CTX_CONFIG_NONE: // no arithmetic solver	×
UNCOV 567	break;	×
568
569	case CTX_CONFIG_DEFAULT: // simplex is the default	4✔
570	case CTX_CONFIG_AUTO: // auto = simplex here too
571	case CTX_CONFIG_ARITH_SIMPLEX:
572	a = arch_add_simplex(a);	4✔
573	break;	4✔
574
UNCOV 575	case CTX_CONFIG_ARITH_IFW:	×
UNCOV 576	a = arch_add_ifw(a);	×
UNCOV 577	break;	×
578
UNCOV 579	case CTX_CONFIG_ARITH_RFW:	×
580	a = arch_add_rfw(a);	×
UNCOV 581	break;	×
582	}
583	return a;	4✔
584	}
585
586
587	/*
588	* Check whether the architecture code a is compatible with mode
589	* - current restriction: IFW and RFW don't support PUSH/POP or MULTIPLE CHECKS
590	*/
591	static bool arch_supports_mode(context_arch_t a, context_mode_t mode) {	4✔
592	return (a != CTX_ARCH_IFW && a != CTX_ARCH_RFW) \|\| mode == CTX_MODE_ONECHECK;	4✔
593	}
594
595
596	/*
597	* Check whether the architecture is supported.
598	*/
599	static bool arch_is_supported(context_arch_t a) {	121✔
600	#if HAVE_MCSAT
601	return true; // all architectures are supported	121✔
602	#else
603	return a != CTX_ARCH_MCSAT;
604	#endif
605	}
606
607
608	/*
609	* Check whether config is valid (and supported by this version of Yices)
610	* and convert it to a tuple (arch, mode, iflag, qflag)
611	* - arch = architecture code as defined in context.h
612	* - mode = one of the context's modes
613	* - iflag = true if the integer solver (in simplex) is required
614	* - qflag = true if support for quantifiers is required
615	*
616	* Return code:
617	* 0 if the config is valid and supported
618	* -1 if the config is invalid
619	* -2 if the config is valid but not currently supported
620	* -3 if the solver combination is valid but does not support the specified mode
621	*/
622	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) {	125✔
623	smt_logic_t logic_code;
624	int32_t a, r;
625
626	r = 0; // default return code	125✔
627
628	logic_code = config->logic;	125✔
629	if (logic_code != SMT_UNKNOWN) {	125✔
630	/*
631	* The intended logic is specified
632	*/
633	assert(0 <= logic_code && logic_code < NUM_SMT_LOGICS);
634
635	/*
636	* Special case: difference logic + mode = ONECHECK + arith_config == AUTO
637	*/
638	if (config->arith_config == CTX_CONFIG_AUTO && config->mode == CTX_MODE_ONECHECK) {	59✔
639	if (logic_code == QF_IDL) {	×
640	*logic = QF_IDL;	×
UNCOV 641	*arch = CTX_ARCH_AUTO_IDL;	×
642	*mode = CTX_MODE_ONECHECK;	×
UNCOV 643	*iflag = false;	×
UNCOV 644	*qflag = false;	×
645	goto done;	×
646	}
647
648	if (logic_code == QF_RDL) {	×
649	*logic = QF_RDL;	×
UNCOV 650	*arch = CTX_ARCH_AUTO_RDL;	×
UNCOV 651	*mode = CTX_MODE_ONECHECK;	×
652	*iflag = false;	×
653	*qflag = false;	×
UNCOV 654	goto done;	×
655	}
656	}
657
658	a = logic2arch[logic_code];	59✔
659	if (a < 0 \|\| !arch_is_supported(a)) {	59✔
660	// not supported
661	r = -2;	×
662	} else {
663	// good configuration
664	*logic = logic_code;	59✔
665	*arch = (context_arch_t) a;	59✔
666	*iflag = iflag_for_logic(logic_code);	59✔
667	*qflag = qflag_for_logic(logic_code);	59✔
668	*mode = config->mode;	59✔
669	}
670
671	} else if (config->solver_type == CTX_SOLVER_TYPE_MCSAT) {	66✔
672	if (arch_is_supported(CTX_ARCH_MCSAT)) {	62✔
673	/*
674	* MCSAT solver/no logic specified
675	*/
676	*logic = SMT_UNKNOWN;	62✔
677	*arch = CTX_ARCH_MCSAT;	62✔
678	*mode = CTX_MODE_PUSHPOP;	62✔
679	*iflag = false;	62✔
680	*qflag = false;	62✔
681	} else {
682	// not compiled with MCSAT support so this is not supported
UNCOV 683	r = -2;	×
684	}
685
686	} else {
687	/*
688	* No logic specified.
689	*/
690
691	a = CTX_ARCH_NOSOLVERS;	4✔
692	if (config->uf_config == CTX_CONFIG_DEFAULT) {	4✔
693	a = arch_add_egraph(a);	4✔
694	}
695	if (config->array_config == CTX_CONFIG_DEFAULT) {	4✔
696	a = arch_add_array(a);	4✔
697	}
698	if (config->bv_config == CTX_CONFIG_DEFAULT) {	4✔
699	a = arch_add_bv(a);	4✔
700	}
701	a = arch_add_arith(a, config->arith_config);	4✔
702
703	// a is either -1 or an architecture code
704	if (a < 0) {	4✔
UNCOV 705	r = -1; // invalid combination of solvers	×
706	} else if (arch_supports_mode(a, config->mode)) {	4✔
707	// good configuration
708	*logic = SMT_UNKNOWN;	4✔
709	*arch = (context_arch_t) a;	4✔
710	*iflag = fragment2iflag[config->arith_fragment];	4✔
711	*qflag = false;	4✔
712	*mode = config->mode;	4✔
713	} else {
714	// mode is not supported by the solvers
UNCOV 715	r = -3;	×
716	}
717	}
718
719	done:	125✔
720	return r;	125✔
721	}
722
723
724	/*
725	* Cleanup a configutation descriptor
726	*/
727	void delete_config(ctx_config_t *config) {	125✔
728	safe_free(config->trace_tags);	125✔
729	}	125✔
730
731
732	/*
733	* Check whether a logic is supported by the MCSAT solver
734	*/
735	bool logic_is_supported_by_mcsat(smt_logic_t code) {	511✔
736	return code == SMT_ALL \|\| !logic_has_quantifiers(code);	511✔
737	}
738
739	/*
740	* Check whether a logic requires the MCSAT solver
741	*/
742	bool logic_requires_mcsat(smt_logic_t code) {	1,648✔
743	return arch_for_logic(code) == CTX_ARCH_MCSAT;	1,648✔
744	}
745
746	/*
747	* Check whether a logic is supported by the exists/forall solver
748	* - logics with quantifiers and BV or linear arithmetic are supported
749	* - logic "NONE" == purely Boolean is supported too
750	*/
751	bool logic_is_supported_by_ef(smt_logic_t code) {	1,648✔
752	return code == NONE \|\| code == BV \|\| code == IDL \|\| code == LRA \|\| code == RDL \|\| code == LIA \|\| code == UF;	1,648✔
753	}
754
755
756	/*
757	* Context architecture for a logic supported by EF
758	*/
759	int32_t ef_arch_for_logic(smt_logic_t code) {	694✔
760	switch (code) {	694✔
UNCOV 761	case NONE:	×
UNCOV 762	return CTX_ARCH_NOSOLVERS;	×
763
764	case UF:	114✔
765	return CTX_ARCH_EG;	114✔
766
767	case BV:	24✔
768	return CTX_ARCH_BV;	24✔
769
770	case IDL:	556✔
771	case LRA:
772	case RDL:
773	case LIA:
774	return CTX_ARCH_SPLX;	556✔
775
UNCOV 776	default:	×
UNCOV 777	return -1;	×
778	}
779	}

SRI-CSL / yices2 / 26675300141

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