1 /** 2 Copyright (c) 2011 Microsoft Corporation 3 4 Module Name: 5 6 spacer_util.cpp 7 8 Abstract: 9 10 Utility functions for SPACER. 11 12 13 Author: 14 15 Krystof Hoder (t-khoder) 2011-8-19. 16 Arie Gurfinkel 17 Anvesh Komuravelli 18 19 Revision History: 20 21 Modified by Anvesh Komuravelli 22 23 Notes: 24 25 26 --*/ 27 28 #include <sstream> 29 #include <algorithm> 30 31 #include "util/util.h" 32 #include "ast/ast.h" 33 #include "ast/occurs.h" 34 #include "ast/ast_pp.h" 35 #include "ast/scoped_proof.h" 36 #include "ast/for_each_expr.h" 37 #include "ast/rewriter/bool_rewriter.h" 38 #include "ast/rewriter/expr_safe_replace.h" 39 #include "ast/array_decl_plugin.h" 40 #include "ast/arith_decl_plugin.h" 41 #include "ast/datatype_decl_plugin.h" 42 #include "ast/bv_decl_plugin.h" 43 #include "ast/rewriter/rewriter.h" 44 #include "ast/rewriter/rewriter_def.h" 45 #include "ast/rewriter/factor_equivs.h" 46 #include "ast/rewriter/expr_replacer.h" 47 48 49 #include "smt/params/smt_params.h" 50 #include "model/model.h" 51 #include "model/model_evaluator.h" 52 #include "model/model_smt2_pp.h" 53 #include "model/model_pp.h" 54 55 #include "qe/qe_lite.h" 56 #include "qe/qe_mbp.h" 57 #include "qe/mbp/mbp_term_graph.h" 58 #include "qe/mbp/mbp_plugin.h" 59 60 #include "tactic/tactical.h" 61 #include "tactic/core/propagate_values_tactic.h" 62 #include "tactic/arith/propagate_ineqs_tactic.h" 63 #include "tactic/arith/arith_bounds_tactic.h" 64 65 #include "muz/base/dl_util.h" 66 #include "muz/spacer/spacer_legacy_mev.h" 67 #include "muz/spacer/spacer_qe_project.h" 68 #include "muz/spacer/spacer_manager.h" 69 #include "muz/spacer/spacer_util.h" 70 71 namespace spacer { 72 is_clause(ast_manager & m,expr * n)73 bool is_clause(ast_manager& m, expr* n) { 74 if (spacer::is_literal(m, n)) 75 return true; 76 if (m.is_or(n)) { 77 for (expr* arg : *to_app(n)) { 78 if (!spacer::is_literal(m, arg)) 79 return false; 80 return true; 81 } 82 } 83 return false; 84 } 85 is_literal(ast_manager & m,expr * n)86 bool is_literal(ast_manager& m, expr* n) { 87 return spacer::is_atom(m, n) || (m.is_not(n) && spacer::is_atom(m, to_app(n)->get_arg(0))); 88 } 89 is_atom(ast_manager & m,expr * n)90 bool is_atom(ast_manager& m, expr* n) { 91 if (is_quantifier(n) || !m.is_bool(n)) 92 return false; 93 if (is_var(n)) 94 return true; 95 SASSERT(is_app(n)); 96 if (to_app(n)->get_family_id() != m.get_basic_family_id()) { 97 return true; 98 } 99 100 if ((m.is_eq(n) && !m.is_bool(to_app(n)->get_arg(0))) || 101 m.is_true(n) || m.is_false(n)) 102 return true; 103 104 // x=y is atomic if x and y are Bool and atomic 105 expr* e1, * e2; 106 if (m.is_eq(n, e1, e2) && spacer::is_atom(m, e1) && spacer::is_atom(m, e2)) 107 return true; 108 return false; 109 } 110 subst_vars(ast_manager & m,app_ref_vector const & vars,model & mdl,expr_ref & fml)111 void subst_vars(ast_manager& m, 112 app_ref_vector const& vars, model& mdl, expr_ref& fml) { 113 model::scoped_model_completion _sc_(mdl, true); 114 expr_safe_replace sub(m); 115 for (app* v : vars) sub.insert(v, mdl(v)); 116 sub(fml); 117 } 118 to_mbp_benchmark(std::ostream & out,expr * fml,const app_ref_vector & vars)119 void to_mbp_benchmark(std::ostream& out, expr* fml, const app_ref_vector& vars) { 120 ast_manager& m = vars.m(); 121 ast_pp_util pp(m); 122 pp.collect(fml); 123 pp.display_decls(out); 124 125 out << "(define-fun mbp_benchmark_fml () Bool\n "; 126 out << mk_pp(fml, m) << ")\n\n"; 127 128 out << "(push 1)\n" 129 << "(assert mbp_benchmark_fml)\n" 130 << "(check-sat)\n" 131 << "(mbp mbp_benchmark_fml ("; 132 for (auto v : vars) { out << mk_pp(v, m) << " "; } 133 out << "))\n" 134 << "(pop 1)\n" 135 << "(exit)\n"; 136 } 137 qe_project_z3(ast_manager & m,app_ref_vector & vars,expr_ref & fml,model & mdl,bool reduce_all_selects,bool use_native_mbp,bool dont_sub)138 void qe_project_z3(ast_manager& m, app_ref_vector& vars, expr_ref& fml, 139 model& mdl, bool reduce_all_selects, bool use_native_mbp, 140 bool dont_sub) { 141 params_ref p; 142 p.set_bool("reduce_all_selects", reduce_all_selects); 143 p.set_bool("dont_sub", dont_sub); 144 145 qe::mbproj mbp(m, p); 146 mbp.spacer(vars, mdl, fml); 147 } 148 149 /* 150 * eliminate simple equalities using qe_lite 151 * then, MBP for Booleans (substitute), reals (based on LW), ints (based on Cooper), and arrays 152 */ qe_project_spacer(ast_manager & m,app_ref_vector & vars,expr_ref & fml,model & mdl,bool reduce_all_selects,bool use_native_mbp,bool dont_sub)153 void qe_project_spacer(ast_manager& m, app_ref_vector& vars, expr_ref& fml, 154 model& mdl, bool reduce_all_selects, bool use_native_mbp, 155 bool dont_sub) { 156 th_rewriter rw(m); 157 TRACE("spacer_mbp", 158 tout << "Before projection:\n"; 159 tout << fml << "\n"; 160 tout << "Vars:\n" << vars;); 161 162 { 163 // Ensure that top-level AND of fml is flat 164 expr_ref_vector flat(m); 165 flatten_and(fml, flat); 166 fml = mk_and(flat); 167 } 168 169 170 // uncomment for benchmarks 171 //to_mbp_benchmark(verbose_stream(), fml, vars); 172 173 app_ref_vector arith_vars(m); 174 app_ref_vector array_vars(m); 175 array_util arr_u(m); 176 arith_util ari_u(m); 177 expr_safe_replace bool_sub(m); 178 expr_ref bval(m); 179 180 while (true) { 181 params_ref p; 182 qe_lite qe(m, p, false); 183 qe(vars, fml); 184 rw(fml); 185 186 TRACE("spacer_mbp", 187 tout << "After qe_lite:\n"; 188 tout << mk_pp(fml, m) << "\n"; 189 tout << "Vars:\n" << vars;); 190 191 SASSERT(!m.is_false(fml)); 192 193 194 // sort out vars into bools, arith (int/real), and arrays 195 for (app* v : vars) { 196 if (m.is_bool(v)) { 197 // obtain the interpretation of the ith var 198 // using model completion 199 model::scoped_model_completion _sc_(mdl, true); 200 bool_sub.insert(v, mdl(v)); 201 } 202 else if (arr_u.is_array(v)) { 203 array_vars.push_back(v); 204 } 205 else { 206 SASSERT(ari_u.is_int(v) || ari_u.is_real(v)); 207 arith_vars.push_back(v); 208 } 209 } 210 211 // substitute Booleans 212 if (!bool_sub.empty()) { 213 bool_sub(fml); 214 // -- bool_sub is not simplifying 215 rw(fml); 216 SASSERT(!m.is_false(fml)); 217 TRACE("spacer_mbp", tout << "Projected Booleans:\n" << fml << "\n"; ); 218 bool_sub.reset(); 219 } 220 221 TRACE("spacer_mbp", tout << "Array vars:\n"; tout << array_vars;); 222 223 vars.reset(); 224 225 // project arrays 226 { 227 scoped_no_proof _sp(m); 228 // -- local rewriter that is aware of current proof mode 229 th_rewriter srw(m); 230 spacer_qe::array_project(mdl, array_vars, fml, vars, reduce_all_selects); 231 SASSERT(array_vars.empty()); 232 srw(fml); 233 SASSERT(!m.is_false(fml)); 234 } 235 236 TRACE("spacer_mbp", 237 tout << "extended model:\n"; 238 model_pp(tout, mdl); 239 tout << "Auxiliary variables of index and value sorts:\n"; 240 tout << vars;); 241 242 if (vars.empty()) { break; } 243 } 244 245 // project reals and ints 246 if (!arith_vars.empty()) { 247 TRACE("spacer_mbp", tout << "Arith vars:\n" << arith_vars;); 248 249 if (use_native_mbp) { 250 qe::mbproj mbp(m); 251 expr_ref_vector fmls(m); 252 flatten_and(fml, fmls); 253 254 mbp(true, arith_vars, mdl, fmls); 255 fml = mk_and(fmls); 256 SASSERT(arith_vars.empty()); 257 } 258 else { 259 scoped_no_proof _sp(m); 260 spacer_qe::arith_project(mdl, arith_vars, fml); 261 } 262 263 TRACE("spacer_mbp", 264 tout << "Projected arith vars:\n" << fml << "\n"; 265 tout << "Remaining arith vars:\n" << arith_vars << "\n";); 266 SASSERT(!m.is_false(fml)); 267 } 268 269 if (!arith_vars.empty()) { 270 mbqi_project(mdl, arith_vars, fml); 271 } 272 273 // substitute any remaining arith vars 274 if (!dont_sub && !arith_vars.empty()) { 275 subst_vars(m, arith_vars, mdl, fml); 276 TRACE("spacer_mbp", 277 tout << "After substituting remaining arith vars:\n"; 278 tout << mk_pp(fml, m) << "\n"; 279 ); 280 // an extra round of simplification because subst_vars is not simplifying 281 rw(fml); 282 } 283 284 DEBUG_CODE( 285 model_evaluator mev(mdl); 286 mev.set_model_completion(false); 287 SASSERT(mev.is_true(fml)); 288 ); 289 290 vars.reset(); 291 if (dont_sub && !arith_vars.empty()) { 292 vars.append(arith_vars); 293 } 294 } 295 296 apply_accessor(ast_manager & m,ptr_vector<func_decl> const & acc,unsigned j,func_decl * f,expr * c)297 static expr* apply_accessor(ast_manager& m, 298 ptr_vector<func_decl> const& acc, 299 unsigned j, 300 func_decl* f, 301 expr* c) { 302 if (is_app(c) && to_app(c)->get_decl() == f) { 303 return to_app(c)->get_arg(j); 304 } 305 else { 306 return m.mk_app(acc[j], c); 307 } 308 } 309 qe_project(ast_manager & m,app_ref_vector & vars,expr_ref & fml,model & mdl,bool reduce_all_selects,bool use_native_mbp,bool dont_sub)310 void qe_project(ast_manager& m, app_ref_vector& vars, expr_ref& fml, 311 model& mdl, bool reduce_all_selects, bool use_native_mbp, 312 bool dont_sub) { 313 if (use_native_mbp) 314 qe_project_z3(m, vars, fml, mdl, 315 reduce_all_selects, use_native_mbp, dont_sub); 316 else 317 qe_project_spacer(m, vars, fml, mdl, 318 reduce_all_selects, use_native_mbp, dont_sub); 319 } 320 expand_literals(ast_manager & m,expr_ref_vector & conjs)321 void expand_literals(ast_manager& m, expr_ref_vector& conjs) { 322 if (conjs.empty()) 323 return; 324 arith_util arith(m); 325 datatype_util dt(m); 326 bv_util bv(m); 327 expr* e1, * e2, * c, * val; 328 rational r; 329 unsigned bv_size; 330 331 TRACE("spacer_expand", tout << "begin expand\n" << conjs << "\n";); 332 333 for (unsigned i = 0; i < conjs.size(); ++i) { 334 expr* e = conjs[i].get(); 335 if (m.is_eq(e, e1, e2) && arith.is_int_real(e1)) { 336 conjs[i] = arith.mk_le(e1, e2); 337 if (i + 1 == conjs.size()) { 338 conjs.push_back(arith.mk_ge(e1, e2)); 339 } 340 else { 341 conjs.push_back(conjs[i + 1].get()); 342 conjs[i + 1] = arith.mk_ge(e1, e2); 343 } 344 ++i; 345 } 346 else if ((m.is_eq(e, c, val) && is_app(val) && dt.is_constructor(to_app(val))) || 347 (m.is_eq(e, val, c) && is_app(val) && dt.is_constructor(to_app(val)))) { 348 func_decl* f = to_app(val)->get_decl(); 349 func_decl* r = dt.get_constructor_is(f); 350 conjs[i] = m.mk_app(r, c); 351 ptr_vector<func_decl> const& acc = *dt.get_constructor_accessors(f); 352 for (unsigned j = 0; j < acc.size(); ++j) { 353 conjs.push_back(m.mk_eq(apply_accessor(m, acc, j, f, c), to_app(val)->get_arg(j))); 354 } 355 } 356 else if ((m.is_eq(e, c, val) && bv.is_numeral(val, r, bv_size)) || 357 (m.is_eq(e, val, c) && bv.is_numeral(val, r, bv_size))) { 358 rational two(2); 359 for (unsigned j = 0; j < bv_size; ++j) { 360 parameter p(j); 361 expr* e = m.mk_eq(m.mk_app(bv.get_family_id(), OP_BIT1), bv.mk_extract(j, j, c)); 362 if ((r % two).is_zero()) { 363 e = m.mk_not(e); 364 } 365 r = div(r, two); 366 if (j == 0) { 367 conjs[i] = e; 368 } 369 else { 370 conjs.push_back(e); 371 } 372 } 373 } 374 } 375 TRACE("spacer_expand", tout << "end expand\n" << conjs << "\n";); 376 } 377 378 namespace { 379 class implicant_picker { 380 model& m_model; 381 ast_manager& m; 382 arith_util m_arith; 383 384 expr_ref_vector m_todo; 385 expr_mark m_visited; 386 387 // add literal to the implicant 388 // applies lightweight normalization add_literal(expr * e,expr_ref_vector & out)389 void add_literal(expr* e, expr_ref_vector& out) { 390 SASSERT(m.is_bool(e)); 391 392 expr_ref res(m), v(m); 393 v = m_model(e); 394 // the literal must have a value 395 SASSERT(m.limit().is_canceled() || m.is_true(v) || m.is_false(v)); 396 397 res = m.is_false(v) ? m.mk_not(e) : e; 398 399 if (m.is_distinct(res)) { 400 // --(distinct a b) == (not (= a b)) 401 if (to_app(res)->get_num_args() == 2) { 402 res = m.mk_eq(to_app(res)->get_arg(0), 403 to_app(res)->get_arg(1)); 404 res = m.mk_not(res); 405 } 406 } 407 408 expr* nres = nullptr, * f1 = nullptr, * f2 = nullptr; 409 if (m.is_not(res, nres)) { 410 // --(not (xor a b)) == (= a b) 411 if (m.is_xor(nres, f1, f2)) 412 res = m.mk_eq(f1, f2); 413 // -- split arithmetic inequality 414 else if (m.is_eq(nres, f1, f2) && m_arith.is_int_real(f1)) { 415 res = m_arith.mk_lt(f1, f2); 416 if (!m_model.is_true(res)) 417 res = m_arith.mk_lt(f2, f1); 418 } 419 } 420 421 422 if (!m_model.is_true(res)) { 423 IF_VERBOSE(2, verbose_stream() 424 << "(spacer-model-anomaly: " << res << ")\n"); 425 } 426 out.push_back(res); 427 } 428 process_app(app * a,expr_ref_vector & out)429 void process_app(app* a, expr_ref_vector& out) { 430 if (m_visited.is_marked(a)) return; 431 SASSERT(m.is_bool(a)); 432 expr_ref v(m); 433 v = m_model(a); 434 bool is_true = m.is_true(v); 435 436 if (!is_true && !m.is_false(v)) return; 437 438 expr* na = nullptr, * f1 = nullptr, * f2 = nullptr, * f3 = nullptr; 439 440 SASSERT(!m.is_false(a)); 441 if (m.is_true(a)) { 442 // noop 443 } 444 else if (a->get_family_id() != m.get_basic_family_id()) { 445 add_literal(a, out); 446 } 447 else if (is_uninterp_const(a)) { 448 add_literal(a, out); 449 } 450 else if (m.is_not(a, na)) { 451 m_todo.push_back(na); 452 } 453 else if (m.is_distinct(a)) { 454 if (!is_true) { 455 expr_ref tmp = mbp::project_plugin::pick_equality(m, m_model, a); 456 m_todo.push_back(tmp); 457 } 458 else if (a->get_num_args() == 2) { 459 add_literal(a, out); 460 } 461 else { 462 m_todo.push_back(m.mk_distinct_expanded(a->get_num_args(), 463 a->get_args())); 464 } 465 } 466 else if (m.is_and(a)) { 467 if (is_true) { 468 m_todo.append(a->get_num_args(), a->get_args()); 469 } 470 else { 471 for (expr* e : *a) { 472 if (m_model.is_false(e)) { 473 m_todo.push_back(e); 474 break; 475 } 476 } 477 } 478 } 479 else if (m.is_or(a)) { 480 if (!is_true) 481 m_todo.append(a->get_num_args(), a->get_args()); 482 else { 483 for (expr* e : *a) { 484 if (m_model.is_true(e)) { 485 m_todo.push_back(e); 486 break; 487 } 488 } 489 } 490 } 491 else if (m.is_eq(a, f1, f2) || 492 (is_true && m.is_not(a, na) && m.is_xor(na, f1, f2))) { 493 if (!m.are_equal(f1, f2) && !m.are_distinct(f1, f2)) { 494 if (m.is_bool(f1) && 495 (!is_uninterp_const(f1) || !is_uninterp_const(f2))) 496 m_todo.append(a->get_num_args(), a->get_args()); 497 else 498 add_literal(a, out); 499 } 500 } 501 else if (m.is_ite(a, f1, f2, f3)) { 502 if (m.are_equal(f2, f3)) { 503 m_todo.push_back(f2); 504 } 505 else if (m_model.is_true(f2) && m_model.is_true(f3)) { 506 m_todo.push_back(f2); 507 m_todo.push_back(f3); 508 } 509 else if (m_model.is_false(f2) && m_model.is_false(f3)) { 510 m_todo.push_back(f2); 511 m_todo.push_back(f3); 512 } 513 else if (m_model.is_true(f1)) { 514 m_todo.push_back(f1); 515 m_todo.push_back(f2); 516 } 517 else if (m_model.is_false(f1)) { 518 m_todo.push_back(f1); 519 m_todo.push_back(f3); 520 } 521 } 522 else if (m.is_xor(a, f1, f2)) { 523 m_todo.append(a->get_num_args(), a->get_args()); 524 } 525 else if (m.is_implies(a, f1, f2)) { 526 if (is_true) { 527 if (m_model.is_true(f2)) 528 m_todo.push_back(f2); 529 else if (m_model.is_false(f1)) 530 m_todo.push_back(f1); 531 } 532 else 533 m_todo.append(a->get_num_args(), a->get_args()); 534 } 535 else { 536 IF_VERBOSE(0, 537 verbose_stream() << "Unexpected expression: " 538 << mk_pp(a, m) << "\n"); 539 UNREACHABLE(); 540 } 541 } 542 pick_literals(expr * e,expr_ref_vector & out)543 void pick_literals(expr* e, expr_ref_vector& out) { 544 SASSERT(m_todo.empty()); 545 if (m_visited.is_marked(e) || !is_app(e)) return; 546 547 // -- keep track of all created expressions to 548 // -- make sure that expression ids are stable 549 expr_ref_vector pinned(m); 550 551 m_todo.reset(); 552 m_todo.push_back(e); 553 while (!m_todo.empty()) { 554 pinned.push_back(m_todo.back()); 555 m_todo.pop_back(); 556 if (!is_app(pinned.back())) continue; 557 app* a = to_app(pinned.back()); 558 process_app(a, out); 559 m_visited.mark(a, true); 560 } 561 m_todo.reset(); 562 } 563 pick_implicant(const expr_ref_vector & in,expr_ref_vector & out)564 bool pick_implicant(const expr_ref_vector& in, expr_ref_vector& out) { 565 m_visited.reset(); 566 bool is_true = m_model.is_true(in); 567 568 for (expr* e : in) { 569 if (is_true || m_model.is_true(e)) { 570 pick_literals(e, out); 571 } 572 } 573 m_visited.reset(); 574 return is_true; 575 } 576 577 public: 578 implicant_picker(model & mdl)579 implicant_picker(model& mdl) : 580 m_model(mdl), m(m_model.get_manager()), m_arith(m), m_todo(m) {} 581 operator ()(expr_ref_vector & in,expr_ref_vector & out)582 void operator()(expr_ref_vector& in, expr_ref_vector& out) { 583 model::scoped_model_completion _sc_(m_model, false); 584 pick_implicant(in, out); 585 } 586 }; 587 } 588 compute_implicant_literals(model & mdl,expr_ref_vector & formula)589 expr_ref_vector compute_implicant_literals(model& mdl, 590 expr_ref_vector& formula) { 591 // flatten the formula and remove all trivial literals 592 593 // TBD: not clear why there is a dependence on it(other than 594 // not handling of Boolean constants by implicant_picker), however, 595 // it was a source of a problem on a benchmark 596 expr_ref_vector res(formula.get_manager()); 597 flatten_and(formula); 598 if (!formula.empty()) { 599 implicant_picker ipick(mdl); 600 ipick(formula, res); 601 } 602 return res; 603 } 604 simplify_bounds_old(expr_ref_vector & cube)605 void simplify_bounds_old(expr_ref_vector& cube) { 606 ast_manager& m = cube.m(); 607 scoped_no_proof _no_pf_(m); 608 goal_ref g(alloc(goal, m, false, false, false)); 609 for (expr* c : cube) 610 g->assert_expr(c); 611 612 goal_ref_buffer result; 613 tactic_ref simplifier = mk_arith_bounds_tactic(m); 614 (*simplifier)(g, result); 615 SASSERT(result.size() == 1); 616 goal* r = result[0]; 617 cube.reset(); 618 for (unsigned i = 0; i < r->size(); ++i) { 619 cube.push_back(r->form(i)); 620 } 621 } 622 simplify_bounds_new(expr_ref_vector & cube)623 void simplify_bounds_new(expr_ref_vector& cube) { 624 ast_manager& m = cube.m(); 625 scoped_no_proof _no_pf_(m); 626 goal_ref g(alloc(goal, m, false, false, false)); 627 for (expr* c : cube) 628 g->assert_expr(c); 629 630 goal_ref_buffer goals; 631 tactic_ref prop_values = mk_propagate_values_tactic(m); 632 tactic_ref prop_bounds = mk_propagate_ineqs_tactic(m); 633 tactic_ref t = and_then(prop_values.get(), prop_bounds.get()); 634 635 (*t)(g, goals); 636 SASSERT(goals.size() == 1); 637 638 g = goals[0]; 639 cube.reset(); 640 for (unsigned i = 0; i < g->size(); ++i) { 641 cube.push_back(g->form(i)); 642 } 643 } 644 simplify_bounds(expr_ref_vector & cube)645 void simplify_bounds(expr_ref_vector& cube) { 646 simplify_bounds_new(cube); 647 } 648 649 /// Adhoc rewriting of arithmetic expressions 650 struct adhoc_rewriter_cfg : public default_rewriter_cfg { 651 ast_manager& m; 652 arith_util m_util; 653 adhoc_rewriter_cfgspacer::adhoc_rewriter_cfg654 adhoc_rewriter_cfg(ast_manager& manager) : m(manager), m_util(m) {} 655 is_lespacer::adhoc_rewriter_cfg656 bool is_le(func_decl const* n) const { return m_util.is_le(n); } is_gespacer::adhoc_rewriter_cfg657 bool is_ge(func_decl const* n) const { return m_util.is_ge(n); } 658 reduce_appspacer::adhoc_rewriter_cfg659 br_status reduce_app(func_decl* f, unsigned num, expr* const* args, 660 expr_ref& result, proof_ref& result_pr) { 661 expr* e; 662 if (is_le(f)) 663 return mk_le_core(args[0], args[1], result); 664 if (is_ge(f)) 665 return mk_ge_core(args[0], args[1], result); 666 if (m.is_not(f) && m.is_not(args[0], e)) { 667 result = e; 668 return BR_DONE; 669 } 670 return BR_FAILED; 671 } 672 mk_le_corespacer::adhoc_rewriter_cfg673 br_status mk_le_core(expr* arg1, expr* arg2, expr_ref& result) { 674 // t <= -1 ==> t < 0 ==> !(t >= 0) 675 if (m_util.is_int(arg1) && m_util.is_minus_one(arg2)) { 676 result = m.mk_not(m_util.mk_ge(arg1, mk_zero())); 677 return BR_DONE; 678 } 679 return BR_FAILED; 680 } mk_ge_corespacer::adhoc_rewriter_cfg681 br_status mk_ge_core(expr* arg1, expr* arg2, expr_ref& result) { 682 // t >= 1 ==> t > 0 ==> !(t <= 0) 683 if (m_util.is_int(arg1) && is_one(arg2)) { 684 685 result = m.mk_not(m_util.mk_le(arg1, mk_zero())); 686 return BR_DONE; 687 } 688 return BR_FAILED; 689 } mk_zerospacer::adhoc_rewriter_cfg690 expr* mk_zero() { return m_util.mk_numeral(rational(0), true); } is_onespacer::adhoc_rewriter_cfg691 bool is_one(expr const* n) const { 692 rational val; return m_util.is_numeral(n, val) && val.is_one(); 693 } 694 }; 695 normalize(expr * e,expr_ref & out,bool use_simplify_bounds,bool use_factor_eqs)696 void normalize(expr* e, expr_ref& out, 697 bool use_simplify_bounds, 698 bool use_factor_eqs) 699 { 700 701 params_ref params; 702 // arith_rewriter 703 params.set_bool("sort_sums", true); 704 params.set_bool("gcd_rounding", true); 705 params.set_bool("arith_lhs", true); 706 // poly_rewriter 707 params.set_bool("som", true); 708 params.set_bool("flat", true); 709 710 // apply rewriter 711 th_rewriter rw(out.m(), params); 712 rw(e, out); 713 714 adhoc_rewriter_cfg adhoc_cfg(out.m()); 715 rewriter_tpl<adhoc_rewriter_cfg> adhoc_rw(out.m(), false, adhoc_cfg); 716 adhoc_rw(out.get(), out); 717 718 if (out.m().is_and(out)) { 719 expr_ref_vector v(out.m()); 720 flatten_and(out, v); 721 722 if (v.size() > 1) { 723 if (use_simplify_bounds) { 724 // remove redundant inequalities 725 simplify_bounds(v); 726 } 727 if (use_factor_eqs) { 728 // -- refactor equivalence classes and choose a representative 729 mbp::term_graph egraph(out.m()); 730 egraph.add_lits(v); 731 v.reset(); 732 egraph.to_lits(v); 733 } 734 // sort arguments of the top-level and 735 std::stable_sort(v.data(), v.data() + v.size(), ast_lt_proc()); 736 737 TRACE("spacer_normalize", 738 tout << "Normalized:\n" 739 << out << "\n" 740 << "to\n" 741 << mk_and(v) << "\n";); 742 TRACE("spacer_normalize", 743 mbp::term_graph egraph(out.m()); 744 for (expr* e : v) egraph.add_lit(to_app(e)); 745 tout << "Reduced app:\n" 746 << mk_pp(egraph.to_expr(), out.m()) << "\n";); 747 out = mk_and(v); 748 } 749 } 750 } 751 752 // rewrite term such that the pretty printing is easier to read 753 struct adhoc_rewriter_rpp : public default_rewriter_cfg { 754 ast_manager& m; 755 arith_util m_arith; 756 adhoc_rewriter_rppspacer::adhoc_rewriter_rpp757 adhoc_rewriter_rpp(ast_manager& manager) : m(manager), m_arith(m) {} 758 is_lespacer::adhoc_rewriter_rpp759 bool is_le(func_decl const* n) const { return m_arith.is_le(n); } is_gespacer::adhoc_rewriter_rpp760 bool is_ge(func_decl const* n) const { return m_arith.is_ge(n); } is_ltspacer::adhoc_rewriter_rpp761 bool is_lt(func_decl const* n) const { return m_arith.is_lt(n); } is_gtspacer::adhoc_rewriter_rpp762 bool is_gt(func_decl const* n) const { return m_arith.is_gt(n); } is_zerospacer::adhoc_rewriter_rpp763 bool is_zero(expr const* n) const { rational val; return m_arith.is_numeral(n, val) && val.is_zero(); } 764 reduce_appspacer::adhoc_rewriter_rpp765 br_status reduce_app(func_decl* f, unsigned num, expr* const* args, 766 expr_ref& result, proof_ref& result_pr) 767 { 768 br_status st = BR_FAILED; 769 expr* e1, * e2, * e3, * e4; 770 771 // rewrites(=(+ A(* -1 B)) 0) into(= A B) 772 if (m.is_eq(f) && is_zero(args[1]) && 773 m_arith.is_add(args[0], e1, e2) && 774 m_arith.is_mul(e2, e3, e4) && m_arith.is_minus_one(e3)) { 775 result = m.mk_eq(e1, e4); 776 return BR_DONE; 777 } 778 // simplify normalized leq, where right side is different from 0 779 // rewrites(<=(+ A(* -1 B)) C) into(<= A B+C) 780 else if ((is_le(f) || is_lt(f) || is_ge(f) || is_gt(f)) && 781 m_arith.is_add(args[0], e1, e2) && 782 m_arith.is_mul(e2, e3, e4) && m_arith.is_minus_one(e3)) { 783 expr_ref rhs(m); 784 rhs = is_zero(args[1]) ? e4 : m_arith.mk_add(e4, args[1]); 785 786 if (is_le(f)) { 787 result = m_arith.mk_le(e1, rhs); 788 st = BR_DONE; 789 } 790 else if (is_lt(f)) { 791 result = m_arith.mk_lt(e1, rhs); 792 st = BR_DONE; 793 } 794 else if (is_ge(f)) { 795 result = m_arith.mk_ge(e1, rhs); 796 st = BR_DONE; 797 } 798 else if (is_gt(f)) { 799 result = m_arith.mk_gt(e1, rhs); 800 st = BR_DONE; 801 } 802 else 803 { 804 UNREACHABLE(); 805 } 806 } 807 // simplify negation of ordering predicate 808 else if (m.is_not(f)) { 809 if (m_arith.is_lt(args[0], e1, e2)) { 810 result = m_arith.mk_ge(e1, e2); 811 st = BR_DONE; 812 } 813 else if (m_arith.is_le(args[0], e1, e2)) { 814 result = m_arith.mk_gt(e1, e2); 815 st = BR_DONE; 816 } 817 else if (m_arith.is_gt(args[0], e1, e2)) { 818 result = m_arith.mk_le(e1, e2); 819 st = BR_DONE; 820 } 821 else if (m_arith.is_ge(args[0], e1, e2)) { 822 result = m_arith.mk_lt(e1, e2); 823 st = BR_DONE; 824 } 825 } 826 return st; 827 } 828 }; 829 mk_epp(ast * t,ast_manager & m,unsigned indent,unsigned num_vars,char const * var_prefix)830 mk_epp::mk_epp(ast* t, ast_manager& m, unsigned indent, 831 unsigned num_vars, char const* var_prefix) : 832 mk_pp(t, m, m_epp_params, indent, num_vars, var_prefix), m_epp_expr(m) { 833 m_epp_params.set_uint("min_alias_size", UINT_MAX); 834 m_epp_params.set_uint("max_depth", UINT_MAX); 835 836 if (is_expr(m_ast)) { 837 rw(to_expr(m_ast), m_epp_expr); 838 m_ast = m_epp_expr; 839 } 840 } 841 rw(expr * e,expr_ref & out)842 void mk_epp::rw(expr* e, expr_ref& out) { 843 adhoc_rewriter_rpp cfg(out.m()); 844 rewriter_tpl<adhoc_rewriter_rpp> arw(out.m(), false, cfg); 845 arw(e, out); 846 } 847 ground_expr(expr * e,expr_ref & out,app_ref_vector & vars)848 void ground_expr(expr* e, expr_ref& out, app_ref_vector& vars) { 849 expr_free_vars fv; 850 ast_manager& m = out.m(); 851 852 fv(e); 853 if (vars.size() < fv.size()) { 854 vars.resize(fv.size()); 855 } 856 for (unsigned i = 0, sz = fv.size(); i < sz; ++i) { 857 sort* s = fv[i] ? fv[i] : m.mk_bool_sort(); 858 vars[i] = mk_zk_const(m, i, s); 859 var_subst vs(m, false); 860 out = vs(e, vars.size(), (expr**)vars.data()); 861 } 862 } 863 864 struct index_term_finder { 865 ast_manager& m; 866 array_util m_array; 867 app_ref m_var; 868 expr_ref_vector& m_res; 869 index_term_finderspacer::index_term_finder870 index_term_finder(ast_manager& mgr, app* v, expr_ref_vector& res) : m(mgr), m_array(m), m_var(v, m), m_res(res) {} operator ()spacer::index_term_finder871 void operator()(var* n) {} operator ()spacer::index_term_finder872 void operator()(quantifier* n) {} operator ()spacer::index_term_finder873 void operator()(app* n) { 874 if (m_array.is_select(n) || m.is_eq(n)) { 875 unsigned i = 0; 876 for (expr* arg : *n) { 877 if ((m.is_eq(n) || i > 0) && m_var != arg) m_res.push_back(arg); 878 ++i; 879 } 880 } 881 } 882 }; 883 mbqi_project_var(model & mdl,app * var,expr_ref & fml)884 bool mbqi_project_var(model& mdl, app* var, expr_ref& fml) { 885 ast_manager& m = fml.get_manager(); 886 model::scoped_model_completion _sc_(mdl, false); 887 888 expr_ref val(m); 889 val = mdl(var); 890 891 TRACE("mbqi_project_verbose", 892 tout << "MBQI: var: " << mk_pp(var, m) << "\n" 893 << "fml: " << fml << "\n";); 894 expr_ref_vector terms(m); 895 index_term_finder finder(m, var, terms); 896 for_each_expr(finder, fml); 897 898 TRACE("mbqi_project_verbose", tout << "terms:\n" << terms << "\n";); 899 900 for (expr* term : terms) { 901 expr_ref tval(m); 902 tval = mdl(term); 903 904 TRACE("mbqi_project_verbose", 905 tout << "term: " << mk_pp(term, m) 906 << " tval: " << tval << " val: " << val << "\n";); 907 908 // -- if the term does not contain an occurrence of var 909 // -- and is in the same equivalence class in the model 910 if (tval == val && !occurs(var, term)) { 911 TRACE("mbqi_project", 912 tout << "MBQI: replacing " << mk_pp(var, m) 913 << " with " << mk_pp(term, m) << "\n";); 914 expr_safe_replace sub(m); 915 sub.insert(var, term); 916 sub(fml); 917 return true; 918 } 919 } 920 921 TRACE("mbqi_project", 922 tout << "MBQI: failed to eliminate " << mk_pp(var, m) 923 << " from " << fml << "\n";); 924 925 return false; 926 } 927 mbqi_project(model & mdl,app_ref_vector & vars,expr_ref & fml)928 void mbqi_project(model& mdl, app_ref_vector& vars, expr_ref& fml) { 929 ast_manager& m = fml.get_manager(); 930 expr_ref tmp(m); 931 model::scoped_model_completion _sc_(mdl, false); 932 // -- evaluate to initialize mev cache 933 tmp = mdl(fml); 934 tmp.reset(); 935 936 unsigned j = 0; 937 for (app* v : vars) 938 if (!mbqi_project_var(mdl, v, fml)) 939 vars[j++] = v; 940 vars.shrink(j); 941 } 942 943 struct found {}; 944 struct check_select { 945 array_util a; check_selectspacer::check_select946 check_select(ast_manager& m) : a(m) {} operator ()spacer::check_select947 void operator()(expr* n) {} operator ()spacer::check_select948 void operator()(app* n) { if (a.is_select(n)) throw found(); } 949 }; 950 contains_selects(expr * fml,ast_manager & m)951 bool contains_selects(expr* fml, ast_manager& m) { 952 check_select cs(m); 953 try { 954 for_each_expr(cs, fml); 955 return false; 956 } 957 catch (const found&) { 958 return true; 959 } 960 } 961 962 struct collect_indices { 963 app_ref_vector& m_indices; 964 array_util a; collect_indicesspacer::collect_indices965 collect_indices(app_ref_vector& indices) : m_indices(indices), 966 a(indices.get_manager()) {} operator ()spacer::collect_indices967 void operator()(expr* n) {} operator ()spacer::collect_indices968 void operator()(app* n) { 969 if (a.is_select(n)) { 970 // for all but first argument 971 for (unsigned i = 1; i < n->get_num_args(); ++i) { 972 expr* arg = n->get_arg(i); 973 if (is_app(arg)) 974 m_indices.push_back(to_app(arg)); 975 } 976 } 977 } 978 }; 979 get_select_indices(expr * fml,app_ref_vector & indices)980 void get_select_indices(expr* fml, app_ref_vector& indices) { 981 collect_indices ci(indices); 982 for_each_expr(ci, fml); 983 } 984 985 struct collect_decls { 986 app_ref_vector& m_decls; 987 std::string& prefix; collect_declsspacer::collect_decls988 collect_decls(app_ref_vector& decls, std::string& p) : m_decls(decls), prefix(p) {} operator ()spacer::collect_decls989 void operator()(expr* n) {} operator ()spacer::collect_decls990 void operator()(app* n) { 991 if (n->get_decl()->get_name().str().find(prefix) != std::string::npos) 992 m_decls.push_back(n); 993 } 994 }; 995 find_decls(expr * fml,app_ref_vector & decls,std::string & prefix)996 void find_decls(expr* fml, app_ref_vector& decls, std::string& prefix) { 997 collect_decls cd(decls, prefix); 998 for_each_expr(cd, fml); 999 } 1000 1001 // set the value of a boolean function to true in model set_true_in_mdl(model & model,func_decl * f)1002 void set_true_in_mdl(model& model, func_decl* f) { 1003 SASSERT(f->get_arity() == 0); 1004 model.unregister_decl(f); 1005 model.register_decl(f, model.get_manager().mk_true()); 1006 model.reset_eval_cache(); 1007 } 1008 } // namespace spacer 1009 template class rewriter_tpl<spacer::adhoc_rewriter_cfg>; 1010 template class rewriter_tpl<spacer::adhoc_rewriter_rpp>; 1011