diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-02-07 09:12:59 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-02-07 09:12:59 -0600 |
| commit | 0533b9009d23a39bcc78ef85d6e98b62ef304351 (patch) | |
| tree | e32b823d509e1c9b54dfe4230d075b8396f48b9c /src/theory/arith/kinds | |
| parent | 82066be04ce068b59b24526fbc8c9b4188503cae (diff) | |
Add remaining transcendental functions (#1551)
Diffstat (limited to 'src/theory/arith/kinds')
| -rw-r--r-- | src/theory/arith/kinds | 22 |
1 files changed, 22 insertions, 0 deletions
diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds index 34ae30f4c..3073d0078 100644 --- a/src/theory/arith/kinds +++ b/src/theory/arith/kinds @@ -31,6 +31,17 @@ operator EXPONENTIAL 1 "exponential" operator SINE 1 "sine" operator COSINE 1 "consine" operator TANGENT 1 "tangent" +operator COSECANT 1 "cosecant" +operator SECANT 1 "secant" +operator COTANGENT 1 "cotangent" +operator ARCSINE 1 "arc sine" +operator ARCCOSINE 1 "arc consine" +operator ARCTANGENT 1 "arc tangent" +operator ARCCOSECANT 1 "arc cosecant" +operator ARCSECANT 1 "arc secant" +operator ARCCOTANGENT 1 "arc cotangent" + +operator SQRT 1 "square root" constant DIVISIBLE_OP \ ::CVC4::Divisible \ @@ -105,6 +116,17 @@ 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 nullaryoperator PI "pi" |