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

Update initialization order

Browse source
This commit is contained in:
Arie Gurfinkel 2018-05-21 09:46:15 -07:00
parent aeb2f3c4bb
commit 4de58a42fe
2 changed files with 35 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

39
src/muz/spacer/spacer_context.cpp
View file

@ -1720,7 +1720,7 @@ void pred_transformer::add_premises(decl2rel const& pts, unsigned lvl, datalog::
} }
} }
void pred_transformer::inherit_properties(pred_transformer& other) void pred_transformer::inherit_lemmas(pred_transformer& other)
{m_frames.inherit_frames (other.m_frames);} {m_frames.inherit_frames (other.m_frames);}
app* pred_transformer::extend_initial (expr *e) app* pred_transformer::extend_initial (expr *e)
@ -2091,24 +2091,37 @@ void context::init_rules(datalog::rule_set& rules, decl2rel& rels)
for (auto &entry : rels) {entry.m_value->init_reach_facts();} for (auto &entry : rels) {entry.m_value->init_reach_facts();}
} }
void context::inherit_properties(const decl2rel &rels) { void context::inherit_lemmas(const decl2rel &rels) {
for (auto &entry : rels) { for (auto &entry : rels) {
pred_transformer *pt = nullptr; pred_transformer *pt = nullptr;
if (m_rels.find(entry.m_key, pt)) { if (m_rels.find(entry.m_key, pt)) {
entry.m_value->inherit_properties(*pt); entry.m_value->inherit_lemmas(*pt);
} }
} }
} }
void context::update_rules(datalog::rule_set& rules) void context::update_rules(datalog::rule_set& rules)
{ {
decl2rel rels; decl2rel rels;
init_lemma_generalizers(rules); // SMT params must be set before any expression is asserted to any
// solver
init_global_smt_params();
// constructs new pred transformers and asserts trans and init
init_rules(rules, rels); init_rules(rules, rels);
inherit_properties(rels); // inherits lemmas from m_rels into rels
reset(); inherit_lemmas(rels);
for (auto &entry : rels) { // switch context to new rels
m_rels.insert(entry.m_key, entry.m_value); init(rels);
// re-initialize lemma generalizers
init_lemma_generalizers();
} }
void context::init(const decl2rel &rels) {
// reset context. Current state is all stored in rels
reset();
// re-initialize context
for (auto &entry : rels)
{m_rels.insert(entry.m_key, entry.m_value);}
} }
unsigned context::get_num_levels(func_decl* p) unsigned context::get_num_levels(func_decl* p)
@ -2250,9 +2263,8 @@ void context::reset_lemma_generalizers()
m_lemma_generalizers.reset(); m_lemma_generalizers.reset();
} }
void context::init_lemma_generalizers(datalog::rule_set& rules) // initialize global SMT parameters shared by all solvers
{ void context::init_global_smt_params() {
reset_lemma_generalizers();
m.toggle_proof_mode(PGM_ENABLED); m.toggle_proof_mode(PGM_ENABLED);
smt_params &fparams = m_pm.fparams (); smt_params &fparams = m_pm.fparams ();
if (!m_params.spacer_eq_prop ()) { if (!m_params.spacer_eq_prop ()) {
@ -2282,6 +2294,11 @@ void context::init_lemma_generalizers(datalog::rule_set& rules)
fparams.m_ng_lift_ite = LI_FULL; fparams.m_ng_lift_ite = LI_FULL;
} }
}
void context::init_lemma_generalizers()
{
reset_lemma_generalizers();
if (m_params.spacer_q3_use_qgen()) { if (m_params.spacer_q3_use_qgen()) {
m_lemma_generalizers.push_back(alloc(lemma_bool_inductive_generalizer, m_lemma_generalizers.push_back(alloc(lemma_bool_inductive_generalizer,
*this, 0, true)); *this, 0, true));

10
src/muz/spacer/spacer_context.h
View file

@ -428,7 +428,7 @@ public:
void add_premises(decl2rel const& pts, unsigned lvl, expr_ref_vector& r); void add_premises(decl2rel const& pts, unsigned lvl, expr_ref_vector& r);
void inherit_properties(pred_transformer& other); void inherit_lemmas(pred_transformer& other);
void ground_free_vars(expr* e, app_ref_vector& vars, ptr_vector<app>& aux_vars, void ground_free_vars(expr* e, app_ref_vector& vars, ptr_vector<app>& aux_vars,
bool is_init); bool is_init);
@ -811,8 +811,9 @@ class context {
// Initialization // Initialization
void init_lemma_generalizers(datalog::rule_set& rules); void init_lemma_generalizers();
void inherit_properties(const decl2rel& rels); void inherit_lemmas(const decl2rel& rels);
void init_global_smt_params();
bool check_invariant(unsigned lvl); bool check_invariant(unsigned lvl);
bool check_invariant(unsigned lvl, func_decl* fn); bool check_invariant(unsigned lvl, func_decl* fn);
@ -821,6 +822,9 @@ class context {
void init_rules(datalog::rule_set& rules, decl2rel& transformers); void init_rules(datalog::rule_set& rules, decl2rel& transformers);
// (re)initialize context with new relations
void init(const decl2rel &rels);
void simplify_formulas(); void simplify_formulas();
void reset_lemma_generalizers(); void reset_lemma_generalizers();