From 05a53a2ac405bcd18a84024247145f161809c3b0 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Thu, 1 Apr 2021 09:56:14 -0700 Subject: Rename namespace CVC5 to cvc5. (#6258) --- src/theory/uf/kinds | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) (limited to 'src/theory/uf/kinds') diff --git a/src/theory/uf/kinds b/src/theory/uf/kinds index ab2e422ee..e4b946105 100644 --- a/src/theory/uf/kinds +++ b/src/theory/uf/kinds @@ -4,32 +4,32 @@ # src/theory/builtin/kinds. # -theory THEORY_UF ::CVC5::theory::uf::TheoryUF "theory/uf/theory_uf.h" +theory THEORY_UF ::cvc5::theory::uf::TheoryUF "theory/uf/theory_uf.h" typechecker "theory/uf/theory_uf_type_rules.h" properties stable-infinite parametric properties check ppStaticLearn presolve -rewriter ::CVC5::theory::uf::TheoryUfRewriter "theory/uf/theory_uf_rewriter.h" +rewriter ::cvc5::theory::uf::TheoryUfRewriter "theory/uf/theory_uf_rewriter.h" parameterized APPLY_UF VARIABLE 1: "application of an uninterpreted function; first parameter is the function, remaining ones are parameters to that function" -typerule APPLY_UF ::CVC5::theory::uf::UfTypeRule +typerule APPLY_UF ::cvc5::theory::uf::UfTypeRule variable BOOLEAN_TERM_VARIABLE "Boolean term variable" operator CARDINALITY_CONSTRAINT 2 "cardinality constraint on sort S: first parameter is (any) term of sort S, second is a positive integer constant k that bounds the cardinality of S" -typerule CARDINALITY_CONSTRAINT ::CVC5::theory::uf::CardinalityConstraintTypeRule +typerule CARDINALITY_CONSTRAINT ::cvc5::theory::uf::CardinalityConstraintTypeRule operator COMBINED_CARDINALITY_CONSTRAINT 1 "combined cardinality constraint; parameter is a positive integer constant k that bounds the sum of the cardinalities of all sorts in the signature" -typerule COMBINED_CARDINALITY_CONSTRAINT ::CVC5::theory::uf::CombinedCardinalityConstraintTypeRule +typerule COMBINED_CARDINALITY_CONSTRAINT ::cvc5::theory::uf::CombinedCardinalityConstraintTypeRule parameterized PARTIAL_APPLY_UF APPLY_UF 1: "partial uninterpreted function application" -typerule PARTIAL_APPLY_UF ::CVC5::theory::uf::PartialTypeRule +typerule PARTIAL_APPLY_UF ::cvc5::theory::uf::PartialTypeRule operator CARDINALITY_VALUE 1 "cardinality value of sort S: first parameter is (any) term of sort S" -typerule CARDINALITY_VALUE ::CVC5::theory::uf::CardinalityValueTypeRule +typerule CARDINALITY_VALUE ::cvc5::theory::uf::CardinalityValueTypeRule operator HO_APPLY 2 "higher-order (partial) function application" -typerule HO_APPLY ::CVC5::theory::uf::HoApplyTypeRule +typerule HO_APPLY ::cvc5::theory::uf::HoApplyTypeRule endtheory -- cgit v1.2.3