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

47.11

/src/frontend/common/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/>.
 */

#if defined(CYGWIN) || defined(MINGW)
#ifndef __YICES_DLLSPEC__
#define __YICES_DLLSPEC__ __declspec(dllexport)
#endif
#endif

#include <assert.h>

#include "frontend/common/parameters.h"
#include "utils/string_utils.h"

/*
 * Parameter names: using the Yices conventions
 * - for the smt2 front end, you prefix these names with ':yices-'
 */
static const char * const param_names[NUM_PARAMETERS] = {
  "arith-elim",
  "aux-eq-quota",
  "aux-eq-ratio",
  "bland-threshold",
  "branching",
  "bvarith-elim",
  "c-factor",
  "c-threshold",
  "cache-tclauses",
  "clause-decay",
  "d-factor",
  "d-threshold",
  "dyn-ack",
  "dyn-ack-threshold",
  "dyn-bool-ack",
  "dyn-bool-ack-threshold",
  "eager-lemmas",
  "ef-flatten-iff",
  "ef-flatten-ite",
  "ef-gen-mode",
  "ef-max-iters",
  "ef-max-lemmas-per-round",
  "ef-max-samples",
  "ematch-cnstr-alpha",
  "ematch-cnstr-epsilon",
  "ematch-cnstr-mode",
  "ematch-en",
  "ematch-inst-per-round",
  "ematch-inst-per-search",
  "ematch-inst-total",
  "ematch-rounds-per-search",
  "ematch-search-total",
  "ematch-term-alpha",
  "ematch-term-epsilon",
  "ematch-term-mode",
  "ematch-trial-fapps",
  "ematch-trial-fdepth",
  "ematch-trial-matches",
  "ematch-trial-vdepth",
  "fast-restarts",
  "flatten",
  "icheck",
  "icheck-period",
  "keep-ite",
  "learn-eq",
  "max-ack",
  "max-bool-ack",
  "max-extensionality",
  "max-interface-eqs",
  "max-update-conflicts",
  "mcsat-bv-var-size",
  "mcsat-na-bound",
  "mcsat-na-bound-max",
  "mcsat-na-bound-min",
  "mcsat-na-mgcd",
  "mcsat-na-nlsat",
  "mcsat-partial-restart",
  "mcsat-rand-dec-freq",
  "mcsat-rand-dec-seed",
  "mcsat-supplement-check",
  "mcsat-var-order",
  "optimistic-fcheck",
  "prop-threshold",
  "r-factor",
  "r-fraction",
  "r-threshold",
  "random-seed",
  "randomness",
  "simplex-adjust",
  "simplex-prop",
  "tclause-size",
  "var-decay",
  "var-elim",
};

// corresponding parameter codes in order
static const yices_param_t param_code[NUM_PARAMETERS] = {
  PARAM_ARITH_ELIM,
  PARAM_AUX_EQ_QUOTA,
  PARAM_AUX_EQ_RATIO,
  PARAM_BLAND_THRESHOLD,
  PARAM_BRANCHING,
  PARAM_BVARITH_ELIM,
  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_EAGER_LEMMAS,
  PARAM_EF_FLATTEN_IFF,
  PARAM_EF_FLATTEN_ITE,
  PARAM_EF_GEN_MODE,
  PARAM_EF_MAX_ITERS,
  PARAM_EF_MAX_LEMMAS_PER_ROUND,
  PARAM_EF_MAX_SAMPLES,
  PARAM_EMATCH_CNSTR_ALPHA,
  PARAM_EMATCH_CNSTR_EPSILON,
  PARAM_EMATCH_CNSTR_MODE,
  PARAM_EMATCH_EN,
  PARAM_EMATCH_INST_PER_ROUND,
  PARAM_EMATCH_INST_PER_SEARCH,
  PARAM_EMATCH_INST_TOTAL,
  PARAM_EMATCH_ROUNDS_PER_SEARCH,
  PARAM_EMATCH_SEARCH_TOTAL,
  PARAM_EMATCH_TERM_ALPHA,
  PARAM_EMATCH_TERM_EPSILON,
  PARAM_EMATCH_TERM_MODE,
  PARAM_EMATCH_TRIAL_FAPPS,
  PARAM_EMATCH_TRIAL_FDEPTH,
  PARAM_EMATCH_TRIAL_MATCHES,
  PARAM_EMATCH_TRIAL_VDEPTH,
  PARAM_FAST_RESTARTS,
  PARAM_FLATTEN,
  PARAM_ICHECK,
  PARAM_ICHECK_PERIOD,
  PARAM_KEEP_ITE,
  PARAM_LEARN_EQ,
  PARAM_MAX_ACK,
  PARAM_MAX_BOOL_ACK,
  PARAM_MAX_EXTENSIONALITY,
  PARAM_MAX_INTERFACE_EQS,
  PARAM_MAX_UPDATE_CONFLICTS,
  PARAM_MCSAT_BV_VAR_SIZE,
  PARAM_MCSAT_NA_BOUND,
  PARAM_MCSAT_NA_BOUND_MAX,
  PARAM_MCSAT_NA_BOUND_MIN,
  PARAM_MCSAT_NA_MGCD,
  PARAM_MCSAT_NA_NLSAT,
  PARAM_MCSAT_PARTIAL_RESTART,
  PARAM_MCSAT_RAND_DEC_FREQ,
  PARAM_MCSAT_RAND_DEC_SEED,
  PARAM_MCSAT_SUPPLEMENT_CHECK,
  PARAM_MCSAT_VAR_ORDER,
  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,
  PARAM_VAR_ELIM,
};



/*
 * Names of each branching mode (in lexicographic order)
 */
#define NUM_BRANCHING_MODES 6

static const char * const branching_modes[NUM_BRANCHING_MODES] = {
  "default",
  "negative",
  "positive",
  "th-neg",
  "th-pos",
  "theory",
};

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

/*
 * Supplementary MCSAT check modes
 */
#define NUM_MCSAT_SUPPLEMENT_CHECK_MODES 2

static const char * const mcsat_supplement_check_modes[NUM_MCSAT_SUPPLEMENT_CHECK_MODES] = {
  "both",
  "final-only",
};

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



/*
 * Names of the generalization modes for the EF solver
 */
#define NUM_EF_GEN_MODES 4

static const char * const ef_gen_modes[NUM_EF_GEN_MODES] = {
  "auto",
  "none",
  "projection",
  "substitution",
};

static const ef_gen_option_t ef_gen_code[NUM_EF_GEN_MODES] = {
  EF_GEN_AUTO_OPTION,
  EF_NOGEN_OPTION,
  EF_GEN_BY_PROJ_OPTION,
  EF_GEN_BY_SUBST_OPTION,
};



/*
 * Names of the ematch modes for the quant solver
 */
#define NUM_EMATCH_MODES 3

static const char * const ematch_modes[NUM_EMATCH_MODES] = {
  "all",
  "epsilongreedy",
  "random",
};

static const iterate_kind_t ematch_mode_code[NUM_EMATCH_MODES] = {
  ITERATE_ALL,
  ITERATE_EPSILONGREEDY,
  ITERATE_RANDOM,
};


/*
 * Tables for converting parameter id to parameter name
 * and branching code to branching name. One more table
 * for converting from EF generalization codes to strings.
 */
const char *param2string[NUM_PARAMETERS];
const char *branching2string[NUM_BRANCHING_MODES];
const char *efgen2string[NUM_EF_GEN_MODES];
const char *ematchmode2string[NUM_EMATCH_MODES];


/*
 * Initialize the table [parameter id --> string]
 * and [branching mode --> string]
 * and [ef gen code --> string]
 */
void init_parameter_name_table(void) {
  uint32_t i, j;
  const char *name;

  for (i=0; i<NUM_PARAMETERS; i++) {
    name = param_names[i];
    j = param_code[i];
    param2string[j] = name;
  }

  for (i=0; i<NUM_BRANCHING_MODES; i++) {
    name = branching_modes[i];
    j = branching_code[i];
    branching2string[j] = name;
  }

  for (i=0; i<NUM_EF_GEN_MODES; i++) {
    name = ef_gen_modes[i];
    j = ef_gen_code[i];
    efgen2string[j] = name;
  }

  for (i=0; i<NUM_EMATCH_MODES; i++) {
    name = ematch_modes[i];
    j = ematch_mode_code[i];
    ematchmode2string[j] = name;
  }
}


/*
 * Search for a parameter of the given name
 * - use binary search in the param_names table
 * - return PARAM_UNKNOWN if there's no parameter with that name
 */
yices_param_t find_param(const char *name) {
  int32_t i;
  i = binary_search_string(name, param_names, NUM_PARAMETERS);
  if (i >= 0) {
    assert(i < NUM_PARAMETERS);
    return param_code[i];
  } else {
    return PARAM_UNKNOWN;
  }
}


/*
 * Convert a parameter value to boolean, int32, float, etc.
 * - name = parameter name, used for error reporting.
 * - return true if the conversion works
 * - return false otherwise and returns an error message/string in *reason
 */
bool param_val_to_bool(const char *name, const param_val_t *v, bool *value, char **reason) {
  bool code;

  code = true;
  if (v->tag == PARAM_VAL_FALSE) {
    *value = false;
  } else if (v->tag == PARAM_VAL_TRUE) {
    *value = true;
  } else {
    *reason = "boolean required";
    code = false;
  }
  return code;
}

bool param_val_to_int32(const char *name, const param_val_t *v, int32_t *value, char **reason) {
  rational_t *q;

  if (v->tag == PARAM_VAL_RATIONAL) {
    q = v->val.rational;
    if (q_is_smallint(q)) {
      *value = q_get_smallint(q);
      return true;
    } else if (q_is_integer(q)) {
      *reason = "integer overflow";
      return false;
    }
    // if q is a rational: same error as not a number
  }

  *reason = "integer required";

  return false;
}

bool param_val_to_pos32(const char *name, const param_val_t *v, int32_t *value, char **reason) {
  if (param_val_to_int32(name, v, value, reason)) {
    if (*value > 0) return true;
    *reason = "must be positive";
  }
  return false;
}

bool param_val_to_pos16(const char *name, const param_val_t *v, int32_t *value, char **reason) {
  if (param_val_to_int32(name, v, value, reason)) {
    if (1 <= *value && *value <= UINT16_MAX) {
      return true;
    }
    *reason = "must be between 1 and 2^16";
  }
  return false;
}

bool param_val_to_nonneg32(const char *name, const param_val_t *v, int32_t *value, char **reason) {
  if (param_val_to_int32(name, v, value, reason)) {
    if (*value >= 0) return true;
    *reason = "cannot be negative";
  }
  return false;
}

bool param_val_to_float(const char *name, const param_val_t *v, double *value, char **reason) {
  mpq_t aux;

  if (v->tag == PARAM_VAL_RATIONAL) {
    mpq_init(aux);
    q_get_mpq(v->val.rational, aux);
    /*
     * NOTE: the GMP documentation says that conversion to double
     * may raise a hardware trap (overflow, underflow, etc.) on
     * some systems. We ignore this here.
     */
    *value = mpq_get_d(aux);
    mpq_clear(aux);
    return true;
  } else {
    *reason = "number required";
    return false;
  }
}

bool param_val_to_posfloat(const char *name, const param_val_t *v, double *value, char **reason) {
  if (param_val_to_float(name, v, value, reason)) {
    if (*value > 0.0) return true;
    *reason = "must be positive";
  }
  return false;
}

// ratio: number between 0 and 1 (inclusive)
bool param_val_to_ratio(const char *name, const param_val_t *v, double *value, char **reason) {
  if (param_val_to_float(name, v, value, reason)) {
    if (0 <= *value && *value <= 1.0) return true;
    *reason = "must be between 0 and 1";
  }
  return false;
}

// factor: must be at least 1
bool param_val_to_factor(const char *name, const param_val_t *v, double *value, char **reason) {
  if (param_val_to_float(name, v, value, reason)) {
    if (1.0 <= *value) return true;
    *reason = "must be at least 1";
  }
  return false;
}

// terms
bool param_val_to_terms(const char *name, const param_val_t *v, ivector_t **value, char **reason) {
  if (v->tag == PARAM_VAL_TERMS) {
    *value = v->val.terms;
    return true;
  }
  *reason = "list of variables required";
  return false;
}

/*
 * Special case: branching mode
 * - allowed modes are 'default' 'positive' 'negative' 'theory' 'th-neg' 'th-pos'
 */
bool param_val_to_branching(const char *name, const param_val_t *v, branch_t *value, char **reason) {
  int32_t i;

  if (v->tag == PARAM_VAL_SYMBOL) {
    i = binary_search_string(v->val.symbol, branching_modes, NUM_BRANCHING_MODES);
    if (i >= 0) {
      assert(i < NUM_BRANCHING_MODES);
      *value = branching_code[i];
      return true;
    }
  }
  *reason = "must be one of 'default' 'positive' 'negative' 'theory' 'th-neg' 'th-pos";

  return false;
}

/*
 * Supplementary MCSAT check mode
 * - allowed modes are "both" and "final-only"
 */
bool param_val_to_mcsat_supplement_check(const char *name, const param_val_t *v,
                                         mcsat_supplement_check_t *value, char **reason) {
  int32_t i;

  if (v->tag == PARAM_VAL_SYMBOL) {
    i = binary_search_string(v->val.symbol, mcsat_supplement_check_modes,
                             NUM_MCSAT_SUPPLEMENT_CHECK_MODES);
    if (i >= 0) {
      assert(i < NUM_MCSAT_SUPPLEMENT_CHECK_MODES);
      *value = mcsat_supplement_check_code[i];
      return true;
    }
  }
  *reason = "must be one of 'both' 'final-only'";

  return false;
}



/*
 * EF generalization mode
 * - allowed modes are "none" or "substitution" or "projection" or "auto"
 * - we use a general implementation so that we can add more modes later
 */
bool param_val_to_genmode(const char *name, const param_val_t *v, ef_gen_option_t *value, char **reason) {
  int32_t i;

  if (v->tag == PARAM_VAL_SYMBOL) {
    i = binary_search_string(v->val.symbol, ef_gen_modes, NUM_EF_GEN_MODES);
    if (i >= 0) {
      assert(i < NUM_EF_GEN_MODES);
      *value = ef_gen_code[i];
      return true;
    }
  }
  *reason = "must be one of 'none' 'substitution' 'projection' 'auto'";

  return false;
}


/*
 * EMATCH mode
 * - allowed modes are "all" or "random" or "epsilongreedy"
 * - we use a general implementation so that we can add more modes later
 */
bool param_val_to_ematchmode(const char *name, const param_val_t *v, iterate_kind_t *value, char **reason) {
  int32_t i;

  if (v->tag == PARAM_VAL_SYMBOL) {
    i = binary_search_string(v->val.symbol, ematch_modes, NUM_EMATCH_MODES);
    if (i >= 0) {
      assert(i < NUM_EMATCH_MODES);
      *value = ematch_mode_code[i];
      return true;
    }
  }
  *reason = "must be one of 'all' 'random' 'epsilongreedy'";

  return false;
}

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	#if defined(CYGWIN) \|\| defined(MINGW)
20	#ifndef __YICES_DLLSPEC__
21	#define __YICES_DLLSPEC__ __declspec(dllexport)
22	#endif
23	#endif
24
25	#include <assert.h>
26
27	#include "frontend/common/parameters.h"
28	#include "utils/string_utils.h"
29
30	/*
31	* Parameter names: using the Yices conventions
32	* - for the smt2 front end, you prefix these names with ':yices-'
33	*/
34	static const char * const param_names[NUM_PARAMETERS] = {
35	"arith-elim",
36	"aux-eq-quota",
37	"aux-eq-ratio",
38	"bland-threshold",
39	"branching",
40	"bvarith-elim",
41	"c-factor",
42	"c-threshold",
43	"cache-tclauses",
44	"clause-decay",
45	"d-factor",
46	"d-threshold",
47	"dyn-ack",
48	"dyn-ack-threshold",
49	"dyn-bool-ack",
50	"dyn-bool-ack-threshold",
51	"eager-lemmas",
52	"ef-flatten-iff",
53	"ef-flatten-ite",
54	"ef-gen-mode",
55	"ef-max-iters",
56	"ef-max-lemmas-per-round",
57	"ef-max-samples",
58	"ematch-cnstr-alpha",
59	"ematch-cnstr-epsilon",
60	"ematch-cnstr-mode",
61	"ematch-en",
62	"ematch-inst-per-round",
63	"ematch-inst-per-search",
64	"ematch-inst-total",
65	"ematch-rounds-per-search",
66	"ematch-search-total",
67	"ematch-term-alpha",
68	"ematch-term-epsilon",
69	"ematch-term-mode",
70	"ematch-trial-fapps",
71	"ematch-trial-fdepth",
72	"ematch-trial-matches",
73	"ematch-trial-vdepth",
74	"fast-restarts",
75	"flatten",
76	"icheck",
77	"icheck-period",
78	"keep-ite",
79	"learn-eq",
80	"max-ack",
81	"max-bool-ack",
82	"max-extensionality",
83	"max-interface-eqs",
84	"max-update-conflicts",
85	"mcsat-bv-var-size",
86	"mcsat-na-bound",
87	"mcsat-na-bound-max",
88	"mcsat-na-bound-min",
89	"mcsat-na-mgcd",
90	"mcsat-na-nlsat",
91	"mcsat-partial-restart",
92	"mcsat-rand-dec-freq",
93	"mcsat-rand-dec-seed",
94	"mcsat-supplement-check",
95	"mcsat-var-order",
96	"optimistic-fcheck",
97	"prop-threshold",
98	"r-factor",
99	"r-fraction",
100	"r-threshold",
101	"random-seed",
102	"randomness",
103	"simplex-adjust",
104	"simplex-prop",
105	"tclause-size",
106	"var-decay",
107	"var-elim",
108	};
109
110	// corresponding parameter codes in order
111	static const yices_param_t param_code[NUM_PARAMETERS] = {
112	PARAM_ARITH_ELIM,
113	PARAM_AUX_EQ_QUOTA,
114	PARAM_AUX_EQ_RATIO,
115	PARAM_BLAND_THRESHOLD,
116	PARAM_BRANCHING,
117	PARAM_BVARITH_ELIM,
118	PARAM_C_FACTOR,
119	PARAM_C_THRESHOLD,
120	PARAM_CACHE_TCLAUSES,
121	PARAM_CLAUSE_DECAY,
122	PARAM_D_FACTOR,
123	PARAM_D_THRESHOLD,
124	PARAM_DYN_ACK,
125	PARAM_DYN_ACK_THRESHOLD,
126	PARAM_DYN_BOOL_ACK,
127	PARAM_DYN_BOOL_ACK_THRESHOLD,
128	PARAM_EAGER_LEMMAS,
129	PARAM_EF_FLATTEN_IFF,
130	PARAM_EF_FLATTEN_ITE,
131	PARAM_EF_GEN_MODE,
132	PARAM_EF_MAX_ITERS,
133	PARAM_EF_MAX_LEMMAS_PER_ROUND,
134	PARAM_EF_MAX_SAMPLES,
135	PARAM_EMATCH_CNSTR_ALPHA,
136	PARAM_EMATCH_CNSTR_EPSILON,
137	PARAM_EMATCH_CNSTR_MODE,
138	PARAM_EMATCH_EN,
139	PARAM_EMATCH_INST_PER_ROUND,
140	PARAM_EMATCH_INST_PER_SEARCH,
141	PARAM_EMATCH_INST_TOTAL,
142	PARAM_EMATCH_ROUNDS_PER_SEARCH,
143	PARAM_EMATCH_SEARCH_TOTAL,
144	PARAM_EMATCH_TERM_ALPHA,
145	PARAM_EMATCH_TERM_EPSILON,
146	PARAM_EMATCH_TERM_MODE,
147	PARAM_EMATCH_TRIAL_FAPPS,
148	PARAM_EMATCH_TRIAL_FDEPTH,
149	PARAM_EMATCH_TRIAL_MATCHES,
150	PARAM_EMATCH_TRIAL_VDEPTH,
151	PARAM_FAST_RESTARTS,
152	PARAM_FLATTEN,
153	PARAM_ICHECK,
154	PARAM_ICHECK_PERIOD,
155	PARAM_KEEP_ITE,
156	PARAM_LEARN_EQ,
157	PARAM_MAX_ACK,
158	PARAM_MAX_BOOL_ACK,
159	PARAM_MAX_EXTENSIONALITY,
160	PARAM_MAX_INTERFACE_EQS,
161	PARAM_MAX_UPDATE_CONFLICTS,
162	PARAM_MCSAT_BV_VAR_SIZE,
163	PARAM_MCSAT_NA_BOUND,
164	PARAM_MCSAT_NA_BOUND_MAX,
165	PARAM_MCSAT_NA_BOUND_MIN,
166	PARAM_MCSAT_NA_MGCD,
167	PARAM_MCSAT_NA_NLSAT,
168	PARAM_MCSAT_PARTIAL_RESTART,
169	PARAM_MCSAT_RAND_DEC_FREQ,
170	PARAM_MCSAT_RAND_DEC_SEED,
171	PARAM_MCSAT_SUPPLEMENT_CHECK,
172	PARAM_MCSAT_VAR_ORDER,
173	PARAM_OPTIMISTIC_FCHECK,
174	PARAM_PROP_THRESHOLD,
175	PARAM_R_FACTOR,
176	PARAM_R_FRACTION,
177	PARAM_R_THRESHOLD,
178	PARAM_RANDOM_SEED,
179	PARAM_RANDOMNESS,
180	PARAM_SIMPLEX_ADJUST,
181	PARAM_SIMPLEX_PROP,
182	PARAM_TCLAUSE_SIZE,
183	PARAM_VAR_DECAY,
184	PARAM_VAR_ELIM,
185	};
186
187
188
189	/*
190	* Names of each branching mode (in lexicographic order)
191	*/
192	#define NUM_BRANCHING_MODES 6
193
194	static const char * const branching_modes[NUM_BRANCHING_MODES] = {
195	"default",
196	"negative",
197	"positive",
198	"th-neg",
199	"th-pos",
200	"theory",
201	};
202
203	static const branch_t branching_code[NUM_BRANCHING_MODES] = {
204	BRANCHING_DEFAULT,
205	BRANCHING_NEGATIVE,
206	BRANCHING_POSITIVE,
207	BRANCHING_TH_NEG,
208	BRANCHING_TH_POS,
209	BRANCHING_THEORY,
210	};
211
212	/*
213	* Supplementary MCSAT check modes
214	*/
215	#define NUM_MCSAT_SUPPLEMENT_CHECK_MODES 2
216
217	static const char * const mcsat_supplement_check_modes[NUM_MCSAT_SUPPLEMENT_CHECK_MODES] = {
218	"both",
219	"final-only",
220	};
221
222	static const mcsat_supplement_check_t mcsat_supplement_check_code[NUM_MCSAT_SUPPLEMENT_CHECK_MODES] = {
223	MCSAT_SUPPLEMENT_CHECK_BOTH,
224	MCSAT_SUPPLEMENT_CHECK_FINAL_ONLY,
225	};
226
227
228
229	/*
230	* Names of the generalization modes for the EF solver
231	*/
232	#define NUM_EF_GEN_MODES 4
233
234	static const char * const ef_gen_modes[NUM_EF_GEN_MODES] = {
235	"auto",
236	"none",
237	"projection",
238	"substitution",
239	};
240
241	static const ef_gen_option_t ef_gen_code[NUM_EF_GEN_MODES] = {
242	EF_GEN_AUTO_OPTION,
243	EF_NOGEN_OPTION,
244	EF_GEN_BY_PROJ_OPTION,
245	EF_GEN_BY_SUBST_OPTION,
246	};
247
248
249
250	/*
251	* Names of the ematch modes for the quant solver
252	*/
253	#define NUM_EMATCH_MODES 3
254
255	static const char * const ematch_modes[NUM_EMATCH_MODES] = {
256	"all",
257	"epsilongreedy",
258	"random",
259	};
260
261	static const iterate_kind_t ematch_mode_code[NUM_EMATCH_MODES] = {
262	ITERATE_ALL,
263	ITERATE_EPSILONGREEDY,
264	ITERATE_RANDOM,
265	};
266
267
268	/*
269	* Tables for converting parameter id to parameter name
270	* and branching code to branching name. One more table
271	* for converting from EF generalization codes to strings.
272	*/
273	const char *param2string[NUM_PARAMETERS];
274	const char *branching2string[NUM_BRANCHING_MODES];
275	const char *efgen2string[NUM_EF_GEN_MODES];
276	const char *ematchmode2string[NUM_EMATCH_MODES];
277
278
279	/*
280	* Initialize the table [parameter id --> string]
281	* and [branching mode --> string]
282	* and [ef gen code --> string]
283	*/
284	void init_parameter_name_table(void) {	1,671✔
285	uint32_t i, j;
286	const char *name;
287
288	for (i=0; i<NUM_PARAMETERS; i++) {	123,654✔
289	name = param_names[i];	121,983✔
290	j = param_code[i];	121,983✔
291	param2string[j] = name;	121,983✔
292	}
293
294	for (i=0; i<NUM_BRANCHING_MODES; i++) {	11,697✔
295	name = branching_modes[i];	10,026✔
296	j = branching_code[i];	10,026✔
297	branching2string[j] = name;	10,026✔
298	}
299
300	for (i=0; i<NUM_EF_GEN_MODES; i++) {	8,355✔
301	name = ef_gen_modes[i];	6,684✔
302	j = ef_gen_code[i];	6,684✔
303	efgen2string[j] = name;	6,684✔
304	}
305
306	for (i=0; i<NUM_EMATCH_MODES; i++) {	6,684✔
307	name = ematch_modes[i];	5,013✔
308	j = ematch_mode_code[i];	5,013✔
309	ematchmode2string[j] = name;	5,013✔
310	}
311	}	1,671✔
312
313
314	/*
315	* Search for a parameter of the given name
316	* - use binary search in the param_names table
317	* - return PARAM_UNKNOWN if there's no parameter with that name
318	*/
319	yices_param_t find_param(const char *name) {	29✔
320	int32_t i;
321	i = binary_search_string(name, param_names, NUM_PARAMETERS);	29✔
322	if (i >= 0) {	29✔
323	assert(i < NUM_PARAMETERS);
324	return param_code[i];	29✔
325	} else {
326	return PARAM_UNKNOWN;	×
327	}
328	}
329
330
331	/*
332	* Convert a parameter value to boolean, int32, float, etc.
333	* - name = parameter name, used for error reporting.
334	* - return true if the conversion works
335	* - return false otherwise and returns an error message/string in *reason
336	*/
337	bool param_val_to_bool(const char name, const param_val_t v, bool value, char *reason) {	9✔
338	bool code;
339
340	code = true;	9✔
341	if (v->tag == PARAM_VAL_FALSE) {	9✔
342	*value = false;	4✔
343	} else if (v->tag == PARAM_VAL_TRUE) {	5✔
344	*value = true;	5✔
345	} else {
346	*reason = "boolean required";	×
347	code = false;	×
348	}
349	return code;	9✔
350	}
351
352	bool param_val_to_int32(const char name, const param_val_t v, int32_t value, char *reason) {	11✔
353	rational_t *q;
354
355	if (v->tag == PARAM_VAL_RATIONAL) {	11✔
356	q = v->val.rational;	11✔
357	if (q_is_smallint(q)) {	11✔
358	*value = q_get_smallint(q);	11✔
359	return true;	11✔
360	} else if (q_is_integer(q)) {	×
361	*reason = "integer overflow";	×
362	return false;	×
363	}
364	// if q is a rational: same error as not a number
365	}
366
367	*reason = "integer required";	×
368
369	return false;	×
370	}
371
372	bool param_val_to_pos32(const char name, const param_val_t v, int32_t value, char *reason) {	9✔
373	if (param_val_to_int32(name, v, value, reason)) {	9✔
374	if (*value > 0) return true;	9✔
375	*reason = "must be positive";	×
376	}
377	return false;	×
378	}
379
380	bool param_val_to_pos16(const char name, const param_val_t v, int32_t value, char *reason) {	×
381	if (param_val_to_int32(name, v, value, reason)) {	×
382	if (1 <= value && value <= UINT16_MAX) {	×
383	return true;	×
384	}
385	*reason = "must be between 1 and 2^16";	×
386	}
387	return false;	×
388	}
389
390	bool param_val_to_nonneg32(const char name, const param_val_t v, int32_t value, char *reason) {	2✔
391	if (param_val_to_int32(name, v, value, reason)) {	2✔
392	if (*value >= 0) return true;	2✔
393	*reason = "cannot be negative";	×
394	}
395	return false;	×
396	}
397
398	bool param_val_to_float(const char name, const param_val_t v, double value, char *reason) {	×
399	mpq_t aux;
400
401	if (v->tag == PARAM_VAL_RATIONAL) {	×
402	mpq_init(aux);	×
403	q_get_mpq(v->val.rational, aux);	×
404	/*
405	* NOTE: the GMP documentation says that conversion to double
406	* may raise a hardware trap (overflow, underflow, etc.) on
407	* some systems. We ignore this here.
408	*/
409	*value = mpq_get_d(aux);	×
410	mpq_clear(aux);	×
411	return true;	×
412	} else {
413	*reason = "number required";	×
414	return false;	×
415	}
416	}
417
418	bool param_val_to_posfloat(const char name, const param_val_t v, double value, char *reason) {	×
419	if (param_val_to_float(name, v, value, reason)) {	×
420	if (*value > 0.0) return true;	×
421	*reason = "must be positive";	×
422	}
423	return false;	×
424	}
425
426	// ratio: number between 0 and 1 (inclusive)
427	bool param_val_to_ratio(const char name, const param_val_t v, double value, char *reason) {	×
428	if (param_val_to_float(name, v, value, reason)) {	×
429	if (0 <= value && value <= 1.0) return true;	×
430	*reason = "must be between 0 and 1";	×
431	}
432	return false;	×
433	}
434
435	// factor: must be at least 1
436	bool param_val_to_factor(const char name, const param_val_t v, double value, char *reason) {	×
437	if (param_val_to_float(name, v, value, reason)) {	×
438	if (1.0 <= *value) return true;	×
439	*reason = "must be at least 1";	×
440	}
441	return false;	×
442	}
443
444	// terms
445	bool param_val_to_terms(const char name, const param_val_t v, ivector_t value, char reason) {	1✔
446	if (v->tag == PARAM_VAL_TERMS) {	1✔
447	*value = v->val.terms;	1✔
448	return true;	1✔
449	}
450	*reason = "list of variables required";	×
451	return false;	×
452	}
453
454	/*
455	* Special case: branching mode
456	* - allowed modes are 'default' 'positive' 'negative' 'theory' 'th-neg' 'th-pos'
457	*/
458	bool param_val_to_branching(const char name, const param_val_t v, branch_t value, char *reason) {	4✔
459	int32_t i;
460
461	if (v->tag == PARAM_VAL_SYMBOL) {	4✔
462	i = binary_search_string(v->val.symbol, branching_modes, NUM_BRANCHING_MODES);	4✔
463	if (i >= 0) {	4✔
464	assert(i < NUM_BRANCHING_MODES);
465	*value = branching_code[i];	4✔
466	return true;	4✔
467	}
468	}
469	*reason = "must be one of 'default' 'positive' 'negative' 'theory' 'th-neg' 'th-pos";	×
470
471	return false;	×
472	}
473
474	/*
475	* Supplementary MCSAT check mode
476	* - allowed modes are "both" and "final-only"
477	*/
NEW 478	bool param_val_to_mcsat_supplement_check(const char name, const param_val_t v,	×
479	mcsat_supplement_check_t value, char *reason) {
480	int32_t i;
481
NEW 482	if (v->tag == PARAM_VAL_SYMBOL) {	×
NEW 483	i = binary_search_string(v->val.symbol, mcsat_supplement_check_modes,	×
484	NUM_MCSAT_SUPPLEMENT_CHECK_MODES);
NEW 485	if (i >= 0) {	×
486	assert(i < NUM_MCSAT_SUPPLEMENT_CHECK_MODES);
NEW 487	*value = mcsat_supplement_check_code[i];	×
NEW 488	return true;	×
489	}
490	}
NEW 491	*reason = "must be one of 'both' 'final-only'";	×
492
NEW 493	return false;	×
494	}
495
496
497
498	/*
499	* EF generalization mode
500	* - allowed modes are "none" or "substitution" or "projection" or "auto"
501	* - we use a general implementation so that we can add more modes later
502	*/
503	bool param_val_to_genmode(const char name, const param_val_t v, ef_gen_option_t value, char *reason) {	4✔
504	int32_t i;
505
506	if (v->tag == PARAM_VAL_SYMBOL) {	4✔
507	i = binary_search_string(v->val.symbol, ef_gen_modes, NUM_EF_GEN_MODES);	4✔
508	if (i >= 0) {	4✔
509	assert(i < NUM_EF_GEN_MODES);
510	*value = ef_gen_code[i];	4✔
511	return true;	4✔
512	}
513	}
514	*reason = "must be one of 'none' 'substitution' 'projection' 'auto'";	×
515
516	return false;	×
517	}
518
519
520	/*
521	* EMATCH mode
522	* - allowed modes are "all" or "random" or "epsilongreedy"
523	* - we use a general implementation so that we can add more modes later
524	*/
525	bool param_val_to_ematchmode(const char name, const param_val_t v, iterate_kind_t value, char *reason) {	×
526	int32_t i;
527
528	if (v->tag == PARAM_VAL_SYMBOL) {	×
529	i = binary_search_string(v->val.symbol, ematch_modes, NUM_EMATCH_MODES);	×
530	if (i >= 0) {	×
531	assert(i < NUM_EMATCH_MODES);
532	*value = ematch_mode_code[i];	×
533	return true;	×
534	}
535	}
536	*reason = "must be one of 'all' 'random' 'epsilongreedy'";	×
537
538	return false;	×
539	}

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