From: Aina Niemetz Date: Mon, 15 Nov 2021 16:10:26 +0000 (-0800) Subject: api: Rename BOUND_VAR_LIST to VARIABLE_LIST. (#7632) X-Git-Tag: cvc5-1.0.0~817 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e8c0874f92d16735d91f5e7d7d437c694e4d3b85;p=cvc5.git api: Rename BOUND_VAR_LIST to VARIABLE_LIST. (#7632) --- diff --git a/examples/api/java/Relations.java b/examples/api/java/Relations.java index 0d78562bb..fb082fc11 100644 --- a/examples/api/java/Relations.java +++ b/examples/api/java/Relations.java @@ -164,7 +164,7 @@ public class Relations Term member = solver.mkTerm(MEMBER, xxTuple, ancestor); Term notMember = solver.mkTerm(NOT, member); - Term quantifiedVariables = solver.mkTerm(BOUND_VAR_LIST, x); + Term quantifiedVariables = solver.mkTerm(VARIABLE_LIST, x); Term noSelfAncestor = solver.mkTerm(FORALL, quantifiedVariables, notMember); // formulas diff --git a/examples/api/java/Statistics.java b/examples/api/java/Statistics.java index 751dda947..7db7cc4f3 100644 --- a/examples/api/java/Statistics.java +++ b/examples/api/java/Statistics.java @@ -206,7 +206,7 @@ public class Statistics Term member = solver.mkTerm(MEMBER, xxTuple, ancestor); Term notMember = solver.mkTerm(NOT, member); - Term quantifiedVariables = solver.mkTerm(BOUND_VAR_LIST, var); + Term quantifiedVariables = solver.mkTerm(VARIABLE_LIST, var); Term noSelfAncestor = solver.mkTerm(FORALL, quantifiedVariables, notMember); // formulas diff --git a/examples/simple_vc_quant_cxx.cpp b/examples/simple_vc_quant_cxx.cpp index 1bdadfca2..ea8aa10a4 100644 --- a/examples/simple_vc_quant_cxx.cpp +++ b/examples/simple_vc_quant_cxx.cpp @@ -33,7 +33,7 @@ int main() { Term x = slv.mkVar(integer, "x"); // make forall x. P( x ) - Term var_list = slv.mkTerm(Kind::BOUND_VAR_LIST, x); + Term var_list = slv.mkTerm(Kind::VARIABLE_LIST, x); Term px = slv.mkTerm(Kind::APPLY_UF, p, x); Term quantpospx = slv.mkTerm(Kind::FORALL, var_list, px); std::cout << "Made expression : " << quantpospx << std::endl; diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 0c7e86c86..b80f68202 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -373,7 +373,7 @@ const static std::unordered_map s_kinds{ /* Quantifiers --------------------------------------------------------- */ {FORALL, cvc5::Kind::FORALL}, {EXISTS, cvc5::Kind::EXISTS}, - {BOUND_VAR_LIST, cvc5::Kind::BOUND_VAR_LIST}, + {VARIABLE_LIST, cvc5::Kind::BOUND_VAR_LIST}, {INST_PATTERN, cvc5::Kind::INST_PATTERN}, {INST_NO_PATTERN, cvc5::Kind::INST_NO_PATTERN}, {INST_POOL, cvc5::Kind::INST_POOL}, @@ -673,7 +673,7 @@ const static std::unordered_map /* Quantifiers ----------------------------------------------------- */ {cvc5::Kind::FORALL, FORALL}, {cvc5::Kind::EXISTS, EXISTS}, - {cvc5::Kind::BOUND_VAR_LIST, BOUND_VAR_LIST}, + {cvc5::Kind::BOUND_VAR_LIST, VARIABLE_LIST}, {cvc5::Kind::INST_PATTERN, INST_PATTERN}, {cvc5::Kind::INST_NO_PATTERN, INST_NO_PATTERN}, {cvc5::Kind::INST_POOL, INST_POOL}, diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h index 29cb130d4..1c1819889 100644 --- a/src/api/cpp/cvc5_kind.h +++ b/src/api/cpp/cvc5_kind.h @@ -159,7 +159,7 @@ enum Kind : int32_t * Lambda expression. * * Parameters: - * - 1: BOUND_VAR_LIST + * - 1: VARIABLE_LIST * - 2: Lambda body * * Create with: @@ -169,7 +169,7 @@ enum Kind : int32_t LAMBDA, /** * The syntax of a witness term is similar to a quantified formula except that - * only one bound variable is allowed. + * only one variable is allowed. * The term `(witness ((x T)) F)` returns an element `x` of type `T` * and asserts `F`. * @@ -201,7 +201,7 @@ enum Kind : int32_t * whereas notice that `(or (= z 0) (not (= z 0)))` is true for any `z`. * * Parameters: - * - 1: BOUND_VAR_LIST + * - 1: VARIABLE_LIST * - 2: Witness body * * Create with: @@ -1954,7 +1954,7 @@ enum Kind : int32_t * is represented by the AST * * (MATCH l - * (MATCH_BIND_CASE (BOUND_VAR_LIST h t) (cons h t) h) + * (MATCH_BIND_CASE (VARIABLE_LIST h t) (cons h t) h) * (MATCH_CASE nil 0)) * * The type of the last argument of each case term could be equal. @@ -1987,7 +1987,7 @@ enum Kind : int32_t * A (non-constant) case expression to be used within a match expression. * * Parameters: - * - 1: a BOUND_VAR_LIST Term containing the free variables of the case + * - 1: a VARIABLE_LIST Term containing the free variables of the case * - 2: Term denoting the pattern expression * - 3: Term denoting the return value * @@ -2228,7 +2228,7 @@ enum Kind : int32_t SET_UNIVERSE, /** * Set comprehension - * A set comprehension is specified by a bound variable list x1 ... xn, + * A set comprehension is specified by a variable list x1 ... xn, * a predicate P[x1...xn], and a term t[x1...xn]. A comprehension C with the * above form has members given by the following semantics: * @f[ @@ -2240,7 +2240,7 @@ enum Kind : int32_t * y in the above formula. * * Parameters: - * - 1: Term BOUND_VAR_LIST + * - 1: Term VARIABLE_LIST * - 2: Term denoting the predicate of the comprehension * - 3: (optional) a Term denoting the generator for the comprehension * @@ -3273,7 +3273,7 @@ enum Kind : int32_t * Universally quantified formula. * * Parameters: - * - 1: BOUND_VAR_LIST Term + * - 1: VARIABLE_LIST Term * - 2: Quantifier body * - 3: (optional) INST_PATTERN_LIST Term * @@ -3287,7 +3287,7 @@ enum Kind : int32_t * Existentially quantified formula. * * Parameters: - * - 1: BOUND_VAR_LIST Term + * - 1: VARIABLE_LIST Term * - 2: Quantifier body * - 3: (optional) INST_PATTERN_LIST Term * @@ -3298,24 +3298,24 @@ enum Kind : int32_t */ EXISTS, /** - * A list of bound variables (used to bind variables under a quantifier) + * A list of variables (used to bind variables under a quantifier) * * Parameters: n > 1 - * - 1..n: Terms with kind BOUND_VARIABLE + * - 1..n: Terms with kind VARIABLE * * Create with: * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2, const Term& child3) const` * - `Solver::mkTerm(Kind kind, const std::vector& children) const` */ - BOUND_VAR_LIST, + VARIABLE_LIST, /** * An instantiation pattern. * Specifies a (list of) terms to be used as a pattern for quantifier * instantiation. * * Parameters: n > 1 - * - 1..n: Terms with kind BOUND_VARIABLE + * - 1..n: Terms of any sort * * Create with: * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` @@ -3329,7 +3329,7 @@ enum Kind : int32_t * quantifier instantiation. * * Parameters: n > 1 - * - 1..n: Terms with kind BOUND_VARIABLE + * - 1..n: Terms of any sort * * Create with: * - `Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const` 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 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 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 & bvlist, { PARSER_STATE->checkLetBinding(bvlist, lhs, rhs, false); std::vector 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 & bvlist, { PARSER_STATE->checkLetBinding(bvlist, lhs, rhs, true); std::vector 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; diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp index 51a0f38b5..b24c85496 100644 --- a/test/unit/api/cpp/solver_black.cpp +++ b/test/unit/api/cpp/solver_black.cpp @@ -1601,7 +1601,7 @@ TEST_F(TestApiBlackSolver, getModelDomainElements2) Term x = d_solver.mkVar(uSort, "x"); Term y = d_solver.mkVar(uSort, "y"); Term eq = d_solver.mkTerm(EQUAL, x, y); - Term bvl = d_solver.mkTerm(BOUND_VAR_LIST, x, y); + Term bvl = d_solver.mkTerm(VARIABLE_LIST, x, y); Term f = d_solver.mkTerm(FORALL, bvl, eq); d_solver.assertFormula(f); d_solver.checkSat(); @@ -1674,7 +1674,7 @@ TEST_F(TestApiBlackSolver, getQuantifierElimination) Term x = d_solver.mkVar(d_solver.getBooleanSort(), "x"); Term forall = d_solver.mkTerm(FORALL, - d_solver.mkTerm(BOUND_VAR_LIST, x), + d_solver.mkTerm(VARIABLE_LIST, x), d_solver.mkTerm(OR, x, d_solver.mkTerm(NOT, x))); ASSERT_THROW(d_solver.getQuantifierElimination(Term()), CVC5ApiException); ASSERT_THROW(d_solver.getQuantifierElimination(Solver().mkBoolean(false)), @@ -1687,7 +1687,7 @@ TEST_F(TestApiBlackSolver, getQuantifierEliminationDisjunct) Term x = d_solver.mkVar(d_solver.getBooleanSort(), "x"); Term forall = d_solver.mkTerm(FORALL, - d_solver.mkTerm(BOUND_VAR_LIST, x), + d_solver.mkTerm(VARIABLE_LIST, x), d_solver.mkTerm(OR, x, d_solver.mkTerm(NOT, x))); ASSERT_THROW(d_solver.getQuantifierEliminationDisjunct(Term()), CVC5ApiException); diff --git a/test/unit/api/java/SolverTest.java b/test/unit/api/java/SolverTest.java index 6a08d79c6..40a7d4157 100644 --- a/test/unit/api/java/SolverTest.java +++ b/test/unit/api/java/SolverTest.java @@ -1645,7 +1645,7 @@ class SolverTest Term x = d_solver.mkVar(uSort, "x"); Term y = d_solver.mkVar(uSort, "y"); Term eq = d_solver.mkTerm(EQUAL, x, y); - Term bvl = d_solver.mkTerm(BOUND_VAR_LIST, x, y); + Term bvl = d_solver.mkTerm(VARIABLE_LIST, x, y); Term f = d_solver.mkTerm(FORALL, bvl, eq); d_solver.assertFormula(f); d_solver.checkSat(); @@ -1713,9 +1713,8 @@ class SolverTest @Test void getQuantifierElimination() { Term x = d_solver.mkVar(d_solver.getBooleanSort(), "x"); - Term forall = d_solver.mkTerm(FORALL, - d_solver.mkTerm(BOUND_VAR_LIST, x), - d_solver.mkTerm(OR, x, d_solver.mkTerm(NOT, x))); + Term forall = d_solver.mkTerm( + FORALL, d_solver.mkTerm(VARIABLE_LIST, x), d_solver.mkTerm(OR, x, d_solver.mkTerm(NOT, x))); assertThrows( CVC5ApiException.class, () -> d_solver.getQuantifierElimination(d_solver.getNullTerm())); Solver slv = new Solver(); @@ -1729,9 +1728,8 @@ class SolverTest @Test void getQuantifierEliminationDisjunct() { Term x = d_solver.mkVar(d_solver.getBooleanSort(), "x"); - Term forall = d_solver.mkTerm(FORALL, - d_solver.mkTerm(BOUND_VAR_LIST, x), - d_solver.mkTerm(OR, x, d_solver.mkTerm(NOT, x))); + Term forall = d_solver.mkTerm( + FORALL, d_solver.mkTerm(VARIABLE_LIST, x), d_solver.mkTerm(OR, x, d_solver.mkTerm(NOT, x))); assertThrows(CVC5ApiException.class, () -> d_solver.getQuantifierEliminationDisjunct(d_solver.getNullTerm()));