mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-19 20:33:38 +00:00
Code Activity

#5482

Browse source 
remove overly permissive filter on select_store axiom
This commit is contained in:
Nikolaj Bjorner 2021-08-27 21:03:30 -07:00
parent e9a30385cf
commit 992daa6d2e
2 changed files with 5 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/sat/smt/array_axioms.cpp
View file

@ -181,8 +181,6 @@ namespace array {
ptr_buffer<expr> sel1_args, sel2_args; ptr_buffer<expr> sel1_args, sel2_args;
unsigned num_args = select->get_num_args(); unsigned num_args = select->get_num_args();
if (expr2enode(store->get_arg(0))->get_root() == expr2enode(select->get_arg(0))->get_root())
return false;
bool has_diff = false; bool has_diff = false;
for (unsigned i = 1; i < num_args; i++) for (unsigned i = 1; i < num_args; i++)
has_diff |= expr2enode(select->get_arg(i))->get_root() != expr2enode(store->get_arg(i))->get_root(); has_diff |= expr2enode(select->get_arg(i))->get_root() != expr2enode(store->get_arg(i))->get_root();

8
src/sat/smt/euf_model.cpp
View file

@ -23,6 +23,7 @@ Author:
namespace euf { namespace euf {
class solver::user_sort { class solver::user_sort {
solver& s;
ast_manager& m; ast_manager& m;
model_ref& mdl; model_ref& mdl;
expr_ref_vector& values; expr_ref_vector& values;
@ -31,7 +32,7 @@ namespace euf {
obj_map<sort, expr_ref_vector*> sort2values; obj_map<sort, expr_ref_vector*> sort2values;
public: public:
user_sort(solver& s, expr_ref_vector& values, model_ref& mdl) : user_sort(solver& s, expr_ref_vector& values, model_ref& mdl) :
m(s.m), mdl(mdl), values(values), factory(m) {} s(s), m(s.m), mdl(mdl), values(values), factory(m) {}
~user_sort() { ~user_sort() {
for (auto kv : sort2values) for (auto kv : sort2values)
@ -41,10 +42,11 @@ namespace euf {
void add(enode* r, sort* srt) { void add(enode* r, sort* srt) {
unsigned id = r->get_expr_id(); unsigned id = r->get_expr_id();
expr_ref value(m); expr_ref value(m);
if (m.is_value(r->get_expr())) if (m.is_value(r->get_expr()))
value = r->get_expr(); value = r->get_expr();
else else
value = factory.get_fresh_value(srt); value = factory.get_fresh_value(srt);
TRACE("model", tout << s.bpp(r) << " := " << value << "\n";);
values.set(id, value); values.set(id, value);
expr_ref_vector* vals = nullptr; expr_ref_vector* vals = nullptr;
if (!sort2values.find(srt, vals)) { if (!sort2values.find(srt, vals)) {