#5429

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

src/parsers/smt2/smt2parser.cpp

@@ -3118,6 +3118,25 @@ namespace smt2 {
             return sexpr_ref(nullptr, sm());
         }
 
+        sort_ref parse_sort_ref(char const* context) {
+            m_num_bindings    = 0;
+            m_num_open_paren = 0;
+
+            unsigned found_errors = 0;
+            try {
+                scan_core();
+                parse_sort(context);
+                if (!sort_stack().empty()) {
+                    return sort_ref(sort_stack().back(), m());
+                }
+            }
+            catch (z3_exception & ex) {
+                error(ex.msg());
+            }
+            return sort_ref(nullptr, m());
+        }
+
+
         bool operator()() {
             m_num_bindings    = 0;
             unsigned found_errors = 0;
@@ -3190,6 +3209,11 @@ bool parse_smt2_commands(cmd_context & ctx, std::istream & is, bool interactive,
     return p();
 }
 
+sort_ref parse_smt2_sort(cmd_context & ctx, std::istream & is, bool interactive, params_ref const & ps, char const * filename) {
+    smt2::parser p(ctx, is, interactive, ps, filename);
+    return p.parse_sort_ref(filename);
+}
+
 sexpr_ref parse_sexpr(cmd_context& ctx, std::istream& is, params_ref const& ps, char const* filename) {
     smt2::parser p(ctx, is, false, ps, filename);
     return p.parse_sexpr_ref();

src/parsers/smt2/smt2parser.h

@@ -24,3 +24,4 @@ bool parse_smt2_commands(cmd_context & ctx, std::istream & is, bool interactive
 
 sexpr_ref parse_sexpr(cmd_context& ctx, std::istream& is, params_ref const& ps, char const* filename);
 
+sort_ref parse_smt2_sort(cmd_context & ctx, std::istream & is, bool interactive, params_ref const & ps, char const * filename);

src/sat/dimacs.cpp

@@ -165,6 +165,10 @@ namespace dimacs {
             return out << "f " << r.m_node_id << " " << r.m_name << " " << r.m_args << "0\n";
         case drat_record::tag_t::is_bool_def:
             return out << "b " << r.m_node_id << " " << r.m_args << "0\n";
+        case drat_record::tag_t::is_var:
+            return out << "v " << r.m_node_id << " " << r.m_name << " " << r.m_args << "0\n";
+        case drat_record::tag_t::is_quantifier:
+            return out << "q " << r.m_node_id << " " << r.m_name << " " << r.m_args << "0\n";
         }
         return out;
     }
@@ -256,6 +260,23 @@ namespace dimacs {
                 m_record.m_args.push_back(n);
             }
         };
+        auto parse_var = [&]() {
+            ++in;
+            skip_whitespace(in);
+            n = parse_int(in, err);                    
+            skip_whitespace(in);
+            m_record.m_name = parse_sexpr();
+            m_record.m_tag = drat_record::tag_t::is_var;
+            m_record.m_node_id = n;
+            m_record.m_args.reset();
+            n = parse_int(in, err);
+            if (n < 0)
+                throw lex_error();
+            m_record.m_args.push_back(n);
+            n = parse_int(in, err);
+            if (n != 0)
+                throw lex_error();
+        };
         try {
         loop:
             skip_whitespace(in);
@@ -290,6 +311,12 @@ namespace dimacs {
                 // parse expression definition
                 parse_ast(drat_record::tag_t::is_node);
                 break;
+            case 'v':
+                parse_var();
+                break;
+            case 'q':
+                parse_ast(drat_record::tag_t::is_quantifier);
+                break;
             case 'f':
                 // parse function declaration
                 parse_ast(drat_record::tag_t::is_decl);

src/sat/dimacs.h

@@ -53,7 +53,7 @@ namespace dimacs {
     };
 
     struct drat_record {
-        enum class tag_t { is_clause, is_node, is_decl, is_sort, is_bool_def };
+        enum class tag_t { is_clause, is_node, is_decl, is_sort, is_bool_def, is_var, is_quantifier };
         tag_t            m_tag{ tag_t::is_clause };
         // a clause populates m_lits and m_status
         // a node populates m_node_id, m_name, m_args

src/sat/smt/euf_proof.cpp

@@ -41,12 +41,32 @@ namespace euf {
             for (expr* arg : *a)
                 get_drat().def_add_arg(arg->get_id());
             get_drat().def_end();
-            m_drat_asts.insert(e);
-            push(insert_obj_trail<ast>(m_drat_asts, e));
         }
-        else {
-            IF_VERBOSE(0, verbose_stream() << "logging binders is TBD\n");
+        else if (is_var(e)) {
+            var* v = to_var(e);
+            std::stringstream strm;
+            strm << mk_pp(e->get_sort(), m);
+            get_drat().def_begin('v', v->get_id(), strm.str());
+            get_drat().def_add_arg(v->get_idx());
+            get_drat().def_end();
         }
+        else if (is_quantifier(e)) {
+            quantifier* q = to_quantifier(e);
+            std::stringstream strm;
+            strm << "(";
+            strm << (is_forall(q) ? "forall" : (is_exists(q) ? "exists" : "lambda"));
+            for (unsigned i = 0; i < q->get_num_decls(); ++i) {
+                strm << " (" << q->get_decl_name(i) << " " << mk_pp(q->get_decl_sort(i), m) << ")";
+            }
+            strm << ")";
+            get_drat().def_begin('q', q->get_id(), strm.str());
+            get_drat().def_add_arg(q->get_expr()->get_id());
+            get_drat().def_end();
+        }
+        else 
+            UNREACHABLE();
+        m_drat_asts.insert(e);
+        push(insert_obj_trail<ast>(m_drat_asts, e));
     }
 
     void solver::drat_log_expr(expr* e) {
@@ -61,6 +81,11 @@ namespace euf {
                 for (expr* arg : *to_app(e))
                     if (!m_drat_asts.contains(arg))
                         m_drat_todo.push_back(arg);
+            if (is_quantifier(e)) {
+                expr* arg = to_quantifier(e)->get_expr();
+                if (!m_drat_asts.contains(arg))
+                    m_drat_todo.push_back(arg);                
+            }                
             if (m_drat_todo.size() != sz)
                 continue;
             drat_log_expr1(e);

src/shell/drat_frontend.cpp

@@ -171,6 +171,34 @@ public:
     unsigned_vector params;
     ptr_vector<sort> sorts;
 
+    void parse_quantifier(sexpr_ref const& sexpr, cmd_context& ctx, quantifier_kind& k, sort_ref_vector& domain, svector<symbol>& names) {
+        k = quantifier_kind::forall_k;
+        if (sexpr->get_kind() != sexpr::kind_t::COMPOSITE)
+            goto bail;
+        unsigned sz = sexpr->get_num_children();
+        if (sz == 0)
+            goto bail;
+        symbol q = sexpr->get_child(0)->get_symbol();
+        if (q == "forall")
+            k = quantifier_kind::forall_k;
+        else if (q == "exists")
+            k = quantifier_kind::exists_k;
+        else if (q == "lambda")            
+            k = quantifier_kind::lambda_k;
+        else
+            goto bail;
+        for (unsigned i = 1; i < sz; ++i) {
+            std::cout << "parse bound\n";
+        }
+        return;
+    bail:
+        std::cout << "Could not parse expression\n";
+        sexpr->display(std::cout);
+        std::cout << "\n";
+        exit(0);        
+
+    }
+
     void parse_sexpr(sexpr_ref const& sexpr, cmd_context& ctx, expr_ref_vector const& args, expr_ref& result) {
         params.reset();
         sorts.reset();
@@ -310,7 +338,17 @@ static void verify_smt(char const* drat_file, char const* smt_file) {
             std::istringstream strm(r.m_name);
             auto sexpr = parse_sexpr(ctx, strm, p, drat_file);
             checker.parse_sexpr(sexpr, ctx, args, e);
-            exprs.reserve(r.m_node_id+1);
+            exprs.reserve(r.m_node_id + 1);
+            exprs.set(r.m_node_id, e);
+            break;
+        }
+        case dimacs::drat_record::tag_t::is_var: {
+            var_ref e(m);
+            SASSERT(r.m_args.size() == 1);
+            std::istringstream strm(r.m_name);
+            auto srt = parse_smt2_sort(ctx, strm, false, p, drat_file);
+            e = m.mk_var(r.m_args[0], srt);
+            exprs.reserve(r.m_node_id + 1);
             exprs.set(r.m_node_id, e);
             break;
         }
@@ -331,12 +369,26 @@ static void verify_smt(char const* drat_file, char const* smt_file) {
                 srt = pd->instantiate(ctx.pm(), sargs.size(), sargs.data());
             else 
                 srt = m.mk_uninterpreted_sort(name);
-            sorts.reserve(r.m_node_id+1);
+            sorts.reserve(r.m_node_id + 1);
             sorts.set(r.m_node_id, srt);
             break;
         }
+        case dimacs::drat_record::tag_t::is_quantifier: {
+            quantifier_ref q(m);      
+            std::istringstream strm(r.m_name);
+            auto sexpr = parse_sexpr(ctx, strm, p, drat_file);
+            sort_ref_vector domain(m);
+            svector<symbol> names;
+            quantifier_kind k;
+            checker.parse_quantifier(sexpr, ctx, k, domain, names);
+            sexpr->display(std::cout << "QQ ");
+            std::cout << "\n";
+            exprs.reserve(r.m_node_id + 1);
+            exprs.set(r.m_node_id, m.mk_true());
+            break;
+        }
         case dimacs::drat_record::tag_t::is_bool_def:
-            bool_var2expr.reserve(r.m_node_id+1);
+            bool_var2expr.reserve(r.m_node_id + 1);
             bool_var2expr.set(r.m_node_id, exprs.get(r.m_args[0]));
             break;
         default: