succinct logging

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Aug 24, 2022 · fb8532b · fb8532b
1 parent 74c61f4
commit fb8532b
Show file tree

Hide file tree

Showing 5 changed files with 81 additions and 18 deletions.
diff --git a/src/ast/ast_pp_util.cpp b/src/ast/ast_pp_util.cpp
@@ -129,11 +129,58 @@ void ast_pp_util::push() {
     m_rec_decls.push();
     m_decls.push();
     m_sorts.push();
+    m_defined_lim.push_back(m_defined.size());
 }
 
 void ast_pp_util::pop(unsigned n) {
     coll.pop(n);
     m_rec_decls.pop(n);
     m_decls.pop(n);
     m_sorts.pop(n);
+    unsigned old_sz = m_defined_lim[m_defined_lim.size() - n];
+    for (unsigned i = m_defined.size(); i-- > old_sz; ) 
+        m_is_defined.mark(m_defined[i], false);
+    m_defined.shrink(old_sz);
+    m_defined_lim.shrink(m_defined_lim.size() - n);
+}
+
+std::ostream& ast_pp_util::define_expr(std::ostream& out, expr* n) {
+    ptr_buffer<expr> visit;
+    visit.push_back(n);
+    while (!visit.empty()) {
+        n = visit.back();
+        if (m_is_defined.is_marked(n)) {
+            visit.pop_back();
+            continue;
+        }
+        if (is_app(n)) {
+            bool all_visit = true;
+            for (auto* e : *to_app(n)) {
+                if (m_is_defined.is_marked(e))
+                    continue;
+                all_visit = false;
+                visit.push_back(e);
+            }
+            if (!all_visit)
+                continue;
+            m_defined.push_back(n);
+            m_is_defined.mark(n, true);
+            visit.pop_back();
+            if (to_app(n)->get_num_args() == 0) 
+                out << "(define-const $" << n->get_id() << " " << mk_pp(n->get_sort(), m) << " " << mk_pp(n, m) << "\n";                
+            else {
+                out << "(define-const $" << n->get_id() << " " << mk_pp(n->get_sort(), m) << " (";            
+                out << to_app(n)->get_name(); // fixme
+                for (auto* e : *to_app(n)) 
+                    out << " $" << e->get_id(); 
+                out << ")\n";
+            }
+            continue;
+        }
+        out << "(define-const $" << n->get_id() << " " << mk_pp(n->get_sort(), m) << " " << mk_pp(n, m) << "\n";                
+        m_defined.push_back(n);
+        m_is_defined.mark(n, true);
+        visit.pop_back();        
+    }
+    return out;
 }
diff --git a/src/ast/ast_pp_util.h b/src/ast/ast_pp_util.h
@@ -30,15 +30,18 @@ class ast_pp_util {
     stacked_value<unsigned> m_rec_decls;
     stacked_value<unsigned> m_decls;
     stacked_value<unsigned> m_sorts;
+    expr_mark               m_is_defined;
+    ptr_vector<expr>        m_defined;
+    unsigned_vector         m_defined_lim;
 
  public:
 
     decl_collector      coll;
 
     ast_pp_util(ast_manager& m): m(m), m_env(m), m_rec_decls(0), m_decls(0), m_sorts(0), coll(m) {}
 
-    void reset() { coll.reset(); m_removed.reset(); m_sorts.clear(0u); m_decls.clear(0u); m_rec_decls.clear(0u); }
-
+    void reset() { coll.reset(); m_removed.reset(); m_sorts.clear(0u); m_decls.clear(0u); m_rec_decls.clear(0u); 
+        m_is_defined.reset(); m_defined.reset(); m_defined_lim.reset(); }
 
     void collect(expr* e);
 
@@ -60,6 +63,8 @@ class ast_pp_util {
 
     std::ostream& display_expr(std::ostream& out, expr* f, bool neat = true);
 
+    std::ostream& define_expr(std::ostream& out, expr* f);
+
     void push();
 
     void pop(unsigned n);

diff --git a/src/sat/smt/euf_proof.cpp b/src/sat/smt/euf_proof.cpp
@@ -195,22 +195,31 @@ namespace euf {
     }
 
     void solver::log_clause(unsigned n, literal const* lits, sat::status st) {
-        if (get_config().m_lemmas2console) {
-            std::function<symbol(int)> ppth = [&](int th) {
-                return m.get_family_name(th);
-            };
-            if (st.is_redundant() || st.is_asserted()) {
-                expr_ref_vector clause(m);
-                for (unsigned i = 0; i < n; ++i) {
-                    expr_ref e = literal2expr(lits[i]);
-                    if (!e)
-                        return;
-                    clause.push_back(e);
-                }
-                expr_ref cl = mk_or(clause);
-                std::cout << sat::status_pp(st, ppth) << " " << cl << "\n";
-            }
+        if (!get_config().m_lemmas2console) 
+            return;
+        if (!st.is_redundant() && !st.is_asserted()) 
+            return;
+        std::function<symbol(int)> ppth = [&](int th) {
+            return m.get_family_name(th);
+        };
+
+        expr_ref_vector clause(m);
+        for (unsigned i = 0; i < n; ++i) {
+            expr_ref e = literal2expr(lits[i]);
+            if (!e)
+                return;
+            clause.push_back(e);
+            m_clause_visitor.collect(e);
         }
+        m_clause_visitor.display_skolem_decls(std::cout);
+        for (expr* e : clause)
+            m_clause_visitor.define_expr(std::cout, e);
+        if (!st.is_sat())
+            std::cout << "; " << sat::status_pp(st, ppth) << "\n";
+        std::cout << "(assert (or";
+        for (expr* e : clause) 
+            std::cout << " $" << e->get_id();
+        std::cout << "))\n";
     }
 
 }
diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp
@@ -49,7 +49,8 @@ namespace euf {
         m_lookahead(nullptr),
         m_to_m(&m),
         m_to_si(&si),
-        m_values(m)
+        m_values(m),
+        m_clause_visitor(m)
     {
         updt_params(p);
         m_relevancy.set_enabled(get_config().m_relevancy_lvl > 2);

diff --git a/src/sat/smt/euf_solver.h b/src/sat/smt/euf_solver.h
@@ -182,6 +182,7 @@ namespace euf {
         obj_hashtable<ast> m_drat_asts;
         bool m_drat_initialized{ false };
         void init_drat();
+        ast_pp_util m_clause_visitor;
         void log_clause(unsigned n, literal const* lits, sat::status st);
 
         // relevancy