mirror of
https://github.com/Z3Prover/z3
synced 2025-08-22 19:17:53 +00:00
ac1552d194
move self-checking functionality to inside sat/smt so it can be used on-line and not just off-line. when self-validation fails, use vs, not clause, to check. It allows self-validation without checking and maintaining RUP validation. new options sat.smt.proof.check_rup, sat.smt.proof.check for online validation. z3 sat.smt.proof.check=true sat.euf=true /v:1 sat.smt.proof.check_rup=true /st file.smt2 sat.smt.proof=p.smt2
58 lines
1.1 KiB
C++
58 lines
1.1 KiB
C++
/*++
|
|
Copyright (c) 2022 Microsoft Corporation
|
|
|
|
Module Name:
|
|
|
|
q_theory_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 theory_checker : public euf::theory_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:
|
|
theory_checker(ast_manager& m):
|
|
m(m),
|
|
m_inst("inst"),
|
|
m_bind("bind") {
|
|
}
|
|
|
|
expr_ref_vector clause(app* jst) override;
|
|
|
|
bool check(app* jst) override { return false; }
|
|
|
|
void register_plugins(euf::theory_checker& pc) override {
|
|
pc.register_plugin(symbol("inst"), this);
|
|
}
|
|
|
|
bool vc(app* jst, expr_ref_vector const& clause, expr_ref_vector& v) override;
|
|
|
|
};
|
|
|
|
}
|