From 6796ea7e49414d93dedc96f16379588b416bd51c Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 7 Oct 2022 19:22:36 +0200
Subject: [PATCH] add new files

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/sat/smt/q_proof_checker.cpp | 60 +++++++++++++++++++++++++++++++++
 src/sat/smt/q_proof_checker.h   | 60 +++++++++++++++++++++++++++++++++
 2 files changed, 120 insertions(+)
 create mode 100644 src/sat/smt/q_proof_checker.cpp
 create mode 100644 src/sat/smt/q_proof_checker.h

diff --git a/src/sat/smt/q_proof_checker.cpp b/src/sat/smt/q_proof_checker.cpp
new file mode 100644
index 000000000..eecf10fe6
--- /dev/null
+++ b/src/sat/smt/q_proof_checker.cpp
@@ -0,0 +1,60 @@
+/*++
+Copyright (c) 2022 Microsoft Corporation
+
+Module Name:
+
+    q_proof_checker.cpp
+
+Abstract:
+
+    Plugin for checking quantifier instantiations
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2022-10-07
+
+--*/
+
+#include "ast/rewriter/var_subst.h"
+#include "sat/smt/q_proof_checker.h"
+#include "sat/smt/q_solver.h"
+
+namespace q {
+        
+    expr_ref_vector proof_checker::clause(app* jst) {
+        expr_ref_vector result(m);
+        for (expr* arg : *jst) 
+            if (!is_bind(arg))
+                result.push_back(arg);
+        return result;
+    }
+
+    expr_ref_vector proof_checker::binding(app* jst) {
+        expr_ref_vector result(m);
+        for (expr* arg : *jst) 
+            if (is_bind(arg))
+                result.push_back(to_app(arg)->get_arg(0));
+        return result;        
+    }
+    
+    void proof_checker::vc(app* jst, expr_ref_vector& clause) {
+        expr* q = nullptr;
+        if (!is_inst(jst))
+            return;
+        SASSERT(clause.size() >= 2);
+        VERIFY(m.is_not(clause.get(0), q) && is_forall(q));
+        auto inst = binding(jst);
+        expr_ref qi = instantiate(m, to_quantifier(q), inst.begin());
+        clause[0] = m.mk_not(qi);
+    }
+
+    bool proof_checker::is_inst(expr* jst) {
+        return is_app(jst) && to_app(jst)->get_name() == m_inst && m.mk_proof_sort() == jst->get_sort();
+    }
+
+    bool proof_checker::is_bind(expr* e) {
+        return is_app(e) && to_app(e)->get_name() == m_bind  && m.mk_proof_sort() == e->get_sort();
+    }
+
+    
+}
diff --git a/src/sat/smt/q_proof_checker.h b/src/sat/smt/q_proof_checker.h
new file mode 100644
index 000000000..d60737585
--- /dev/null
+++ b/src/sat/smt/q_proof_checker.h
@@ -0,0 +1,60 @@
+/*++
+Copyright (c) 2022 Microsoft Corporation
+
+Module Name:
+
+    q_proof_checker.h
+
+Abstract:
+
+    Plugin for checking quantifier instantiations
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2022-10-07
+
+
+--*/
+#pragma once
+
+#include "util/obj_pair_set.h"
+#include "ast/ast_trail.h"
+#include "ast/ast_util.h"
+#include "sat/smt/euf_proof_checker.h"
+#include <iostream>
+
+namespace q {
+
+    class proof_checker : public euf::proof_checker_plugin {
+        ast_manager& m;
+        symbol       m_inst;
+        symbol       m_bind;
+
+        expr_ref_vector binding(app* jst);
+
+        bool is_inst(expr* jst);
+
+        bool is_bind(expr* e);
+        
+    public:
+        proof_checker(ast_manager& m): 
+            m(m),
+            m_inst("inst"),
+            m_bind("bind") {
+            }
+
+        ~proof_checker() override {}
+        
+        expr_ref_vector clause(app* jst) override;
+
+        bool check(app* jst) override { return false; }
+
+        void register_plugins(euf::proof_checker& pc) override {
+            pc.register_plugin(symbol("inst"), this);
+        }
+
+        void vc(app* jst, expr_ref_vector& clause) override;
+        
+    };
+
+}