1 /*++ 2 Copyright (c) 2020 Microsoft Corporation 3 4 Module Name: 5 6 q_mbi.h 7 8 Abstract: 9 10 Model-based quantifier instantiation plugin 11 12 Author: 13 14 Nikolaj Bjorner (nbjorner) 2020-09-29 15 16 --*/ 17 #pragma once 18 19 #include "solver/solver.h" 20 #include "qe/mbp/mbp_plugin.h" 21 #include "sat/smt/sat_th.h" 22 #include "sat/smt/q_model_fixer.h" 23 #include "sat/sat_solver.h" 24 25 namespace euf { 26 class solver; 27 } 28 29 namespace q { 30 31 class solver; 32 33 class mbqi { 34 struct stats { 35 unsigned m_num_instantiations; 36 unsigned m_num_checks; 37 statsstats38 stats() { reset(); } 39 resetstats40 void reset() { 41 memset(this, 0, sizeof(*this)); 42 } 43 }; 44 struct q_body { 45 app_ref_vector vars; 46 bool_vector free_vars; // variables that occur in positive equalities 47 expr_ref mbody; // body specialized with respect to model 48 expr_ref_vector vbody; // (negation of) body specialized with respect to vars 49 expr_ref_vector domain_eqs; // additional domain restrictions 50 51 svector<std::pair<app*, unsigned>> var_args; // (uninterpreted) functions in vbody that contain arguments with variables q_bodyq_body52 q_body(ast_manager& m) : vars(m), mbody(m), vbody(m), domain_eqs(m) {} set_freeq_body53 void set_free(unsigned idx) { free_vars.setx(idx, true, false); } is_freeq_body54 bool is_free(unsigned idx) const { return free_vars.get(idx, false); } is_freeq_body55 bool is_free(expr* e) const { return is_var(e) && is_free(to_var(e)->get_idx()); } 56 }; 57 58 euf::solver& ctx; 59 solver& m_qs; 60 ast_manager& m; 61 stats m_stats; 62 model_fixer m_model_fixer; 63 model_ref m_model; 64 sat::no_drat_params m_no_drat_params; 65 ref<::solver> m_solver; 66 scoped_ptr_vector<obj_hashtable<expr>> m_values; 67 scoped_ptr_vector<mbp::project_plugin> m_plugins; 68 obj_map<quantifier, q_body*> m_q2body; 69 unsigned m_max_cex{ 1 }; 70 unsigned m_max_quick_check_rounds { 100 }; 71 unsigned m_max_unbounded_equalities { 10 }; 72 unsigned m_max_choose_candidates { 10 }; 73 unsigned m_generation_bound{ UINT_MAX }; 74 unsigned m_generation_max { UINT_MAX }; 75 typedef std::tuple<sat::literal, expr_ref, unsigned> instantiation_t; 76 vector<instantiation_t> m_instantiations; 77 78 void restrict_to_universe(expr * sk, ptr_vector<expr> const & universe); 79 // void register_value(expr* e); 80 expr_ref replace_model_value(expr* e); 81 expr_ref choose_term(euf::enode* r); 82 lbool check_forall(quantifier* q); 83 q_body* specialize(quantifier* q); 84 q_body* q2body(quantifier* q); 85 expr_ref solver_project(model& mdl, q_body& qb, expr_ref_vector& eqs, bool use_inst); 86 void add_universe_restriction(quantifier* q, q_body& qb); 87 void add_domain_eqs(model& mdl, q_body& qb); 88 void add_domain_bounds(model& mdl, q_body& qb); 89 void eliminate_nested_vars(expr_ref_vector& fmls, q_body& qb); 90 void extract_var_args(expr* t, q_body& qb); 91 void extract_free_vars(quantifier* q, q_body& qb); 92 void init_model(); 93 void init_solver(); 94 mbp::project_plugin* get_plugin(app* var); 95 void add_plugin(mbp::project_plugin* p); 96 void add_instantiation(quantifier* q, expr_ref& proj); 97 98 bool check_forall_default(quantifier* q, q_body& qb, model& mdl); 99 bool check_forall_subst(quantifier* q, q_body& qb, model& mdl); 100 101 bool quick_check(quantifier* q, quantifier* q_flat, q_body& qb); 102 bool next_offset(unsigned_vector& offsets, app_ref_vector const& vars); 103 bool first_offset(unsigned_vector& offsets, app_ref_vector const& vars); 104 bool next_offset(unsigned_vector& offsets, app_ref_vector const& vars, unsigned i, unsigned start); 105 void set_binding(unsigned_vector const& offsets, app_ref_vector const& vars, expr_ref_vector& binding); 106 107 public: 108 109 mbqi(euf::solver& ctx, solver& s); 110 111 lbool operator()(); 112 113 void init_search(); 114 115 void finalize_model(model& mdl); 116 117 void collect_statistics(statistics& st) const; 118 }; 119 120 } 121