overhaul of proof format for new solver

This commit overhauls the proof format (in development) for the new core.

NOTE: this functionality is work in progress with a long way to go.
It is shielded by the sat.euf option, which is off by default and in pre-release state.
It is too early to fuzz or use it. It is pushed into master to shed light on road-map for certifying inferences of sat.euf.

It retires the ad-hoc extension of DRUP used by the SAT solver.
Instead it relies on SMT with ad-hoc extensions for proof terms.
It adds the following commands (consumed by proof_cmds.cpp):

- assume  - for input clauses
- learn   - when a clause is learned (or redundant clause is added)
- del     - when a clause is deleted.

The commands take a list of expressions of type Bool and the
last argument can optionally be of type Proof.
When the last argument is of type Proof it is provided as a hint
to justify the learned clause.

Proof hints can be checked using a self-contained proof
checker. The sat/smt/euf_proof_checker.h class provides
a plugin dispatcher for checkers.
It is instantiated with a checker for arithmetic lemmas,
so far for Farkas proofs.

Use example:
```
(set-option :sat.euf true)
(set-option :tactic.default_tactic smt)
(set-option :sat.smt.proof f.proof)
(declare-const x Int)
(declare-const y Int)
(declare-const z Int)
(declare-const u Int)
(assert (< x y))
(assert (< y z))
(assert (< z x))
(check-sat)
```

Run z3 on a file with above content.
Then run z3 on f.proof

```
(verified-smt)
(verified-smt)
(verified-smt)
(verified-farkas)
(verified-smt)
```

src/ast/ast.cpp

@@ -889,8 +889,10 @@ void basic_decl_plugin::set_manager(ast_manager * m, family_id id) {
 }
 
 void basic_decl_plugin::get_sort_names(svector<builtin_name> & sort_names, symbol const & logic) {
-    if (logic == symbol::null)
+    if (logic == symbol::null) {
         sort_names.push_back(builtin_name("bool", BOOL_SORT));
+        sort_names.push_back(builtin_name("Proof", PROOF_SORT)); // reserved name?
+    }
     sort_names.push_back(builtin_name("Bool", BOOL_SORT));
 }
 

src/ast/ast_pp_util.cpp

@@ -175,14 +175,14 @@ std::ostream& ast_pp_util::define_expr(std::ostream& out, expr* n) {
             visit.pop_back();
             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
+                out << mk_ismt2_func(to_app(n)->get_decl(), m);
                 for (auto* e : *to_app(n)) 
                     display_expr_def(out << " ", e);
-                out << ")\n";
+                out << "))\n";
             }
             continue;
         }
-        out << "(define-const $" << n->get_id() << " " << mk_pp(n->get_sort(), m) << " " << mk_pp(n, m) << "\n";                
+        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();        

src/ast/scoped_proof.h

@@ -29,8 +29,8 @@ class scoped_proof_mode {
         m.toggle_proof_mode(mode);
     }
     ~scoped_proof_mode() {
-            m.toggle_proof_mode(m_mode);            
-        }
+        m.toggle_proof_mode(m_mode);            
+    }
 
 };
 

src/cmd_context/CMakeLists.txt

@@ -11,6 +11,7 @@ z3_add_component(cmd_context
     simplify_cmd.cpp
     tactic_cmds.cpp
     tactic_manager.cpp
+    proof_cmds.cpp
   COMPONENT_DEPENDENCIES
     rewriter
     solver

src/cmd_context/cmd_context.cpp

@@ -561,6 +561,7 @@ cmd_context::~cmd_context() {
     finalize_cmds();
     finalize_tactic_cmds();
     finalize_probes();
+    m_proof_cmds = nullptr;
     reset(true);
     m_mcs.reset();
     m_solver = nullptr;

src/cmd_context/cmd_context.h

@@ -39,6 +39,7 @@ Module Name:
 #include "solver/progress_callback.h"
 #include "cmd_context/pdecl.h"
 #include "cmd_context/tactic_manager.h"
+#include "cmd_context/proof_cmds.h"
 #include "params/context_params.h"
 
 
@@ -172,6 +173,7 @@ class ast_context_params : public context_params {
     bool owns_manager() const { return m_manager != nullptr; }
 };
 
+
 class cmd_context : public progress_callback, public tactic_manager, public ast_printer_context {
 public:
     enum status {
@@ -225,6 +227,7 @@ class cmd_context : public progress_callback, public tactic_manager, public ast_
     bool                         m_ignore_check = false;      // used by the API to disable check-sat() commands when parsing SMT 2.0 files.
     bool                         m_exit_on_error = false;
     bool                         m_allow_duplicate_declarations = false;
+    scoped_ptr<proof_cmds>       m_proof_cmds;
 
     static std::ostringstream    g_error_stream;
 
@@ -397,6 +400,8 @@ class cmd_context : public progress_callback, public tactic_manager, public ast_
     pdecl_manager & pm() const { if (!m_pmanager) const_cast<cmd_context*>(this)->init_manager(); return *m_pmanager; }
     sexpr_manager & sm() const { if (!m_sexpr_manager) const_cast<cmd_context*>(this)->m_sexpr_manager = alloc(sexpr_manager); return *m_sexpr_manager; }
 
+    proof_cmds& get_proof_cmds() { if (!m_proof_cmds) m_proof_cmds = proof_cmds::mk(m()); return *m_proof_cmds; }
+
     void set_solver_factory(solver_factory * s);
     void set_check_sat_result(check_sat_result * r) { m_check_sat_result = r; }
     check_sat_result * get_check_sat_result() const { return m_check_sat_result.get(); }

src/cmd_context/proof_cmds.cpp

@@ -0,0 +1,207 @@
+/*++
+Copyright (c) 2022 Microsoft Corporation
+
+Module Name:
+
+    proof_cmds.cpp
+
+Abstract:
+
+    Commands for reading and checking proofs.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2022-8-26
+
+Notes:
+
+- add theory hint bypass using proof checker plugins of SMT
+  - arith_proof_checker.h is currently
+- could use m_drat for drup premises.
+
+--*/
+
+#include "util/small_object_allocator.h"
+#include "ast/ast_util.h"
+#include "cmd_context/cmd_context.h"
+#include "smt/smt_solver.h"
+#include "sat/sat_solver.h"
+#include "sat/sat_drat.h"
+#include "sat/smt/euf_proof_checker.h"
+#include <iostream>
+
+class smt_checker {
+    ast_manager& m;
+    params_ref   m_params;
+    euf::proof_checker m_checker;
+
+    scoped_ptr<solver> m_solver;
+
+#if 0
+    sat::solver  sat_solver;
+    sat::drat    m_drat;
+    sat::literal_vector m_units;
+    sat::literal_vector m_drup_units;
+
+    void add_units() {
+        auto const& units = m_drat.units();
+        for (unsigned i = m_units.size(); i < units.size(); ++i)
+            m_units.push_back(units[i].first);
+    }
+#endif
+
+public:
+    smt_checker(ast_manager& m):
+        m(m),
+        m_checker(m)
+        // sat_solver(m_params, m.limit()), 
+        // m_drat(sat_solver) 
+    {
+        m_solver = mk_smt_solver(m, m_params, symbol());
+    }
+
+    void check(expr_ref_vector const& clause, expr* proof_hint) {
+
+        if (m_checker.check(clause, proof_hint)) {
+            if (is_app(proof_hint))
+                std::cout << "(verified-" << to_app(proof_hint)->get_name() << ")\n";
+            else
+                std::cout << "(verified-checker)\n";
+            return;
+        }
+
+        m_solver->push();
+        for (expr* lit : clause)
+            m_solver->assert_expr(m.mk_not(lit));
+        lbool is_sat = m_solver->check_sat();
+        if (is_sat != l_false) {
+            std::cout << "did not verify: " << is_sat << " " << clause << "\n\n";
+            m_solver->display(std::cout);
+            if (is_sat == l_true) {
+                model_ref mdl;
+                m_solver->get_model(mdl);
+                std::cout << *mdl << "\n";
+            }                
+            exit(0);
+        }
+        m_solver->pop(1);
+        std::cout << "(verified-smt)\n";
+        // assume(clause);
+    }
+
+    void assume(expr_ref_vector const& clause) {
+        m_solver->assert_expr(mk_or(clause));
+    }
+};
+
+class proof_cmds::imp {
+    ast_manager& m;
+    expr_ref_vector m_lits;
+    expr_ref m_proof_hint;
+    smt_checker m_checker;
+public:
+    imp(ast_manager& m): m(m), m_lits(m), m_proof_hint(m), m_checker(m) {}
+
+    void add_literal(expr* e) {
+        if (m.is_proof(e))
+            m_proof_hint = e;
+        else
+            m_lits.push_back(e);
+    }
+
+    void end_assumption() {
+        m_checker.assume(m_lits);
+        m_lits.reset();
+        m_proof_hint.reset();
+    }
+
+    void end_learned() {
+        m_checker.check(m_lits, m_proof_hint);
+        m_lits.reset();
+        m_proof_hint.reset();
+    }
+
+    void end_deleted() {
+        m_lits.reset();
+        m_proof_hint.reset();
+    }
+};
+
+proof_cmds* proof_cmds::mk(ast_manager& m) {
+    return alloc(proof_cmds, m);
+}
+
+proof_cmds::proof_cmds(ast_manager& m) {
+    m_imp = alloc(imp, m);
+}
+
+proof_cmds::~proof_cmds() {
+    dealloc(m_imp);
+}
+
+void proof_cmds::add_literal(expr* e) {
+    m_imp->add_literal(e);
+}
+
+void proof_cmds::end_assumption() {
+    m_imp->end_assumption();
+}
+
+void proof_cmds::end_learned() {
+    m_imp->end_learned();
+}
+
+void proof_cmds::end_deleted() {
+    m_imp->end_deleted();
+}
+
+// assumption
+class assume_cmd : public cmd {
+public:
+    assume_cmd():cmd("assume") {}
+    char const* get_usage() const override { return "<expr>+"; }
+    char const * get_descr(cmd_context& ctx) const override { return "proof command for adding assumption (input assertion)"; }
+    unsigned get_arity() const override { return VAR_ARITY; }
+    void prepare(cmd_context & ctx) override {}
+    void finalize(cmd_context & ctx) override {}
+    void failure_cleanup(cmd_context & ctx) override {}
+    cmd_arg_kind next_arg_kind(cmd_context & ctx) const override { return CPK_EXPR; }    
+    void set_next_arg(cmd_context & ctx, expr * arg) override { ctx.get_proof_cmds().add_literal(arg); }
+    void execute(cmd_context& ctx) override { ctx.get_proof_cmds().end_assumption(); }
+};
+
+// deleted clause
+class del_cmd : public cmd {
+public:
+    del_cmd():cmd("del") {}
+    char const* get_usage() const override { return "<expr>+"; }
+    char const * get_descr(cmd_context& ctx) const override { return "proof command for clause deletion"; }
+    unsigned get_arity() const override { return VAR_ARITY; }
+    void prepare(cmd_context & ctx) override {}
+    void finalize(cmd_context & ctx) override {}
+    void failure_cleanup(cmd_context & ctx) override {}
+    cmd_arg_kind next_arg_kind(cmd_context & ctx) const override { return CPK_EXPR; }    
+    void set_next_arg(cmd_context & ctx, expr * arg) override { ctx.get_proof_cmds().add_literal(arg); }
+    void execute(cmd_context& ctx) override { ctx.get_proof_cmds().end_deleted(); }
+};
+
+// learned/redundant clause
+class learn_cmd : public cmd {
+public:
+    learn_cmd():cmd("learn") {}
+    char const* get_usage() const override { return "<expr>+"; }
+    char const * get_descr(cmd_context& ctx) const override { return "proof command for learned (redundant) clauses"; }
+    unsigned get_arity() const override { return VAR_ARITY; }
+    void prepare(cmd_context & ctx) override {}
+    void finalize(cmd_context & ctx) override {}
+    void failure_cleanup(cmd_context & ctx) override {}
+    cmd_arg_kind next_arg_kind(cmd_context & ctx) const override { return CPK_EXPR; }    
+    void set_next_arg(cmd_context & ctx, expr * arg) override { ctx.get_proof_cmds().add_literal(arg); }
+    void execute(cmd_context& ctx) override { ctx.get_proof_cmds().end_learned(); }
+};
+
+void install_proof_cmds(cmd_context & ctx) {
+    ctx.insert(alloc(del_cmd));
+    ctx.insert(alloc(learn_cmd));
+    ctx.insert(alloc(assume_cmd));
+}

src/cmd_context/proof_cmds.h

@@ -0,0 +1,49 @@
+/*++
+Copyright (c) 2022 Microsoft Corporation
+
+Module Name:
+
+    proof_cmds.h
+
+Abstract:
+    Commands for reading proofs.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2022-8-26
+
+Notes:
+
+--*/
+#pragma once
+
+/**
+   proof_cmds is a structure that tracks an evidence trail.
+
+   The main interface is to:
+     add literals one by one,
+     add proof hints
+     until receiving end-command: assumption, learned, deleted.
+   Evidence can be checked:
+     - By DRUP
+     - Theory lemmas
+
+*/
+
+
+class proof_cmds {
+    class imp;
+    imp* m_imp;
+public:
+    static proof_cmds* mk(ast_manager& m);
+    proof_cmds(ast_manager& m);
+    ~proof_cmds();
+    void add_literal(expr* e);
+    void end_assumption();
+    void end_learned();
+    void end_deleted();
+};
+
+class cmd_context;
+void install_proof_cmds(cmd_context & ctx);
+