diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-07-14 21:14:39 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-07-14 21:14:39 +0000 |
commit | 1c42109395b566a0068cc3ae9067fc87ab8f8e7b (patch) | |
tree | 3f1d0969cf11e48a19bbdb52542e90e51e62e034 /src | |
parent | c0b6815fc17bf798988be66931ea7ba914956fc4 (diff) |
Applying Dejan's patch for bug #369, which resolves it by adding a new (let..) form for each introduced binding.
Diffstat (limited to 'src')
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 24 |
1 files changed, 10 insertions, 14 deletions
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 7fa00a6e4..640f4209c 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -46,28 +46,24 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, visitor.run(dv, n); const theory::SubstitutionMap& lets = dv.getLets(); if(!lets.empty()) { - out << "(let ("; - bool first = true; - for(theory::SubstitutionMap::const_iterator i = lets.begin(); - i != lets.end(); - ++i) { - if(!first) { - out << ' '; - } else { - first = false; - } - out << '('; + theory::SubstitutionMap::const_iterator i = lets.begin(); + theory::SubstitutionMap::const_iterator i_end = lets.end(); + for(; i != i_end; ++ i) { + out << "(let (("; toStream(out, (*i).second, toDepth, types); out << ' '; toStream(out, (*i).first, toDepth, types); - out << ')'; + out << ")) "; } - out << ") "; } Node body = dv.getDagifiedBody(); toStream(out, body, toDepth, types); if(!lets.empty()) { - out << ')'; + theory::SubstitutionMap::const_iterator i = lets.begin(); + theory::SubstitutionMap::const_iterator i_end = lets.end(); + for(; i != i_end; ++ i) { + out << ")"; + } } } else { toStream(out, n, toDepth, types); |