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/printer | |
| parent | 82066be04ce068b59b24526fbc8c9b4188503cae (diff) | |
Add remaining transcendental functions (#1551)
Diffstat (limited to 'src/printer')
| -rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 20 |
1 files changed, 20 insertions, 0 deletions
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 24fd0924f..e06f8c062 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -425,6 +425,16 @@ void Smt2Printer::toStream(std::ostream& out, case kind::SINE: case kind::COSINE: case kind::TANGENT: + case kind::COSECANT: + case kind::SECANT: + case kind::COTANGENT: + case kind::ARCSINE: + case kind::ARCCOSINE: + case kind::ARCTANGENT: + case kind::ARCCOSECANT: + case kind::ARCSECANT: + case kind::ARCCOTANGENT: + case kind::SQRT: case kind::MINUS: case kind::UMINUS: case kind::LT: @@ -891,6 +901,16 @@ static string smtKindString(Kind k) case kind::SINE: return "sin"; case kind::COSINE: return "cos"; case kind::TANGENT: return "tan"; + case kind::COSECANT: return "csc"; + case kind::SECANT: return "sec"; + case kind::COTANGENT: return "cot"; + case kind::ARCSINE: return "arcsin"; + case kind::ARCCOSINE: return "arccos"; + case kind::ARCTANGENT: return "arctan"; + case kind::ARCCOSECANT: return "arccsc"; + case kind::ARCSECANT: return "arcsec"; + case kind::ARCCOTANGENT: return "arccot"; + case kind::SQRT: return "sqrt"; case kind::MINUS: return "-"; case kind::UMINUS: return "-"; case kind::LT: return "<"; |