diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-04-28 15:50:17 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-04-28 15:50:23 +0200 |
commit | c6855bb13420c020690cf63c8b770186f278081c (patch) | |
tree | 7b8e6a340ce9561a223f5417dda16440d784e8c9 /src/printer | |
parent | 1261597c32e3c8a98225a91fdd7b420867f89329 (diff) |
Fix smt2 printing of fun-def. Simplification of mbqi interface.
Diffstat (limited to 'src/printer')
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index a98a106a1..7648a1587 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -32,6 +32,7 @@ #include "theory/theory_model.h" #include "theory/arrays/theory_arrays_rewriter.h" +#include "theory/quantifiers/term_database.h" using namespace std; @@ -589,9 +590,14 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, case kind::INST_PATTERN: break; case kind::INST_PATTERN_LIST: - // TODO user patterns for(unsigned i=0; i<n.getNumChildren(); i++) { - out << ":pattern " << n[i]; + if( n[i].getKind()==kind::INST_ATTRIBUTE ){ + if( n[i][0].getAttribute(theory::FunDefAttribute()) ){ + out << ":fun-def"; + } + }else{ + out << ":pattern " << n[i]; + } } return; break; |