summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@gmail.com>2012-07-14 21:14:39 +0000
committerMorgan Deters <mdeters@gmail.com>2012-07-14 21:14:39 +0000
commit1c42109395b566a0068cc3ae9067fc87ab8f8e7b (patch)
tree3f1d0969cf11e48a19bbdb52542e90e51e62e034 /src
parentc0b6815fc17bf798988be66931ea7ba914956fc4 (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.cpp24
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);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback