mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 03:32:28 +00:00
Code Activity

cleanup, fix repeated use of fmls in validator

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2012-12-03 16:02:04 -08:00
parent 72e09759ee
commit 1cd1a42618
5 changed files with 8 additions and 64 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/muz_qe/dl_context.cpp
View file

@ -925,13 +925,14 @@ namespace datalog {
m_cancel = false;
if (m_pdr.get()) m_pdr->cleanup();
if (m_bmc.get()) m_bmc->cleanup();
if (m_rel.get()) m_rel->cleanup();
}
class context::engine_type_proc {
ast_manager& m;
arith_util a;
ast_manager& m;
arith_util a;
datatype_util dt;
DL_ENGINE m_engine;
DL_ENGINE m_engine;
public:
engine_type_proc(ast_manager& m): m(m), a(m), dt(m), m_engine(DATALOG_ENGINE) {}

9
src/muz_qe/dl_context.h
View file

@ -417,15 +417,6 @@ namespace datalog {
*/
bool result_contains_fact(relation_fact const& f);
#if 0
/**
\brief display facts generated for query.
*/
void display_output_facts(std::ostream & out) const {
get_rel_context().get_rmanager().display_output_tables(out);
}
#endif
rel_context& get_rel_context() { ensure_rel(); return *m_rel; }
private:

3
src/muz_qe/pdr_context.cpp
View file

@ -1387,7 +1387,7 @@ namespace pdr {
break;
}
case l_false: {
expr_ref_vector refs(m), fmls(m);
expr_ref_vector refs(m);
expr_ref tmp(m);
model_ref model;
vector<relation_info> rs;
@ -1402,6 +1402,7 @@ namespace pdr {
for (unsigned i = 0; i < rules.size(); ++i) {
datalog::rule& r = *rules[i];
model->eval(r.get_head(), tmp);
expr_ref_vector fmls(m);
fmls.push_back(m.mk_not(tmp));
unsigned utsz = r.get_uninterpreted_tail_size();
unsigned tsz = r.get_tail_size();

50
src/muz_qe/pdr_util.cpp
View file

@ -86,48 +86,6 @@ namespace pdr {
return res.str();
}
/////////////////////////
// select elimination rewriter
//
class select_elim {
ast_manager& m;
array_util a;
model_ref m_model;
public:
select_elim(ast_manager& m, model_ref& md): m(m), a(m), m_model(md) {}
br_status mk_app_core(func_decl* f, unsigned num_args, expr* const* args, expr_ref& result) {
if (a.is_select(f)) {
expr_ref tmp(m);
tmp = m.mk_app(f, num_args, args);
m_model->eval(tmp, result);
return BR_DONE;
}
else {
return BR_FAILED;
}
}
};
struct select_elim_cfg: public default_rewriter_cfg {
select_elim m_r;
bool rewrite_patterns() const { return false; }
br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
return m_r.mk_app_core(f, num, args, result);
}
select_elim_cfg(ast_manager & m, model_ref& md, params_ref const & p):m_r(m, md) {}
};
class select_elim_star : public rewriter_tpl<select_elim_cfg> {
select_elim_cfg m_cfg;
public:
select_elim_star(ast_manager & m, model_ref& md, params_ref const & p = params_ref()):
rewriter_tpl<select_elim_cfg>(m, false, m_cfg),
m_cfg(m, md, p) {}
};
/////////////////////////
@ -238,13 +196,6 @@ namespace pdr {
result.push_back(m.mk_not(e));
}
}
#if 0
select_elim_star select_elim(m, m_model);
for (unsigned i = 0; i < result.size(); ++i) {
select_elim(result[i].get(), tmp);
result[i] = tmp;
}
#endif
reset();
TRACE("pdr",
tout << "minimized model:\n";
@ -1266,6 +1217,5 @@ namespace pdr {
template class rewriter_tpl<pdr::ite_hoister_cfg>;
template class rewriter_tpl<pdr::select_elim_cfg>;

3
src/muz_qe/rel_context.h
View file

@ -73,7 +73,8 @@ namespace datalog {
void inherit_predicate_kind(func_decl* new_pred, func_decl* orig_pred);
void cancel() { m_cancel = true; }
void cleanup() { m_cancel = false; }
/**