api: Rename BOUND_VAR_LIST to VARIABLE_LIST. (#7632)

3 files changed, 21 insertions, 21 deletions

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 4b4b7c10b..211fb4c80 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1396,7 +1396,7 @@ termNonVariable[cvc5::api::Term& expr, cvc5::api::Term& expr2]
           cargs.push_back(f);
           cargs.insert(cargs.end(),args.begin(),args.end());
           api::Term c = MK_TERM(api::APPLY_CONSTRUCTOR,cargs);
-          api::Term bvla = MK_TERM(api::BOUND_VAR_LIST,args);
+          api::Term bvla = MK_TERM(api::VARIABLE_LIST,args);
           api::Term mc = MK_TERM(api::MATCH_BIND_CASE, bvla, c, f3);
           matchcases.push_back(mc);
           // now, pop the scope
@@ -1427,7 +1427,7 @@ termNonVariable[cvc5::api::Term& expr, cvc5::api::Term& expr2]
           api::Term mc;
           if (f.getKind() == api::VARIABLE)
           {
-            api::Term bvlf = MK_TERM(api::BOUND_VAR_LIST, f);
+            api::Term bvlf = MK_TERM(api::VARIABLE_LIST, f);
             mc = MK_TERM(api::MATCH_BIND_CASE, bvlf, f, f3);
           }
           else
@@ -1935,7 +1935,7 @@ boundVarList[cvc5::api::Term& expr]
    {
      std::vector<cvc5::api::Term> args =
          PARSER_STATE->bindBoundVars(sortedVarNames);
-     expr = MK_TERM(api::BOUND_VAR_LIST, args);
+     expr = MK_TERM(api::VARIABLE_LIST, args);
    }
  ;
 
diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g
index 9ef04c348..419acafc0 100644
--- a/src/parser/tptp/Tptp.g
+++ b/src/parser/tptp/Tptp.g
@@ -151,7 +151,7 @@ parseCommand returns [cvc5::Command* cmd = NULL]
   { PARSER_STATE->popScope();
     std::vector<api::Term> bvl = PARSER_STATE->getFreeVar();
     if(!bvl.empty()) {
-      expr = MK_TERM(api::FORALL,MK_TERM(api::BOUND_VAR_LIST,bvl),expr);
+      expr = MK_TERM(api::FORALL,MK_TERM(api::VARIABLE_LIST,bvl),expr);
     };
   }
     (COMMA_TOK anything*)? RPAREN_TOK DOT_TOK
@@ -469,9 +469,9 @@ definedPred[cvc5::ParseOp& p]
                   MK_TERM(api::NOT,
                           MK_TERM(api::EQUAL, r, SOLVER->mkInteger(0))),
                   MK_TERM(api::EQUAL, qr, MK_TERM(api::MULT, n, rr)));
-      api::Term bvl = MK_TERM(api::BOUND_VAR_LIST, q, r);
+      api::Term bvl = MK_TERM(api::VARIABLE_LIST, q, r);
       body = MK_TERM(api::EXISTS, bvl, body);
-      api::Term lbvl = MK_TERM(api::BOUND_VAR_LIST, n);
+      api::Term lbvl = MK_TERM(api::VARIABLE_LIST, n);
       p.d_kind = api::LAMBDA;
       p.d_expr = MK_TERM(api::LAMBDA, lbvl, body);
     }
@@ -529,9 +529,9 @@ thfDefinedPred[cvc5::ParseOp& p]
           MK_TERM(api::NOT,
                   MK_TERM(api::EQUAL, r, SOLVER->mkInteger(0))),
           MK_TERM(api::EQUAL, qr, MK_TERM(api::MULT, n, rr)));
-      api::Term bvl = MK_TERM(api::BOUND_VAR_LIST, q, r);
+      api::Term bvl = MK_TERM(api::VARIABLE_LIST, q, r);
       body = MK_TERM(api::EXISTS, bvl, body);
-      api::Term lbvl = MK_TERM(api::BOUND_VAR_LIST, n);
+      api::Term lbvl = MK_TERM(api::VARIABLE_LIST, n);
       p.d_kind = api::LAMBDA;
       p.d_expr = MK_TERM(api::LAMBDA, lbvl, body);
     }
@@ -591,7 +591,7 @@ definedFun[cvc5::ParseOp& p]
     {
       api::Term n = SOLVER->mkVar(SOLVER->getRealSort(), "N");
       api::Term d = SOLVER->mkVar(SOLVER->getRealSort(), "D");
-      api::Term formals = MK_TERM(api::BOUND_VAR_LIST, n, d);
+      api::Term formals = MK_TERM(api::VARIABLE_LIST, n, d);
       api::Term expr = MK_TERM(api::DIVISION, n, d);
       expr = MK_TERM(api::ITE,
                      MK_TERM(api::GEQ, d, SOLVER->mkReal(0)),
@@ -614,7 +614,7 @@ definedFun[cvc5::ParseOp& p]
     {
       api::Term n = SOLVER->mkVar(SOLVER->getRealSort(), "N");
       api::Term d = SOLVER->mkVar(SOLVER->getRealSort(), "D");
-      api::Term formals = MK_TERM(api::BOUND_VAR_LIST, n, d);
+      api::Term formals = MK_TERM(api::VARIABLE_LIST, n, d);
       api::Term expr = MK_TERM(api::DIVISION, n, d);
       expr = MK_TERM(api::ITE,
                      MK_TERM(api::GEQ, expr, SOLVER->mkReal(0)),
@@ -637,7 +637,7 @@ definedFun[cvc5::ParseOp& p]
     {
       api::Term n = SOLVER->mkVar(SOLVER->getRealSort(), "N");
       api::Term d = SOLVER->mkVar(SOLVER->getRealSort(), "D");
-      api::Term formals = MK_TERM(api::BOUND_VAR_LIST, n, d);
+      api::Term formals = MK_TERM(api::VARIABLE_LIST, n, d);
       api::Term expr = MK_TERM(api::DIVISION, n, d);
       expr = MK_TERM(api::TO_INTEGER, expr);
       if (remainder)
@@ -655,7 +655,7 @@ definedFun[cvc5::ParseOp& p]
   | '$ceiling'
     {
       api::Term n = SOLVER->mkVar(SOLVER->getRealSort(), "N");
-      api::Term formals = MK_TERM(api::BOUND_VAR_LIST, n);
+      api::Term formals = MK_TERM(api::VARIABLE_LIST, n);
       api::Term expr = MK_TERM(api::UMINUS,
                           MK_TERM(api::TO_INTEGER, MK_TERM(api::UMINUS, n)));
       p.d_kind = api::LAMBDA;
@@ -664,7 +664,7 @@ definedFun[cvc5::ParseOp& p]
   | '$truncate'
     {
       api::Term n = SOLVER->mkVar(SOLVER->getRealSort(), "N");
-      api::Term formals = MK_TERM(api::BOUND_VAR_LIST, n);
+      api::Term formals = MK_TERM(api::VARIABLE_LIST, n);
       api::Term expr =
           MK_TERM(api::ITE,
                   MK_TERM(api::GEQ, n, SOLVER->mkReal(0)),
@@ -677,7 +677,7 @@ definedFun[cvc5::ParseOp& p]
   | '$round'
     {
       api::Term n = SOLVER->mkVar(SOLVER->getRealSort(), "N");
-      api::Term formals = MK_TERM(api::BOUND_VAR_LIST, n);
+      api::Term formals = MK_TERM(api::VARIABLE_LIST, n);
       api::Term decPart = MK_TERM(api::MINUS, n, MK_TERM(api::TO_INTEGER, n));
       api::Term expr = MK_TERM(
           api::ITE,
@@ -884,7 +884,7 @@ fofUnitaryFormula[cvc5::api::Term& expr]
       ( COMMA_TOK bindvariable[expr] { bv.push_back(expr); } )* ) RBRACK_TOK
     COLON_TOK fofUnitaryFormula[expr]
     { PARSER_STATE->popScope();
-      expr = MK_TERM(kind, MK_TERM(api::BOUND_VAR_LIST, bv), expr);
+      expr = MK_TERM(kind, MK_TERM(api::VARIABLE_LIST, bv), expr);
     }
   ;
 
@@ -1280,10 +1280,10 @@ thfUnitaryFormula[cvc5::ParseOp& p]
       {
         // apply body of lambda to flatten vars
         expr = PARSER_STATE->mkHoApply(expr, flattenVars);
-        // add variables to BOUND_VAR_LIST
+        // add variables to VARIABLE_LIST
         bv.insert(bv.end(), flattenVars.begin(), flattenVars.end());
       }
-      p.d_expr = MK_TERM(p.d_kind, MK_TERM(api::BOUND_VAR_LIST, bv), expr);
+      p.d_expr = MK_TERM(p.d_kind, MK_TERM(api::VARIABLE_LIST, bv), expr);
     }
   ;
 
@@ -1393,7 +1393,7 @@ tffUnitaryFormula[cvc5::api::Term& expr]
       ( COMMA_TOK tffbindvariable[expr] { bv.push_back(expr); } )* ) RBRACK_TOK
     COLON_TOK tffUnitaryFormula[expr]
     { PARSER_STATE->popScope();
-      expr = MK_TERM(kind, MK_TERM(api::BOUND_VAR_LIST, bv), expr);
+      expr = MK_TERM(kind, MK_TERM(api::VARIABLE_LIST, bv), expr);
     }
   | '$ite_f' LPAREN_TOK tffLogicFormula[expr] COMMA_TOK tffLogicFormula[lhs] COMMA_TOK tffLogicFormula[rhs] RPAREN_TOK
     { expr = MK_TERM(api::ITE, expr, lhs, rhs); }
@@ -1428,7 +1428,7 @@ tffLetTermBinding[std::vector<cvc5::api::Term> & bvlist,
   {
     PARSER_STATE->checkLetBinding(bvlist, lhs, rhs, false);
     std::vector<api::Term> lchildren(++lhs.begin(), lhs.end());
-    rhs = MK_TERM(api::LAMBDA, MK_TERM(api::BOUND_VAR_LIST, lchildren), rhs);
+    rhs = MK_TERM(api::LAMBDA, MK_TERM(api::VARIABLE_LIST, lchildren), rhs);
     // since lhs is always APPLY_UF (otherwise we'd have had a parser error in
     // checkLetBinding) the function to be replaced is always the first
     // argument. Note that the way in which lchildren is built above is also
@@ -1454,7 +1454,7 @@ tffLetFormulaBinding[std::vector<cvc5::api::Term> & bvlist,
   {
     PARSER_STATE->checkLetBinding(bvlist, lhs, rhs, true);
     std::vector<api::Term> lchildren(++lhs.begin(), lhs.end());
-    rhs = MK_TERM(api::LAMBDA, MK_TERM(api::BOUND_VAR_LIST, lchildren), rhs);
+    rhs = MK_TERM(api::LAMBDA, MK_TERM(api::VARIABLE_LIST, lchildren), rhs);
     // since lhs is always APPLY_UF (otherwise we'd have had a parser error in
     // checkLetBinding) the function to be replaced is always the first
     // argument. Note that the way in which lchildren is built above is also
diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp
index 7c65f5c57..b8b81df24 100644
--- a/src/parser/tptp/tptp.cpp
+++ b/src/parser/tptp/tptp.cpp
@@ -524,7 +524,7 @@ api::Term Tptp::mkLambdaWrapper(api::Kind k, api::Sort argType)
   // apply body of lambda to variables
   api::Term wrapper =
       d_solver->mkTerm(api::LAMBDA,
-                       d_solver->mkTerm(api::BOUND_VAR_LIST, lvars),
+                       d_solver->mkTerm(api::VARIABLE_LIST, lvars),
                        d_solver->mkTerm(k, lvars));
 
   return wrapper;