diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2019-04-25 18:02:57 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-04-25 18:02:57 -0700 |
| commit | 78ae0a579b91af102b48f7ac1db60afc09ccf727 (patch) | |
| tree | 148a067616aa4168047859e331c70f39f0ba91fc /src/api/cvc4cppkind.h | |
| parent | caf32b8e9940e90cd0bfe2e029b4a55c6e601f31 (diff) | |
New C++ API: Clean up API: mkVar vs mkConst vs mkBoundVar. (#2977)
This cleans up naming of API functions to create first-order constants and variables.
mkVar -> mkConst
mkBoundVar -> mkVar
declareConst is redundant (= mkConst) and thus, in an effort to avoid redundancy, removed.
Note that we want to avoid redundancy in order to reduce code duplication and maintenance
overhead (we do not allow nested API calls, since this is problematic when tracing API calls).
Diffstat (limited to 'src/api/cvc4cppkind.h')
| -rw-r--r-- | src/api/cvc4cppkind.h | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/src/api/cvc4cppkind.h b/src/api/cvc4cppkind.h index 3aba6cebb..d4f6880f9 100644 --- a/src/api/cvc4cppkind.h +++ b/src/api/cvc4cppkind.h @@ -123,25 +123,25 @@ enum CVC4_PUBLIC Kind : int32_t */ DISTINCT, /** - * Variable. + * First-order constant. * Not permitted in bindings (forall, exists, ...). * Parameters: - * See mkVar(). + * See mkConst(). * Create with: - * mkVar(const std::string& symbol, Sort sort) - * mkVar(Sort sort) + * mkConst(const std::string& symbol, Sort sort) + * mkConst(Sort sort) */ - VARIABLE, + CONSTANT, /** - * Bound variable. + * (Bound) variable. * Permitted in bindings and in the lambda and quantifier bodies only. * Parameters: - * See mkBoundVar(). + * See mkVar(). * Create with: - * mkBoundVar(const std::string& symbol, Sort sort) - * mkBoundVar(Sort sort) + * mkVar(const std::string& symbol, Sort sort) + * mkVar(Sort sort) */ - BOUND_VARIABLE, + VARIABLE, #if 0 /* Skolem variable (internal only) */ SKOLEM, |