mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00
Code Activity

Merge pull request #9 from TheRealNebus/opt

Browse source 
Opt
This commit is contained in:
Nikolaj Bjorner 2017-11-21 13:32:05 -08:00 committed by GitHub
parent c6cb739b44 773d938925
commit 2d4d51d1e9
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
4 changed files with 110 additions and 42 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/api/dotnet/Solver.cs
View file

@ -429,11 +429,12 @@ namespace Microsoft.Z3
var lvl = BacktrackLevel;
BacktrackLevel = uint.MaxValue;
ASTVector r = new ASTVector(Context, Native.Z3_solver_cube(Context.nCtx, NativeObject, lvl));
if (r.Size == 1 && ((Expr)r[0]).IsFalse) {
var v = r.ToBoolExprArray();
if (v.Length == 1 && v[0].IsFalse) {
break;
}
yield return r.ToBoolExprArray();
if (r.Size == 0) {
yield return v;
if (v.Length == 0) {
break;
}
}

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);
}
};

95
src/tactic/generic_model_converter.cpp
View file

@ -18,6 +18,7 @@ Notes:
--*/
#include "ast/ast_pp.h"
#include "ast/for_each_expr.h"
#include "tactic/generic_model_converter.h"
#include "model/model_v2_pp.h"
#include "model/model_evaluator.h"
@ -30,59 +31,89 @@ void generic_model_converter::operator()(model_ref & md) {
ev.set_expand_array_equalities(false);
expr_ref val(m);
unsigned arity;
for (unsigned i = m_entries.size(); i-- > 0; ) {
entry const& e = m_entries[i];
switch (e.m_instruction) {
case HIDE:
md->unregister_decl(e.m_f);
break;
case ADD:
ev(e.m_def, val);
TRACE("model_converter", tout << e.m_f->get_name() << " ->\n" << e.m_def << "\n==>\n" << val << "\n";);
arity = e.m_f->get_arity();
if (arity == 0) {
md->register_decl(e.m_f, val);
}
else {
func_interp * new_fi = alloc(func_interp, m, arity);
new_fi->set_else(val);
md->register_decl(e.m_f, new_fi);
}
break;
for (unsigned i = m_hide_entries.size(); i-- > 0; ) {
entry const& e = m_hide_entries[i];
md->unregister_decl(e.m_f);
}
for (unsigned i = m_add_entries.size(); i-- > 0; ) {
entry const& e = m_add_entries[i];
ev(e.m_def, val);
TRACE("model_converter", tout << e.m_f->get_name() << " ->\n" << e.m_def << "\n==>\n" << val << "\n";);
arity = e.m_f->get_arity();
if (arity == 0) {
md->register_decl(e.m_f, val);
}
else {
func_interp * new_fi = alloc(func_interp, m, arity);
new_fi->set_else(val);
md->register_decl(e.m_f, new_fi);
}
}
TRACE("model_converter", tout << "after generic_model_converter\n"; model_v2_pp(tout, *md););
}
void generic_model_converter::display(std::ostream & out) {
for (entry const& e : m_entries) {
switch (e.m_instruction) {
case HIDE:
display_del(out, e.m_f);
break;
case ADD:
display_add(out, m, e.m_f, e.m_def);
break;
}
for (entry const& e : m_hide_entries) {
display_del(out, e.m_f);
}
for (entry const& e : m_add_entries) {
display_del(out, e.m_f);
}
}
model_converter * generic_model_converter::translate(ast_translation & translator) {
ast_manager& to = translator.to();
generic_model_converter * res = alloc(generic_model_converter, to);
for (entry const& e : m_entries)
res->m_entries.push_back(entry(translator(e.m_f.get()), translator(e.m_def.get()), to, e.m_instruction));
for (entry const& e : m_hide_entries) {
res->m_hide_entries.push_back(entry(translator(e.m_f.get()), translator(e.m_def.get()), to, e.m_instruction));
}
for (entry const& e : m_add_entries) {
res->m_add_entries.push_back(entry(translator(e.m_f.get()), translator(e.m_def.get()), to, e.m_instruction));
}
return res;
}
void generic_model_converter::collect(ast_pp_util& visitor) {
m_env = &visitor.env();
for (entry const& e : m_entries) {
for (entry const& e : m_hide_entries) {
visitor.coll.visit_func(e.m_f);
}
for (entry const& e : m_add_entries) {
visitor.coll.visit_func(e.m_f);
if (e.m_def) visitor.coll.visit(e.m_def);
}
}
struct min_app_idx_proc {
unsigned m_min;
obj_map<func_decl, unsigned>& m_idxs;
min_app_idx_proc(obj_map<func_decl, unsigned>& idxs) : m_min(UINT_MAX), m_idxs(idxs) {}
void operator()(app * n) {
unsigned idx;
if (m_idxs.find(n->get_decl(), idx)) {
m_min = std::min(m_min, idx);
}
}
void operator()(var * n) {}
void operator()(quantifier * n) {}
};
void generic_model_converter::operator()(expr_ref& fml) {
NOT_IMPLEMENTED_YET();
min_app_idx_proc min_proc(m_first_idx);
for_each_expr(min_proc, 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];
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));
}
else {
NOT_IMPLEMENTED_YET();
}
if (m_first_idx[e.m_f] == i) {
m_first_idx.remove(e.m_f);
}
m_add_entries.pop_back();
}
}

16
src/tactic/generic_model_converter.h
View file

@ -32,19 +32,25 @@ class generic_model_converter : public model_converter {
m_f(f, m), m_def(d, m), m_instruction(i) {}
};
ast_manager& m;
vector<entry> m_entries;
vector<entry> m_add_entries;
vector<entry> m_hide_entries;
obj_map<func_decl, unsigned> m_first_idx;
public:
generic_model_converter(ast_manager & m): m(m) {}
generic_model_converter(ast_manager & m) : m(m) {}
virtual ~generic_model_converter() { }
void hide(expr* e) { SASSERT(is_app(e) && to_app(e)->get_num_args() == 0); hide(to_app(e)->get_decl()); }
void hide(func_decl * f) { m_entries.push_back(entry(f, 0, m, HIDE)); }
void hide(func_decl * f) { m_hide_entries.push_back(entry(f, 0, m, HIDE)); }
void add(func_decl * d, expr* e) { m_entries.push_back(entry(d, e, m, ADD)); }
void add(func_decl * d, expr* e) {
struct entry et(d, e, m, ADD);
m_first_idx.insert_if_not_there(et.m_f, m_add_entries.size());
m_add_entries.push_back(et);
}
void add(expr * d, expr* e) { SASSERT(is_app(d) && to_app(d)->get_num_args() == 0); m_entries.push_back(entry(to_app(d)->get_decl(), e, m, ADD)); }
void add(expr * d, expr* e) { SASSERT(is_app(d) && to_app(d)->get_num_args() == 0); add(to_app(d)->get_decl(), e); }
void operator()(labels_vec & labels) override {}