25368527405

Committed 05 May 2026 09:28AM UTC coverage: 66.87% (+0.2%) from 66.687%

Build # 25368527405

Build Type

Pull #611

github

Committed by

disteph

Commit Message

Merge branch 'master' into mcsat-supplement-cdclt

Conflicts resolved with a hybrid of both sides:

- tests/regress/run_test.sh: keep this branch's explicit --dpllt for
  the non-mcsat side of /both/ tests (symmetric with --mcsat), because
  yices' default solver path is heuristically chosen and is not
  guaranteed to be DPLL(T) for every logic. Also adopt master's new
  per-mode .mcsat.gold / .dpllt.gold override mechanism so tests that
  intentionally differ between the two solvers can supply separate
  gold files.

- tests/regress/both/README.md: document the symmetric --mcsat /
  --dpllt pair and the per-mode gold-override convention in one place.

Pull Request Pull Request #611: Wrap MCSAT as a Nelson-Oppen theory solver in CDCL(T) architecture

Coverage Stats

690 of 1006 new or added lines in 15 files covered. (68.59%)

2 existing lines in 2 files now uncovered.

84342 of 126128 relevant lines covered (66.87%)

1634859.8 hits per line

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

8.25

/src/api/search_parameters.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/>.
 */

/*
 * THE SEARCH PARAMETERS/OPTIONS USED BY THE SOLVER
 */

#include <float.h>
#include <assert.h>

#include "api/search_parameters.h"
#include "solvers/funs/fun_solver.h"
#include "solvers/simplex/simplex.h"
#include "solvers/quant/quant_solver.h"
#include "utils/string_utils.h"



/*******************************
 *  DEFAULT SEARCH PARAMETERS  *
 ******************************/

/*
 * Default restart parameters for SMT solving
 * Minisat-like behavior
 */
#define DEFAULT_FAST_RESTART false
#define DEFAULT_C_THRESHOLD  100
#define DEFAULT_D_THRESHOLD  100
#define DEFAULT_C_FACTOR     1.5
#define DEFAULT_D_FACTOR     1.5

/*
 * Restart parameters if option --fast-restarts is set
 */
#define FAST_RESTART_C_THRESHOLD 100
#define FAST_RESTART_D_THRESHOLD 100
#define FAST_RESTART_C_FACTOR    1.1
#define FAST_RESTART_D_FACTOR    1.1

/*
 * Default clause deletion parameters
 */
#define DEFAULT_R_THRESHOLD   1000
#define DEFAULT_R_FRACTION    0.25
#define DEFAULT_R_FACTOR      1.05


/*
 * The default SMT parameters are copied from smt_core.h
 * - VAR_DECAY_FACTOR  = 0.95
 * - VAR_RANDOM_FACTOR = 0.02
 * - CLAUSE_DECAY_FACTOR = 0.999
 * - clause caching is disabled
 */
#define DEFAULT_VAR_DECAY      VAR_DECAY_FACTOR
#define DEFAULT_RANDOMNESS     VAR_RANDOM_FACTOR
#define DEFAULT_CLAUSE_DECAY   CLAUSE_DECAY_FACTOR
#define DEFAULT_CACHE_TCLAUSES false
#define DEFAULT_TCLAUSE_SIZE   0


/*
 * Default random seed as in smt_core.d
 */
#define DEFAULT_RANDOM_SEED    0xabcdef98

/*
 * Default branching = the smt_core default
 */
#define DEFAULT_BRANCHING  BRANCHING_DEFAULT

/*
 * The default EGRAPH parameters are defined in egraph_types.h
 * - DEFAULT_MAX_ACKERMANN = 1000
 * - DEFAULT_MAX_BOOLACKERMANN = 600000
 * - DEFAULT_AUX_EQ_QUOTA = 100
 * - DEFAULT_ACKERMANN_THRESHOLD = 8
 * - DEFAULT_BOOLACK_THRESHOLD = 8
 * - DEFAULT_MAX_INTERFACE_EQS = 200
 *
 * The dynamic ackermann heuristic is disabled for both
 * boolean and non-boolean terms.
 */
#define DEFAULT_USE_DYN_ACK           false
#define DEFAULT_USE_BOOL_DYN_ACK      false
#define DEFAULT_USE_OPTIMISTIC_FCHECK true
#define DEFAULT_AUX_EQ_RATIO          0.3
#define DEFAULT_MCSAT_SUPPLEMENT_CHECK MCSAT_SUPPLEMENT_CHECK_BOTH


/*
 * Default SIMPLEX parameters defined in simplex_types.h
 * - SIMPLEX_DEFAULT_BLAND_THRESHOLD = 1000
 * - SIMPLEX_DEFAULT_PROP_ROW_SIZE = 30
 * - SIMPLEX_DEFAULT_CHECK_PERIOD = infinity
 * - propagation is disabled by default
 * - model adjustment is also disabled
 * - integer check is disabled too
 */
#define DEFAULT_SIMPLEX_PROP_FLAG     false
#define DEFAULT_SIMPLEX_ADJUST_FLAG   false
#define DEFAULT_SIMPLEX_ICHECK_FLAG   false

/*
 * Default parameters for the array solver (defined in fun_solver.h
 * - MAX_UPDATE_CONFLICTS = 20
 * - MAX_EXTENSIONALITY = 1
 */


/*
 * All default parameters
 */
static const param_t default_settings = {
  DEFAULT_FAST_RESTART,
  DEFAULT_C_THRESHOLD,
  DEFAULT_D_THRESHOLD,
  DEFAULT_C_FACTOR,
  DEFAULT_D_FACTOR,

  DEFAULT_R_THRESHOLD,
  DEFAULT_R_FRACTION,
  DEFAULT_R_FACTOR,

  DEFAULT_VAR_DECAY,
  DEFAULT_RANDOMNESS,
  DEFAULT_RANDOM_SEED,
  DEFAULT_BRANCHING,
  DEFAULT_CLAUSE_DECAY,
  DEFAULT_CACHE_TCLAUSES,
  DEFAULT_TCLAUSE_SIZE,

  DEFAULT_USE_DYN_ACK,
  DEFAULT_USE_BOOL_DYN_ACK,
  DEFAULT_USE_OPTIMISTIC_FCHECK,
  DEFAULT_MAX_ACKERMANN,
  DEFAULT_MAX_BOOLACKERMANN,
  DEFAULT_AUX_EQ_QUOTA,
  DEFAULT_AUX_EQ_RATIO,
  DEFAULT_ACKERMANN_THRESHOLD,
  DEFAULT_BOOLACK_THRESHOLD,
  DEFAULT_MAX_INTERFACE_EQS,

  DEFAULT_SIMPLEX_PROP_FLAG,
  DEFAULT_SIMPLEX_ADJUST_FLAG,
  DEFAULT_SIMPLEX_ICHECK_FLAG,
  SIMPLEX_DEFAULT_PROP_ROW_SIZE,
  SIMPLEX_DEFAULT_BLAND_THRESHOLD,
  SIMPLEX_DEFAULT_CHECK_PERIOD,

  DEFAULT_MAX_UPDATE_CONFLICTS,
  DEFAULT_MAX_EXTENSIONALITY,
  DEFAULT_MCSAT_SUPPLEMENT_CHECK,
};



/*************************************
 *  GLOBAL TABLES: PARAMETER NAMES   *
 ************************************/

/*
 * Search parameters and options can be set individually.
 *
 * We use an integer code to identify the parameters + a table of
 * parameter names in lexicographic order. Each parameter
 * is described in context.h
 */
typedef enum param_key {
  // restart parameters
  PARAM_FAST_RESTART,
  PARAM_C_THRESHOLD,
  PARAM_D_THRESHOLD,
  PARAM_C_FACTOR,
  PARAM_D_FACTOR,
  // clause deletion heuristic
  PARAM_R_THRESHOLD,
  PARAM_R_FRACTION,
  PARAM_R_FACTOR,
  // branching heuristic
  PARAM_VAR_DECAY,
  PARAM_RANDOMNESS,
  PARAM_RANDOM_SEED,
  PARAM_BRANCHING,
  // learned clauses
  PARAM_CLAUSE_DECAY,
  PARAM_CACHE_TCLAUSES,
  PARAM_TCLAUSE_SIZE,
  // egraph parameters
  PARAM_DYN_ACK,
  PARAM_DYN_BOOL_ACK,
  PARAM_OPTIMISTIC_FCHECK,
  PARAM_MAX_ACK,
  PARAM_MAX_BOOL_ACK,
  PARAM_AUX_EQ_QUOTA,
  PARAM_AUX_EQ_RATIO,
  PARAM_DYN_ACK_THRESHOLD,
  PARAM_DYN_BOOL_ACK_THRESHOLD,
  PARAM_MAX_INTERFACE_EQS,
  // simplex parameters
  PARAM_SIMPLEX_PROP,
  PARAM_SIMPLEX_ADJUST,
  PARAM_SIMPLEX_ICHECK,
  PARAM_PROP_THRESHOLD,
  PARAM_BLAND_THRESHOLD,
  PARAM_ICHECK_PERIOD,
  // array solver
  PARAM_MAX_UPDATE_CONFLICTS,
  PARAM_MAX_EXTENSIONALITY,
  PARAM_MCSAT_SUPPLEMENT_CHECK,
} param_key_t;

#define NUM_PARAM_KEYS (PARAM_MCSAT_SUPPLEMENT_CHECK+1)

// parameter names in lexicographic ordering
static const char *const param_key_names[NUM_PARAM_KEYS] = {
  "aux-eq-quota",
  "aux-eq-ratio",
  "bland-threshold",
  "branching",
  "c-factor",
  "c-threshold",
  "cache-tclauses",
  "clause-decay",
  "d-factor",
  "d-threshold",
  "dyn-ack",
  "dyn-ack-threshold",
  "dyn-bool-ack",
  "dyn-bool-ack-threshold",
  "fast-restarts",
  "icheck",
  "icheck-period",
  "max-ack",
  "max-bool-ack",
  "max-extensionality",
  "max-interface-eqs",
  "max-update-conflicts",
  "mcsat-supplement-check",
  "optimistic-final-check",
  "prop-threshold",
  "r-factor",
  "r-fraction",
  "r-threshold",
  "random-seed",
  "randomness",
  "simplex-adjust",
  "simplex-prop",
  "tclause-size",
  "var-decay",
};

// corresponding parameter codes in order
static const int32_t param_code[NUM_PARAM_KEYS] = {
  PARAM_AUX_EQ_QUOTA,
  PARAM_AUX_EQ_RATIO,
  PARAM_BLAND_THRESHOLD,
  PARAM_BRANCHING,
  PARAM_C_FACTOR,
  PARAM_C_THRESHOLD,
  PARAM_CACHE_TCLAUSES,
  PARAM_CLAUSE_DECAY,
  PARAM_D_FACTOR,
  PARAM_D_THRESHOLD,
  PARAM_DYN_ACK,
  PARAM_DYN_ACK_THRESHOLD,
  PARAM_DYN_BOOL_ACK,
  PARAM_DYN_BOOL_ACK_THRESHOLD,
  PARAM_FAST_RESTART,
  PARAM_SIMPLEX_ICHECK,
  PARAM_ICHECK_PERIOD,
  PARAM_MAX_ACK,
  PARAM_MAX_BOOL_ACK,
  PARAM_MAX_EXTENSIONALITY,
  PARAM_MAX_INTERFACE_EQS,
  PARAM_MAX_UPDATE_CONFLICTS,
  PARAM_MCSAT_SUPPLEMENT_CHECK,
  PARAM_OPTIMISTIC_FCHECK,
  PARAM_PROP_THRESHOLD,
  PARAM_R_FACTOR,
  PARAM_R_FRACTION,
  PARAM_R_THRESHOLD,
  PARAM_RANDOM_SEED,
  PARAM_RANDOMNESS,
  PARAM_SIMPLEX_ADJUST,
  PARAM_SIMPLEX_PROP,
  PARAM_TCLAUSE_SIZE,
  PARAM_VAR_DECAY,
};



/*
 * Names of each branching mode (in lexicographic order)
 */
static const char * const branching_modes[NUM_BRANCHING_MODES] = {
  "default",
  "negative",
  "positive",
  "th-neg",
  "th-pos",
  "theory",
};

static const int32_t branching_code[NUM_BRANCHING_MODES] = {
  BRANCHING_DEFAULT,
  BRANCHING_NEGATIVE,
  BRANCHING_POSITIVE,
  BRANCHING_TH_NEG,
  BRANCHING_TH_POS,
  BRANCHING_THEORY,
};

/*
 * Supplementary MCSAT checking modes (in lexicographic order)
 */
static const char * const mcsat_supplement_check_modes[NUM_MCSAT_SUPPLEMENT_CHECK_MODES] = {
  "both",
  "final-only",
};

static const int32_t mcsat_supplement_check_code[NUM_MCSAT_SUPPLEMENT_CHECK_MODES] = {
  MCSAT_SUPPLEMENT_CHECK_BOTH,
  MCSAT_SUPPLEMENT_CHECK_FINAL_ONLY,
};




/****************
 *  FUNCTIONS   *
 ***************/

/*
 * Initialize params with a copy of default_settings
 */
void init_params_to_defaults(param_t *parameters) {
  *parameters = default_settings;
}


/*
 * Return the default parameters
 */
const param_t *get_default_params(void) {
  return &default_settings;
}


/*
 * Parse value as a boolean. Store the result in *v
 * - return 0 if this works
 * - return -2 otherwise
 */
static int32_t set_bool_param(const char *value, bool *v) {
  int32_t k;

  k = parse_as_boolean(value, v);
  return (k == valid_boolean) ? 0 : -2;
}


/*
 * Parse value as a branching mode. Store the result in *v
 * - return 0 if this works
 * - return -2 otherwise
 */
static int32_t set_branching_param(const char *value, branch_t *v) {
  int32_t k;

  k = parse_as_keyword(value, branching_modes, branching_code, NUM_BRANCHING_MODES);
  assert(k >= 0 || k == -1);

  if (k >= 0) {
    assert(BRANCHING_DEFAULT <= k && k <= BRANCHING_TH_POS);
    *v = (branch_t) k;
    k = 0;
  } else {
    k = -2;
  }

  return k;
}

/*
 * Parse value as supplementary MCSAT check mode. Store the result in *v.
 * - return 0 if this works
 * - return -2 otherwise
 */
static int32_t set_mcsat_supplement_check_param(const char *value, mcsat_supplement_check_t *v) {
  int32_t k;

  k = parse_as_keyword(value, mcsat_supplement_check_modes, mcsat_supplement_check_code,
                       NUM_MCSAT_SUPPLEMENT_CHECK_MODES);
  assert(k >= 0 || k == -1);

  if (k >= 0) {
    assert(MCSAT_SUPPLEMENT_CHECK_BOTH <= k && k <= MCSAT_SUPPLEMENT_CHECK_FINAL_ONLY);
    *v = (mcsat_supplement_check_t) k;
    k = 0;
  } else {
    k = -2;
  }

  return k;
}


/*
 * Parse val as a signed 32bit integer. Check whether
 * the result is in the interval [low, high].
 * - if so, store the result into *v and return 0
 * - if val is not an integer, return -2
 * - if the result is not in the interval, return -2
 */
static int32_t set_int32_param(const char *value, int32_t *v, int32_t low, int32_t high) {
  integer_parse_code_t k;
  int32_t aux;

  k = parse_as_integer(value, &aux);
  switch (k) {
  case valid_integer:
    if (low <= aux && aux <= high) {
      *v = aux;
      aux = 0;
    } else {
      aux = -2;
    }
    break;

  case integer_overflow:
  case invalid_integer:
  default: // prevent GCC warning
    aux = -2;
    break;
  }

  return aux;
}


/*
 * Parse value as an unsigned integer
 * - no interval check
 * - if val is not an unsigned integer, return -2
 */
static int32_t set_uint32_param(const char *value, uint32_t *v) {
  integer_parse_code_t k;
  int32_t code;

  k = parse_as_uint(value, v);
  switch (k) {
  case valid_integer:
    code = 0;
    break;

  case integer_overflow:
  case invalid_integer:
  default:
    code = -2;
    break;
  }

  return code;
}



/*
 * Parse value as a double. Check whether
 * the result is in the interval [low, high].
 * - if so, store the result into *v and return 0
 * - if the string can't be parse as a double, return -1
 * - if the result is not in the interval, return -2
 */
static int32_t set_double_param(const char *value, double *v, double low, double high) {
  double_parse_code_t k;
  double aux;
  int32_t result;

  k = parse_as_double(value, &aux);
  switch (k) {
  case valid_double:
    if (low <= aux && aux <= high) {
      *v = aux;
      result = 0;
    } else {
      result = -2;
    }
    break;

  case double_overflow:
  case invalid_double:
  default: // prevent GCC warning
    result = -1;
    break;
  }

  return result;
}




/*
 * Set a field in the parameter record.
 * - 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 has the wrong type for the key
 *    0 otherwise (i.e., success)
 */
int32_t params_set_field(param_t *parameters, const char *key, const char *value) {
  int32_t k, r;
  int32_t z;
  double x;

  z = 0; // to prevent GCC warning

  k = parse_as_keyword(key, param_key_names, param_code, NUM_PARAM_KEYS);
  switch (k) {
  case PARAM_FAST_RESTART:
    r = set_bool_param(value, &parameters->fast_restart);
    break;

  case PARAM_C_THRESHOLD:
    r = set_int32_param(value, &z, 1, INT32_MAX);
    if (r == 0) {
      parameters->c_threshold = (uint32_t) z;
    }
    break;

  case PARAM_D_THRESHOLD:
    r = set_int32_param(value, &z, 1, INT32_MAX);
    if (r == 0) {
      parameters->d_threshold = (uint32_t) z;
    }
    break;

  case PARAM_C_FACTOR:
    r = set_double_param(value, &parameters->c_factor, 1.0, DBL_MAX);
    break;

  case PARAM_D_FACTOR:
    r = set_double_param(value, &parameters->d_factor, 1.0, DBL_MAX);
    break;

  case PARAM_R_THRESHOLD:
    r = set_int32_param(value, &z, 1, INT32_MAX);
    if (r == 0) {
      parameters->r_threshold = z;
    }
    break;

  case PARAM_R_FRACTION:
    r = set_double_param(value, &parameters->r_fraction, 0.0, 1.0);
    break;

  case PARAM_R_FACTOR:
    r = set_double_param(value, &parameters->r_factor, 1.0, DBL_MAX);
    break;

  case PARAM_VAR_DECAY:
    r = set_double_param(value, &parameters->var_decay, 0.0, 1.0);
    break;

  case PARAM_RANDOMNESS:
    r = set_double_param(value, &x, 0.0, 1.0);
    if (r == 0) {
      parameters->randomness = (float) x;
    }
    break;

  case PARAM_RANDOM_SEED:
    r = set_uint32_param(value, &parameters->random_seed);
    break;

  case PARAM_BRANCHING:
    r = set_branching_param(value, &parameters->branching);
    break;

  case PARAM_CLAUSE_DECAY:
    r = set_double_param(value, &x, 0.0, 1.0);
    if (r == 0) {
      parameters->clause_decay = (float) x;
    }
    break;

  case PARAM_CACHE_TCLAUSES:
    r = set_bool_param(value, &parameters->cache_tclauses);
    break;

  case PARAM_TCLAUSE_SIZE:
    r = set_int32_param(value, &z, 2, INT32_MAX);
    if (r == 0) {
      parameters->tclause_size = (uint32_t) z;
    }
    break;

  case PARAM_DYN_ACK:
    r = set_bool_param(value, &parameters->use_dyn_ack);
    break;

  case PARAM_DYN_BOOL_ACK:
    r = set_bool_param(value, &parameters->use_bool_dyn_ack);
    break;

  case PARAM_OPTIMISTIC_FCHECK:
    r = set_bool_param(value, &parameters->use_optimistic_fcheck);
    break;

  case PARAM_MAX_ACK:
    r = set_int32_param(value, &z, 1, INT32_MAX);
    if (r == 0) {
      parameters->max_ackermann = (uint32_t) z;
    }
    break;

  case PARAM_MAX_BOOL_ACK:
    r = set_int32_param(value, &z, 1, INT32_MAX);
    if (r == 0) {
      parameters->max_boolackermann = (uint32_t) z;
    }
    break;

  case PARAM_AUX_EQ_QUOTA:
    r = set_int32_param(value, &z, 1, INT32_MAX);
    if (r == 0) {
      parameters->aux_eq_quota = (uint32_t) z;
    }
    break;

  case PARAM_AUX_EQ_RATIO:
    r = set_double_param(value, &x, 0.0, (double) FLT_MAX);
    if (r == 0) {
      if (x > 0.0) {
        parameters->aux_eq_ratio = (float) x;
      } else {
        r = -2;
      }
    }
    break;

  case PARAM_DYN_ACK_THRESHOLD:
    r = set_int32_param(value, &z, 1, (int32_t) UINT16_MAX);
    if (r == 0) {
      parameters->dyn_ack_threshold = (uint16_t) z;
    }
    break;


  case PARAM_DYN_BOOL_ACK_THRESHOLD:
    r = set_int32_param(value, &z, 1, (int32_t) UINT16_MAX);
    if (r == 0) {
      parameters->dyn_bool_ack_threshold = (uint16_t) z;
    }
    break;

  case PARAM_MAX_INTERFACE_EQS:
    r = set_int32_param(value, &z, 1, INT32_MAX);
    if (r == 0) {
      parameters->max_interface_eqs = (uint32_t) z;
    }
    break;

  case PARAM_SIMPLEX_PROP:
    r = set_bool_param(value, &parameters->use_simplex_prop);
    break;

  case PARAM_SIMPLEX_ADJUST:
    r = set_bool_param(value, &parameters->adjust_simplex_model);
    break;

  case PARAM_SIMPLEX_ICHECK:
    r = set_bool_param(value, &parameters->integer_check);
    break;

  case PARAM_PROP_THRESHOLD:
    r = set_int32_param(value, &z, 0, INT32_MAX);
    if (r == 0) {
      parameters->max_prop_row_size = (uint32_t) z;
    }
    break;

  case PARAM_BLAND_THRESHOLD:
    r = set_int32_param(value, &z, 1, INT32_MAX);
    if (r == 0) {
      parameters->bland_threshold = (uint32_t) z;
    }
    break;

  case PARAM_ICHECK_PERIOD:
    r = set_int32_param(value, &parameters->integer_check_period, 1, INT32_MAX);
    break;

  case PARAM_MAX_UPDATE_CONFLICTS:
    r = set_int32_param(value, &z, 1, INT32_MAX);
    if (r == 0) {
      parameters->max_update_conflicts = (uint32_t) z;
    }
    break;

  case PARAM_MAX_EXTENSIONALITY:
    r = set_int32_param(value, &z, 1, INT32_MAX);
    if (r == 0) {
      parameters->max_extensionality = (uint32_t) z;
    }
    break;

  case PARAM_MCSAT_SUPPLEMENT_CHECK:
    r = set_mcsat_supplement_check_param(value, &parameters->mcsat_supplement_check);
    break;

  default:
    assert(k == -1);
    r = -1;
    break;
  }

  return r;
}


/*
 * Utility function: so that yices and yices_smt2
 * can keep a copy of the initial random seed
 */
uint32_t params_default_random_seed(void) {
  return DEFAULT_RANDOM_SEED;
}

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	* THE SEARCH PARAMETERS/OPTIONS USED BY THE SOLVER
21	*/
22
23	#include <float.h>
24	#include <assert.h>
25
26	#include "api/search_parameters.h"
27	#include "solvers/funs/fun_solver.h"
28	#include "solvers/simplex/simplex.h"
29	#include "solvers/quant/quant_solver.h"
30	#include "utils/string_utils.h"
31
32
33
34	/*******************************
35	* DEFAULT SEARCH PARAMETERS *
36	******************************/
37
38	/*
39	* Default restart parameters for SMT solving
40	* Minisat-like behavior
41	*/
42	#define DEFAULT_FAST_RESTART false
43	#define DEFAULT_C_THRESHOLD 100
44	#define DEFAULT_D_THRESHOLD 100
45	#define DEFAULT_C_FACTOR 1.5
46	#define DEFAULT_D_FACTOR 1.5
47
48	/*
49	* Restart parameters if option --fast-restarts is set
50	*/
51	#define FAST_RESTART_C_THRESHOLD 100
52	#define FAST_RESTART_D_THRESHOLD 100
53	#define FAST_RESTART_C_FACTOR 1.1
54	#define FAST_RESTART_D_FACTOR 1.1
55
56	/*
57	* Default clause deletion parameters
58	*/
59	#define DEFAULT_R_THRESHOLD 1000
60	#define DEFAULT_R_FRACTION 0.25
61	#define DEFAULT_R_FACTOR 1.05
62
63
64	/*
65	* The default SMT parameters are copied from smt_core.h
66	* - VAR_DECAY_FACTOR = 0.95
67	* - VAR_RANDOM_FACTOR = 0.02
68	* - CLAUSE_DECAY_FACTOR = 0.999
69	* - clause caching is disabled
70	*/
71	#define DEFAULT_VAR_DECAY VAR_DECAY_FACTOR
72	#define DEFAULT_RANDOMNESS VAR_RANDOM_FACTOR
73	#define DEFAULT_CLAUSE_DECAY CLAUSE_DECAY_FACTOR
74	#define DEFAULT_CACHE_TCLAUSES false
75	#define DEFAULT_TCLAUSE_SIZE 0
76
77
78	/*
79	* Default random seed as in smt_core.d
80	*/
81	#define DEFAULT_RANDOM_SEED 0xabcdef98
82
83	/*
84	* Default branching = the smt_core default
85	*/
86	#define DEFAULT_BRANCHING BRANCHING_DEFAULT
87
88	/*
89	* The default EGRAPH parameters are defined in egraph_types.h
90	* - DEFAULT_MAX_ACKERMANN = 1000
91	* - DEFAULT_MAX_BOOLACKERMANN = 600000
92	* - DEFAULT_AUX_EQ_QUOTA = 100
93	* - DEFAULT_ACKERMANN_THRESHOLD = 8
94	* - DEFAULT_BOOLACK_THRESHOLD = 8
95	* - DEFAULT_MAX_INTERFACE_EQS = 200
96	*
97	* The dynamic ackermann heuristic is disabled for both
98	* boolean and non-boolean terms.
99	*/
100	#define DEFAULT_USE_DYN_ACK false
101	#define DEFAULT_USE_BOOL_DYN_ACK false
102	#define DEFAULT_USE_OPTIMISTIC_FCHECK true
103	#define DEFAULT_AUX_EQ_RATIO 0.3
104	#define DEFAULT_MCSAT_SUPPLEMENT_CHECK MCSAT_SUPPLEMENT_CHECK_BOTH
105
106
107	/*
108	* Default SIMPLEX parameters defined in simplex_types.h
109	* - SIMPLEX_DEFAULT_BLAND_THRESHOLD = 1000
110	* - SIMPLEX_DEFAULT_PROP_ROW_SIZE = 30
111	* - SIMPLEX_DEFAULT_CHECK_PERIOD = infinity
112	* - propagation is disabled by default
113	* - model adjustment is also disabled
114	* - integer check is disabled too
115	*/
116	#define DEFAULT_SIMPLEX_PROP_FLAG false
117	#define DEFAULT_SIMPLEX_ADJUST_FLAG false
118	#define DEFAULT_SIMPLEX_ICHECK_FLAG false
119
120	/*
121	* Default parameters for the array solver (defined in fun_solver.h
122	* - MAX_UPDATE_CONFLICTS = 20
123	* - MAX_EXTENSIONALITY = 1
124	*/
125
126
127	/*
128	* All default parameters
129	*/
130	static const param_t default_settings = {
131	DEFAULT_FAST_RESTART,
132	DEFAULT_C_THRESHOLD,
133	DEFAULT_D_THRESHOLD,
134	DEFAULT_C_FACTOR,
135	DEFAULT_D_FACTOR,
136
137	DEFAULT_R_THRESHOLD,
138	DEFAULT_R_FRACTION,
139	DEFAULT_R_FACTOR,
140
141	DEFAULT_VAR_DECAY,
142	DEFAULT_RANDOMNESS,
143	DEFAULT_RANDOM_SEED,
144	DEFAULT_BRANCHING,
145	DEFAULT_CLAUSE_DECAY,
146	DEFAULT_CACHE_TCLAUSES,
147	DEFAULT_TCLAUSE_SIZE,
148
149	DEFAULT_USE_DYN_ACK,
150	DEFAULT_USE_BOOL_DYN_ACK,
151	DEFAULT_USE_OPTIMISTIC_FCHECK,
152	DEFAULT_MAX_ACKERMANN,
153	DEFAULT_MAX_BOOLACKERMANN,
154	DEFAULT_AUX_EQ_QUOTA,
155	DEFAULT_AUX_EQ_RATIO,
156	DEFAULT_ACKERMANN_THRESHOLD,
157	DEFAULT_BOOLACK_THRESHOLD,
158	DEFAULT_MAX_INTERFACE_EQS,
159
160	DEFAULT_SIMPLEX_PROP_FLAG,
161	DEFAULT_SIMPLEX_ADJUST_FLAG,
162	DEFAULT_SIMPLEX_ICHECK_FLAG,
163	SIMPLEX_DEFAULT_PROP_ROW_SIZE,
164	SIMPLEX_DEFAULT_BLAND_THRESHOLD,
165	SIMPLEX_DEFAULT_CHECK_PERIOD,
166
167	DEFAULT_MAX_UPDATE_CONFLICTS,
168	DEFAULT_MAX_EXTENSIONALITY,
169	DEFAULT_MCSAT_SUPPLEMENT_CHECK,
170	};
171
172
173
174	/*************************************
175	* GLOBAL TABLES: PARAMETER NAMES *
176	************************************/
177
178	/*
179	* Search parameters and options can be set individually.
180	*
181	* We use an integer code to identify the parameters + a table of
182	* parameter names in lexicographic order. Each parameter
183	* is described in context.h
184	*/
185	typedef enum param_key {
186	// restart parameters
187	PARAM_FAST_RESTART,
188	PARAM_C_THRESHOLD,
189	PARAM_D_THRESHOLD,
190	PARAM_C_FACTOR,
191	PARAM_D_FACTOR,
192	// clause deletion heuristic
193	PARAM_R_THRESHOLD,
194	PARAM_R_FRACTION,
195	PARAM_R_FACTOR,
196	// branching heuristic
197	PARAM_VAR_DECAY,
198	PARAM_RANDOMNESS,
199	PARAM_RANDOM_SEED,
200	PARAM_BRANCHING,
201	// learned clauses
202	PARAM_CLAUSE_DECAY,
203	PARAM_CACHE_TCLAUSES,
204	PARAM_TCLAUSE_SIZE,
205	// egraph parameters
206	PARAM_DYN_ACK,
207	PARAM_DYN_BOOL_ACK,
208	PARAM_OPTIMISTIC_FCHECK,
209	PARAM_MAX_ACK,
210	PARAM_MAX_BOOL_ACK,
211	PARAM_AUX_EQ_QUOTA,
212	PARAM_AUX_EQ_RATIO,
213	PARAM_DYN_ACK_THRESHOLD,
214	PARAM_DYN_BOOL_ACK_THRESHOLD,
215	PARAM_MAX_INTERFACE_EQS,
216	// simplex parameters
217	PARAM_SIMPLEX_PROP,
218	PARAM_SIMPLEX_ADJUST,
219	PARAM_SIMPLEX_ICHECK,
220	PARAM_PROP_THRESHOLD,
221	PARAM_BLAND_THRESHOLD,
222	PARAM_ICHECK_PERIOD,
223	// array solver
224	PARAM_MAX_UPDATE_CONFLICTS,
225	PARAM_MAX_EXTENSIONALITY,
226	PARAM_MCSAT_SUPPLEMENT_CHECK,
227	} param_key_t;
228
229	#define NUM_PARAM_KEYS (PARAM_MCSAT_SUPPLEMENT_CHECK+1)
230
231	// parameter names in lexicographic ordering
232	static const char *const param_key_names[NUM_PARAM_KEYS] = {
233	"aux-eq-quota",
234	"aux-eq-ratio",
235	"bland-threshold",
236	"branching",
237	"c-factor",
238	"c-threshold",
239	"cache-tclauses",
240	"clause-decay",
241	"d-factor",
242	"d-threshold",
243	"dyn-ack",
244	"dyn-ack-threshold",
245	"dyn-bool-ack",
246	"dyn-bool-ack-threshold",
247	"fast-restarts",
248	"icheck",
249	"icheck-period",
250	"max-ack",
251	"max-bool-ack",
252	"max-extensionality",
253	"max-interface-eqs",
254	"max-update-conflicts",
255	"mcsat-supplement-check",
256	"optimistic-final-check",
257	"prop-threshold",
258	"r-factor",
259	"r-fraction",
260	"r-threshold",
261	"random-seed",
262	"randomness",
263	"simplex-adjust",
264	"simplex-prop",
265	"tclause-size",
266	"var-decay",
267	};
268
269	// corresponding parameter codes in order
270	static const int32_t param_code[NUM_PARAM_KEYS] = {
271	PARAM_AUX_EQ_QUOTA,
272	PARAM_AUX_EQ_RATIO,
273	PARAM_BLAND_THRESHOLD,
274	PARAM_BRANCHING,
275	PARAM_C_FACTOR,
276	PARAM_C_THRESHOLD,
277	PARAM_CACHE_TCLAUSES,
278	PARAM_CLAUSE_DECAY,
279	PARAM_D_FACTOR,
280	PARAM_D_THRESHOLD,
281	PARAM_DYN_ACK,
282	PARAM_DYN_ACK_THRESHOLD,
283	PARAM_DYN_BOOL_ACK,
284	PARAM_DYN_BOOL_ACK_THRESHOLD,
285	PARAM_FAST_RESTART,
286	PARAM_SIMPLEX_ICHECK,
287	PARAM_ICHECK_PERIOD,
288	PARAM_MAX_ACK,
289	PARAM_MAX_BOOL_ACK,
290	PARAM_MAX_EXTENSIONALITY,
291	PARAM_MAX_INTERFACE_EQS,
292	PARAM_MAX_UPDATE_CONFLICTS,
293	PARAM_MCSAT_SUPPLEMENT_CHECK,
294	PARAM_OPTIMISTIC_FCHECK,
295	PARAM_PROP_THRESHOLD,
296	PARAM_R_FACTOR,
297	PARAM_R_FRACTION,
298	PARAM_R_THRESHOLD,
299	PARAM_RANDOM_SEED,
300	PARAM_RANDOMNESS,
301	PARAM_SIMPLEX_ADJUST,
302	PARAM_SIMPLEX_PROP,
303	PARAM_TCLAUSE_SIZE,
304	PARAM_VAR_DECAY,
305	};
306
307
308
309	/*
310	* Names of each branching mode (in lexicographic order)
311	*/
312	static const char * const branching_modes[NUM_BRANCHING_MODES] = {
313	"default",
314	"negative",
315	"positive",
316	"th-neg",
317	"th-pos",
318	"theory",
319	};
320
321	static const int32_t branching_code[NUM_BRANCHING_MODES] = {
322	BRANCHING_DEFAULT,
323	BRANCHING_NEGATIVE,
324	BRANCHING_POSITIVE,
325	BRANCHING_TH_NEG,
326	BRANCHING_TH_POS,
327	BRANCHING_THEORY,
328	};
329
330	/*
331	* Supplementary MCSAT checking modes (in lexicographic order)
332	*/
333	static const char * const mcsat_supplement_check_modes[NUM_MCSAT_SUPPLEMENT_CHECK_MODES] = {
334	"both",
335	"final-only",
336	};
337
338	static const int32_t mcsat_supplement_check_code[NUM_MCSAT_SUPPLEMENT_CHECK_MODES] = {
339	MCSAT_SUPPLEMENT_CHECK_BOTH,
340	MCSAT_SUPPLEMENT_CHECK_FINAL_ONLY,
341	};
342
343
344
345
346	/****************
347	* FUNCTIONS *
348	***************/
349
350	/*
351	* Initialize params with a copy of default_settings
352	*/
353	void init_params_to_defaults(param_t *parameters) {	7,097✔
354	*parameters = default_settings;	7,097✔
355	}	7,097✔
356
357
358	/*
359	* Return the default parameters
360	*/
361	const param_t *get_default_params(void) {	×
362	return &default_settings;	×
363	}
364
365
366	/*
367	* Parse value as a boolean. Store the result in *v
368	* - return 0 if this works
369	* - return -2 otherwise
370	*/
371	static int32_t set_bool_param(const char value, bool v) {	×
372	int32_t k;
373
374	k = parse_as_boolean(value, v);	×
375	return (k == valid_boolean) ? 0 : -2;	×
376	}
377
378
379	/*
380	* Parse value as a branching mode. Store the result in *v
381	* - return 0 if this works
382	* - return -2 otherwise
383	*/
384	static int32_t set_branching_param(const char value, branch_t v) {	×
385	int32_t k;
386
387	k = parse_as_keyword(value, branching_modes, branching_code, NUM_BRANCHING_MODES);	×
388	assert(k >= 0 \|\| k == -1);
389
390	if (k >= 0) {	×
391	assert(BRANCHING_DEFAULT <= k && k <= BRANCHING_TH_POS);
392	*v = (branch_t) k;	×
393	k = 0;	×
394	} else {
395	k = -2;	×
396	}
397
398	return k;	×
399	}
400
401	/*
402	* Parse value as supplementary MCSAT check mode. Store the result in *v.
403	* - return 0 if this works
404	* - return -2 otherwise
405	*/
406	static int32_t set_mcsat_supplement_check_param(const char value, mcsat_supplement_check_t v) {	2✔
407	int32_t k;
408
409	k = parse_as_keyword(value, mcsat_supplement_check_modes, mcsat_supplement_check_code,	2✔
410	NUM_MCSAT_SUPPLEMENT_CHECK_MODES);
411	assert(k >= 0 \|\| k == -1);
412
413	if (k >= 0) {	2✔
414	assert(MCSAT_SUPPLEMENT_CHECK_BOTH <= k && k <= MCSAT_SUPPLEMENT_CHECK_FINAL_ONLY);
415	*v = (mcsat_supplement_check_t) k;	2✔
416	k = 0;	2✔
417	} else {
NEW 418	k = -2;	×
419	}
420
421	return k;	2✔
422	}
423
424
425	/*
426	* Parse val as a signed 32bit integer. Check whether
427	* the result is in the interval [low, high].
428	* - if so, store the result into *v and return 0
429	* - if val is not an integer, return -2
430	* - if the result is not in the interval, return -2
431	*/
432	static int32_t set_int32_param(const char value, int32_t v, int32_t low, int32_t high) {	×
433	integer_parse_code_t k;
434	int32_t aux;
435
436	k = parse_as_integer(value, &aux);	×
437	switch (k) {	×
438	case valid_integer:	×
439	if (low <= aux && aux <= high) {	×
440	*v = aux;	×
441	aux = 0;	×
442	} else {
443	aux = -2;	×
444	}
445	break;	×
446
447	case integer_overflow:	×
448	case invalid_integer:
449	default: // prevent GCC warning
450	aux = -2;	×
451	break;	×
452	}
453
454	return aux;	×
455	}
456
457
458	/*
459	* Parse value as an unsigned integer
460	* - no interval check
461	* - if val is not an unsigned integer, return -2
462	*/
463	static int32_t set_uint32_param(const char value, uint32_t v) {	×
464	integer_parse_code_t k;
465	int32_t code;
466
467	k = parse_as_uint(value, v);	×
468	switch (k) {	×
469	case valid_integer:	×
470	code = 0;	×
471	break;	×
472
473	case integer_overflow:	×
474	case invalid_integer:
475	default:
476	code = -2;	×
477	break;	×
478	}
479
480	return code;	×
481	}
482
483
484
485	/*
486	* Parse value as a double. Check whether
487	* the result is in the interval [low, high].
488	* - if so, store the result into *v and return 0
489	* - if the string can't be parse as a double, return -1
490	* - if the result is not in the interval, return -2
491	*/
492	static int32_t set_double_param(const char value, double v, double low, double high) {	×
493	double_parse_code_t k;
494	double aux;
495	int32_t result;
496
497	k = parse_as_double(value, &aux);	×
498	switch (k) {	×
499	case valid_double:	×
500	if (low <= aux && aux <= high) {	×
501	*v = aux;	×
502	result = 0;	×
503	} else {
504	result = -2;	×
505	}
506	break;	×
507
508	case double_overflow:	×
509	case invalid_double:
510	default: // prevent GCC warning
511	result = -1;	×
512	break;	×
513	}
514
515	return result;	×
516	}
517
518
519
520
521	/*
522	* Set a field in the parameter record.
523	* - key = field name
524	* - value = value for that field
525	*
526	* Return code:
527	* -1 if the key is not recognized
528	* -2 if the value is not recognized
529	* -3 if the value has the wrong type for the key
530	* 0 otherwise (i.e., success)
531	*/
532	int32_t params_set_field(param_t parameters, const char key, const char *value) {	2✔
533	int32_t k, r;
534	int32_t z;
535	double x;
536
537	z = 0; // to prevent GCC warning	2✔
538
539	k = parse_as_keyword(key, param_key_names, param_code, NUM_PARAM_KEYS);	2✔
540	switch (k) {	2✔
541	case PARAM_FAST_RESTART:	×
542	r = set_bool_param(value, &parameters->fast_restart);	×
543	break;	×
544
545	case PARAM_C_THRESHOLD:	×
546	r = set_int32_param(value, &z, 1, INT32_MAX);	×
547	if (r == 0) {	×
548	parameters->c_threshold = (uint32_t) z;	×
549	}
550	break;	×
551
552	case PARAM_D_THRESHOLD:	×
553	r = set_int32_param(value, &z, 1, INT32_MAX);	×
554	if (r == 0) {	×
555	parameters->d_threshold = (uint32_t) z;	×
556	}
557	break;	×
558
559	case PARAM_C_FACTOR:	×
560	r = set_double_param(value, &parameters->c_factor, 1.0, DBL_MAX);	×
561	break;	×
562
563	case PARAM_D_FACTOR:	×
564	r = set_double_param(value, &parameters->d_factor, 1.0, DBL_MAX);	×
565	break;	×
566
567	case PARAM_R_THRESHOLD:	×
568	r = set_int32_param(value, &z, 1, INT32_MAX);	×
569	if (r == 0) {	×
570	parameters->r_threshold = z;	×
571	}
572	break;	×
573
574	case PARAM_R_FRACTION:	×
575	r = set_double_param(value, &parameters->r_fraction, 0.0, 1.0);	×
576	break;	×
577
578	case PARAM_R_FACTOR:	×
579	r = set_double_param(value, &parameters->r_factor, 1.0, DBL_MAX);	×
580	break;	×
581
582	case PARAM_VAR_DECAY:	×
583	r = set_double_param(value, &parameters->var_decay, 0.0, 1.0);	×
584	break;	×
585
586	case PARAM_RANDOMNESS:	×
587	r = set_double_param(value, &x, 0.0, 1.0);	×
588	if (r == 0) {	×
589	parameters->randomness = (float) x;	×
590	}
591	break;	×
592
593	case PARAM_RANDOM_SEED:	×
594	r = set_uint32_param(value, &parameters->random_seed);	×
595	break;	×
596
597	case PARAM_BRANCHING:	×
598	r = set_branching_param(value, &parameters->branching);	×
599	break;	×
600
601	case PARAM_CLAUSE_DECAY:	×
602	r = set_double_param(value, &x, 0.0, 1.0);	×
603	if (r == 0) {	×
604	parameters->clause_decay = (float) x;	×
605	}
606	break;	×
607
608	case PARAM_CACHE_TCLAUSES:	×
609	r = set_bool_param(value, &parameters->cache_tclauses);	×
610	break;	×
611
612	case PARAM_TCLAUSE_SIZE:	×
613	r = set_int32_param(value, &z, 2, INT32_MAX);	×
614	if (r == 0) {	×
615	parameters->tclause_size = (uint32_t) z;	×
616	}
617	break;	×
618
619	case PARAM_DYN_ACK:	×
620	r = set_bool_param(value, &parameters->use_dyn_ack);	×
621	break;	×
622
623	case PARAM_DYN_BOOL_ACK:	×
624	r = set_bool_param(value, &parameters->use_bool_dyn_ack);	×
625	break;	×
626
627	case PARAM_OPTIMISTIC_FCHECK:	×
628	r = set_bool_param(value, &parameters->use_optimistic_fcheck);	×
629	break;	×
630
631	case PARAM_MAX_ACK:	×
632	r = set_int32_param(value, &z, 1, INT32_MAX);	×
633	if (r == 0) {	×
634	parameters->max_ackermann = (uint32_t) z;	×
635	}
636	break;	×
637
638	case PARAM_MAX_BOOL_ACK:	×
639	r = set_int32_param(value, &z, 1, INT32_MAX);	×
640	if (r == 0) {	×
641	parameters->max_boolackermann = (uint32_t) z;	×
642	}
643	break;	×
644
645	case PARAM_AUX_EQ_QUOTA:	×
646	r = set_int32_param(value, &z, 1, INT32_MAX);	×
647	if (r == 0) {	×
648	parameters->aux_eq_quota = (uint32_t) z;	×
649	}
650	break;	×
651
652	case PARAM_AUX_EQ_RATIO:	×
653	r = set_double_param(value, &x, 0.0, (double) FLT_MAX);	×
654	if (r == 0) {	×
655	if (x > 0.0) {	×
656	parameters->aux_eq_ratio = (float) x;	×
657	} else {
658	r = -2;	×
659	}
660	}
661	break;	×
662
663	case PARAM_DYN_ACK_THRESHOLD:	×
664	r = set_int32_param(value, &z, 1, (int32_t) UINT16_MAX);	×
665	if (r == 0) {	×
666	parameters->dyn_ack_threshold = (uint16_t) z;	×
667	}
668	break;	×
669
670
671	case PARAM_DYN_BOOL_ACK_THRESHOLD:	×
672	r = set_int32_param(value, &z, 1, (int32_t) UINT16_MAX);	×
673	if (r == 0) {	×
674	parameters->dyn_bool_ack_threshold = (uint16_t) z;	×
675	}
676	break;	×
677
678	case PARAM_MAX_INTERFACE_EQS:	×
679	r = set_int32_param(value, &z, 1, INT32_MAX);	×
680	if (r == 0) {	×
681	parameters->max_interface_eqs = (uint32_t) z;	×
682	}
683	break;	×
684
685	case PARAM_SIMPLEX_PROP:	×
686	r = set_bool_param(value, &parameters->use_simplex_prop);	×
687	break;	×
688
689	case PARAM_SIMPLEX_ADJUST:	×
690	r = set_bool_param(value, &parameters->adjust_simplex_model);	×
691	break;	×
692
693	case PARAM_SIMPLEX_ICHECK:	×
694	r = set_bool_param(value, &parameters->integer_check);	×
695	break;	×
696
697	case PARAM_PROP_THRESHOLD:	×
698	r = set_int32_param(value, &z, 0, INT32_MAX);	×
699	if (r == 0) {	×
700	parameters->max_prop_row_size = (uint32_t) z;	×
701	}
702	break;	×
703
704	case PARAM_BLAND_THRESHOLD:	×
705	r = set_int32_param(value, &z, 1, INT32_MAX);	×
706	if (r == 0) {	×
707	parameters->bland_threshold = (uint32_t) z;	×
708	}
709	break;	×
710
711	case PARAM_ICHECK_PERIOD:	×
712	r = set_int32_param(value, &parameters->integer_check_period, 1, INT32_MAX);	×
713	break;	×
714
715	case PARAM_MAX_UPDATE_CONFLICTS:	×
716	r = set_int32_param(value, &z, 1, INT32_MAX);	×
717	if (r == 0) {	×
718	parameters->max_update_conflicts = (uint32_t) z;	×
719	}
720	break;	×
721
722	case PARAM_MAX_EXTENSIONALITY:	×
723	r = set_int32_param(value, &z, 1, INT32_MAX);	×
724	if (r == 0) {	×
725	parameters->max_extensionality = (uint32_t) z;	×
726	}
727	break;	×
728
729	case PARAM_MCSAT_SUPPLEMENT_CHECK:	2✔
730	r = set_mcsat_supplement_check_param(value, &parameters->mcsat_supplement_check);	2✔
731	break;	2✔
732
UNCOV 733	default:	×
734	assert(k == -1);
735	r = -1;	×
736	break;	×
737	}
738
739	return r;	2✔
740	}
741
742
743	/*
744	* Utility function: so that yices and yices_smt2
745	* can keep a copy of the initial random seed
746	*/
747	uint32_t params_default_random_seed(void) {	×
748	return DEFAULT_RANDOM_SEED;	×
749	}

SRI-CSL / yices2 / 25368527405

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