mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
add new files
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
35639c5ac0
commit
6796ea7e49
60
src/sat/smt/q_proof_checker.cpp
Normal file
60
src/sat/smt/q_proof_checker.cpp
Normal file
|
@ -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();
|
||||
}
|
||||
|
||||
|
||||
}
|
60
src/sat/smt/q_proof_checker.h
Normal file
60
src/sat/smt/q_proof_checker.h
Normal file
|
@ -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;
|
||||
|
||||
};
|
||||
|
||||
}
|
Loading…
Reference in a new issue