From c6855bb13420c020690cf63c8b770186f278081c Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Tue, 28 Apr 2015 15:50:17 +0200
Subject: Fix smt2 printing of fun-def. Simplification of mbqi interface.

---
 src/printer/smt2/smt2_printer.cpp | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

(limited to 'src/printer/smt2/smt2_printer.cpp')

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;
-- 
cgit v1.2.3