diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-09-28 20:18:22 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-09-28 20:18:22 -0700 |
commit | d06cf394473cbe09c2e1acc333526c41a6dd9687 (patch) | |
tree | cec81c5557fdcf0e144da5a275471e92063e4e45 /src/theory/arith | |
parent | e25f99329c9905c67a565481dcb0d6a4499a7557 (diff) |
Introduce template classes for simple type rules (#2835)
This commit introduces two template classes `SimpleTypeRule` and
`SimpleTypeRuleVar` to help define simple type rules without writing
lots of redundant code. The main advantages of this approach are:
- Less code
- More consistent error reporting
- Easier to extend type checking with other functionality (e.g. getting
the type of a symbol)
Diffstat (limited to 'src/theory/arith')
-rw-r--r-- | src/theory/arith/kinds | 56 | ||||
-rw-r--r-- | src/theory/arith/theory_arith_type_rules.h | 94 |
2 files changed, 28 insertions, 122 deletions
diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds index 95d1aa9c1..409534050 100644 --- a/src/theory/arith/kinds +++ b/src/theory/arith/kinds @@ -94,40 +94,40 @@ typerule POW ::CVC4::theory::arith::ArithOperatorTypeRule typerule CONST_RATIONAL ::CVC4::theory::arith::ArithConstantTypeRule -typerule LT ::CVC4::theory::arith::ArithPredicateTypeRule -typerule LEQ ::CVC4::theory::arith::ArithPredicateTypeRule -typerule GT ::CVC4::theory::arith::ArithPredicateTypeRule -typerule GEQ ::CVC4::theory::arith::ArithPredicateTypeRule +typerule LT "SimpleTypeRule<RBool, AReal, AReal>" +typerule LEQ "SimpleTypeRule<RBool, AReal, AReal>" +typerule GT "SimpleTypeRule<RBool, AReal, AReal>" +typerule GEQ "SimpleTypeRule<RBool, AReal, AReal>" typerule TO_REAL ::CVC4::theory::arith::ArithOperatorTypeRule typerule TO_INTEGER ::CVC4::theory::arith::ArithOperatorTypeRule -typerule IS_INTEGER ::CVC4::theory::arith::ArithUnaryPredicateTypeRule +typerule IS_INTEGER "SimpleTypeRule<RBool, AReal>" -typerule ABS ::CVC4::theory::arith::IntOperatorTypeRule -typerule INTS_DIVISION ::CVC4::theory::arith::IntOperatorTypeRule -typerule INTS_MODULUS ::CVC4::theory::arith::IntOperatorTypeRule -typerule DIVISIBLE ::CVC4::theory::arith::IntUnaryPredicateTypeRule -typerule DIVISIBLE_OP ::CVC4::theory::arith::DivisibleOpTypeRule +typerule ABS "SimpleTypeRule<RInteger, AInteger>" +typerule INTS_DIVISION "SimpleTypeRule<RInteger, AInteger, AInteger>" +typerule INTS_MODULUS "SimpleTypeRule<RInteger, AInteger, AInteger>" +typerule DIVISIBLE "SimpleTypeRule<RBool, AInteger>" +typerule DIVISIBLE_OP "SimpleTypeRule<RBuiltinOperator>" typerule DIVISION_TOTAL ::CVC4::theory::arith::ArithOperatorTypeRule -typerule INTS_DIVISION_TOTAL ::CVC4::theory::arith::IntOperatorTypeRule -typerule INTS_MODULUS_TOTAL ::CVC4::theory::arith::IntOperatorTypeRule - -typerule EXPONENTIAL ::CVC4::theory::arith::RealOperatorTypeRule -typerule SINE ::CVC4::theory::arith::RealOperatorTypeRule -typerule COSINE ::CVC4::theory::arith::RealOperatorTypeRule -typerule TANGENT ::CVC4::theory::arith::RealOperatorTypeRule -typerule COSECANT ::CVC4::theory::arith::RealOperatorTypeRule -typerule SECANT ::CVC4::theory::arith::RealOperatorTypeRule -typerule COTANGENT ::CVC4::theory::arith::RealOperatorTypeRule -typerule ARCSINE ::CVC4::theory::arith::RealOperatorTypeRule -typerule ARCCOSINE ::CVC4::theory::arith::RealOperatorTypeRule -typerule ARCTANGENT ::CVC4::theory::arith::RealOperatorTypeRule -typerule ARCCOSECANT ::CVC4::theory::arith::RealOperatorTypeRule -typerule ARCSECANT ::CVC4::theory::arith::RealOperatorTypeRule -typerule ARCCOTANGENT ::CVC4::theory::arith::RealOperatorTypeRule - -typerule SQRT ::CVC4::theory::arith::RealOperatorTypeRule +typerule INTS_DIVISION_TOTAL "SimpleTypeRule<RInteger, AInteger, AInteger>" +typerule INTS_MODULUS_TOTAL "SimpleTypeRule<RInteger, AInteger, AInteger>" + +typerule EXPONENTIAL "SimpleTypeRule<RReal, AReal>" +typerule SINE "SimpleTypeRule<RReal, AReal>" +typerule COSINE "SimpleTypeRule<RReal, AReal>" +typerule TANGENT "SimpleTypeRule<RReal, AReal>" +typerule COSECANT "SimpleTypeRule<RReal, AReal>" +typerule SECANT "SimpleTypeRule<RReal, AReal>" +typerule COTANGENT "SimpleTypeRule<RReal, AReal>" +typerule ARCSINE "SimpleTypeRule<RReal, AReal>" +typerule ARCCOSINE "SimpleTypeRule<RReal, AReal>" +typerule ARCTANGENT "SimpleTypeRule<RReal, AReal>" +typerule ARCCOSECANT "SimpleTypeRule<RReal, AReal>" +typerule ARCSECANT "SimpleTypeRule<RReal, AReal>" +typerule ARCCOTANGENT "SimpleTypeRule<RReal, AReal>" + +typerule SQRT "SimpleTypeRule<RReal, AReal>" nullaryoperator PI "pi" diff --git a/src/theory/arith/theory_arith_type_rules.h b/src/theory/arith/theory_arith_type_rules.h index c32b612e2..8b587c0fb 100644 --- a/src/theory/arith/theory_arith_type_rules.h +++ b/src/theory/arith/theory_arith_type_rules.h @@ -73,88 +73,6 @@ public: } };/* class ArithOperatorTypeRule */ -class IntOperatorTypeRule { -public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - { - TNode::iterator child_it = n.begin(); - TNode::iterator child_it_end = n.end(); - if(check) { - for(; child_it != child_it_end; ++child_it) { - TypeNode childType = (*child_it).getType(check); - if (!childType.isInteger()) { - throw TypeCheckingExceptionPrivate(n, "expecting an integer subterm"); - } - } - } - return nodeManager->integerType(); - } -};/* class IntOperatorTypeRule */ - -class RealOperatorTypeRule { -public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - { - TNode::iterator child_it = n.begin(); - TNode::iterator child_it_end = n.end(); - if(check) { - for(; child_it != child_it_end; ++child_it) { - TypeNode childType = (*child_it).getType(check); - if (!childType.isReal()) { - throw TypeCheckingExceptionPrivate(n, "expecting a real subterm"); - } - } - } - return nodeManager->realType(); - } -};/* class RealOperatorTypeRule */ - -class ArithPredicateTypeRule { -public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - { - if( check ) { - TypeNode lhsType = n[0].getType(check); - if (!lhsType.isReal()) { - throw TypeCheckingExceptionPrivate(n, "expecting an arithmetic term on the left-hand-side"); - } - TypeNode rhsType = n[1].getType(check); - if (!rhsType.isReal()) { - throw TypeCheckingExceptionPrivate(n, "expecting an arithmetic term on the right-hand-side"); - } - } - return nodeManager->booleanType(); - } -};/* class ArithPredicateTypeRule */ - -class ArithUnaryPredicateTypeRule { -public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - { - if( check ) { - TypeNode t = n[0].getType(check); - if (!t.isReal()) { - throw TypeCheckingExceptionPrivate(n, "expecting an arithmetic term"); - } - } - return nodeManager->booleanType(); - } -};/* class ArithUnaryPredicateTypeRule */ - -class IntUnaryPredicateTypeRule { -public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - { - if( check ) { - TypeNode t = n[0].getType(check); - if (!t.isInteger()) { - throw TypeCheckingExceptionPrivate(n, "expecting an integer term"); - } - } - return nodeManager->booleanType(); - } -};/* class IntUnaryPredicateTypeRule */ - class RealNullaryOperatorTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) @@ -169,18 +87,6 @@ public: } };/* class RealNullaryOperatorTypeRule */ -class DivisibleOpTypeRule -{ - public: - inline static TypeNode computeType(NodeManager* nodeManager, - TNode n, - bool check) - { - Assert(n.getKind() == kind::DIVISIBLE_OP); - return nodeManager->builtinOperatorType(); - } -}; /* class DivisibleOpTypeRule */ - }/* CVC4::theory::arith namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ |