diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-04-29 20:27:20 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-04-29 20:27:20 -0500 |
commit | 19a93d5e0f924c70e7f77719e0310c730c8fbc61 (patch) | |
tree | 2ce2d68279ebb4b031ab314f7e206862abbc12f8 /src/theory/builtin | |
parent | b351cce04bc13e00b4b63f1bba403b5d549d56bf (diff) |
Eliminate APPLY kind (#2976)
Diffstat (limited to 'src/theory/builtin')
-rw-r--r-- | src/theory/builtin/kinds | 4 | ||||
-rw-r--r-- | src/theory/builtin/theory_builtin_type_rules.h | 38 |
2 files changed, 0 insertions, 42 deletions
diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds index 3313a684f..15891dfad 100644 --- a/src/theory/builtin/kinds +++ b/src/theory/builtin/kinds @@ -289,9 +289,6 @@ constant BUILTIN \ "expr/kind.h" \ "the kind of expressions representing built-in operators" -variable FUNCTION "a defined function" -parameterized APPLY FUNCTION 0: "application of a defined function" - operator EQUAL 2 "equality (two parameters only, sorts must match)" operator DISTINCT 2: "disequality (N-ary, sorts must match)" variable VARIABLE "a variable (not permitted in bindings)" @@ -332,7 +329,6 @@ well-founded SEXPR_TYPE \ "::CVC4::theory::builtin::SExprProperties::mkGroundTerm(%TYPE%)" \ "theory/builtin/theory_builtin_type_rules.h" -typerule APPLY ::CVC4::theory::builtin::ApplyTypeRule typerule EQUAL ::CVC4::theory::builtin::EqualityTypeRule typerule DISTINCT ::CVC4::theory::builtin::DistinctTypeRule typerule SEXPR ::CVC4::theory::builtin::SExprTypeRule diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h index 2c726d12f..db427d21e 100644 --- a/src/theory/builtin/theory_builtin_type_rules.h +++ b/src/theory/builtin/theory_builtin_type_rules.h @@ -31,44 +31,6 @@ namespace CVC4 { namespace theory { namespace builtin { -class ApplyTypeRule { - public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - { - TNode f = n.getOperator(); - TypeNode fType = f.getType(check); - if( !fType.isFunction() && n.getNumChildren() > 0 ) { - throw TypeCheckingExceptionPrivate(n, "operator does not have function type"); - } - if( check ) { - if(fType.isFunction()) { - if(n.getNumChildren() != fType.getNumChildren() - 1) { - throw TypeCheckingExceptionPrivate(n, "number of arguments does not match the function type"); - } - TNode::iterator argument_it = n.begin(); - TNode::iterator argument_it_end = n.end(); - TypeNode::iterator argument_type_it = fType.begin(); - for(; argument_it != argument_it_end; ++argument_it, ++argument_type_it) { - if(!(*argument_it).getType().isComparableTo(*argument_type_it)) { - std::stringstream ss; - ss << "argument types do not match the function type:\n" - << "argument: " << *argument_it << "\n" - << "has type: " << (*argument_it).getType() << "\n" - << "not equal: " << *argument_type_it; - throw TypeCheckingExceptionPrivate(n, ss.str()); - } - } - } else { - if( n.getNumChildren() > 0 ) { - throw TypeCheckingExceptionPrivate(n, "number of arguments does not match the function type"); - } - } - } - return fType.isFunction() ? fType.getRangeType() : fType; - } -};/* class ApplyTypeRule */ - - class EqualityTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, |