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

na

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-09-07 18:22:16 +03:00
parent d44081db7d
commit 5ba4d8d0f1
1 changed files with 28 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

28
src/tactic/fd_solver/smtfd_solver.cpp
View file

@ -590,6 +590,10 @@ namespace smtfd {
return mk_and(r); return mk_and(r);
} }
void check_extensionality(expr* a, expr* b) {
// sort* s = m.get_sort(a);
}
public: public:
a_plugin(smtfd_abs& a, expr_ref_vector& lemmas, model* mdl): a_plugin(smtfd_abs& a, expr_ref_vector& lemmas, model* mdl):
@ -625,6 +629,30 @@ namespace smtfd {
unsigned max_rounds() override { return 2; } unsigned max_rounds() override { return 2; }
void global_check(expr_ref_vector const& core) {
obj_map<sort, obj_map<expr, expr*>*> sort2val2array;
expr_ref_vector pinned(m);
for (expr* t : subterms(core)) {
if (m_autil.is_array(t)) {
sort* s = m.get_sort(t);
obj_map<expr, expr*>* v2a = nullptr;
if (!sort2val2array.find(s, v2a)) {
v2a = alloc(obj_map<expr, expr*>);
sort2val2array.insert(s, v2a);
}
expr* a = nullptr;
expr_ref v = eval_abs(t);
pinned.push_back(v);
if (v2a->find(v, a)) {
check_extensionality(a, t);
}
else {
v2a->insert(v, t);
}
}
}
}
}; };
struct stats { struct stats {