diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-04-14 20:41:19 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-04-14 20:41:19 +0000 |
commit | 068985035a64d556cbfc2e46af44566c01e0a5e0 (patch) | |
tree | 5c6a9c58eb0d740dec1f651bb7701028ae1beb73 /src/printer | |
parent | 7e289e28e54afa144032048443202a88fa124cb5 (diff) |
Three things:
1. Infrastructure for unit T-conflicts added to SAT proxy
(and also the theory output channel documentation);
previously theories could not communicate unit T-conflicts
with the SAT layer because that layer had an implicit
assumption (not asserted) that the conflict nodes were an AND.
2. UF now pre-rewrites trivial equalities to "true". These could
conceivably occur in artificial benchmarks in this form:
(let (?x BIG-HUGE-TERM) ... (= ?x ?x) ... )
3. The SMT-LIBv2 printer now properly prints Bool constants.
Diffstat (limited to 'src/printer')
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 91a529bc2..9bad4c7b5 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -74,6 +74,11 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, } break; } + case kind::CONST_BOOLEAN: + // the default would print "1" or "0" for bool, that's not correct + // for our purposes + out << (n.getConst<bool>() ? "true" : "false"); + break; default: // fall back on whatever operator<< does on underlying type; we // might luck out and be SMT-LIB v2 compliant |