25574532210

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

Build # 25574532210

Build Type

push

github

Committed by

web-flow

Commit Message

Merge pull request #607 from SRI-CSL/context_delegates

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

Coverage Stats

84 of 307 new or added lines in 7 files covered. (27.36%)

4 existing lines in 3 files now uncovered.

85205 of 126691 relevant lines covered (67.25%)

1626652.44 hits per line

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

52.94

/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;

  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_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,764✔
286	assert(code != SMT_UNKNOWN);
287	return fragment2iflag[arith_fragment(code)];	2,764✔
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) {	94✔
300	*config = default_config;	94✔
301	}	94✔
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) {	31✔
315	smt_logic_t code;
316	int32_t r;
317
318	code = smt_logic_code(logic);	31✔
319	if (code == SMT_UNKNOWN) {	31✔
320	r = -1;	×
321	} else if (logic2arch[code] < 0) {	31✔
322	r = -2;	×
323	} else {
324	config->logic = (smt_logic_t) code;	31✔
325	r = 0;	31✔
326	}
327
328	return r;	31✔
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) {	×
336	int32_t v, r;
337
338	v = parse_as_keyword(value, solver_code_names, solver_code, NUM_SOLVER_CODES);	×
339	if (v < 0) {	×
340	r = -2;	×
341	} else if (v >= CTX_CONFIG_AUTO) {	×
342	r = -3;	×
343	} else {
344	assert(v == CTX_CONFIG_DEFAULT \|\| v == CTX_CONFIG_NONE);
345	*dest = (solver_code_t) v;	×
346	r = 0;	×
347	}
348
349	return r;	×
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) {	117✔
365	int32_t k, v, r;
366	arith_fragment_t arith;
367
368	r = 0; // return code	117✔
369
370	k = parse_as_keyword(key, config_key_names, config_key, NUM_CONFIG_KEYS);	117✔
371	switch (k) {	117✔
372	case CTX_CONFIG_KEY_MODE:	36✔
373	v = parse_as_keyword(value, mode_names, mode, NUM_MODES);	36✔
374	if (v < 0) {	36✔
375	r = -2;	×
376	} else {
377	config->mode = v;	36✔
378	}
379	break;	36✔
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:	×
395	arith = arith_fragment_code(value);	×
396	if (arith == ARITH_NONE) {	×
397	r = -2;	×
398	} else {
399	config->arith_fragment = arith;	×
400	}
401	break;	×
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:	×
408	r = set_solver_code(value, &config->array_config);	×
409	break;	×
410
411	case CTX_CONFIG_KEY_BV_SOLVER:	×
412	r = set_solver_code(value, &config->bv_config);	×
413	break;	×
414
415	case CTX_CONFIG_KEY_ARITH_SOLVER:	×
416	v = parse_as_keyword(value, solver_code_names, solver_code, NUM_SOLVER_CODES);	×
417	if (v < 0) {	×
418	r = -2;	×
419	} else {
420	assert(0 <= v && v <= NUM_SOLVER_CODES);
421	config->arith_config = v;	×
422	}
423	break;	×
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✔
NEW 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✔
NEW 438	r = -2;	×
439	}
440	break;	3✔
UNCOV 441	default:	×
442	assert(k == -1);
443	r = -1;	×
444	break;	×
445	}
446
447	return r;	117✔
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) {	4✔
463	if (a == CTX_ARCH_NOSOLVERS) {	4✔
464	a = CTX_ARCH_EG;	4✔
465	} else {
466	a = -1;	×
467	}
468	return a;	4✔
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) {	4✔
481	switch (a) {	4✔
482	case CTX_ARCH_NOSOLVERS:	×
483	a = CTX_ARCH_BV;	×
484	break;	×
485
486	case CTX_ARCH_EG:	×
487	a = CTX_ARCH_EGBV;	×
488	break;	×
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
498	default:	×
499	a = -1;	×
500	break;	×
501	}
502
503	return a;	4✔
504	}
505
506	// add the simplex solver
507	static int32_t arch_add_simplex(int32_t a) {	4✔
508	switch (a) {	4✔
509	case CTX_ARCH_NOSOLVERS:	×
510	a = CTX_ARCH_SPLX;	×
511	break;	×
512
513	case CTX_ARCH_BV:	×
514	a = CTX_ARCH_EGSPLXBV;	×
515	break;	×
516
517	case CTX_ARCH_EG:	×
518	a = CTX_ARCH_EGSPLX;	×
519	break;	×
520
521	case CTX_ARCH_EGFUN:	×
522	a = CTX_ARCH_EGFUNSPLX;	×
523	break;	×
524
525	case CTX_ARCH_EGBV:	×
526	a = CTX_ARCH_EGSPLXBV;	×
527	break;	×
528
529	case CTX_ARCH_EGFUNBV:	4✔
530	a = CTX_ARCH_EGFUNSPLXBV;	4✔
531	break;	4✔
532
533	default:	×
534	a = -1;	×
535	break;	×
536	}
537
538	return a;	4✔
539	}
540
541	// add a Floyd-Warshall solver
542	static int32_t arch_add_ifw(int32_t a) {	×
543	if (a == CTX_ARCH_NOSOLVERS) {	×
544	a = CTX_ARCH_IFW;	×
545	} else {
546	a = -1;	×
547	}
548	return a;	×
549	}
550
551	static int32_t arch_add_rfw(int32_t a) {	×
552	if (a == CTX_ARCH_NOSOLVERS) {	×
553	a = CTX_ARCH_RFW;	×
554	} else {
555	a = -1;	×
556	}
557	return a;	×
558	}
559
560
561	// add solver identified by code c to a
562	static int32_t arch_add_arith(int32_t a, solver_code_t c) {	4✔
563	switch (c) {	4✔
564	case CTX_CONFIG_NONE: // no arithmetic solver	×
565	break;	×
566
567	case CTX_CONFIG_DEFAULT: // simplex is the default	4✔
568	case CTX_CONFIG_AUTO: // auto = simplex here too
569	case CTX_CONFIG_ARITH_SIMPLEX:
570	a = arch_add_simplex(a);	4✔
571	break;	4✔
572
573	case CTX_CONFIG_ARITH_IFW:	×
574	a = arch_add_ifw(a);	×
575	break;	×
576
577	case CTX_CONFIG_ARITH_RFW:	×
578	a = arch_add_rfw(a);	×
579	break;	×
580	}
581	return a;	4✔
582	}
583
584
585	/*
586	* Check whether the architecture code a is compatible with mode
587	* - current restriction: IFW and RFW don't support PUSH/POP or MULTIPLE CHECKS
588	*/
589	static bool arch_supports_mode(context_arch_t a, context_mode_t mode) {	4✔
590	return (a != CTX_ARCH_IFW && a != CTX_ARCH_RFW) \|\| mode == CTX_MODE_ONECHECK;	4✔
591	}
592
593
594	/*
595	* Check whether the architecture is supported.
596	*/
597	static bool arch_is_supported(context_arch_t a) {	90✔
598	#if HAVE_MCSAT
599	return true; // all architectures are supported	90✔
600	#else
601	return a != CTX_ARCH_MCSAT;
602	#endif
603	}
604
605
606	/*
607	* Check whether config is valid (and supported by this version of Yices)
608	* and convert it to a tuple (arch, mode, iflag, qflag)
609	* - arch = architecture code as defined in context.h
610	* - mode = one of the context's modes
611	* - iflag = true if the integer solver (in simplex) is required
612	* - qflag = true if support for quantifiers is required
613	*
614	* Return code:
615	* 0 if the config is valid and supported
616	* -1 if the config is invalid
617	* -2 if the config is valid but not currently supported
618	* -3 if the solver combination is valid but does not support the specified mode
619	*/
620	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) {	94✔
621	smt_logic_t logic_code;
622	int32_t a, r;
623
624	r = 0; // default return code	94✔
625
626	logic_code = config->logic;	94✔
627	if (logic_code != SMT_UNKNOWN) {	94✔
628	/*
629	* The intended logic is specified
630	*/
631	assert(0 <= logic_code && logic_code < NUM_SMT_LOGICS);
632
633	/*
634	* Special case: difference logic + mode = ONECHECK + arith_config == AUTO
635	*/
636	if (config->arith_config == CTX_CONFIG_AUTO && config->mode == CTX_MODE_ONECHECK) {	31✔
637	if (logic_code == QF_IDL) {	×
638	*logic = QF_IDL;	×
639	*arch = CTX_ARCH_AUTO_IDL;	×
640	*mode = CTX_MODE_ONECHECK;	×
641	*iflag = false;	×
642	*qflag = false;	×
643	goto done;	×
644	}
645
646	if (logic_code == QF_RDL) {	×
647	*logic = QF_RDL;	×
648	*arch = CTX_ARCH_AUTO_RDL;	×
649	*mode = CTX_MODE_ONECHECK;	×
650	*iflag = false;	×
651	*qflag = false;	×
652	goto done;	×
653	}
654	}
655
656	a = logic2arch[logic_code];	31✔
657	if (a < 0 \|\| !arch_is_supported(a)) {	31✔
658	// not supported
659	r = -2;	×
660	} else {
661	// good configuration
662	*logic = logic_code;	31✔
663	*arch = (context_arch_t) a;	31✔
664	*iflag = iflag_for_logic(logic_code);	31✔
665	*qflag = qflag_for_logic(logic_code);	31✔
666	*mode = config->mode;	31✔
667	}
668
669	} else if (config->solver_type == CTX_SOLVER_TYPE_MCSAT) {	63✔
670	if (arch_is_supported(CTX_ARCH_MCSAT)) {	59✔
671	/*
672	* MCSAT solver/no logic specified
673	*/
674	*logic = SMT_UNKNOWN;	59✔
675	*arch = CTX_ARCH_MCSAT;	59✔
676	*mode = CTX_MODE_PUSHPOP;	59✔
677	*iflag = false;	59✔
678	*qflag = false;	59✔
679	} else {
680	// not compiled with MCSAT support so this is not supported
681	r = -2;	×
682	}
683
684	} else {
685	/*
686	* No logic specified.
687	*/
688
689	a = CTX_ARCH_NOSOLVERS;	4✔
690	if (config->uf_config == CTX_CONFIG_DEFAULT) {	4✔
691	a = arch_add_egraph(a);	4✔
692	}
693	if (config->array_config == CTX_CONFIG_DEFAULT) {	4✔
694	a = arch_add_array(a);	4✔
695	}
696	if (config->bv_config == CTX_CONFIG_DEFAULT) {	4✔
697	a = arch_add_bv(a);	4✔
698	}
699	a = arch_add_arith(a, config->arith_config);	4✔
700
701	// a is either -1 or an architecture code
702	if (a < 0) {	4✔
703	r = -1; // invalid combination of solvers	×
704	} else if (arch_supports_mode(a, config->mode)) {	4✔
705	// good configuration
706	*logic = SMT_UNKNOWN;	4✔
707	*arch = (context_arch_t) a;	4✔
708	*iflag = fragment2iflag[config->arith_fragment];	4✔
709	*qflag = false;	4✔
710	*mode = config->mode;	4✔
711	} else {
712	// mode is not supported by the solvers
713	r = -3;	×
714	}
715	}
716
717	done:	94✔
718	return r;	94✔
719	}
720
721
722	/*
723	* Cleanup a configutation descriptor
724	*/
725	void delete_config(ctx_config_t *config) {	93✔
726	safe_free(config->trace_tags);	93✔
727	}	93✔
728
729
730	/*
731	* Check whether a logic is supported by the MCSAT solver
732	*/
733	bool logic_is_supported_by_mcsat(smt_logic_t code) {	511✔
734	return code == SMT_ALL \|\| !logic_has_quantifiers(code);	511✔
735	}
736
737	/*
738	* Check whether a logic requires the MCSAT solver
739	*/
740	bool logic_requires_mcsat(smt_logic_t code) {	1,633✔
741	return arch_for_logic(code) == CTX_ARCH_MCSAT;	1,633✔
742	}
743
744	/*
745	* Check whether a logic is supported by the exists/forall solver
746	* - logics with quantifiers and BV or linear arithmetic are supported
747	* - logic "NONE" == purely Boolean is supported too
748	*/
749	bool logic_is_supported_by_ef(smt_logic_t code) {	1,633✔
750	return code == NONE \|\| code == BV \|\| code == IDL \|\| code == LRA \|\| code == RDL \|\| code == LIA \|\| code == UF;	1,633✔
751	}
752
753
754	/*
755	* Context architecture for a logic supported by EF
756	*/
757	int32_t ef_arch_for_logic(smt_logic_t code) {	694✔
758	switch (code) {	694✔
759	case NONE:	×
760	return CTX_ARCH_NOSOLVERS;	×
761
762	case UF:	114✔
763	return CTX_ARCH_EG;	114✔
764
765	case BV:	24✔
766	return CTX_ARCH_BV;	24✔
767
768	case IDL:	556✔
769	case LRA:
770	case RDL:
771	case LIA:
772	return CTX_ARCH_SPLX;	556✔
773
774	default:	×
775	return -1;	×
776	}
777	}

SRI-CSL / yices2 / 25574532210

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