mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

na

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-10-07 08:27:50 -07:00
parent b80ba24ba6
commit 49dfaeb406
3 changed files with 59 additions and 15 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/api/ml/z3.mli
View file

@ -736,6 +736,7 @@ sig
(** Create a quantifier pattern. *)
val mk_pattern : context -> Expr.expr list -> Pattern.pattern
(** Create a universal Quantifier. *)
val mk_forall : context -> Sort.sort list -> Symbol.symbol list -> Expr.expr -> int option -> Pattern.pattern list -> Expr.expr list -> Symbol.symbol option -> Symbol.symbol option -> quantifier

42
src/sat/smt/q_model_fixer.cpp
View file

@ -43,22 +43,20 @@ namespace q {
class arith_projection : public projection_function {
ast_manager& m;
arith_util a;
public:
bool operator()(expr* e1, expr* e2) const { return lt(a, e1, e2); }
public:
arith_projection(ast_manager& m): m(m), a(m) {}
~arith_projection() override {}
void sort(ptr_buffer<expr>& values) override { std::sort(values.begin(), values.end(), *this); }
bool operator()(expr* e1, expr* e2) const override { return lt(a, e1, e2); }
expr* mk_lt(expr* x, expr* y) override { return a.mk_lt(x, y); }
};
class ubv_projection : public projection_function {
ast_manager& m;
bv_util bvu;
public:
bool operator()(expr* e1, expr* e2) const { return lt(bvu, e1, e2); }
public:
ubv_projection(ast_manager& m): m(m), bvu(m) {}
~ubv_projection() override {}
void sort(ptr_buffer<expr>& values) override { std::sort(values.begin(), values.end(), *this); }
bool operator()(expr* e1, expr* e2) const override { return lt(bvu, e1, e2); }
expr* mk_lt(expr* x, expr* y) override { return m.mk_not(bvu.mk_ule(y, x)); }
};
@ -76,6 +74,8 @@ namespace q {
return;
m_dependencies.reset();
m_projection_data.reset();
m_projection_pinned.reset();
ptr_vector<quantifier> residue;
simple_macro_solver sms(m, *this);
@ -140,24 +140,38 @@ namespace q {
projection_function* proj = get_projection(srt);
if (!proj)
return expr_ref(m.mk_var(idx, srt), m);
ptr_buffer<expr> values;
for (euf::enode* n : ctx.get_egraph().enodes_of(f))
values.push_back(mdl(n->get_arg(idx)->get_expr()));
scoped_ptr<projection_meta_data> md = alloc(projection_meta_data, m);
expr_ref_vector& values = md->values;
for (euf::enode* n : ctx.get_egraph().enodes_of(f)) {
expr* t = n->get_arg(idx)->get_expr();
values.push_back(mdl(t));
md->v2t.insert(values.back(), t);
md->t2v.insert(t, values.back());
}
if (values.empty())
return expr_ref(m.mk_var(idx, srt), m);
proj->sort(values);
struct lt {
projection_function* p;
lt(projection_function* p) : p(p) {}
bool operator()(expr* a, expr* b) const { return (*p)(a, b); }
};
lt _lt(proj);
std::sort(values.c_ptr(), values.c_ptr() + values.size(), _lt);
unsigned j = 0;
for (unsigned i = 0; i < values.size(); ++i)
if (i == 0 || values[i-1] != values[i])
values[j++] = values[i];
if (i == 0 || values.get(i-1) != values.get(i))
values[j++] = values.get(i);
values.shrink(j);
m_projection_data.insert(indexed_decl(f, idx), md.get());
m_projection_pinned.push_back(md.detach());
unsigned sz = values.size();
expr_ref var(m.mk_var(0, srt), m);
expr_ref pi(values.get(sz-1), m);
for (unsigned i = sz - 1; i >= 1; i--) {
expr* c = proj->mk_lt(var, values[i]);
pi = m.mk_ite(c, values[i - 1], pi);
expr* c = proj->mk_lt(var, values.get(i));
pi = m.mk_ite(c, values.get(i - 1), pi);
}
func_interp* rpi = alloc(func_interp, m, 1);
rpi->set_else(pi);

31
src/sat/smt/q_model_fixer.h
View file

@ -40,8 +40,29 @@ namespace q {
class projection_function {
public:
virtual ~projection_function() {}
virtual void sort(ptr_buffer<expr>& values) = 0;
virtual expr* mk_lt(expr* a, expr* b) = 0;
virtual bool operator()(expr* a, expr* b) const = 0;
};
/**
* meta-data for a projection function for f at index idx (indexed-decl).
* The meta-data contains the set of model values that the idx'th argument of f
* has and a map from model values to terms and back.
*/
struct projection_meta_data {
projection_meta_data(ast_manager& m) : values(m) {}
expr_ref_vector values;
obj_map<expr, expr*> v2t;
obj_map<expr, expr*> t2v;
};
struct indexed_decl {
func_decl* f;
unsigned idx;
indexed_decl() : f(nullptr), idx(0) {}
indexed_decl(func_decl* f, unsigned idx): f(f), idx(idx) {}
struct hash { unsigned operator()(indexed_decl const& d) const { return d.idx + d.f->hash(); } };
struct eq { bool operator()(indexed_decl const& a, indexed_decl const& b) const { return a.idx == b.idx && a.f == b.f; } };
};
class model_fixer : public quantifier2macro_infos {
@ -51,6 +72,8 @@ namespace q {
obj_map<quantifier, quantifier_macro_info*> m_q2info;
func_decl_dependencies m_dependencies;
obj_map<sort, projection_function*> m_projections;
map<indexed_decl, projection_meta_data*, indexed_decl::hash, indexed_decl::eq> m_projection_data;
scoped_ptr_vector<projection_meta_data> m_projection_pinned;
void add_projection_functions(model& mdl, ptr_vector<quantifier> const& qs);
void add_projection_functions(model& mdl, func_decl* f);
@ -72,6 +95,12 @@ namespace q {
void operator()(model& mdl);
quantifier_macro_info* operator()(quantifier* q);
projection_meta_data* operator()(func_decl* f, unsigned idx) const {
projection_meta_data* r = nullptr;
m_projection_data.find(indexed_decl(f, idx), r);
return r;
}
};