Merge pull request #387 from SRI-CSL/terminology_fix

Clarified the use of variable in API comments.

src/include/yices.h

@@ -1998,8 +1998,9 @@ __YICES_DLLSPEC__ extern term_t yices_parse_term(const char *s);
  * - map must be an array of n terms
  * - the type of map[i] must be a subtype of var[i]'s type
  * - every occurrence of var[i] in t is replaced by map[i]
- * - if a variable occurs several times in v, the last occurrence
- *   counts. (e.g., if v[i] = x and v[j] = x with i < j, and
+ * - if an uninterpreted term / variable occurs several times in v,
+ *   the last occurrence counts.
+ *   (e.g., if v[i] = x and v[j] = x with i < j, and
  *   there are no other occurrences of x in v, then x is
  *   replaced by map[j]).
  *
@@ -3019,7 +3020,9 @@ __YICES_DLLSPEC__ extern int32_t yices_pop(context_t *ctx);
  * unless you really know what you're doing.
  *
  * The following functions selectively enable/disable a preprocessing
- * option. The current options include:
+ * option. In the description below we use "variable" for what should be
+ * "uninterpreted term" (in the sense of Yices), to stick to standard
+ * terminology. The current options include:
  *
  *   var-elim: whether to eliminate variables by substitution
  *
@@ -3169,8 +3172,7 @@ __YICES_DLLSPEC__ extern smt_status_t yices_check_context_with_assumptions(conte
 /*
  * Check satisfiability modulo a model.
  *
- * Check whether the assertions stored in ctx conjoined with a variable assignment defined by a
- * model are satisfiable.
+ * Check whether the assertions stored in ctx conjoined with a model are satisfiable.
  * - ctx must be a context initialized with support for MCSAT
  *   (see yices_new_context, yices_new_config, yices_set_config).
  * - params is an optional structure to store heuristic parameters
@@ -3213,7 +3215,7 @@ __YICES_DLLSPEC__ extern smt_status_t yices_check_context_with_model(context_t *
  * Check satisfiability and compute interpolant.
  *
  * Check whether the combined assertions stored in ctx are satisfiable. If they are
- * not compute an interpolants (defined on variables common to both contexts).
+ * not, compute an interpolant (whose uninterpreted terms are common to both contexts).
  * - params is an optional structure to store heuristic parameters
  * - if params is NULL, default parameter settings are used.
  *
@@ -3228,12 +3230,12 @@ __YICES_DLLSPEC__ extern smt_status_t yices_check_context_with_model(context_t *
  *
  * To call this function:
  * - ctx->ctx_A must be a context initialized with support for MCSAT and interpolation.
- * - ctx->ctx_B can be an other context (not necessarily with MCSAT support)
+ * - ctx->ctx_B can be another context (not necessarily with MCSAT support)
  *
  * If this function returns STATUS_UNSAT, then an interpolant is returned in ctx->interpolant.
  *
  * If this function returns STATUS_SAT and build_model is true, then
- * a model is returned in ctx->model. This model must be freed when no-longer need by
+ * a model is returned in ctx->model. This model must be freed when no-longer needed by
  * calling yices_free_model.
  *
  * If something is wrong, the function returns STATUS_ERROR and sets the yices error report
@@ -3391,7 +3393,7 @@ __YICES_DLLSPEC__ extern term_t yices_get_model_interpolant(context_t *ctx);
 /*
  * Build a model from ctx
  * - keep_subst indicates whether the model should include
- *   the eliminated variables:
+ *   the uninterpreted terms that have been eliminated by simplification:
  *   keep_subst = 0 means don't keep substitutions,
  *   keep_subst != 0 means keep them
  * - ctx status must be STATUS_SAT or STATUS_UNKNOWN
@@ -3400,25 +3402,25 @@ __YICES_DLLSPEC__ extern term_t yices_get_model_interpolant(context_t *ctx);
  * and sets an error report (code = CTX_INVALID_OPERATION).
  *
  * When assertions are added to the context, the simplifications may
- * eliminate variables (cf. simplification options above).  The flag
- * 'keep_subst' indicates whether the model should keep track of these
- * eliminated variables and include their value.
+ * eliminate some uninterpreted terms (cf. simplification options above).
+ * The flag 'keep_subst' indicates whether the model should keep track
+ * of these eliminated terms and include their value.
  *
  * Example: after the following assertions
  *
  *    (= x (bv-add y z))
  *    (bv-gt y 0b000)
  *    (bg-gt z 0b000)
  *
- * variable 'x' gets eliminated. Then a call to 'check_context' will
+ * uninterpreted term 'x' gets eliminated. Then a call to 'check_context' will
  * return STATUS_SAT and we can ask for a model 'M'
  * - if 'keep_subst' is false then the value of 'x' in 'M' is unavailable.
  * - if 'keep_subst' is true then the value of 'x' in 'M' is computed,
  *   based on the value of 'y' and 'z' in 'M'.
  *
  * It's always better to set 'keep_subst' true. The only exceptions
- * are some of the large SMT_LIB benchmarks where millions of variables
- * are eliminated.  In such cases, it saves memory to set 'keep_subst'
+ * are some of the large SMT_LIB benchmarks where millions of uninterpreted 
+ * terms are eliminated.  In such cases, it saves memory to set 'keep_subst'
  * false, and model construction is faster too.
  */
 __YICES_DLLSPEC__ extern model_t *yices_get_model(context_t *ctx, int32_t keep_subst);
@@ -3462,7 +3464,7 @@ __YICES_DLLSPEC__ extern model_t *yices_model_from_map(uint32_t n, const term_t
 
 
 /*
- * The following functions extend a model by assigning a value to a variable
+ * The following functions extend a model by assigning a value to an uninterpreted term
  * - var must be an uninterpreted term
  * - var must not have a value in model
  *
@@ -3472,23 +3474,23 @@ __YICES_DLLSPEC__ extern model_t *yices_model_from_map(uint32_t n, const term_t
  * Error report:
  * - code = INVALID_TERM if var is not valid
  * - code = MDL_UNINT_REQUIRED if var is not uninterpreted
- * - code = TYPE_MISMATCH if the variable and the value don't have compatible types.
+ * - code = TYPE_MISMATCH if the uninterpreted term and the value don't have compatible types.
  * - code = MDL_DUPLICATE_VAR if var already has a value in model
  */
 
 /*
- * Assign a value to a Boolean variable
+ * Assign a value to a Boolean uninterpreted term
  * - val 0 means false, anything else means true.
  *
  * Since 2.6.4.
  */
 __YICES_DLLSPEC__ extern int32_t yices_model_set_bool(model_t *model, term_t var, int32_t val);
 
 /*
- * Assign a value to a numerical variable.  The value can be given as
+ * Assign a value to a numerical uninterpreted term.  The value can be given as
  * an integer, a GMP integer, a GMP rational, or an algebraic number.
  *
- * The assignment fails (TYPE_MISMATCH) is the variable has integer type
+ * The assignment fails (TYPE_MISMATCH) is the uninterpreted term has integer type
  * and the value is not an integer.
  *
  * For functions yices_model_set_rational32 and
@@ -3513,7 +3515,7 @@ __YICES_DLLSPEC__ extern int32_t yices_model_set_algebraic_number(model_t *model
 
 
 /*
- * Assign an integer value to a bitvector variable.
+ * Assign an integer value to a bitvector uninterpreted term.
  *
  * Rules for truncation and zero/sign extension:
  * - let n be the number of bits in var
@@ -3541,8 +3543,8 @@ __YICES_DLLSPEC__ extern int32_t yices_model_set_bv_mpz(model_t *model, term_t v
 
 
 /*
- * Assign a bitvector variable using an array of bits.
- * - var = bitvector variable
+ * Assign a bitvector value to a bitvector uninterpreted term, using an array of bits.
+ * - var = bitvector uninterpreted term
  * - a = array of n bits
  * - var must be an uninterpreted term of type (bitvector n)
  *   (and var must not have a value in model).
@@ -3579,7 +3581,7 @@ __YICES_DLLSPEC__ extern int32_t yices_model_set_bv_from_array(model_t *model, t
  *
  *   (assert (> y 0))
  *
- * then variable 'x' does not occur in the simplified assertions and will
+ * then uninterpreted term 'x' does not occur in the simplified assertions and will
  * not be included in vector 'v'.
  */
 __YICES_DLLSPEC__ extern void yices_model_collect_defined_terms(model_t *mdl, term_vector_t *v);
@@ -4346,7 +4348,10 @@ __YICES_DLLSPEC__ extern int32_t yices_implicant_for_formulas(model_t *mdl, uint
  * MODEL GENERALIZATION
  */
 
-/*
+/* In the description below we use "variable" for what should be
+ * "uninterpreted term" (in the sense of Yices), to stick to standard
+ * terminology.
+ *
  * Given a model mdl for a formula F(X, Y). The following generalization functions
  * eliminate variables Y from F(X, Y) in a way that is guided by the model.
  *