mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity

re-adding simplified constraints based on model converter

Browse source 
Signed-off-by: Miguel Angelo Da Terra Neves <t-mineve@microsoft.com>
This commit is contained in:
Miguel Angelo Da Terra Neves 2017-11-21 13:24:14 -08:00
parent d2f52ca359
commit 773d938925
2 changed files with 33 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

34
src/sat/tactic/goal2sat.cpp
View file

@ -885,7 +885,8 @@ struct sat2goal::imp {
sat::model_converter m_mc;
expr_ref_vector m_var2expr;
generic_model_converter_ref m_fmc; // filter for eliminating fresh variables introduced in the assertion-set --> sat conversion
generic_model_converter_ref m_imc; // used to ensure correctness in incremental calls with simplifications that require model conversions
sat_model_converter(ast_manager & m):
m_var2expr(m) {
}
@ -894,6 +895,7 @@ struct sat2goal::imp {
sat_model_converter(ast_manager & m, sat::solver const & s):m_var2expr(m) {
m_mc.copy(s.get_model_converter());
m_fmc = alloc(generic_model_converter, m);
m_imc = nullptr;
}
ast_manager & m() { return m_var2expr.get_manager(); }
@ -920,6 +922,7 @@ struct sat2goal::imp {
insert(l.var(), m().mk_fresh_const(0, m().mk_bool_sort()), true);
}
}
m_imc = nullptr;
}
virtual void operator()(model_ref & md) {
@ -1026,7 +1029,34 @@ struct sat2goal::imp {
}
void operator()(expr_ref& formula) override {
NOT_IMPLEMENTED_YET();
if (!m_imc) {
m_imc = alloc(generic_model_converter, m());
sat::literal_vector updates;
m_mc.expand(updates);
sat::literal_vector clause;
expr_ref_vector tail(m());
expr_ref def(m());
for (sat::literal l : updates) {
if (l == sat::null_literal) {
sat::literal lit0 = clause[0];
for (unsigned i = 1; i < clause.size(); ++i) {
tail.push_back(lit2expr(~clause[i]));
}
def = m().mk_or(lit2expr(lit0), mk_and(tail));
if (lit0.sign()) {
lit0.neg();
def = m().mk_not(def);
}
m_imc->add(lit2expr(lit0), def);
clause.reset();
tail.reset();
}
else {
clause.push_back(l);
}
}
}
(*m_imc)(formula);
}
};

2
src/tactic/generic_model_converter.cpp
View file

@ -104,7 +104,6 @@ void generic_model_converter::operator()(expr_ref& fml) {
unsigned min_idx = min_proc.m_min;
for (unsigned i = m_add_entries.size(); i-- > min_idx;) {
entry const& e = m_add_entries[i];
m_add_entries.pop_back();
unsigned arity = e.m_f->get_arity();
if (arity == 0) {
fml = m.mk_and(fml, m.mk_eq(m.mk_const(e.m_f), e.m_def));
@ -115,5 +114,6 @@ void generic_model_converter::operator()(expr_ref& fml) {
if (m_first_idx[e.m_f] == i) {
m_first_idx.remove(e.m_f);
}
m_add_entries.pop_back();
}
}