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