diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-04-14 16:34:59 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-04-14 16:34:59 -0500 |
commit | 9d7766ed1e41da53d59ad16e9ef8be8f522226df (patch) | |
tree | a0b20c6b013c2a7731c080abee6793cd91b30b1d /src/printer/smt2 | |
parent | 8748256b518f5ad4b1cefe46d9445b562199871c (diff) |
Fix nullary operator printers, minor.
Diffstat (limited to 'src/printer/smt2')
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 41 |
1 files changed, 18 insertions, 23 deletions
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index fcb6be366..57c02f3c7 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -117,29 +117,21 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, // variable if(n.isVar()) { - if( n.getKind() == kind::SEP_NIL ){ - out << "(as sep.nil " << n.getType() << ")"; - return; - }else if( n.getKind() == kind::UNIVERSE_SET ){ - out << "(as univset " << n.getType() << ")"; - return; - }else{ - string s; - if(n.getAttribute(expr::VarNameAttr(), s)) { - out << maybeQuoteSymbol(s); + string s; + if(n.getAttribute(expr::VarNameAttr(), s)) { + out << maybeQuoteSymbol(s); + } else { + if(n.getKind() == kind::VARIABLE) { + out << "var_"; } else { - if(n.getKind() == kind::VARIABLE) { - out << "var_"; - } else { - out << n.getKind() << '_'; - } - out << n.getId(); - } - if(types) { - // print the whole type, but not *its* type - out << ":"; - n.getType().toStream(out, language::output::LANG_SMTLIB_V2_5); + out << n.getKind() << '_'; } + out << n.getId(); + } + if(types) { + // print the whole type, but not *its* type + out << ":"; + n.getType().toStream(out, language::output::LANG_SMTLIB_V2_5); } return; @@ -520,7 +512,8 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, case kind::SET_TYPE: case kind::SINGLETON: case kind::COMPLEMENT:out << smtKindString(k) << " "; break; - + case kind::UNIVERSE_SET:out << "(as univset " << n.getType() << ")";break; + // fp theory case kind::FLOATINGPOINT_FP: case kind::FLOATINGPOINT_EQ: @@ -594,12 +587,14 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, case kind::PARAMETRIC_DATATYPE: break; - //separation + //separation logic case kind::SEP_EMP: case kind::SEP_PTO: case kind::SEP_STAR: case kind::SEP_WAND:out << smtKindString(k) << " "; break; + case kind::SEP_NIL:out << "(as sep.nil " << n.getType() << ")";break; + // quantifiers case kind::FORALL: case kind::EXISTS: |