set low-level pretty printer by default from fixedpoint context

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/ast/ast_smt_pp.cpp

@@ -949,6 +949,10 @@ public:
         mark.mark(s, true);
     }
 
+    void operator()(sort* s) {
+        ast_mark mark;
+        pp_sort_decl(mark, s);
+    }
 
     void operator()(func_decl* d) {
         if (m_is_smt2) {
@@ -962,7 +966,6 @@ public:
             m_out << ") ";
             visit_sort(d->get_range());
             m_out << ")";
-            newline();
         }
         else {
             m_out << "(";
@@ -1021,6 +1024,22 @@ void ast_smt_pp::display_expr_smt2(std::ostream& strm, expr* n, unsigned indent,
     p(n);
 }
 
+void ast_smt_pp::display_ast_smt2(std::ostream& strm, ast* a, unsigned indent, unsigned num_var_names, char const* const* var_names) {
+    ptr_vector<quantifier> ql;
+    smt_renaming rn;
+    smt_printer p(strm, m_manager, ql, rn, m_logic, false, true, m_simplify_implies, indent, num_var_names, var_names);
+    if (is_expr(a)) {
+        p(to_expr(a));
+    }
+    else if (is_func_decl(a)) {
+        p(to_func_decl(a));
+    }
+    else {
+        SASSERT(is_sort(a));
+        p(to_sort(a));
+    }
+}
+
 
 void ast_smt_pp::display_smt2(std::ostream& strm, expr* n) {
     ptr_vector<quantifier> ql;
@@ -1071,6 +1090,7 @@ void ast_smt_pp::display_smt2(std::ostream& strm, expr* n) {
         if (!(*m_is_declared)(d)) {
             smt_printer p(strm, m_manager, ql, rn, m_logic, true, true, m_simplify_implies, 0);
             p(d);
+            strm << "\n";
         }
     }
 
@@ -1079,6 +1099,7 @@ void ast_smt_pp::display_smt2(std::ostream& strm, expr* n) {
         if (!(*m_is_declared)(d)) {
             smt_printer p(strm, m_manager, ql, rn, m_logic, true, true, m_simplify_implies, 0);
             p(d);
+            strm << "\n";
         }
     }
 

src/ast/ast_smt_pp.h

@@ -79,22 +79,23 @@ public:
     void display_smt2(std::ostream& strm, expr* n);
     void display_expr(std::ostream& strm, expr* n);
     void display_expr_smt2(std::ostream& strm, expr* n, unsigned indent = 0, unsigned num_var_names = 0, char const* const* var_names = 0);
+    void display_ast_smt2(std::ostream& strm, ast* n, unsigned indent = 0, unsigned num_var_names = 0, char const* const* var_names = 0);
 
 };
 
 struct mk_smt_pp {
-    expr * m_expr;
+    ast*   m_ast;
     ast_manager& m_manager;
     unsigned m_indent;
     unsigned m_num_var_names;
     char const* const* m_var_names;
-    mk_smt_pp(expr* e, ast_manager & m, unsigned indent = 0, unsigned num_var_names = 0, char const* const* var_names = 0) :
+    mk_smt_pp(ast* e, ast_manager & m, unsigned indent = 0, unsigned num_var_names = 0, char const* const* var_names = 0) :
-        m_expr(e), m_manager(m), m_indent(indent), m_num_var_names(num_var_names), m_var_names(var_names) {}
+        m_ast(e), m_manager(m), m_indent(indent), m_num_var_names(num_var_names), m_var_names(var_names) {}
 };
 
 inline std::ostream& operator<<(std::ostream& out, const mk_smt_pp & p) {
     ast_smt_pp pp(p.m_manager);
-    pp.display_expr_smt2(out, p.m_expr, p.m_indent, p.m_num_var_names, p.m_var_names);
+    pp.display_ast_smt2(out, p.m_ast, p.m_indent, p.m_num_var_names, p.m_var_names);
     return out;
 }
 

src/muz_qe/dl_context.cpp

@@ -994,6 +994,7 @@ namespace datalog {
         p.insert(":profile-timeout-milliseconds", CPK_UINT, "instructions and rules that took less than the threshold will not be printed when printed the instruction/rule list");
                       
         p.insert(":print-with-fixedpoint-extensions", CPK_BOOL, "(default true) use SMT-LIB2 fixedpoint extensions, instead of pure SMT2, when printing rules");
+        p.insert(":print-low-level-smt2", CPK_BOOL, "(default true) use (faster) low-level SMT2 printer (the printer is scalable but the result may not be as readable)");
         
         PRIVATE_PARAMS(
             p.insert(":dbg-fpr-nonempty-relation-signature", CPK_BOOL, 
@@ -1650,6 +1651,9 @@ namespace datalog {
         expr_ref_vector rules(m);
         svector<symbol> names;
         bool use_fixedpoint_extensions = m_params.get_bool(":print-with-fixedpoint-extensions", true);
+        bool print_low_level = m_params.get_bool(":print-low-level-smt2", true);
+
+#define PP(_e_) if (print_low_level) out << mk_smt_pp(_e_, m); else ast_smt2_pp(out, _e_, env, params);
 
         get_rules_as_formulas(rules, names);
 
@@ -1684,18 +1688,18 @@ namespace datalog {
         obj_hashtable<sort>& sorts = visitor.sorts();
         obj_hashtable<sort>::iterator sit = sorts.begin(), send = sorts.end();
         for (; sit != send; ++sit) {
-            ast_smt2_pp(out, *sit, env, params);
+            PP(*sit);
         }
         for (; it != end; ++it) {
             func_decl* f = *it;
-            ast_smt2_pp(out, f, env, params);
+            PP(f);
             out << "\n";
         }
         it = rels.begin(); end = rels.end();
         for (; it != end; ++it) {
             func_decl* f = *it;
             out << "(declare-rel " << f->get_name() << " (";
-            for (unsigned i = 0; i < f->get_arity(); ++i) {
+            for (unsigned i = 0; i < f->get_arity(); ++i) {                
                 ast_smt2_pp(out, f->get_domain(i), env, params);
                 if (i + 1 < f->get_arity()) {
                     out << " ";
@@ -1714,7 +1718,7 @@ namespace datalog {
 
         for (unsigned i = 0; i < num_axioms; ++i) {
             out << "(assert ";
-            ast_smt2_pp(out, axioms[i], env, params);
+            PP(axioms[i]);
             out << ")\n";
         }
         for (unsigned i = 0; i < rules.size(); ++i) {            
@@ -1724,12 +1728,7 @@ namespace datalog {
             if (symbol::null != nm) {
                 out << "(! ";
             }
-            if (use_fixedpoint_extensions) {
+            PP(r);
-                ast_smt2_pp(out, r, env, params);
-            }
-            else {
-                out << mk_smt_pp(r, m);
-            }
             if (symbol::null != nm) {
                 while (fresh_names.contains(nm)) {
                     std::ostringstream s;
@@ -1744,7 +1743,7 @@ namespace datalog {
         if (use_fixedpoint_extensions) {
             for (unsigned i = 0; i < num_queries; ++i) {
                 out << "(query ";
-                ast_smt2_pp(out, queries[i], env, params);
+                PP(queries[i]);
                 out << ")\n";
             }
         }
@@ -1754,7 +1753,7 @@ namespace datalog {
                 out << "(assert ";
                 expr_ref q(m);
                 q = m.mk_not(queries[i]);
-                ast_smt2_pp(out, q, env, params);
+                PP(q);
                 out << ")\n";
                 out << "(check-sat)\n";
                 if (num_queries > 1) out << "(pop)\n";