diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-07-10 16:22:19 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-07-10 16:22:26 -0500 |
| commit | 2c0482cfb9b8164670cf56187e127d38c5d05bcf (patch) | |
| tree | 804f7806944b9175fdaea8cc919566ca302ddf09 /src/printer | |
| parent | 0e513c05b2e0ae3b8e2d08514ccb8007258f963b (diff) | |
Merge ntExt branch. Adds support for transcendental functions. Refactoring of non-linear extension. Add factoring lemma scheme for non-linear. Add regressions.
Diffstat (limited to 'src/printer')
| -rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 074041262..2ba593377 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -383,6 +383,10 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, case kind::PLUS: case kind::MULT: case kind::NONLINEAR_MULT: + case kind::EXPONENTIAL: + case kind::SINE: + case kind::COSINE: + case kind::TANGENT: case kind::MINUS: case kind::UMINUS: case kind::LT: @@ -817,6 +821,10 @@ static string smtKindString(Kind k) throw() { case kind::PLUS: return "+"; case kind::MULT: case kind::NONLINEAR_MULT: return "*"; + case kind::EXPONENTIAL: return "exp"; + case kind::SINE: return "sin"; + case kind::COSINE: return "cos"; + case kind::TANGENT: return "tan"; case kind::MINUS: return "-"; case kind::UMINUS: return "-"; case kind::LT: return "<"; |