updates to printer to get instantiations, take 1

src/ast/ast_pp_util.cpp

@@ -139,11 +139,18 @@ void ast_pp_util::pop(unsigned 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_is_defined.mark(m_defined.get(i), false);
     m_defined.shrink(old_sz);
     m_defined_lim.shrink(m_defined_lim.size() - n);
 }
 
+std::ostream& ast_pp_util::display_expr_def(std::ostream& out, expr* n) {
+    if (is_app(n) && to_app(n)->get_num_args() == 0)
+        return out << mk_pp(n, m);
+    else
+        return out << "$" << n->get_id();
+}
+
 std::ostream& ast_pp_util::define_expr(std::ostream& out, expr* n) {
     ptr_buffer<expr> visit;
     visit.push_back(n);
@@ -166,13 +173,11 @@ std::ostream& ast_pp_util::define_expr(std::ostream& out, expr* n) {
             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 {
+            if (to_app(n)->get_num_args() > 0) {
                 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(); 
+                    display_expr_def(out << " ", e);
                 out << ")\n";
             }
             continue;

src/ast/ast_pp_util.h

@@ -31,14 +31,14 @@ class ast_pp_util {
     stacked_value<unsigned> m_decls;
     stacked_value<unsigned> m_sorts;
     expr_mark               m_is_defined;
-    ptr_vector<expr>        m_defined;
+    expr_ref_vector         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) {}
+    
+    ast_pp_util(ast_manager& m): m(m), m_env(m), m_rec_decls(0), m_decls(0), m_sorts(0), coll(m), m_defined(m) {}
 
     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(); }
@@ -65,6 +65,8 @@ class ast_pp_util {
 
     std::ostream& define_expr(std::ostream& out, expr* f);
 
+    std::ostream& display_expr_def(std::ostream& out, expr* f);
+
     void push();
 
     void pop(unsigned n);

src/params/solver_params.pyg

@@ -6,6 +6,7 @@ def_module_params('solver',
                           ('cancel_backup_file', SYMBOL, '', "file to save partial search state if search is canceled"),
                           ('timeout', UINT, UINT_MAX, "timeout on the solver object; overwrites a global timeout"),
                           ('lemmas2console', BOOL, False, 'print lemmas during search'),
+                          ('instantiations2console', BOOL, False, 'print quantifier instantiations to the console'),
                           ('axioms2files', BOOL, False, 'print negated theory axioms to separate files during search'),
                           ))
 

src/sat/smt/euf_proof.cpp

@@ -199,27 +199,51 @@ namespace euf {
             return;
         if (!st.is_redundant() && !st.is_asserted()) 
             return;
+
+
+        if (!visit_clause(n, lits))
+            return;
+
         std::function<symbol(int)> ppth = [&](int th) {
             return m.get_family_name(th);
         };
-
-        expr_ref_vector clause(m);
+        if (!st.is_sat())
+            std::cout << "; " << sat::status_pp(st, ppth) << "\n";
+
+        display_clause(n, lits);
+    }
+
+
+    bool solver::visit_clause(unsigned n, literal const* lits) {
         for (unsigned i = 0; i < n; ++i) {
-            expr_ref e = literal2expr(lits[i]);
+            expr* e = bool_var2expr(lits[i].var());
             if (!e)
-                return;
-            clause.push_back(e);
-            m_clause_visitor.collect(e);
+                return false;
+            visit_expr(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";
+        return true;
+    }
+
+    void solver::display_clause(unsigned n, literal const* lits) {
         std::cout << "(assert (or";
-        for (expr* e : clause) 
-            std::cout << " $" << e->get_id();
+        for (unsigned i = 0; i < n; ++i) {
+            expr* e = bool_var2expr(lits[i].var());
+            if (lits[i].sign())
+                m_clause_visitor.display_expr_def(std::cout << " (not ", e) << ")";
+            else
+                m_clause_visitor.display_expr_def(std::cout << " ", e);
+        }
         std::cout << "))\n";
     }
 
+    void solver::visit_expr(expr* e) {
+        m_clause_visitor.collect(e);
+        m_clause_visitor.display_skolem_decls(std::cout);
+        m_clause_visitor.define_expr(std::cout, e);
+    }
+
+    void solver::display_expr(expr* e) {
+        m_clause_visitor.display_expr_def(std::cout, e);
+    }
+
 }

src/sat/smt/euf_solver.h

@@ -185,6 +185,7 @@ namespace euf {
         ast_pp_util m_clause_visitor;
         void log_clause(unsigned n, literal const* lits, sat::status st);
 
+
         // relevancy
         //bool_vector m_relevant_expr_ids;
         //bool_vector m_relevant_visited;
@@ -348,6 +349,10 @@ namespace euf {
         void drat_bool_def(sat::bool_var v, expr* n);
         void drat_eq_def(sat::literal lit, expr* eq);
         void drat_log_expr(expr* n);
+        bool visit_clause(unsigned n, literal const* lits);
+        void display_clause(unsigned n, literal const* lits);
+        void visit_expr(expr* e);
+        void display_expr(expr* e);
 
         // decompile
         bool extract_pb(std::function<void(unsigned sz, literal const* c, unsigned k)>& card,

src/sat/smt/q_ematch.cpp

@@ -382,7 +382,7 @@ namespace q {
         lits.push_back(~j.m_clause.m_literal);
         for (unsigned i = 0; i < j.m_clause.size(); ++i) 
             lits.push_back(instantiate(j.m_clause, j.m_binding, j.m_clause[i]));            
-        m_qs.log_instantiation(lits);
+        m_qs.log_instantiation(lits, &j);
         m_qs.add_clause(lits);               
     }
 

src/sat/smt/q_solver.cpp

@@ -24,6 +24,7 @@ Module Name:
 #include "sat/smt/euf_solver.h"
 #include "sat/smt/sat_th.h"
 #include "qe/lite/qe_lite.h"
+#include <iostream>
 
 
 namespace q {
@@ -356,7 +357,22 @@ namespace q {
         m_ematch.get_antecedents(l, idx, r, probing);
     }
 
-    void solver::log_instantiation(unsigned n, sat::literal const* lits) {
+    void solver::log_instantiation(unsigned n, sat::literal const* lits, justification* j) {
         TRACE("q", for (unsigned i = 0; i < n; ++i) tout << literal2expr(lits[i]) << "\n";);
+        if (get_config().m_instantiations2console) {
+
+            ctx.visit_clause(n, lits);
+            if (j) {
+                for (unsigned i = 0; i < j->m_clause.num_decls(); ++i)
+                    ctx.visit_expr(j->m_binding[i]->get_expr());
+                std::cout << "; (instantiation";
+                for (unsigned i = 0; i < j->m_clause.num_decls(); ++i) {
+                    std::cout << " ";
+                    ctx.display_expr(j->m_binding[i]->get_expr());
+                }
+                std::cout << ")\n";
+            }
+            ctx.display_clause(n, lits);
+        }
     }
 }

src/sat/smt/q_solver.h

@@ -88,9 +88,9 @@ namespace q {
         sat::literal_vector const& universal() const { return m_universal; }
         quantifier* flatten(quantifier* q);
 
-        void log_instantiation(sat::literal q, sat::literal i) { sat::literal lits[2] = { q, i }; log_instantiation(2, lits); }
-        void log_instantiation(sat::literal_vector const& lits) { log_instantiation(lits.size(), lits.data()); }
-        void log_instantiation(unsigned n, sat::literal const* lits);
+        void log_instantiation(sat::literal q, sat::literal i, justification* j = nullptr) { sat::literal lits[2] = { q, i }; log_instantiation(2, lits, j); }
+        void log_instantiation(sat::literal_vector const& lits, justification* j) { log_instantiation(lits.size(), lits.data(), j); }
+        void log_instantiation(unsigned n, sat::literal const* lits, justification* j);
 
     };
 }

src/smt/params/smt_params.cpp

@@ -63,6 +63,7 @@ void smt_params::updt_local_params(params_ref const & _p) {
     solver_params sp(_p);
     m_axioms2files = sp.axioms2files();
     m_lemmas2console = sp.lemmas2console();
+    m_instantiations2console = sp.instantiations2console();
 }
 
 void smt_params::updt_params(params_ref const & p) {

src/smt/params/smt_params.h

@@ -175,6 +175,7 @@ struct smt_params : public preprocessor_params,
     // -----------------------------------
     bool              m_axioms2files = false;
     bool              m_lemmas2console = false;
+    bool              m_instantiations2console = false;
     symbol            m_logic = symbol::null;
 
     // -----------------------------------