mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-28 17:08:45 +00:00
Code Activity

continue updates for adding proof-log to smt core

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-11-23 07:59:32 +07:00
parent c7781f346d
commit 5374142e3e
2 changed files with 3 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/params/smt_params.cpp
View file

@ -64,6 +64,7 @@ void smt_params::updt_local_params(params_ref const & _p) {
m_axioms2files = sp.axioms2files(); m_axioms2files = sp.axioms2files();
m_lemmas2console = sp.lemmas2console(); m_lemmas2console = sp.lemmas2console();
m_instantiations2console = sp.instantiations2console(); m_instantiations2console = sp.instantiations2console();
m_proof_log = sp.proof_log();
} }
void smt_params::updt_params(params_ref const & p) { void smt_params::updt_params(params_ref const & p) {
@ -126,6 +127,7 @@ void smt_params::display(std::ostream & out) const {
DISPLAY_PARAM(m_ematching); DISPLAY_PARAM(m_ematching);
DISPLAY_PARAM(m_induction); DISPLAY_PARAM(m_induction);
DISPLAY_PARAM(m_clause_proof); DISPLAY_PARAM(m_clause_proof);
DISPLAY_PARAM(m_proof_log);
DISPLAY_PARAM(m_case_split_strategy); DISPLAY_PARAM(m_case_split_strategy);
DISPLAY_PARAM(m_rel_case_split_order); DISPLAY_PARAM(m_rel_case_split_order);

1
src/smt/params/smt_params.h
View file

@ -112,6 +112,7 @@ struct smt_params : public preprocessor_params,
bool m_ematching = true; bool m_ematching = true;
bool m_induction = false; bool m_induction = false;
bool m_clause_proof = false; bool m_clause_proof = false;
symbol m_proof_log;
// ----------------------------------- // -----------------------------------
// //