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/parser | |
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/parser')
-rw-r--r-- | src/parser/smt2/Smt2.g | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 00f2e944d..75df38637 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -2307,8 +2307,8 @@ termAtomic[CVC4::api::Term& atomTerm] sortSymbol[type,CHECK_DECLARED] sortSymbol[type2,CHECK_DECLARED] { - api::Term v1 = SOLVER->mkVar(api::Sort(type), "_emp1"); - api::Term v2 = SOLVER->mkVar(api::Sort(type2), "_emp2"); + api::Term v1 = SOLVER->mkConst(api::Sort(type), "_emp1"); + api::Term v2 = SOLVER->mkConst(api::Sort(type2), "_emp2"); atomTerm = SOLVER->mkTerm(api::SEP_EMP, v1, v2); } |