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/parser/smt2 | |
| parent | 82066be04ce068b59b24526fbc8c9b4188503cae (diff) | |
Add remaining transcendental functions (#1551)
Diffstat (limited to 'src/parser/smt2')
| -rw-r--r-- | src/parser/smt2/smt2.cpp | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index e4f6569b8..77b50af4c 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -61,6 +61,17 @@ void Smt2::addArithmeticOperators() { addOperator(kind::SINE, "sin"); addOperator(kind::COSINE, "cos"); addOperator(kind::TANGENT, "tan"); + addOperator(kind::COSECANT, "csc"); + addOperator(kind::SECANT, "sec"); + addOperator(kind::COTANGENT, "cot"); + addOperator(kind::ARCSINE, "arcsin"); + addOperator(kind::ARCCOSINE, "arccos"); + addOperator(kind::ARCTANGENT, "arctan"); + addOperator(kind::ARCCOSECANT, "arccsc"); + addOperator(kind::ARCSECANT, "arcsec"); + addOperator(kind::ARCCOTANGENT, "arccot"); + + addOperator(kind::SQRT, "sqrt"); } void Smt2::addBitvectorOperators() { |