diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-02-20 14:49:02 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-02-20 14:49:02 -0600 |
commit | 5489ef01beb91e256e343e2fd2d734b48b42ad6e (patch) | |
tree | f6a535c768ae4f3cfbbed765b0697300f4412657 /src/theory/builtin/kinds | |
parent | 32fdf625f66b8ebf260756962a53d63eec771c12 (diff) |
Remove front-end support for Chain (#3767)
Diffstat (limited to 'src/theory/builtin/kinds')
-rw-r--r-- | src/theory/builtin/kinds | 9 |
1 files changed, 0 insertions, 9 deletions
diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds index 15891dfad..c90419def 100644 --- a/src/theory/builtin/kinds +++ b/src/theory/builtin/kinds @@ -300,13 +300,6 @@ operator LAMBDA 2 "a lambda expression; first parameter is a BOUND_VAR_LIST, sec operator CHOICE 2 "a Hilbert choice (epsilon) expression; first parameter is a BOUND_VAR_LIST, second is the Hilbert choice body" -parameterized CHAIN CHAIN_OP 2: "chained operator (N-ary), turned into a conjunction of binary applications of the operator on adjoining parameters; first parameter is a CHAIN_OP representing a binary operator, rest are arguments to that operator" -constant CHAIN_OP \ - ::CVC4::Chain \ - ::CVC4::ChainHashFunction \ - "expr/chain.h" \ - "the chained operator; payload is an instance of the CVC4::Chain class" - constant TYPE_CONSTANT \ ::CVC4::TypeConstant \ ::CVC4::TypeConstantHashFunction \ @@ -334,8 +327,6 @@ typerule DISTINCT ::CVC4::theory::builtin::DistinctTypeRule typerule SEXPR ::CVC4::theory::builtin::SExprTypeRule typerule LAMBDA ::CVC4::theory::builtin::LambdaTypeRule typerule CHOICE ::CVC4::theory::builtin::ChoiceTypeRule -typerule CHAIN ::CVC4::theory::builtin::ChainTypeRule -typerule CHAIN_OP ::CVC4::theory::builtin::ChainedOperatorTypeRule # lambda expressions that are isomorphic to array constants can be considered constants construle LAMBDA ::CVC4::theory::builtin::LambdaTypeRule |