From 78ae0a579b91af102b48f7ac1db60afc09ccf727 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Thu, 25 Apr 2019 18:02:57 -0700 Subject: 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). --- src/parser/smt2/Smt2.g | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'src/parser') 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); } -- cgit v1.2.3