1 /*++
2 Copyright (c) 2020 Microsoft Corporation
3 
4 Module Name:
5 
6     array_internalize.cpp
7 
8 Abstract:
9 
10     Internalize routines for arrays
11 
12 Author:
13 
14     Nikolaj Bjorner (nbjorner) 2020-09-08
15 
16 --*/
17 
18 #include "sat/smt/array_solver.h"
19 #include "sat/smt/euf_solver.h"
20 
21 namespace array {
22 
internalize(expr * e,bool sign,bool root,bool redundant)23     sat::literal solver::internalize(expr* e, bool sign, bool root, bool redundant) {
24         SASSERT(m.is_bool(e));
25         if (!visit_rec(m, e, sign, root, redundant)) {
26             TRACE("array", tout << mk_pp(e, m) << "\n";);
27             return sat::null_literal;
28         }
29         auto lit = expr2literal(e);
30         if (sign)
31             lit.neg();
32         return lit;
33     }
34 
internalize(expr * e,bool redundant)35     void solver::internalize(expr* e, bool redundant) {
36         visit_rec(m, e, false, false, redundant);
37     }
38 
mk_var(euf::enode * n)39     euf::theory_var solver::mk_var(euf::enode* n) {
40         theory_var r = euf::th_euf_solver::mk_var(n);
41         m_find.mk_var();
42         ctx.attach_th_var(n, this, r);
43         m_var_data.push_back(alloc(var_data));
44         return r;
45     }
46 
ensure_var(euf::enode * n)47     void solver::ensure_var(euf::enode* n) {
48         theory_var v = n->get_th_var(get_id());
49         if (v == euf::null_theory_var) {
50             mk_var(n);
51             if (is_lambda(n->get_expr()))
52                 internalize_lambda(n);
53         }
54     }
55 
apply_sort_cnstr(euf::enode * n,sort * s)56     void solver::apply_sort_cnstr(euf::enode * n, sort * s) {
57         ensure_var(n);
58     }
59 
internalize_store(euf::enode * n)60     void solver::internalize_store(euf::enode* n) {
61         add_parent_lambda(n->get_arg(0)->get_th_var(get_id()), n);
62         push_axiom(store_axiom(n));
63         add_lambda(n->get_th_var(get_id()), n);
64         SASSERT(!get_var_data(n->get_th_var(get_id())).m_prop_upward);
65     }
66 
internalize_map(euf::enode * n)67     void solver::internalize_map(euf::enode* n) {
68         for (auto* arg : euf::enode_args(n)) {
69             add_parent_lambda(arg->get_th_var(get_id()), n);
70             set_prop_upward(arg);
71         }
72         push_axiom(default_axiom(n));
73         add_lambda(n->get_th_var(get_id()), n);
74         SASSERT(!get_var_data(n->get_th_var(get_id())).m_prop_upward);
75     }
76 
internalize_lambda(euf::enode * n)77     void solver::internalize_lambda(euf::enode* n) {
78         set_prop_upward(n);
79         if (!a.is_store(n->get_expr()))
80             push_axiom(default_axiom(n));
81         add_lambda(n->get_th_var(get_id()), n);
82     }
83 
internalize_select(euf::enode * n)84     void solver::internalize_select(euf::enode* n) {
85         add_parent_select(n->get_arg(0)->get_th_var(get_id()), n);
86     }
87 
internalize_ext(euf::enode * n)88     void solver::internalize_ext(euf::enode* n) {
89         SASSERT(is_array(n->get_arg(0)));
90         push_axiom(extensionality_axiom(n->get_arg(0), n->get_arg(1)));
91     }
92 
internalize_default(euf::enode * n)93     void solver::internalize_default(euf::enode* n) {
94         add_parent_default(n->get_arg(0)->get_th_var(get_id()), n);
95         set_prop_upward(n);
96     }
97 
visited(expr * e)98     bool solver::visited(expr* e) {
99         euf::enode* n = expr2enode(e);
100         return n && n->is_attached_to(get_id());
101     }
102 
visit(expr * e)103     bool solver::visit(expr* e) {
104         if (visited(e))
105             return true;
106         if (!is_app(e) || to_app(e)->get_family_id() != get_id()) {
107             ctx.internalize(e, m_is_redundant);
108             euf::enode* n = expr2enode(e);
109             ensure_var(n);
110             return true;
111         }
112         m_stack.push_back(sat::eframe(e));
113         return false;
114     }
115 
post_visit(expr * e,bool sign,bool root)116     bool solver::post_visit(expr* e, bool sign, bool root) {
117         euf::enode* n = expr2enode(e);
118         app* a = to_app(e);
119         SASSERT(!n || !n->is_attached_to(get_id()));
120         if (!n)
121             n = mk_enode(e, false);
122         SASSERT(!n->is_attached_to(get_id()));
123         mk_var(n);
124         for (auto* arg : euf::enode_args(n))
125             ensure_var(arg);
126         switch (a->get_decl_kind()) {
127         case OP_STORE:
128             internalize_store(n);
129             break;
130         case OP_SELECT:
131             internalize_select(n);
132             break;
133         case OP_AS_ARRAY:
134         case OP_CONST_ARRAY:
135             internalize_lambda(n);
136             break;
137         case OP_ARRAY_EXT:
138             internalize_ext(n);
139             break;
140         case OP_ARRAY_DEFAULT:
141             internalize_default(n);
142             break;
143         case OP_ARRAY_MAP:
144             internalize_map(n);
145             break;
146         case OP_SET_UNION:
147         case OP_SET_INTERSECT:
148         case OP_SET_DIFFERENCE:
149         case OP_SET_COMPLEMENT:
150         case OP_SET_SUBSET:
151         case OP_SET_HAS_SIZE:
152         case OP_SET_CARD:
153             ctx.unhandled_function(a->get_decl());
154             break;
155         default:
156             UNREACHABLE();
157             break;
158         }
159         return true;
160     }
161 
162     /**
163         \brief Return true if v is shared between two different "instances" of the array theory.
164         It is shared if it is used in more than one role. The possible roles are: array, index, and value.
165         Example:
166           (store v i j) <--- v is used as an array
167           (select A v)  <--- v is used as an index
168           (store A i v) <--- v is used as an value
169      */
is_shared(theory_var v) const170     bool solver::is_shared(theory_var v) const {
171         euf::enode* n = var2enode(v);
172         euf::enode* r = n->get_root();
173         bool is_array = false;
174         bool is_index = false;
175         bool is_value = false;
176         auto set_array = [&](euf::enode* arg) { if (arg->get_root() == r) is_array = true; };
177         auto set_index = [&](euf::enode* arg) { if (arg->get_root() == r) is_index = true; };
178         auto set_value = [&](euf::enode* arg) { if (arg->get_root() == r) is_value = true; };
179 
180         for (euf::enode* parent : euf::enode_parents(r)) {
181             app* p = parent->get_app();
182             unsigned num_args = parent->num_args();
183             if (a.is_store(p)) {
184                 set_array(parent->get_arg(0));
185                 for (unsigned i = 1; i < num_args - 1; i++)
186                     set_index(parent->get_arg(i));
187                 set_value(parent->get_arg(num_args - 1));
188             }
189             else if (a.is_select(p)) {
190                 set_array(parent->get_arg(0));
191                 for (unsigned i = 1; i < num_args - 1; i++)
192                     set_index(parent->get_arg(i));
193             }
194             else if (a.is_const(p)) {
195                 set_value(parent->get_arg(0));
196             }
197             if (is_array + is_index + is_value > 1)
198                 return true;
199         }
200         return false;
201     }
202 
sort2diff(sort * s)203     func_decl_ref_vector const& solver::sort2diff(sort* s) {
204         func_decl_ref_vector* result = nullptr;
205         if (m_sort2diff.find(s, result))
206             return *result;
207 
208         unsigned dimension = get_array_arity(s);
209         result = alloc(func_decl_ref_vector, m);
210         for (unsigned i = 0; i < dimension; ++i)
211             result->push_back(a.mk_array_ext(s, i));
212         m_sort2diff.insert(s, result);
213         ctx.push(insert_map<euf::solver, obj_map<sort, func_decl_ref_vector*>, sort*>(m_sort2diff, s));
214         ctx.push(new_obj_trail<euf::solver,func_decl_ref_vector>(result));
215         return *result;
216     }
217 
218 }
219 
220