diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2021-04-01 09:56:14 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-04-01 16:56:14 +0000 |
| commit | 05a53a2ac405bcd18a84024247145f161809c3b0 (patch) | |
| tree | 34241c0a82f79d717ddbfbb0c294f9a09c7edb0c /src/theory/uf/kinds | |
| parent | afaf4413775ff7d6054a5893f1397ad908e0773c (diff) | |
Rename namespace CVC5 to cvc5. (#6258)
Diffstat (limited to 'src/theory/uf/kinds')
| -rw-r--r-- | src/theory/uf/kinds | 16 |
1 files changed, 8 insertions, 8 deletions
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 |