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

16.52

/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
#define DEFAULT_SAT_DELEGATE SAT_DELEGATE_NONE

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


/*
 * 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_SAT_DELEGATE,

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



/*************************************
 *  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,
  PARAM_DELEGATE,
  // 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_key_t;

#define NUM_PARAM_KEYS (PARAM_MAX_EXTENSIONALITY+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",
  "delegate",
  "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",
  "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_DELEGATE,
  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_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,
};

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

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

const char *sat_delegate_name(sat_delegate_t mode) {
  switch (mode) {
  case SAT_DELEGATE_Y2SAT:
    return "y2sat";
  case SAT_DELEGATE_CADICAL:
    return "cadical";
  case SAT_DELEGATE_CRYPTOMINISAT:
    return "cryptominisat";
  case SAT_DELEGATE_KISSAT:
    return "kissat";
  case SAT_DELEGATE_NONE:
  default:
    return NULL;
  }
}

int32_t parse_sat_delegate(const char *value, sat_delegate_t *v) {
  int32_t k;

  k = parse_as_keyword(value, sat_delegate_modes, sat_delegate_code, NUM_SAT_DELEGATES);
  assert(k >= 0 || k == -1);

  if (k >= 0) {
    assert(SAT_DELEGATE_NONE <= k && k <= SAT_DELEGATE_KISSAT);
    *v = (sat_delegate_t) k;
    return 0;
  }

  return -2;
}

sat_delegate_t effective_sat_delegate_mode(sat_delegate_t config_delegate, const param_t *params, bool *one_shot) {
  sat_delegate_t req;

  req = SAT_DELEGATE_NONE;
  if (params != NULL) {
    req = params->delegate;
  }

  if (req != SAT_DELEGATE_NONE) {
    if (one_shot != NULL) {
      *one_shot = (req != config_delegate || config_delegate == SAT_DELEGATE_NONE);
    }
    return req;
  }

  if (one_shot != NULL) {
    *one_shot = false;
  }
  return config_delegate;
}




/****************
 *  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 a SAT delegate mode. Store the result in *v
 * - return 0 if this works
 * - return -2 otherwise
 */
static int32_t set_sat_delegate_param(const char *value, sat_delegate_t *v) {
  return parse_sat_delegate(value, v);
}


/*
 * 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_DELEGATE:
    r = set_sat_delegate_param(value, &parameters->delegate);
    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;

  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	#define DEFAULT_SAT_DELEGATE SAT_DELEGATE_NONE
88
89	/*
90	* The default EGRAPH parameters are defined in egraph_types.h
91	* - DEFAULT_MAX_ACKERMANN = 1000
92	* - DEFAULT_MAX_BOOLACKERMANN = 600000
93	* - DEFAULT_AUX_EQ_QUOTA = 100
94	* - DEFAULT_ACKERMANN_THRESHOLD = 8
95	* - DEFAULT_BOOLACK_THRESHOLD = 8
96	* - DEFAULT_MAX_INTERFACE_EQS = 200
97	*
98	* The dynamic ackermann heuristic is disabled for both
99	* boolean and non-boolean terms.
100	*/
101	#define DEFAULT_USE_DYN_ACK false
102	#define DEFAULT_USE_BOOL_DYN_ACK false
103	#define DEFAULT_USE_OPTIMISTIC_FCHECK true
104	#define DEFAULT_AUX_EQ_RATIO 0.3
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	DEFAULT_SAT_DELEGATE,
149
150	DEFAULT_USE_DYN_ACK,
151	DEFAULT_USE_BOOL_DYN_ACK,
152	DEFAULT_USE_OPTIMISTIC_FCHECK,
153	DEFAULT_MAX_ACKERMANN,
154	DEFAULT_MAX_BOOLACKERMANN,
155	DEFAULT_AUX_EQ_QUOTA,
156	DEFAULT_AUX_EQ_RATIO,
157	DEFAULT_ACKERMANN_THRESHOLD,
158	DEFAULT_BOOLACK_THRESHOLD,
159	DEFAULT_MAX_INTERFACE_EQS,
160
161	DEFAULT_SIMPLEX_PROP_FLAG,
162	DEFAULT_SIMPLEX_ADJUST_FLAG,
163	DEFAULT_SIMPLEX_ICHECK_FLAG,
164	SIMPLEX_DEFAULT_PROP_ROW_SIZE,
165	SIMPLEX_DEFAULT_BLAND_THRESHOLD,
166	SIMPLEX_DEFAULT_CHECK_PERIOD,
167
168	DEFAULT_MAX_UPDATE_CONFLICTS,
169	DEFAULT_MAX_EXTENSIONALITY,
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	PARAM_DELEGATE,
193	// clause deletion heuristic
194	PARAM_R_THRESHOLD,
195	PARAM_R_FRACTION,
196	PARAM_R_FACTOR,
197	// branching heuristic
198	PARAM_VAR_DECAY,
199	PARAM_RANDOMNESS,
200	PARAM_RANDOM_SEED,
201	PARAM_BRANCHING,
202	// learned clauses
203	PARAM_CLAUSE_DECAY,
204	PARAM_CACHE_TCLAUSES,
205	PARAM_TCLAUSE_SIZE,
206	// egraph parameters
207	PARAM_DYN_ACK,
208	PARAM_DYN_BOOL_ACK,
209	PARAM_OPTIMISTIC_FCHECK,
210	PARAM_MAX_ACK,
211	PARAM_MAX_BOOL_ACK,
212	PARAM_AUX_EQ_QUOTA,
213	PARAM_AUX_EQ_RATIO,
214	PARAM_DYN_ACK_THRESHOLD,
215	PARAM_DYN_BOOL_ACK_THRESHOLD,
216	PARAM_MAX_INTERFACE_EQS,
217	// simplex parameters
218	PARAM_SIMPLEX_PROP,
219	PARAM_SIMPLEX_ADJUST,
220	PARAM_SIMPLEX_ICHECK,
221	PARAM_PROP_THRESHOLD,
222	PARAM_BLAND_THRESHOLD,
223	PARAM_ICHECK_PERIOD,
224	// array solver
225	PARAM_MAX_UPDATE_CONFLICTS,
226	PARAM_MAX_EXTENSIONALITY,
227	} param_key_t;
228
229	#define NUM_PARAM_KEYS (PARAM_MAX_EXTENSIONALITY+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	"delegate",
244	"dyn-ack",
245	"dyn-ack-threshold",
246	"dyn-bool-ack",
247	"dyn-bool-ack-threshold",
248	"fast-restarts",
249	"icheck",
250	"icheck-period",
251	"max-ack",
252	"max-bool-ack",
253	"max-extensionality",
254	"max-interface-eqs",
255	"max-update-conflicts",
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_DELEGATE,
282	PARAM_DYN_ACK,
283	PARAM_DYN_ACK_THRESHOLD,
284	PARAM_DYN_BOOL_ACK,
285	PARAM_DYN_BOOL_ACK_THRESHOLD,
286	PARAM_FAST_RESTART,
287	PARAM_SIMPLEX_ICHECK,
288	PARAM_ICHECK_PERIOD,
289	PARAM_MAX_ACK,
290	PARAM_MAX_BOOL_ACK,
291	PARAM_MAX_EXTENSIONALITY,
292	PARAM_MAX_INTERFACE_EQS,
293	PARAM_MAX_UPDATE_CONFLICTS,
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	* Names of delegate solvers (in lexicographic order)
332	*/
333	static const char * const sat_delegate_modes[NUM_SAT_DELEGATES] = {
334	"cadical",
335	"cryptominisat",
336	"kissat",
337	"none",
338	"y2sat",
339	};
340
341	static const int32_t sat_delegate_code[NUM_SAT_DELEGATES] = {
342	SAT_DELEGATE_CADICAL,
343	SAT_DELEGATE_CRYPTOMINISAT,
344	SAT_DELEGATE_KISSAT,
345	SAT_DELEGATE_NONE,
346	SAT_DELEGATE_Y2SAT,
347	};
348
349	const char *sat_delegate_name(sat_delegate_t mode) {	2,703✔
350	switch (mode) {	2,703✔
351	case SAT_DELEGATE_Y2SAT:	20✔
352	return "y2sat";	20✔
353	case SAT_DELEGATE_CADICAL:	1✔
354	return "cadical";	1✔
NEW 355	case SAT_DELEGATE_CRYPTOMINISAT:	×
NEW 356	return "cryptominisat";	×
NEW 357	case SAT_DELEGATE_KISSAT:	×
NEW 358	return "kissat";	×
359	case SAT_DELEGATE_NONE:	2,682✔
360	default:
361	return NULL;	2,682✔
362	}
363	}
364
365	int32_t parse_sat_delegate(const char value, sat_delegate_t v) {	17✔
366	int32_t k;
367
368	k = parse_as_keyword(value, sat_delegate_modes, sat_delegate_code, NUM_SAT_DELEGATES);	17✔
369	assert(k >= 0 \|\| k == -1);
370
371	if (k >= 0) {	17✔
372	assert(SAT_DELEGATE_NONE <= k && k <= SAT_DELEGATE_KISSAT);
373	*v = (sat_delegate_t) k;	16✔
374	return 0;	16✔
375	}
376
377	return -2;	1✔
378	}
379
380	sat_delegate_t effective_sat_delegate_mode(sat_delegate_t config_delegate, const param_t params, bool one_shot) {	2,703✔
381	sat_delegate_t req;
382
383	req = SAT_DELEGATE_NONE;	2,703✔
384	if (params != NULL) {	2,703✔
385	req = params->delegate;	2,703✔
386	}
387
388	if (req != SAT_DELEGATE_NONE) {	2,703✔
389	if (one_shot != NULL) {	17✔
390	*one_shot = (req != config_delegate \|\| config_delegate == SAT_DELEGATE_NONE);	17✔
391	}
392	return req;	17✔
393	}
394
395	if (one_shot != NULL) {	2,686✔
396	*one_shot = false;	2,686✔
397	}
398	return config_delegate;	2,686✔
399	}
400
401
402
403
404	/****************
405	* FUNCTIONS *
406	***************/
407
408	/*
409	* Initialize params with a copy of default_settings
410	*/
411	void init_params_to_defaults(param_t *parameters) {	7,153✔
412	*parameters = default_settings;	7,153✔
413	}	7,153✔
414
415
416	/*
417	* Return the default parameters
418	*/
419	const param_t *get_default_params(void) {	×
420	return &default_settings;	×
421	}
422
423
424	/*
425	* Parse value as a boolean. Store the result in *v
426	* - return 0 if this works
427	* - return -2 otherwise
428	*/
429	static int32_t set_bool_param(const char value, bool v) {	×
430	int32_t k;
431
432	k = parse_as_boolean(value, v);	×
433	return (k == valid_boolean) ? 0 : -2;	×
434	}
435
436
437	/*
438	* Parse value as a branching mode. Store the result in *v
439	* - return 0 if this works
440	* - return -2 otherwise
441	*/
442	static int32_t set_branching_param(const char value, branch_t v) {	×
443	int32_t k;
444
445	k = parse_as_keyword(value, branching_modes, branching_code, NUM_BRANCHING_MODES);	×
446	assert(k >= 0 \|\| k == -1);
447
448	if (k >= 0) {	×
449	assert(BRANCHING_DEFAULT <= k && k <= BRANCHING_TH_POS);
450	*v = (branch_t) k;	×
451	k = 0;	×
452	} else {
453	k = -2;	×
454	}
455
456	return k;	×
457	}
458
459	/*
460	* Parse value as a SAT delegate mode. Store the result in *v
461	* - return 0 if this works
462	* - return -2 otherwise
463	*/
464	static int32_t set_sat_delegate_param(const char value, sat_delegate_t v) {	14✔
465	return parse_sat_delegate(value, v);	14✔
466	}
467
468
469	/*
470	* Parse val as a signed 32bit integer. Check whether
471	* the result is in the interval [low, high].
472	* - if so, store the result into *v and return 0
473	* - if val is not an integer, return -2
474	* - if the result is not in the interval, return -2
475	*/
476	static int32_t set_int32_param(const char value, int32_t v, int32_t low, int32_t high) {	×
477	integer_parse_code_t k;
478	int32_t aux;
479
480	k = parse_as_integer(value, &aux);	×
481	switch (k) {	×
482	case valid_integer:	×
483	if (low <= aux && aux <= high) {	×
484	*v = aux;	×
485	aux = 0;	×
486	} else {
487	aux = -2;	×
488	}
489	break;	×
490
491	case integer_overflow:	×
492	case invalid_integer:
493	default: // prevent GCC warning
494	aux = -2;	×
495	break;	×
496	}
497
498	return aux;	×
499	}
500
501
502	/*
503	* Parse value as an unsigned integer
504	* - no interval check
505	* - if val is not an unsigned integer, return -2
506	*/
507	static int32_t set_uint32_param(const char value, uint32_t v) {	×
508	integer_parse_code_t k;
509	int32_t code;
510
511	k = parse_as_uint(value, v);	×
512	switch (k) {	×
513	case valid_integer:	×
514	code = 0;	×
515	break;	×
516
517	case integer_overflow:	×
518	case invalid_integer:
519	default:
520	code = -2;	×
521	break;	×
522	}
523
524	return code;	×
525	}
526
527
528
529	/*
530	* Parse value as a double. Check whether
531	* the result is in the interval [low, high].
532	* - if so, store the result into *v and return 0
533	* - if the string can't be parse as a double, return -1
534	* - if the result is not in the interval, return -2
535	*/
536	static int32_t set_double_param(const char value, double v, double low, double high) {	×
537	double_parse_code_t k;
538	double aux;
539	int32_t result;
540
541	k = parse_as_double(value, &aux);	×
542	switch (k) {	×
543	case valid_double:	×
544	if (low <= aux && aux <= high) {	×
545	*v = aux;	×
546	result = 0;	×
547	} else {
548	result = -2;	×
549	}
550	break;	×
551
552	case double_overflow:	×
553	case invalid_double:
554	default: // prevent GCC warning
555	result = -1;	×
556	break;	×
557	}
558
559	return result;	×
560	}
561
562
563
564
565	/*
566	* Set a field in the parameter record.
567	* - key = field name
568	* - value = value for that field
569	*
570	* Return code:
571	* -1 if the key is not recognized
572	* -2 if the value is not recognized
573	* -3 if the value has the wrong type for the key
574	* 0 otherwise (i.e., success)
575	*/
576	int32_t params_set_field(param_t parameters, const char key, const char *value) {	14✔
577	int32_t k, r;
578	int32_t z;
579	double x;
580
581	z = 0; // to prevent GCC warning	14✔
582
583	k = parse_as_keyword(key, param_key_names, param_code, NUM_PARAM_KEYS);	14✔
584	switch (k) {	14✔
585	case PARAM_FAST_RESTART:	×
586	r = set_bool_param(value, &parameters->fast_restart);	×
587	break;	×
588
589	case PARAM_C_THRESHOLD:	×
590	r = set_int32_param(value, &z, 1, INT32_MAX);	×
591	if (r == 0) {	×
592	parameters->c_threshold = (uint32_t) z;	×
593	}
594	break;	×
595
596	case PARAM_D_THRESHOLD:	×
597	r = set_int32_param(value, &z, 1, INT32_MAX);	×
598	if (r == 0) {	×
599	parameters->d_threshold = (uint32_t) z;	×
600	}
601	break;	×
602
603	case PARAM_C_FACTOR:	×
604	r = set_double_param(value, &parameters->c_factor, 1.0, DBL_MAX);	×
605	break;	×
606
607	case PARAM_D_FACTOR:	×
608	r = set_double_param(value, &parameters->d_factor, 1.0, DBL_MAX);	×
609	break;	×
610
611	case PARAM_DELEGATE:	14✔
612	r = set_sat_delegate_param(value, &parameters->delegate);	14✔
613	break;	14✔
614
615	case PARAM_R_THRESHOLD:	×
616	r = set_int32_param(value, &z, 1, INT32_MAX);	×
617	if (r == 0) {	×
618	parameters->r_threshold = z;	×
619	}
620	break;	×
621
622	case PARAM_R_FRACTION:	×
623	r = set_double_param(value, &parameters->r_fraction, 0.0, 1.0);	×
624	break;	×
625
626	case PARAM_R_FACTOR:	×
627	r = set_double_param(value, &parameters->r_factor, 1.0, DBL_MAX);	×
628	break;	×
629
630	case PARAM_VAR_DECAY:	×
631	r = set_double_param(value, &parameters->var_decay, 0.0, 1.0);	×
632	break;	×
633
634	case PARAM_RANDOMNESS:	×
635	r = set_double_param(value, &x, 0.0, 1.0);	×
636	if (r == 0) {	×
637	parameters->randomness = (float) x;	×
638	}
639	break;	×
640
641	case PARAM_RANDOM_SEED:	×
642	r = set_uint32_param(value, &parameters->random_seed);	×
643	break;	×
644
645	case PARAM_BRANCHING:	×
646	r = set_branching_param(value, &parameters->branching);	×
647	break;	×
648
649	case PARAM_CLAUSE_DECAY:	×
650	r = set_double_param(value, &x, 0.0, 1.0);	×
651	if (r == 0) {	×
652	parameters->clause_decay = (float) x;	×
653	}
654	break;	×
655
656	case PARAM_CACHE_TCLAUSES:	×
657	r = set_bool_param(value, &parameters->cache_tclauses);	×
658	break;	×
659
660	case PARAM_TCLAUSE_SIZE:	×
661	r = set_int32_param(value, &z, 2, INT32_MAX);	×
662	if (r == 0) {	×
663	parameters->tclause_size = (uint32_t) z;	×
664	}
665	break;	×
666
667	case PARAM_DYN_ACK:	×
668	r = set_bool_param(value, &parameters->use_dyn_ack);	×
669	break;	×
670
671	case PARAM_DYN_BOOL_ACK:	×
672	r = set_bool_param(value, &parameters->use_bool_dyn_ack);	×
673	break;	×
674
675	case PARAM_OPTIMISTIC_FCHECK:	×
676	r = set_bool_param(value, &parameters->use_optimistic_fcheck);	×
677	break;	×
678
679	case PARAM_MAX_ACK:	×
680	r = set_int32_param(value, &z, 1, INT32_MAX);	×
681	if (r == 0) {	×
682	parameters->max_ackermann = (uint32_t) z;	×
683	}
684	break;	×
685
686	case PARAM_MAX_BOOL_ACK:	×
687	r = set_int32_param(value, &z, 1, INT32_MAX);	×
688	if (r == 0) {	×
689	parameters->max_boolackermann = (uint32_t) z;	×
690	}
691	break;	×
692
693	case PARAM_AUX_EQ_QUOTA:	×
694	r = set_int32_param(value, &z, 1, INT32_MAX);	×
695	if (r == 0) {	×
696	parameters->aux_eq_quota = (uint32_t) z;	×
697	}
698	break;	×
699
700	case PARAM_AUX_EQ_RATIO:	×
701	r = set_double_param(value, &x, 0.0, (double) FLT_MAX);	×
702	if (r == 0) {	×
703	if (x > 0.0) {	×
704	parameters->aux_eq_ratio = (float) x;	×
705	} else {
706	r = -2;	×
707	}
708	}
709	break;	×
710
711	case PARAM_DYN_ACK_THRESHOLD:	×
712	r = set_int32_param(value, &z, 1, (int32_t) UINT16_MAX);	×
713	if (r == 0) {	×
714	parameters->dyn_ack_threshold = (uint16_t) z;	×
715	}
716	break;	×
717
718
719	case PARAM_DYN_BOOL_ACK_THRESHOLD:	×
720	r = set_int32_param(value, &z, 1, (int32_t) UINT16_MAX);	×
721	if (r == 0) {	×
722	parameters->dyn_bool_ack_threshold = (uint16_t) z;	×
723	}
724	break;	×
725
726	case PARAM_MAX_INTERFACE_EQS:	×
727	r = set_int32_param(value, &z, 1, INT32_MAX);	×
728	if (r == 0) {	×
729	parameters->max_interface_eqs = (uint32_t) z;	×
730	}
731	break;	×
732
733	case PARAM_SIMPLEX_PROP:	×
734	r = set_bool_param(value, &parameters->use_simplex_prop);	×
735	break;	×
736
737	case PARAM_SIMPLEX_ADJUST:	×
738	r = set_bool_param(value, &parameters->adjust_simplex_model);	×
739	break;	×
740
741	case PARAM_SIMPLEX_ICHECK:	×
742	r = set_bool_param(value, &parameters->integer_check);	×
743	break;	×
744
745	case PARAM_PROP_THRESHOLD:	×
746	r = set_int32_param(value, &z, 0, INT32_MAX);	×
747	if (r == 0) {	×
748	parameters->max_prop_row_size = (uint32_t) z;	×
749	}
750	break;	×
751
752	case PARAM_BLAND_THRESHOLD:	×
753	r = set_int32_param(value, &z, 1, INT32_MAX);	×
754	if (r == 0) {	×
755	parameters->bland_threshold = (uint32_t) z;	×
756	}
757	break;	×
758
759	case PARAM_ICHECK_PERIOD:	×
760	r = set_int32_param(value, &parameters->integer_check_period, 1, INT32_MAX);	×
761	break;	×
762
763	case PARAM_MAX_UPDATE_CONFLICTS:	×
764	r = set_int32_param(value, &z, 1, INT32_MAX);	×
765	if (r == 0) {	×
766	parameters->max_update_conflicts = (uint32_t) z;	×
767	}
768	break;	×
769
770	case PARAM_MAX_EXTENSIONALITY:	×
771	r = set_int32_param(value, &z, 1, INT32_MAX);	×
772	if (r == 0) {	×
773	parameters->max_extensionality = (uint32_t) z;	×
774	}
775	break;	×
776
777	default:	×
778	assert(k == -1);
779	r = -1;	×
780	break;	×
781	}
782
783	return r;	14✔
784	}
785
786
787	/*
788	* Utility function: so that yices and yices_smt2
789	* can keep a copy of the initial random seed
790	*/
791	uint32_t params_default_random_seed(void) {	×
792	return DEFAULT_RANDOM_SEED;	×
793	}

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